Project Statistics

theorems contains the number of theorems (not axioms) that were invented by the user.
proofs shows how many proofs were done, for a completed project this is equal to the number of user defined theorems + the number of (generated) proof obligations.
proof steps shows the number of rule applications of the calculus.
interactions is the number rule applications that were done by the user.

Proofs spec-name data? lib? theorems proofs proof steps interactions nonlib specs 11 11 124 46 lib specs 1466 1466 5822 1930 total 1477 1477 5946 1976 int-array No No 0 0 0 0 int-array-ops No No 10 10 103 42 kadane No No 1 1 21 4 array No Yes 21 21 78 20 array-copy No Yes 67 67 334 103 elem No Yes 0 0 0 0 int-abs No Yes 273 273 509 37 int-basic1 No Yes 50 50 148 42 int-basic2 No Yes 54 54 208 51 int-div No Yes 460 460 2744 1120 int-mult No Yes 296 296 1150 452 nat No Yes 120 120 296 66 nat-basic No Yes 125 125 355 39

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 546 67 30 5 all lib specs No No 408 60 24 4 all nonlib specs No No 138 7 6 1 all data specs No No 0 0 0 0 all nondata specs No No 546 67 30 5 all data lib specs No No 0 0 0 0 all nondata lib specs No No 408 60 24 4 all data nonlib specs No No 0 0 0 0 all nondata nonlib specs No No 138 7 6 1 int-array No No 33 0 0 1 int-array-ops No No 52 7 6 0 kadane No No 53 0 0 0 array No Yes 48 5 2 1 array-copy No Yes 103 15 5 0 elem No Yes 22 0 0 1 int-abs No Yes 36 7 6 0 int-basic1 No Yes 33 6 3 1 int-basic2 No Yes 24 3 1 0 int-div No Yes 41 4 0 0 int-mult No Yes 28 3 1 0 nat No Yes 31 5 3 0 nat-basic No Yes 42 12 3 1