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 theorems.
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 27 27 450 161 lib specs 939 939 2893 666 total 966 966 3343 827 BFS No No 5 5 200 65 INV No No 6 6 147 57 graph No No 16 16 103 39 nat_or_fail Yes No 0 0 0 0 elem No Yes 0 0 0 0 list No Yes 128 128 336 71 list-data Yes Yes 30 30 46 0 list-dup No Yes 99 99 580 161 list-last No Yes 156 156 391 111 nat No Yes 119 119 227 66 nat-basic1 Yes Yes 64 64 105 4 nat-basic2 No Yes 65 65 182 56 set-basic No Yes 95 95 428 88 set-union No Yes 183 183 598 109

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 359 80 51 5 all lib specs No No 226 66 41 4 all nonlib specs No No 133 14 10 1 all data specs No No 30 42 18 4 all nondata specs No No 338 54 39 2 all data lib specs No No 15 21 9 2 all nondata lib specs No No 211 45 32 2 all data nonlib specs No No 6 5 3 1 all nondata nonlib specs No No 127 9 7 0 BFS No No 43 0 0 0 INV No No 42 2 2 0 graph No No 42 7 5 0 nat_or_fail Yes No 6 5 3 1 elem No Yes 6 0 0 1 list No Yes 29 6 5 0 list-data Yes Yes 9 12 6 1 list-dup No Yes 30 7 4 0 list-last No Yes 54 11 8 0 nat No Yes 15 5 4 0 nat-basic1 Yes Yes 6 9 3 1 nat-basic2 No Yes 13 5 1 0 set-basic No Yes 39 6 5 1 set-union No Yes 25 5 5 0