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 1 1 49 11 lib specs 8760 8760 59847 25173 total 8761 8761 59896 25184 Challenge1 No No 1 1 49 11 addarray No Yes 340 340 2404 1099 addfuns No Yes 484 484 3074 1065 assoclist No Yes 55 55 334 126 assoclista No Yes 0 0 0 0 bitlista No Yes 22 22 45 2 bitopsaux No Yes 161 161 932 346 bool Yes Yes 0 0 0 0 byte No Yes 392 392 2749 1538 bytelist No Yes 0 0 0 0 bytes No Yes 245 245 4561 2421 char No Yes 0 0 0 0 classname Yes Yes 0 0 0 0 classnamefuns No Yes 2 2 2 2 classnames No Yes 2 2 5 2 contains No Yes 99 99 2101 843 cyclic No Yes 183 183 5319 2143 data No Yes 0 0 0 0 elem No Yes 0 0 0 0 elemdata No Yes 0 0 0 0 fieldinit No Yes 5 5 8 4 fieldname Yes Yes 0 0 0 0 fieldspec Yes Yes 1 1 1 0 float No Yes 0 0 0 0 gelem No Yes 0 0 0 0 initstate Yes 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 int-pot No Yes 133 133 662 326 int-square No Yes 25 25 474 347 int-total No Yes 0 0 0 0 int2bits No Yes 311 311 2710 1389 intlist No Yes 20 20 160 66 intlista No Yes 0 0 0 0 intnat No Yes 133 133 403 164 intops No Yes 363 363 5258 2699 javachar No Yes 0 0 0 0 javastore No Yes 108 108 224 49 javatype Yes Yes 3 3 5 1 javatypes No Yes 0 0 0 0 javavalue Yes Yes 37 37 65 6 javavalues No Yes 0 0 0 0 junkrefs No Yes 493 493 5502 2165 label Yes Yes 0 0 0 0 list No Yes 128 128 336 71 list-data Yes Yes 30 30 46 0 list-del No Yes 269 269 1109 264 list-dup No Yes 99 99 580 161 list-last No Yes 156 156 391 111 list-perm No Yes 95 95 689 232 list-set No Yes 116 116 464 119 multiarrays No Yes 104 104 999 403 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 oelem No Yes 8 8 10 2 okfuns No Yes 485 485 3131 1120 olist No Yes 49 49 312 90 olist-sort No Yes 23 23 57 29 olista No Yes 0 0 0 0 oset No Yes 108 108 223 74 oseta No Yes 0 0 0 0 ostore No Yes 40 40 123 43 ostore+oset No Yes 0 0 0 0 ostorea No Yes 0 0 0 0 pair Yes Yes 0 0 0 0 pointers No Yes 76 76 1540 712 predefined No Yes 43 43 194 32 reference No Yes 14 14 26 10 references No Yes 0 0 0 0 refkey Yes Yes 3 3 3 0 refkeykeys Yes Yes 0 0 0 0 refkeyvalues No Yes 0 0 0 0 reflistset No Yes 0 0 0 0 set-basic No Yes 95 95 428 88 set-union No Yes 183 183 598 109 setlist No Yes 22 22 88 37 specialkeys No Yes 54 54 56 2 store No Yes 71 71 356 127 storearrays No Yes 307 307 1701 791 storefuns No Yes 306 306 1423 583 storefunsx No Yes 107 107 819 295 storekey Yes Yes 3 3 5 1 storekeys No Yes 0 0 0 0 string-append No Yes 15 15 34 11 string-data Yes Yes 4 4 7 0 string-less No Yes 38 38 135 58 typefuns No Yes 203 203 643 337 value+type Yes Yes 0 0 0 0 valuefuns No Yes 81 81 283 43 valuesfuns No Yes 62 62 318 122 valuetypes No Yes 0 0 0 0

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 5151 1607 545 48 all lib specs No No 5150 1607 545 48 all nonlib specs No No 1 0 0 0 all data specs No No 334 1494 228 32 all nondata specs No No 4984 860 431 32 all data lib specs No No 167 747 114 16 all nondata lib specs No No 4983 860 431 32 all data nonlib specs No No 0 0 0 0 all nondata nonlib specs No No 1 0 0 0 Challenge1 No No 1 0 0 0 addarray No Yes 70 8 6 0 addfuns No Yes 251 37 17 0 assoclist No Yes 36 10 5 0 assoclista No Yes 16 0 0 1 bitlista No Yes 17 0 0 1 bitopsaux No Yes 64 15 5 0 bool Yes Yes 5 2 2 1 byte No Yes 101 31 25 4 bytelist No Yes 17 0 0 1 bytes No Yes 66 13 7 0 char No Yes 19 0 0 1 classname Yes Yes 6 4 2 1 classnamefuns No Yes 39 6 3 0 classnames No Yes 25 0 0 1 contains No Yes 58 5 4 0 cyclic No Yes 89 9 5 0 data No Yes 6 0 0 1 elem No Yes 6 0 0 1 elemdata No Yes 2 0 0 0 fieldinit No Yes 21 0 0 1 fieldname Yes Yes 8 4 2 1 fieldspec Yes Yes 13 6 4 1 float No Yes 18 0 6 2 gelem No Yes 8 0 0 0 initstate Yes Yes 5 4 3 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 int-pot No Yes 17 3 1 0 int-square No Yes 13 2 2 0 int-total No Yes 9 1 0 0 int2bits No Yes 53 11 4 0 intlist No Yes 45 12 6 0 intlista No Yes 18 0 0 1 intnat No Yes 15 5 2 0 intops No Yes 223 29 17 0 javachar No Yes 20 1 3 1 javastore No Yes 11 0 0 1 javatype Yes Yes 14 112 17 1 javatypes No Yes 16 0 0 1 javavalue Yes Yes 47 550 52 1 javavalues No Yes 17 0 0 1 junkrefs No Yes 247 29 25 0 label Yes Yes 6 4 2 1 list No Yes 21 6 5 0 list-data Yes Yes 9 12 6 1 list-del No Yes 63 26 11 0 list-dup No Yes 27 7 4 0 list-last No Yes 37 11 8 0 list-perm No Yes 20 5 3 0 list-set No Yes 26 8 4 0 multiarrays No Yes 204 26 9 0 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 oelem No Yes 13 3 1 0 okfuns No Yes 550 87 34 0 olist No Yes 29 9 4 0 olist-sort No Yes 10 2 1 0 olista No Yes 1 0 0 1 oset No Yes 30 8 6 0 oseta No Yes 1 0 0 1 ostore No Yes 18 4 3 0 ostore+oset No Yes 2 0 0 0 ostorea No Yes 1 0 0 1 pair Yes Yes 6 5 3 1 pointers No Yes 96 8 5 0 predefined No Yes 408 49 4 0 reference No Yes 24 7 3 1 references No Yes 24 0 0 1 refkey Yes Yes 8 5 3 1 refkeykeys Yes Yes 8 5 3 1 refkeyvalues No Yes 21 0 0 1 reflistset No Yes 7 0 0 1 set-basic No Yes 35 6 5 1 set-union No Yes 25 5 5 0 setlist No Yes 20 4 2 0 specialkeys No Yes 68 10 8 0 store No Yes 61 12 9 2 storearrays No Yes 117 21 15 0 storefuns No Yes 188 41 32 0 storefunsx No Yes 147 24 22 0 storekey Yes Yes 10 14 6 1 storekeys No Yes 16 0 0 1 string-append No Yes 14 3 2 0 string-data Yes Yes 8 6 3 1 string-less No Yes 63 16 5 0 typefuns No Yes 236 36 19 0 value+type Yes Yes 8 5 3 1 valuefuns No Yes 410 112 16 0 valuesfuns No Yes 131 32 17 0 valuetypes No Yes 16 0 0 1