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 383 439 9209 1699 lib specs 2489 2518 11294 2773 total 2872 2957 20503 4472 abstract-volume No No 0 0 0 0 abstract-volumes No No 0 0 0 0 bag-max No No 33 33 230 70 ebaentry Yes No 0 0 0 0 ebatbl No No 0 0 0 0 ebm-asm No No 0 25 356 39 ebm-base No No 9 9 88 26 encoding-volid No No 0 0 0 0 encoding-vtbl No No 6 6 261 98 erasequeue No No 30 30 348 23 erasequeue-base No No 0 0 0 0 erasequeueentry Yes No 0 0 0 0 leb Yes No 0 0 0 0 lebadress Yes No 0 0 0 0 lebref Yes No 0 0 0 0 lebrefset No No 0 0 0 0 nat-bag No No 0 0 0 0 recovery-entries No No 0 0 0 0 recovery-entry Yes No 0 0 0 0 sqns No No 17 17 154 35 store-union No No 9 9 41 15 ubi-abs No No 28 28 402 70 ubi-asm No No 46 62 2999 605 ubi-base No No 104 104 1453 141 ubi-crash-recovery-base No No 40 40 696 187 ubi-quality No No 3 3 549 55 ubi-quality-base No No 14 14 317 52 ubi-refine No No 7 22 1054 197 valid-peb No No 18 18 86 19 volumes No No 0 0 0 0 vtbl No No 0 0 0 0 vtbl-conv No No 5 5 56 28 wlarray No No 14 14 119 39 wlarray-base No No 0 0 0 0 wlentry Yes No 0 0 0 0 wlstatus Yes No 0 0 0 0 aecheader Yes Yes 1 1 3 1 align No Yes 77 77 377 89 apeb Yes Yes 0 0 0 0 apebs No Yes 0 0 0 0 array No Yes 14 14 46 11 array-copy No Yes 53 53 277 85 array-indices No Yes 24 24 148 51 array-splice No Yes 84 84 752 300 aubi-io-asm No Yes 0 29 460 38 avidheader Yes Yes 1 1 3 1 bag-basic No Yes 7 7 24 6 bag-union No Yes 45 45 253 98 bool Yes Yes 0 0 0 0 buffer No Yes 2 2 9 5 char No Yes 0 0 0 0 checksum No Yes 2 2 4 2 data No Yes 0 0 0 0 datasize No Yes 35 35 345 71 debug No Yes 0 0 0 0 elem No Yes 0 0 0 0 elemdata No Yes 0 0 0 0 encoding No Yes 3 3 31 17 encoding-elem-size No Yes 0 0 0 0 encoding-fixed-size No Yes 1 1 2 1 encoding-nat No Yes 0 0 0 0 eraseblock No Yes 54 54 214 77 error Yes Yes 0 0 0 0 error-class No Yes 19 19 36 9 gelem No Yes 0 0 0 0 list No Yes 130 130 440 87 list+set No Yes 5 5 19 10 list-data Yes Yes 29 29 68 0 list-del No Yes 311 311 1700 334 list-dup No Yes 104 104 600 147 list-last No Yes 163 163 579 153 list-prefixn No Yes 49 49 229 43 list-set No Yes 136 136 696 145 min-max No Yes 30 30 65 7 nat No Yes 120 120 302 69 nat-basic No Yes 129 129 356 39 nat-div No Yes 139 139 488 165 nat-list-less No Yes 4 4 27 5 nat-list-set No Yes 0 0 0 0 nat-mult No Yes 213 213 648 238 nat-set No Yes 6 6 36 18 oelem No Yes 8 8 18 3 oset No Yes 111 111 328 76 set-basic No Yes 96 96 444 86 set-union No Yes 197 197 770 140 store No Yes 76 76 444 141 string No Yes 0 0 0 0 ubi-io-inv No Yes 11 11 53 5 ubi-io-pre No Yes 0 0 0 0 volid No Yes 0 0 0 0

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 5726 633 272 38 all lib specs No No 2418 453 167 20 all nonlib specs No No 3308 180 105 18 all data specs No No 266 462 82 12 all nondata specs No No 5469 314 199 24 all data lib specs No No 133 231 41 6 all nondata lib specs No No 2285 222 126 14 all data nonlib specs No No 124 88 32 8 all nondata nonlib specs No No 3184 92 73 10 abstract-volume No No 32 0 0 1 abstract-volumes No No 30 0 0 1 bag-max No No 27 2 2 0 ebaentry Yes No 18 7 2 1 ebatbl No No 32 0 0 1 ebm-asm No No 267 0 0 0 ebm-base No No 63 7 5 0 encoding-volid No No 21 0 0 0 encoding-vtbl No No 153 3 2 0 erasequeue No No 61 11 7 0 erasequeue-base No No 57 0 0 1 erasequeueentry Yes No 15 11 5 1 leb Yes No 17 18 4 1 lebadress Yes No 14 11 5 1 lebref Yes No 15 12 2 1 lebrefset No No 27 0 0 1 nat-bag No No 27 0 0 1 recovery-entries No No 30 0 0 1 recovery-entry Yes No 14 11 5 1 sqns No No 38 3 2 0 store-union No No 28 3 2 0 ubi-abs No No 144 11 8 0 ubi-asm No No 1492 0 0 0 ubi-base No No 171 17 18 0 ubi-crash-recovery-base No No 159 15 12 0 ubi-quality No No 22 0 0 0 ubi-quality-base No No 43 7 4 0 ubi-refine No No 27 0 0 0 valid-peb No No 35 2 2 0 volumes No No 30 0 0 1 vtbl No No 32 0 0 1 vtbl-conv No No 30 2 3 0 wlarray No No 64 9 6 0 wlarray-base No No 42 0 0 1 wlentry Yes No 14 11 5 1 wlstatus Yes No 17 7 4 1 aecheader Yes Yes 19 13 4 1 align No Yes 30 3 3 0 apeb Yes Yes 20 38 11 1 apebs No Yes 32 0 0 1 array No Yes 48 5 2 1 array-copy No Yes 100 14 4 0 array-indices No Yes 83 14 10 0 array-splice No Yes 68 10 8 0 aubi-io-asm No Yes 302 0 0 0 avidheader Yes Yes 25 45 4 1 bag-basic No Yes 36 3 3 1 bag-union No Yes 49 11 7 0 bool Yes Yes 16 2 2 1 buffer No Yes 40 0 0 1 char No Yes 34 0 0 1 checksum No Yes 25 1 1 0 data No Yes 23 0 0 1 datasize No Yes 30 3 2 0 debug No Yes 23 1 1 0 elem No Yes 22 0 0 1 elemdata No Yes 23 0 0 0 encoding No Yes 59 5 3 0 encoding-elem-size No Yes 34 0 1 0 encoding-fixed-size No Yes 26 2 0 0 encoding-nat No Yes 21 0 0 0 eraseblock No Yes 56 11 10 0 error Yes Yes 32 121 16 1 error-class No Yes 39 1 1 0 gelem No Yes 26 0 0 0 list No Yes 38 7 5 0 list+set No Yes 24 1 1 0 list-data Yes Yes 21 12 4 1 list-del No Yes 101 26 5 0 list-dup No Yes 39 7 4 0 list-last No Yes 62 14 5 0 list-prefixn No Yes 31 3 3 0 list-set No Yes 41 8 4 0 min-max No Yes 26 2 2 0 nat No Yes 31 5 3 0 nat-basic No Yes 42 12 3 1 nat-div No Yes 32 2 0 0 nat-list-less No Yes 25 2 1 0 nat-list-set No Yes 72 0 0 1 nat-mult No Yes 23 2 1 0 nat-set No Yes 34 0 0 1 oelem No Yes 27 3 1 0 oset No Yes 61 8 2 0 set-basic No Yes 42 6 5 1 set-union No Yes 35 5 5 0 store No Yes 58 11 6 1 string No Yes 53 0 0 1 ubi-io-inv No Yes 51 4 4 0 ubi-io-pre No Yes 85 10 10 0 volid No Yes 23 0 0 1