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 2225 2225 23163 12047 lib specs 3957 3957 14636 5528 total 6182 6182 37799 17575 assoclist No No 55 55 334 126 assoclista No No 0 0 0 0 bitlista No No 22 22 45 2 bitopsaux No No 161 161 932 346 byte No No 392 392 2747 1538 bytelist No No 0 0 0 0 bytes No No 245 245 4558 2421 charlist No No 0 0 0 0 decimal No No 45 45 451 252 decimal-complex-ops No No 20 20 229 142 decimal-simple-ops No No 68 68 655 387 hexstring No No 7 7 35 13 int-fac No No 114 114 1199 674 int-mod No No 82 82 1158 651 int-total No No 0 0 0 0 int2bits No No 311 311 2710 1390 intlist No No 119 119 1039 480 intlista No No 0 0 0 0 intops No No 363 363 5250 2693 natlist No No 9 9 21 9 natlista No No 2 2 4 2 pair Yes No 0 0 0 0 rational No No 89 89 857 521 set-nogen-basic No No 0 0 0 0 set-nogen-union No No 0 0 0 0 setlist No No 22 22 88 37 store-nogen No No 10 10 29 12 string-ops No No 32 32 228 107 string2list No No 14 14 159 42 string2nat No No 43 43 435 202 stringlist No No 0 0 0 0 bool Yes Yes 0 0 0 0 char No Yes 0 0 0 0 data No Yes 0 0 0 0 elem No Yes 0 0 0 0 elemdata No Yes 0 0 0 0 gelem No Yes 0 0 0 0 int-abs No Yes 281 281 455 82 int-basic1 No Yes 51 51 115 39 int-basic2 No Yes 55 55 170 47 int-div No Yes 463 463 2327 1104 int-gcd No Yes 192 192 1487 904 int-min No Yes 49 49 138 43 int-mult No Yes 296 296 934 425 int-pot No Yes 159 159 863 462 int-square No Yes 60 60 236 131 intnat No Yes 133 133 385 159 list No Yes 132 132 353 86 list-data Yes Yes 30 30 44 0 list-del No Yes 313 313 1462 325 list-dup No Yes 104 104 513 139 list-last No Yes 167 167 449 141 list-perm No Yes 129 129 724 254 list-set No Yes 137 137 606 136 nat No Yes 121 121 239 71 nat-basic1 Yes Yes 62 62 94 4 nat-basic2 No Yes 68 68 184 56 nat-div No Yes 139 139 385 156 nat-mult No Yes 214 214 527 204 nat-pot No Yes 44 44 165 88 oelem No Yes 8 8 10 2 olist No Yes 57 57 416 124 olist-sort No Yes 27 27 71 38 olista No Yes 0 0 0 0 oset No Yes 112 112 216 66 oseta No Yes 2 2 2 2 set-basic No Yes 97 97 323 62 set-union No Yes 197 197 587 119 string-append No Yes 15 15 29 8 string-data Yes Yes 4 4 7 0 string-less No Yes 39 39 120 51

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 3429 500 286 28 all lib specs No No 1310 211 118 11 all nonlib specs No No 2119 289 168 17 all data specs No No 162 58 28 8 all nondata specs No No 3327 466 269 23 all data lib specs No No 81 29 14 4 all nondata lib specs No No 1229 182 104 7 all data nonlib specs No No 21 5 3 1 all nondata nonlib specs No No 2098 284 165 16 assoclist No No 46 10 5 0 assoclista No No 67 0 0 1 bitlista No No 67 0 0 1 bitopsaux No No 69 15 5 0 byte No No 135 31 25 4 bytelist No No 67 0 0 1 bytes No No 68 13 7 0 charlist No No 95 0 0 1 decimal No No 83 14 7 1 decimal-complex-ops No No 64 8 6 0 decimal-simple-ops No No 57 11 11 0 hexstring No No 83 28 5 0 int-fac No No 54 9 5 0 int-mod No No 37 5 3 0 int-total No No 24 1 0 0 int2bits No No 63 11 4 0 intlist No No 102 23 12 0 intlista No No 73 0 0 1 intops No No 206 29 17 0 natlist No No 30 4 2 0 natlista No No 95 0 0 1 pair Yes No 21 5 3 1 rational No No 98 21 15 1 set-nogen-basic No No 37 4 4 1 set-nogen-union No No 35 5 5 0 setlist No No 32 4 2 0 store-nogen No No 43 6 5 2 string-ops No No 122 24 16 0 string2list No No 30 4 2 0 string2nat No No 43 4 2 0 stringlist No No 73 0 0 1 bool Yes Yes 16 2 2 1 char No Yes 34 0 0 1 data No Yes 23 0 0 1 elem No Yes 22 0 0 1 elemdata No Yes 23 0 0 0 gelem No Yes 26 0 0 0 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 35 4 2 0 int-gcd No Yes 44 7 4 0 int-min No Yes 38 8 5 0 int-mult No Yes 28 3 1 0 int-pot No Yes 33 3 1 0 int-square No Yes 27 3 3 0 intnat No Yes 31 5 2 0 list No Yes 36 6 5 0 list-data Yes Yes 30 12 6 1 list-del No Yes 93 26 11 0 list-dup No Yes 39 7 4 0 list-last No Yes 54 11 8 0 list-perm No Yes 32 5 3 0 list-set No Yes 41 8 4 0 nat No Yes 28 5 4 0 nat-basic1 Yes Yes 16 9 3 1 nat-basic2 No Yes 27 3 1 0 nat-div No Yes 26 2 2 0 nat-mult No Yes 23 2 1 0 nat-pot No Yes 37 6 4 0 oelem No Yes 27 3 1 0 olist No Yes 42 9 4 0 olist-sort No Yes 25 2 1 0 olista No Yes 9 0 0 1 oset No Yes 41 8 6 0 oseta No Yes 9 0 0 1 set-basic No Yes 42 6 5 1 set-union No Yes 35 5 5 0 string-append No Yes 26 3 2 0 string-data Yes Yes 19 6 3 1 string-less No Yes 80 16 5 0