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 5342 5351 25601 10465 lib specs 0 0 0 0 total 5342 5351 25601 10465 Ref No No 0 0 0 0 approx-fixpoint No No 6 6 101 60 array No No 14 14 40 11 array-copy No No 51 51 249 81 array-list No No 1 1 17 10 assoclist No No 34 34 170 62 assoclista No No 0 0 0 0 bag-basic No No 7 7 22 6 bag-union No No 45 45 181 73 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 compat-store No No 0 9 26 13 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 fixpoint-induction No No 3 3 40 26 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 442 209 infinite-append No No 9 9 688 326 infset-basic No No 53 53 99 1 infset-union No No 137 137 343 35 int-abs No No 281 281 436 65 int-basic1 No No 51 51 115 39 int-basic2 No No 55 55 167 45 int-div No No 463 463 2333 1107 int-gcd No No 192 192 1475 897 int-inf No No 5 5 10 5 int-inf-basic Yes No 1 1 2 0 int-min No No 49 49 138 43 int-mult No No 296 296 934 424 int-pair No No 14 14 66 34 int-pot No No 159 159 852 453 int-square No No 58 58 350 207 intnat No No 133 133 385 159 lincell No No 0 0 0 0 linheap No No 0 0 0 0 list No No 132 132 350 85 list-data Yes No 30 30 44 0 list-del No No 314 314 1463 326 list-dup No No 104 104 498 137 list-last No No 167 167 448 141 list-perm No No 129 129 724 254 list-set No No 137 137 605 135 list-setequal No No 13 13 30 8 lookup No No 2 2 2 2 mon-lim-filter-count No No 93 93 2166 1111 monotone-set-fixpoint No No 16 16 113 70 nat No No 121 121 233 68 nat-basic1 Yes No 63 63 95 4 nat-basic2 No No 68 68 184 56 nat-div No No 139 139 383 154 nat-even No No 51 51 221 46 nat-inf No No 69 69 159 65 nat-inf-basic Yes No 3 3 5 2 nat-mult No No 214 214 527 204 nat-pair No No 36 36 163 119 nat-pot No No 44 44 165 88 nat-prime No No 103 103 570 310 nat-sgn No No 5 5 7 1 natstream No No 0 0 0 0 oelem No No 8 8 10 2 oelem-min-max No No 0 0 0 0 olist No No 57 57 416 124 olist-min-max No No 25 25 404 130 olist-sort No No 27 27 71 38 olista No No 0 0 0 0 oset No No 112 112 216 66 oseta No No 2 2 2 2 ostore No No 40 40 102 32 ostorea No No 0 0 0 0 pair Yes No 0 0 0 0 path-reachable No No 70 70 1107 540 reflist No No 0 0 0 0 rtc No No 5 5 39 18 rtc-rel No No 12 12 109 51 set-basic No No 97 97 323 62 set-union No No 200 200 599 123 setelems No No 0 0 0 0 store No No 79 79 360 125 store+set No No 43 43 147 54 store-map No No 0 0 0 0 stream No No 218 218 851 407 stream-basic Yes No 4 4 6 3 stream-of-streams No No 0 0 0 0 streamseq-mon-lim No No 4 4 207 118 string-append No No 15 15 29 8 string-data Yes No 4 4 7 0 string-less No No 39 39 120 51 string-less-new No No 39 39 102 42 string-new No No 0 0 0 0 stut-mon No No 65 65 1482 664

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 3509 470 295 31 all lib specs No No 0 0 0 0 all nonlib specs No No 3509 470 295 31 all data specs No No 0 0 0 0 all nondata specs No No 3360 415 266 23 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 149 55 29 8 all nondata nonlib specs No No 3360 415 266 23 Ref No No 20 0 1 1 approx-fixpoint No No 37 4 3 0 array No No 43 5 4 1 array-copy No No 81 14 11 0 array-list No No 43 5 5 0 assoclist No No 46 10 5 0 assoclista No No 60 0 0 1 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 compat-store No No 10 0 0 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 fixpoint-induction No No 22 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 35 4 2 0 int-gcd No No 44 7 4 0 int-inf No No 31 5 1 0 int-inf-basic Yes No 16 6 4 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 33 3 1 0 int-square No No 27 3 3 0 intnat No No 31 5 2 0 lincell No No 23 0 1 1 linheap No No 33 0 0 1 list No No 36 6 5 0 list-data Yes No 30 12 6 1 list-del No No 93 26 11 0 list-dup No No 39 7 4 0 list-last No No 54 11 8 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 lookup No No 26 2 2 0 mon-lim-filter-count No No 66 12 7 0 monotone-set-fixpoint No No 45 7 7 0 nat No No 28 5 4 0 nat-basic1 Yes No 16 9 3 1 nat-basic2 No No 27 3 1 0 nat-div No No 26 2 2 0 nat-even No No 34 6 4 0 nat-inf No No 34 8 3 0 nat-inf-basic Yes No 15 5 3 1 nat-mult No No 23 2 1 0 nat-pair No No 40 6 5 0 nat-pot No No 37 6 4 0 nat-prime No No 32 7 4 0 nat-sgn No No 25 2 1 0 natstream No No 97 0 0 1 oelem No No 27 3 1 0 oelem-min-max No No 24 2 2 0 olist No No 42 9 4 0 olist-min-max No No 28 4 2 0 olist-sort No No 25 2 1 0 olista No No 9 0 0 1 oset No No 41 8 6 0 oseta No No 9 0 0 1 ostore No No 32 4 3 0 ostorea No No 9 0 0 1 pair Yes No 21 5 3 1 path-reachable No No 59 9 5 0 reflist No No 64 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 61 12 9 2 store+set No No 42 8 5 0 store-map No No 32 4 2 0 stream No No 88 30 16 0 stream-basic Yes No 16 10 5 1 stream-of-streams No No 87 0 0 1 streamseq-mon-lim No No 35 3 3 0 string-append No No 26 3 2 0 string-data Yes No 19 6 3 1 string-less No No 80 16 5 0 string-less-new No No 64 11 3 0 string-new No No 60 0 0 1 stut-mon No No 77 7 8 0