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 3463 3491 28084 9796 lib specs 531 531 1656 377 total 3994 4022 29740 10173 approx-fixpoint No No 6 6 107 61 array No No 21 21 97 25 array-as-listinstance No No 0 6 41 18 array-copy No No 73 73 435 113 array-listops No No 1 1 18 9 assoclist No No 33 33 199 62 bag-basic No No 7 7 28 6 bag-union No No 46 46 301 103 cube No No 42 42 248 18 cube+array No No 3 3 24 9 filter-count No No 37 37 283 79 gen-ring No No 0 0 0 0 gen-tord No No 0 0 0 0 gen-tord-min-max No No 0 0 0 0 gen-weakord No No 0 0 0 0 get-outside No No 0 0 0 0 inf-app-list No No 5 5 428 213 inf-app-list-old No No 5 5 441 210 infinite-append No No 12 12 772 365 infinite-append-old No No 9 9 689 323 infset-basic No No 67 67 210 11 infset-union No No 179 179 671 46 list No No 137 137 501 83 list-as-arrayinstance No No 0 18 237 108 list-data Yes No 28 28 70 0 list-del No No 309 309 1795 342 list-dup No No 101 101 624 146 list-getput No No 9 9 58 15 list-last No No 165 165 632 149 list-perm No No 142 142 880 265 list-set No No 136 136 767 144 matrix No No 30 30 250 2 matrix+array No No 2 2 16 6 matrixops No No 21 21 237 123 mon-lim-filter-count No No 84 84 2184 1085 mon-lim-filter-count-old No No 84 84 2190 1089 monotone-set-fixpoint No No 14 14 127 66 natset No No 6 6 30 15 oarray-sort No No 0 2 10 3 olist No No 86 86 627 193 olist-min-max No No 108 108 875 155 olist-sort No No 27 27 98 38 oset No No 113 113 366 85 ostore No No 40 40 151 36 ostore+set No No 42 42 187 54 path-reachable No No 67 67 1197 535 putoutside-id No No 0 0 0 0 ring No No 12 12 53 37 rowcol-upd No No 47 47 281 108 rtc No No 5 5 44 19 set-basic No No 99 99 485 90 set-union No No 209 209 859 139 store No No 79 79 459 140 stream No No 239 239 1009 391 stream-basic Yes No 4 4 8 0 stream-old No No 222 222 1073 417 streamseq-mon-lim No No 9 9 595 322 streamseq-mon-lim-old No No 3 3 233 131 stut-mon No No 65 65 1544 663 stut-mon-old No No 65 65 1547 665 tord No No 3 3 8 2 tord-min-max No No 4 4 9 0 weakord No No 5 5 10 0 wellfounded No No 14 14 166 77 woarray No No 0 2 10 3 wolist No No 82 82 590 184 Ref No Yes 0 0 0 0 genlincell No Yes 0 0 0 0 lincell No Yes 0 0 0 0 nat No Yes 120 120 327 61 nat-basic No Yes 125 125 386 39 nat-inf No Yes 73 73 243 77 nat-mult No Yes 213 213 700 200

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 3297 481 208 15 all lib specs No No 151 32 14 4 all nonlib specs No No 3146 449 194 11 all data specs No No 151 32 14 4 all nondata specs No No 3257 459 201 13 all data lib specs No No 0 0 0 0 all nondata lib specs No No 151 32 14 4 all data nonlib specs No No 40 22 7 2 all nondata nonlib specs No No 3106 427 187 9 approx-fixpoint No No 33 4 3 0 array No No 42 5 2 1 array-as-listinstance No No 13 0 0 0 array-copy No No 87 12 4 0 array-listops No No 35 5 3 0 assoclist No No 54 10 3 0 bag-basic No No 31 3 3 1 bag-union No No 56 11 7 0 cube No No 75 12 4 1 cube+array No No 49 6 0 0 filter-count No No 65 8 3 0 gen-ring No No 6 0 0 0 gen-tord No No 6 0 0 0 gen-tord-min-max No No 6 0 0 0 gen-weakord No No 6 0 0 0 get-outside No No 15 1 0 0 inf-app-list No No 19 0 0 0 inf-app-list-old No No 19 0 0 0 infinite-append No No 23 0 0 0 infinite-append-old No No 21 0 0 0 infset-basic No No 47 6 6 1 infset-union No No 35 5 5 0 list No No 58 11 7 0 list-as-arrayinstance No No 55 0 0 0 list-data Yes No 23 12 4 1 list-del No No 102 22 5 0 list-dup No No 44 7 4 0 list-getput No No 35 4 0 0 list-last No No 74 14 5 0 list-perm No No 39 5 3 0 list-set No No 50 8 4 0 matrix No No 60 9 3 1 matrix+array No No 31 4 0 0 matrixops No No 107 19 3 0 mon-lim-filter-count No No 72 11 5 0 mon-lim-filter-count-old No No 71 11 5 0 monotone-set-fixpoint No No 43 7 5 0 natset No No 18 1 1 0 oarray-sort No No 74 0 0 0 olist No No 59 11 4 0 olist-min-max No No 64 12 8 0 olist-sort No No 22 2 1 0 oset No No 47 8 2 0 ostore No No 33 4 1 0 ostore+set No No 47 8 5 0 path-reachable No No 53 9 5 0 putoutside-id No No 20 2 0 0 ring No No 63 9 5 1 rowcol-upd No No 79 12 4 0 rtc No No 26 3 2 0 set-basic No No 47 6 5 1 set-union No No 53 9 8 0 store No No 67 11 6 1 stream No No 135 30 7 0 stream-basic Yes No 17 10 3 1 stream-old No No 135 30 7 0 streamseq-mon-lim No No 39 2 1 0 streamseq-mon-lim-old No No 37 2 1 0 stut-mon No No 81 7 5 0 stut-mon-old No No 80 7 5 0 tord No No 19 1 0 0 tord-min-max No No 21 2 2 0 weakord No No 24 3 1 1 wellfounded No No 61 5 5 0 woarray No No 59 0 0 0 wolist No No 59 11 4 0 Ref No Yes 11 0 1 1 genlincell No Yes 7 0 0 0 lincell No Yes 15 0 1 1 nat No Yes 25 5 3 0 nat-basic No Yes 28 12 3 1 nat-inf No Yes 47 13 5 1 nat-mult No Yes 18 2 1 0