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 62 62 1816 266 lib specs 647 647 1597 528 total 709 709 3413 794 OUTREDUCE No No 14 14 1442 110 context No No 0 0 0 0 rawcontext Yes No 0 0 0 0 reduce No No 23 23 219 97 subst No No 12 12 128 43 term Yes No 0 0 0 0 term_or_none Yes No 0 0 0 0 termfuns No No 8 8 19 11 value No No 5 5 8 5 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-even No Yes 47 47 115 8 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 325 100 47 4 all lib specs No No 81 29 15 1 all nonlib specs No No 244 71 32 3 all data specs No No 12 18 6 2 all nondata specs No No 287 48 26 0 all data lib specs No No 6 9 3 1 all nondata lib specs No No 75 20 12 0 all data nonlib specs No No 32 43 18 3 all nondata nonlib specs No No 212 28 14 0 OUTREDUCE No No 60 2 2 0 context No No 18 3 1 0 rawcontext Yes No 14 23 8 1 reduce No No 52 6 5 0 subst No No 16 3 1 0 term Yes No 12 15 7 1 term_or_none Yes No 6 5 3 1 termfuns No No 37 9 4 0 value No No 29 5 1 0 nat No Yes 15 5 4 0 nat-basic1 Yes Yes 6 9 3 1 nat-basic2 No Yes 13 5 1 0 nat-div No Yes 13 2 2 0 nat-even No Yes 26 6 4 0 nat-mult No Yes 8 2 1 0