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 24 24 513 124 lib specs 2037 2037 6507 2528 total 2061 2061 7020 2652 build No No 7 7 353 43 build-base No No 17 17 160 81 intlist No No 0 0 0 0 tree Yes No 0 0 0 0 treeorfail Yes No 0 0 0 0 elem No Yes 0 0 0 0 int-abs No Yes 276 276 505 107 int-basic1 No Yes 51 51 120 40 int-basic2 No Yes 55 55 164 40 int-div No Yes 439 439 2416 1148 int-min No Yes 34 34 82 9 int-mult No Yes 291 291 953 429 intnat No Yes 133 133 403 164 list No Yes 128 128 336 71 list-data Yes Yes 30 30 46 0 nat No Yes 119 119 227 66 nat-basic1 Yes Yes 64 64 105 4 nat-basic2 No Yes 65 65 182 56 nat-div No Yes 138 138 395 155 nat-mult No Yes 214 214 573 239

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 320 95 53 7 all lib specs No No 227 77 42 4 all nonlib specs No No 93 18 11 3 all data specs No No 30 42 18 4 all nondata specs No No 294 63 37 3 all data lib specs No No 15 21 9 2 all nondata lib specs No No 212 56 33 2 all data nonlib specs No No 11 11 7 2 all nondata nonlib specs No No 82 7 4 1 build No No 41 0 0 0 build-base No No 35 7 4 0 intlist No No 6 0 0 1 tree Yes No 5 6 4 1 treeorfail Yes No 6 5 3 1 elem No Yes 6 0 0 1 int-abs No Yes 21 7 6 0 int-basic1 No Yes 21 6 3 1 int-basic2 No Yes 11 3 1 0 int-div No Yes 25 4 2 0 int-min No Yes 21 8 5 0 int-mult No Yes 14 3 1 0 intnat No Yes 15 5 2 0 list No Yes 21 6 5 0 list-data Yes Yes 9 12 6 1 nat No Yes 17 5 4 0 nat-basic1 Yes Yes 6 9 3 1 nat-basic2 No Yes 15 5 1 0 nat-div No Yes 15 2 2 0 nat-mult No Yes 10 2 1 0