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 334 341 2619 1288 lib specs 1036 1036 3340 866 total 1370 1377 5959 2154 aux No No 0 0 0 0 cell Yes No 0 0 0 0 cell-heap No No 0 0 0 0 cell-heap-aux No No 3 3 44 16 embed-aux No No 36 36 545 298 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 55 55 292 132 heap-aux No No 0 0 0 0 heap-fun No No 35 35 148 70 heap-sep No No 62 62 330 178 iter-set No No 7 7 67 32 iter-store No No 8 8 62 34 linked-list No No 6 6 49 24 linked-list-aux No No 15 15 146 72 linked-list-seg No No 14 14 102 36 linked-tree No No 6 6 21 10 maplet No No 33 33 226 113 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 33 2 ownership No No 0 0 0 0 reachable No No 0 0 0 0 ref 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 147 55 rtc-ref No No 0 0 0 0 separation No No 13 13 85 47 separation-rg No No 26 26 287 166 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 352 86 list-data Yes Yes 30 30 46 0 list-dup No Yes 104 104 574 167 list-last No Yes 160 160 425 130 nat No Yes 121 121 239 71 nat-basic1 Yes Yes 62 62 98 4 nat-basic2 No Yes 66 66 187 56 rtc No Yes 5 5 39 18 set-basic No Yes 96 96 390 84 set-union No Yes 186 186 619 124 store No Yes 76 76 371 126

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 981 224 137 20 all lib specs No No 317 81 52 7 all nonlib specs No No 664 143 85 13 all data specs No No 30 42 18 4 all nondata specs No No 936 148 104 14 all data lib specs No No 15 21 9 2 all nondata lib specs No No 302 60 43 5 all data nonlib specs No No 30 55 24 4 all nondata nonlib specs No No 634 88 61 9 aux No No 6 0 0 1 cell Yes No 7 11 5 1 cell-heap No No 6 0 0 1 cell-heap-aux No No 9 0 0 1 embed-aux No No 10 1 1 0 gaux No No 8 0 0 0 gobj No No 8 0 0 0 gownership Yes No 6 5 3 1 gref No No 8 0 0 0 heap No No 104 22 12 1 heap-aux No No 15 0 0 0 heap-fun No No 19 3 2 0 heap-sep No No 73 15 15 0 iter-set No No 22 4 2 0 iter-store No No 23 4 2 0 linked-list No No 13 2 1 0 linked-list-aux No No 23 4 3 0 linked-list-seg No No 44 5 3 0 linked-tree No No 15 2 1 0 maplet No No 33 6 6 0 node Yes No 7 18 7 1 node-heap No No 6 0 0 1 obj No No 6 0 0 1 ops No No 18 7 0 0 ops-impl No No 38 1 0 0 ops-inst No No 1 0 0 0 ownership No No 5 0 0 1 reachable No No 12 1 1 0 ref No No 8 0 1 1 refobj No No 2 0 0 0 refset No No 7 0 0 1 rg No No 30 3 3 0 rtc-ref No No 6 0 0 0 separation No No 13 2 2 0 separation-rg No No 43 6 6 0 tree Yes No 10 21 9 1 data No Yes 6 0 0 1 elem No Yes 6 0 0 1 elemdata No Yes 2 0 0 0 list No Yes 29 6 5 0 list-data Yes Yes 9 12 6 1 list-dup No Yes 30 7 4 0 list-last No Yes 54 11 8 0 nat No Yes 15 5 4 0 nat-basic1 Yes Yes 6 9 3 1 nat-basic2 No Yes 13 5 1 0 rtc No Yes 20 3 2 0 set-basic No Yes 39 6 5 1 set-union No Yes 25 5 5 0 store No Yes 63 12 9 2