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 3670 3700 30177 10580 lib specs 531 531 1655 378 total 4201 4231 31832 10958 approx-fixpoint No No 6 6 107 61 array No No 21 21 97 25 array-as-listinstance No No 0 8 45 18 array-copy No No 73 73 435 113 array-fsarray No No 0 0 0 0 array-listops No No 1 1 18 9 assoclist No No 34 34 214 64 bag-basic No No 7 7 28 6 bag-union No No 49 49 270 85 char No No 0 0 0 0 contfun-lim No No 18 18 1336 686 cube No No 42 42 248 18 cube+array No No 3 3 24 9 either No No 0 0 0 0 filter-count No No 44 44 360 90 forall-indexWhere No No 23 23 189 22 fsarray No No 20 20 79 0 fsarray-copy No No 50 50 277 39 funops No No 3 3 9 0 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 774 365 infinite-append-old No No 9 9 691 323 infset-basic No No 67 67 210 11 infset-union No No 179 179 671 46 list No No 140 140 520 91 list-as-arrayinstance No No 0 18 237 108 list-data Yes No 30 30 77 2 list-del No No 318 318 1800 334 list-dup No No 102 102 659 161 list-getput No No 9 9 58 15 list-last No No 168 168 642 153 list-perm No No 150 150 899 274 list-set No No 136 136 767 144 map No No 79 79 459 138 map+set No No 54 54 238 72 map-ops No No 0 0 0 0 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 2160 1072 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 625 191 olist-min-max No No 108 108 875 155 olist-sort No No 27 27 98 38 omap No No 40 40 151 36 option No No 2 2 6 0 oset No No 113 113 366 85 path-reachable No No 67 67 1197 535 putoutside-id No No 0 0 0 0 relops No No 5 5 44 19 ring No No 12 12 53 37 rowcol-upd No No 47 47 281 108 set-basic No No 101 101 489 90 set-union No No 218 218 891 152 stream No No 269 269 1035 409 stream-basic Yes No 4 4 8 0 stream-old No No 221 221 998 386 streamseq-mon-lim No No 11 11 616 335 streamseq-mon-lim-old No No 3 3 233 131 string No No 0 0 0 0 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 182 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 699 201

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 4181 638 299 20 all lib specs No No 145 32 14 4 all nonlib specs No No 4036 606 285 16 all data specs No No 145 32 14 4 all nondata specs No No 4141 616 292 18 all data lib specs No No 0 0 0 0 all nondata lib specs No No 145 32 14 4 all data nonlib specs No No 40 22 7 2 all nondata nonlib specs No No 3996 584 278 14 approx-fixpoint No No 32 4 3 0 array No No 51 7 3 1 array-as-listinstance No No 14 0 0 0 array-copy No No 164 20 5 0 array-fsarray No No 69 8 1 0 array-listops No No 34 5 3 0 assoclist No No 57 11 3 0 bag-basic No No 30 3 3 1 bag-union No No 84 19 11 0 char No No 17 0 0 1 contfun-lim No No 243 32 24 0 cube No No 77 12 4 1 cube+array No No 48 6 0 0 either No No 82 26 11 1 filter-count No No 64 8 3 0 forall-indexWhere No No 39 7 3 0 fsarray No No 48 5 4 1 fsarray-copy No No 80 11 4 0 funops No No 31 4 4 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 14 1 0 0 inf-app-list No No 18 0 0 0 inf-app-list-old No No 18 0 0 0 infinite-append No No 22 0 0 0 infinite-append-old No No 20 0 0 0 infset-basic No No 46 6 6 1 infset-union No No 34 5 5 0 list No No 59 11 7 0 list-as-arrayinstance No No 59 0 0 0 list-data Yes No 23 12 4 1 list-del No No 102 22 5 0 list-dup No No 46 7 4 0 list-getput No No 34 4 0 0 list-last No No 74 14 5 0 list-perm No No 38 5 3 0 list-set No No 49 8 4 0 map No No 68 11 6 1 map+set No No 46 8 5 0 map-ops No No 55 12 8 0 matrix No No 62 9 3 1 matrix+array No No 30 4 0 0 matrixops No No 106 19 3 0 mon-lim-filter-count No No 71 11 5 0 mon-lim-filter-count-old No No 71 11 5 0 monotone-set-fixpoint No No 41 7 5 0 natset No No 17 1 1 0 oarray-sort No No 78 0 0 0 olist No No 58 11 4 0 olist-min-max No No 63 12 8 0 olist-sort No No 21 2 1 0 omap No No 32 4 1 0 option No No 51 12 7 1 oset No No 46 8 2 0 path-reachable No No 52 9 5 0 putoutside-id No No 19 2 0 0 relops No No 68 13 11 0 ring No No 60 9 5 1 rowcol-upd No No 78 12 4 0 set-basic No No 48 6 5 1 set-union No No 68 13 10 0 stream No No 123 27 8 0 stream-basic Yes No 17 10 3 1 stream-old No No 120 26 7 0 streamseq-mon-lim No No 38 2 1 0 streamseq-mon-lim-old No No 36 2 1 0 string No No 48 14 7 1 stut-mon No No 80 7 5 0 stut-mon-old No No 80 7 5 0 tord No No 18 1 0 0 tord-min-max No No 20 2 2 0 weakord No No 22 3 1 1 wellfounded No No 60 5 5 0 woarray No No 63 0 0 0 wolist No No 58 11 4 0 Ref No Yes 10 0 1 1 genlincell No Yes 7 0 0 0 lincell No Yes 14 0 1 1 nat No Yes 24 5 3 0 nat-basic No Yes 27 12 3 1 nat-inf No Yes 46 13 5 1 nat-mult No Yes 17 2 1 0