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 5447 5473 32543 11179 lib specs 0 0 0 0 total 10894 10946 65086 22358 Ref No No 0 0 0 0 approx-fixpoint No No 7 7 101 52 array No No 21 21 97 25 array-as-listinstance No No 0 6 51 23 array-copy No No 75 75 447 122 array-listops No No 1 1 18 9 array-revin No No 6 6 46 14 assoclist No No 34 34 202 62 bag-basic No No 7 7 28 6 bag-union No No 46 46 290 97 bool Yes No 0 0 0 0 celem No No 0 0 0 0 char No No 0 0 0 0 choice No No 2 2 58 29 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 filter-count No No 24 24 181 61 gelem No No 0 0 0 0 gelem-min-max No No 0 0 0 0 genRef No No 0 0 0 0 genlincell No No 0 0 0 0 get-outside No No 0 0 0 0 hilbert-choice No No 0 0 0 0 inf-app-list No No 5 5 443 212 infinite-append No No 9 9 692 326 infset-basic No No 53 53 184 7 infset-union No No 179 179 670 42 int-abs No No 273 273 617 37 int-basic1 No No 50 50 162 42 int-basic2 No No 54 54 206 45 int-div No No 460 460 2775 1124 int-gcd No No 181 181 1471 790 int-inf No No 5 5 17 7 int-inf-basic Yes No 1 1 3 0 int-min No No 43 43 157 34 int-mult No No 295 295 1232 450 int-pair No No 14 14 79 34 int-pot No No 153 153 1058 480 int-square No No 51 51 463 303 intnat No No 132 132 494 157 lexical No No 3 3 27 9 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 466 80 list+array-ops No No 5 5 41 15 list-as-arrayinstance No No 0 18 234 108 list-data Yes No 28 28 70 0 list-del No No 316 316 1823 344 list-dup No No 101 101 624 146 list-getput No No 9 9 58 15 list-last No No 163 163 628 148 list-perm No No 138 138 866 259 list-set No No 136 136 767 145 list-setequal No No 13 13 42 8 matrix No No 29 29 246 0 matrix+array No No 0 0 0 0 matrixops No No 21 21 245 127 mon-lim-filter-count No No 93 93 2237 1108 monotone-set-fixpoint No No 14 14 127 66 nat No No 120 120 327 61 nat-basic No No 125 125 386 39 nat-div No No 140 140 527 166 nat-even No No 50 50 272 48 nat-inf No No 73 73 243 77 nat-mult No No 212 212 698 199 nat-pair No No 36 36 187 114 nat-pot No No 45 45 220 96 nat-prime No No 97 97 658 310 nat-sgn No No 5 5 12 2 natset No No 6 6 30 15 natstream No No 0 0 0 0 oarray No No 0 0 0 0 oarray-sort No No 0 2 3 2 oelem No No 8 8 19 3 oelem-min-max No No 4 4 9 0 olist No No 60 60 475 130 olist-act No No 0 0 0 0 olist-min-max No No 25 25 427 137 olist-sort No No 27 27 98 38 oset No No 111 111 347 79 ostore No No 40 40 151 36 pair Yes No 0 0 0 0 path-reachable No No 70 70 1213 541 putoutside-id No No 0 0 0 0 reflist No No 0 0 0 0 ring No No 12 12 53 37 rowcol-upd No No 36 36 249 96 rtc No No 5 5 44 18 rtc-rel No No 10 10 114 49 set-basic No No 99 99 486 91 set-union No No 200 200 888 152 setelems No No 0 0 0 0 store No No 78 78 457 140 store+set No No 42 42 187 54 store-map No No 0 0 0 0 stream No No 217 217 1058 411 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 37 37 128 42 stut-mon No No 65 65 1547 665 wellfounded No No 1 1 4 1 wellfounded-TL No No 3 3 62 41 Ref 0 0 0 0 approx-fixpoint 7 7 101 52 array 21 21 97 25 array-as-listinstance 0 6 51 23 array-copy 75 75 447 122 array-listops 1 1 18 9 array-revin 6 6 46 14 assoclist 34 34 202 62 bag-basic 7 7 28 6 bag-union 46 46 290 97 bool 0 0 0 0 celem 0 0 0 0 char 0 0 0 0 choice 2 2 58 29 data 0 0 0 0 elem 0 0 0 0 elem-rel 0 0 0 0 elemdata 0 0 0 0 filter-count 24 24 181 61 gelem 0 0 0 0 gelem-min-max 0 0 0 0 genRef 0 0 0 0 genlincell 0 0 0 0 get-outside 0 0 0 0 hilbert-choice 0 0 0 0 inf-app-list 5 5 443 212 infinite-append 9 9 692 326 infset-basic 53 53 184 7 infset-union 179 179 670 42 int-abs 273 273 617 37 int-basic1 50 50 162 42 int-basic2 54 54 206 45 int-div 460 460 2775 1124 int-gcd 181 181 1471 790 int-inf 5 5 17 7 int-inf-basic 1 1 3 0 int-min 43 43 157 34 int-mult 295 295 1232 450 int-pair 14 14 79 34 int-pot 153 153 1058 480 int-square 51 51 463 303 intnat 132 132 494 157 lexical 3 3 27 9 lexical-param 0 0 0 0 lincell 0 0 0 0 linheap 0 0 0 0 list 130 130 466 80 list+array-ops 5 5 41 15 list-as-arrayinstance 0 18 234 108 list-data 28 28 70 0 list-del 316 316 1823 344 list-dup 101 101 624 146 list-getput 9 9 58 15 list-last 163 163 628 148 list-perm 138 138 866 259 list-set 136 136 767 145 list-setequal 13 13 42 8 matrix 29 29 246 0 matrix+array 0 0 0 0 matrixops 21 21 245 127 mon-lim-filter-count 93 93 2237 1108 monotone-set-fixpoint 14 14 127 66 nat 120 120 327 61 nat-basic 125 125 386 39 nat-div 140 140 527 166 nat-even 50 50 272 48 nat-inf 73 73 243 77 nat-mult 212 212 698 199 nat-pair 36 36 187 114 nat-pot 45 45 220 96 nat-prime 97 97 658 310 nat-sgn 5 5 12 2 natset 6 6 30 15 natstream 0 0 0 0 oarray 0 0 0 0 oarray-sort 0 2 3 2 oelem 8 8 19 3 oelem-min-max 4 4 9 0 olist 60 60 475 130 olist-act 0 0 0 0 olist-min-max 25 25 427 137 olist-sort 27 27 98 38 oset 111 111 347 79 ostore 40 40 151 36 pair 0 0 0 0 path-reachable 70 70 1213 541 putoutside-id 0 0 0 0 reflist 0 0 0 0 ring 12 12 53 37 rowcol-upd 36 36 249 96 rtc 5 5 44 18 rtc-rel 10 10 114 49 set-basic 99 99 486 91 set-union 200 200 888 152 setelems 0 0 0 0 store 78 78 457 140 store+set 42 42 187 54 store-map 0 0 0 0 stream 217 217 1058 411 stream-basic 4 4 10 3 stream-of-streams 0 0 0 0 streamseq-mon-lim 4 4 211 118 string 0 0 0 0 string-less 37 37 128 42 stut-mon 65 65 1547 665 wellfounded 1 1 4 1 wellfounded-TL 3 3 62 41

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 3838 516 241 29 all lib specs No No 0 0 0 0 all nonlib specs No No 3838 516 241 29 all data specs No No 0 0 0 0 all nondata specs No No 3762 480 226 24 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 76 36 15 5 all nondata nonlib specs No No 3762 480 226 24 Ref No No 11 0 1 1 approx-fixpoint No No 42 5 4 0 array No No 41 5 2 1 array-as-listinstance No No 13 0 0 0 array-copy No No 89 12 4 0 array-listops No No 36 5 3 0 array-revin No No 33 4 2 0 assoclist No No 96 10 3 0 bag-basic No No 32 3 3 1 bag-union No No 56 11 7 0 bool Yes No 10 2 2 1 celem No No 9 0 1 0 char No No 20 0 0 1 choice No No 24 0 3 0 data No No 8 0 0 1 elem No No 10 0 0 1 elem-rel No No 9 0 1 0 elemdata No No 6 0 0 0 filter-count No No 55 5 2 0 gelem No No 6 0 0 0 gelem-min-max No No 6 0 0 0 genRef No No 6 0 0 0 genlincell No No 7 0 0 0 get-outside No No 15 1 0 0 hilbert-choice No No 15 1 1 1 inf-app-list No No 19 0 0 0 infinite-append No No 22 0 0 0 infset-basic No No 48 6 6 1 infset-union No No 35 5 5 0 int-abs No No 39 7 6 0 int-basic1 No No 36 6 3 1 int-basic2 No No 20 3 1 0 int-div No No 28 4 0 0 int-gcd No No 43 7 4 0 int-inf No No 29 5 1 0 int-inf-basic Yes No 14 7 3 1 int-min No No 42 8 5 0 int-mult No No 25 3 1 0 int-pair No No 60 11 7 0 int-pot No No 30 3 0 0 int-square No No 22 2 1 0 intnat No No 31 5 2 0 lexical No No 27 1 1 0 lexical-param No No 16 0 0 0 lincell No No 15 0 1 1 linheap No No 18 0 0 1 list No No 45 7 5 0 list+array-ops No No 5 0 0 0 list-as-arrayinstance No No 53 0 0 0 list-data Yes No 24 12 4 1 list-del No No 103 22 5 0 list-dup No No 44 7 4 0 list-getput No No 35 4 0 0 list-last No No 75 14 5 0 list-perm No No 39 5 3 0 list-set No No 50 8 4 0 list-setequal No No 21 1 1 0 matrix No No 63 9 3 1 matrix+array No No 31 4 0 0 matrixops No No 124 19 3 0 mon-lim-filter-count No No 74 12 6 0 monotone-set-fixpoint No No 53 7 5 0 nat No No 25 5 3 0 nat-basic No No 28 12 3 1 nat-div No No 19 2 0 0 nat-even No No 36 6 4 0 nat-inf No No 47 13 5 1 nat-mult No No 18 2 1 0 nat-pair No No 35 6 5 0 nat-pot No No 36 6 2 0 nat-prime No No 29 7 4 0 nat-sgn No No 20 2 1 0 natset No No 35 1 1 0 natstream No No 72 0 0 1 oarray No No 8 0 0 1 oarray-sort No No 62 0 0 0 oelem No No 21 3 1 0 oelem-min-max No No 17 2 2 0 olist No No 56 11 4 0 olist-act No No 8 0 0 1 olist-min-max No No 27 4 0 0 olist-sort No No 22 2 1 0 oset No No 47 8 2 0 ostore No No 35 4 1 0 pair Yes No 11 5 3 1 path-reachable No No 55 9 5 0 putoutside-id No No 20 2 0 0 reflist No No 47 0 0 1 ring No No 64 9 5 0 rowcol-upd No No 79 12 4 0 rtc No No 24 3 2 0 rtc-rel No No 29 5 4 0 set-basic No No 47 6 5 1 set-union No No 29 5 5 0 setelems No No 8 0 0 1 store No No 65 11 6 1 store+set No No 46 8 5 0 store-map No No 28 4 2 0 stream No No 132 30 7 0 stream-basic Yes No 17 10 3 1 stream-of-streams No No 65 0 0 1 streamseq-mon-lim No No 33 3 2 0 string No No 43 0 0 1 string-less No No 68 11 3 0 stut-mon No No 75 7 5 0 wellfounded No No 20 2 1 1 wellfounded-TL No No 17 0 0 0