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 380 387 3109 1429 lib specs 1049 1049 4045 880 total 1429 1436 7154 2309 aux No No 0 0 0 0 calculus No No 7 7 55 24 cell Yes No 0 0 0 0 cell-heap No No 0 0 0 0 cell-heap-aux No No 3 3 45 16 embed-aux No No 36 36 563 296 existential No No 2 2 24 11 gaux No No 0 0 0 0 gobj No No 0 0 0 0 gownership Yes No 0 0 0 0 gref No No 0 0 0 0 heap No No 59 59 346 145 heap-aux No No 0 0 0 0 heap-fun No No 35 35 164 70 heap-mod No No 5 5 76 42 heap-sep No No 82 82 473 235 iter-n No No 9 9 67 30 iter-set No No 7 7 73 32 iter-store No No 8 8 69 34 linked-list No No 6 6 51 24 linked-list-aux No No 15 15 148 70 linked-list-seg No No 14 14 112 36 linked-tree No No 6 6 25 10 maplet No No 36 36 228 101 node Yes No 0 0 0 0 node-heap No No 0 0 0 0 obj No No 0 0 0 0 ops No No 0 0 35 3 ops-impl No No 0 0 0 0 ops-inst No No 0 7 26 3 ownership No No 0 0 0 0 reachable No No 0 0 0 0 ref No No 0 0 0 0 reflist No No 0 0 0 0 refobj No No 0 0 0 0 refset No No 0 0 0 0 rg No No 15 15 155 53 rtc-heap No No 0 0 0 0 rtc-ref No No 0 0 0 0 separation No No 15 15 100 45 separation-rg No No 20 20 274 149 tree Yes No 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 list No Yes 130 130 440 87 list-data Yes Yes 29 29 68 0 list-dup No Yes 104 104 600 147 list-last No Yes 163 163 579 153 nat No Yes 120 120 302 69 nat-basic No Yes 129 129 356 39 rtc No Yes 5 5 42 18 set-basic No Yes 96 96 444 86 set-union No Yes 197 197 770 140 store No Yes 76 76 444 141

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 1791 230 125 20 all lib specs No No 466 82 42 6 all nonlib specs No No 1325 148 83 14 all data specs No No 42 24 8 2 all nondata specs No No 1692 163 103 15 all data lib specs No No 21 12 4 1 all nondata lib specs No No 445 70 38 5 all data nonlib specs No No 78 55 18 4 all nondata nonlib specs No No 1247 93 65 10 aux No No 22 0 0 1 calculus No No 22 0 0 0 cell Yes No 20 11 5 1 cell-heap No No 19 0 0 1 cell-heap-aux No No 36 0 0 1 embed-aux No No 25 1 1 0 existential No No 27 1 1 0 gaux No No 26 0 0 0 gobj No No 26 0 0 0 gownership Yes No 18 5 3 1 gref No No 26 0 0 0 heap No No 89 22 12 1 heap-aux No No 65 0 0 0 heap-fun No No 27 3 2 0 heap-mod No No 39 4 4 0 heap-sep No No 91 16 16 0 iter-n No No 26 2 1 0 iter-set No No 35 4 2 0 iter-store No No 37 4 2 0 linked-list No No 27 2 1 0 linked-list-aux No No 37 4 3 0 linked-list-seg No No 49 5 3 0 linked-tree No No 29 2 1 0 maplet No No 40 6 6 0 node Yes No 18 18 7 1 node-heap No No 19 0 0 1 obj No No 22 0 0 1 ops No No 33 7 0 0 ops-impl No No 40 1 0 0 ops-inst No No 9 0 0 0 ownership No No 23 0 0 1 reachable No No 24 1 1 0 ref No No 22 0 1 1 reflist No No 42 0 0 1 refobj No No 23 0 0 0 refset No No 27 0 0 1 rg No No 45 3 3 0 rtc-heap No No 18 0 0 0 rtc-ref No No 18 0 0 0 separation No No 26 2 2 0 separation-rg No No 36 3 3 0 tree Yes No 22 21 3 1 data No Yes 23 0 0 1 elem No Yes 22 0 0 1 elemdata No Yes 23 0 0 0 list No Yes 38 7 5 0 list-data Yes Yes 21 12 4 1 list-dup No Yes 39 7 4 0 list-last No Yes 62 14 5 0 nat No Yes 31 5 3 0 nat-basic No Yes 42 12 3 1 rtc No Yes 30 3 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