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 5198 5203 29151 10743 lib specs 0 0 0 0 total 5198 5203 29151 10743 Ref No No 0 0 0 0 approx-fixpoint No No 6 6 103 61 array No No 14 14 46 11 array-copy No No 53 53 277 85 array-list No No 1 1 19 10 assoclist No No 34 34 194 64 bag-basic No No 7 7 24 6 bag-union No No 45 45 253 98 bool Yes No 0 0 0 0 char No No 0 0 0 0 characteristic No No 0 0 0 0 choice No No 2 2 56 28 data No No 0 0 0 0 elem No No 0 0 0 0 elem-rel No No 0 0 0 0 elemdata No No 0 0 0 0 gelem No No 0 0 0 0 genRef No No 0 0 0 0 genlincell No No 0 0 0 0 hilbert-choice No No 0 0 0 0 inf-app-list No No 5 5 445 212 infinite-append No No 9 9 692 329 infset-basic No No 52 52 156 5 infset-union No No 135 135 416 36 int-abs No No 275 275 595 95 int-basic1 No No 50 50 148 42 int-basic2 No No 55 55 210 51 int-div No No 461 461 2749 1122 int-gcd No No 181 181 1421 791 int-inf No No 5 5 17 7 int-inf-basic Yes No 1 1 3 0 int-min No No 43 43 139 34 int-mult No No 296 296 1174 465 int-pair No No 14 14 76 39 int-pot No No 153 153 1040 484 int-square No No 51 51 432 299 intnat No No 133 133 447 159 lexical No No 0 3 36 19 lexical-param No No 0 0 0 0 lincell No No 0 0 0 0 linheap No No 0 0 0 0 list No No 130 130 440 87 list-data Yes No 29 29 68 0 list-del No No 311 311 1700 334 list-dup No No 104 104 600 147 list-last No No 163 163 579 153 list-perm No No 126 126 797 253 list-set No No 136 136 696 145 list-setequal No No 13 13 40 8 mon-lim-filter-count No No 93 93 2217 1119 monotone-set-fixpoint No No 14 14 116 65 nat No No 120 120 302 69 nat-basic No No 129 129 356 39 nat-div No No 139 139 488 165 nat-even No No 50 50 244 48 nat-inf No No 72 72 203 76 nat-mult No No 213 213 648 238 nat-pair No No 36 36 164 115 nat-pot No No 44 44 185 89 nat-prime No No 97 97 630 314 nat-sgn No No 5 5 11 3 natstream No No 0 0 0 0 oelem No No 8 8 18 3 oelem-min-max No No 0 0 0 0 olist No No 57 57 451 124 olist-min-max No No 25 25 425 134 olist-sort No No 27 27 79 38 oset No No 111 111 328 76 ostore No No 40 40 142 36 pair Yes No 0 0 0 0 path-reachable No No 70 70 1182 546 reflist No No 0 0 0 0 rtc No No 5 5 42 18 rtc-rel No No 10 10 109 49 set-basic No No 96 96 444 86 set-union No No 197 197 770 140 setelems No No 0 0 0 0 store No No 76 76 444 141 store+set No No 40 40 163 52 store-map No No 0 0 0 0 stream No No 218 218 957 408 stream-basic Yes No 4 4 10 3 stream-of-streams No No 0 0 0 0 streamseq-mon-lim No No 4 4 211 118 string No No 0 0 0 0 string-less No No 39 39 118 47 stut-mon No No 65 65 1541 664 wellfounded No No 1 1 4 1 wellfounded-TL No No 0 2 61 40

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 3574 451 219 26 all lib specs No No 0 0 0 0 all nonlib specs No No 3574 451 219 26 all data specs No No 0 0 0 0 all nondata specs No No 3483 415 204 21 all data lib specs No No 0 0 0 0 all nondata lib specs No No 0 0 0 0 all data nonlib specs No No 91 36 15 5 all nondata nonlib specs No No 3483 415 204 21 Ref No No 20 0 1 1 approx-fixpoint No No 37 4 3 0 array No No 48 5 2 1 array-copy No No 100 14 4 0 array-list No No 42 5 3 0 assoclist No No 115 10 3 0 bag-basic No No 36 3 3 1 bag-union No No 49 11 7 0 bool Yes No 16 2 2 1 char No No 34 0 0 1 characteristic No No 26 2 2 0 choice No No 26 0 3 0 data No No 23 0 0 1 elem No No 22 0 0 1 elem-rel No No 22 0 1 0 elemdata No No 23 0 0 0 gelem No No 26 0 0 0 genRef No No 26 0 0 0 genlincell No No 26 0 0 0 hilbert-choice No No 21 1 1 1 inf-app-list No No 23 0 0 0 infinite-append No No 30 0 0 0 infset-basic No No 40 4 4 1 infset-union No No 35 5 5 0 int-abs No No 36 7 6 0 int-basic1 No No 33 6 3 1 int-basic2 No No 24 3 1 0 int-div No No 41 4 0 0 int-gcd No No 45 7 4 0 int-inf No No 31 5 1 0 int-inf-basic Yes No 16 7 3 1 int-min No No 38 8 5 0 int-mult No No 28 3 1 0 int-pair No No 55 11 7 0 int-pot No No 36 3 0 0 int-square No No 25 2 1 0 intnat No No 31 5 2 0 lexical No No 44 1 1 0 lexical-param No No 57 0 0 0 lincell No No 23 0 1 1 linheap No No 30 0 0 1 list No No 38 7 5 0 list-data Yes No 21 12 4 1 list-del No No 101 26 5 0 list-dup No No 39 7 4 0 list-last No No 62 14 5 0 list-perm No No 32 5 3 0 list-set No No 41 8 4 0 list-setequal No No 23 1 1 0 mon-lim-filter-count No No 69 12 6 0 monotone-set-fixpoint No No 52 7 5 0 nat No No 31 5 3 0 nat-basic No No 42 12 3 1 nat-div No No 32 2 0 0 nat-even No No 34 6 4 0 nat-inf No No 48 13 5 1 nat-mult No No 23 2 1 0 nat-pair No No 40 6 5 0 nat-pot No No 36 6 2 0 nat-prime No No 32 7 4 0 nat-sgn No No 25 2 1 0 natstream No No 90 0 0 1 oelem No No 27 3 1 0 oelem-min-max No No 24 2 2 0 olist No No 66 11 4 0 olist-min-max No No 28 4 0 0 olist-sort No No 25 2 1 0 oset No No 61 8 2 0 ostore No No 50 4 1 0 pair Yes No 21 5 3 1 path-reachable No No 55 9 5 0 reflist No No 57 0 0 1 rtc No No 30 3 2 0 rtc-rel No No 33 5 4 0 set-basic No No 42 6 5 1 set-union No No 35 5 5 0 setelems No No 20 0 0 1 store No No 58 11 6 1 store+set No No 42 8 5 0 store-map No No 32 4 2 0 stream No No 114 30 7 0 stream-basic Yes No 17 10 3 1 stream-of-streams No No 80 0 0 1 streamseq-mon-lim No No 38 3 2 0 string No No 53 0 0 1 string-less No No 64 11 3 0 stut-mon No No 80 7 5 0 wellfounded No No 26 2 1 1 wellfounded-TL No No 26 0 0 0