[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

Project Statistics

The following tables contain statistical data about the project. The most significant numbers that give an impression about the effort for the project are Proofs - nonlib specs. This line contains a summary for specifications that are not imported from a library, but unique for the project. (Library specifications are orange in the development graph, the other either blue or green, depending on their status.)

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 6155 6181 35682 12278
lib specs 0 0 0 0
total 6155 6181 35682 12278
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 76 76 449 123
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
gen-ring 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 276 276 677 62
int-basic1 No No 50 50 162 42
int-basic2 No No 54 54 206 45
int-div No No 460 460 2766 1117
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 41 41 161 36
int-mult No No 296 296 1205 436
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 131 131 471 80
list+array-ops No No 5 5 41 15
list-as-arrayinstance No No 0 18 235 108
list-data Yes No 30 30 76 1
list-del No No 318 318 1826 346
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 139 139 868 260
list-set No No 136 136 767 145
list-setequal No No 13 13 42 8
matrix No No 30 30 250 2
matrix+array No No 0 0 0 0
matrixops No No 21 21 248 128
mon-lim-filter-count No No 84 84 2206 1095
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 143 143 535 168
nat-even No No 53 53 294 51
nat-inf No No 73 73 243 77
nat-mult No No 213 213 700 200
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 7 2
oelem No No 8 8 19 3
oelem-min-max No No 6 6 14 0
olist No No 81 81 565 171
olist-act No No 0 0 0 0
olist-min-max No No 107 107 855 175
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
real-abs No No 142 142 355 34
real-basic No No 95 95 272 87
real-floor-ceil No No 35 35 209 153
real-limit No No 17 17 342 208
real-min-max No No 18 18 82 0
real-multdiv No No 231 231 832 341
real-supinf No No 6 6 92 38
reflist No No 0 0 0 0
ring No No 12 12 53 37
rowcol-upd No No 47 47 277 102
rtc No No 5 5 44 18
rtc-rel No No 10 10 114 49
set-basic No No 99 99 487 91
set-union No No 225 225 939 155
setelems No No 0 0 0 0
store No No 80 80 461 140
store+set No No 42 42 187 54
store-map No No 0 0 0 0
stream No No 222 222 1076 420
stream-basic Yes No 4 4 10 3
stream-of-streams No No 0 0 0 0
streamseq-mon-lim No No 12 12 482 252
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
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 4185 574 272 30
all lib specs No No 0 0 0 0
all nonlib specs No No 4185 574 272 30
all data specs No No 0 0 0 0
all nondata specs No No 4109 538 257 25
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 4109 538 257 25
Ref No No 11 0 1 1
approx-fixpoint No No 39 5 4 0
array No No 41 5 2 1
array-as-listinstance No No 13 0 0 0
array-copy No No 86 12 4 0
array-listops No No 35 5 3 0
array-revin No No 33 4 2 0
assoclist No No 97 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 19 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 51 5 2 0
gelem No No 6 0 0 0
gelem-min-max No No 6 0 0 0
gen-ring 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 20 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 42 7 4 0
int-inf No No 29 5 1 0
int-inf-basic Yes No 14 7 3 1
int-min No No 44 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 26 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 61 9 3 1
matrix+array No No 31 4 0 0
matrixops No No 109 19 3 0
mon-lim-filter-count No No 69 11 5 0
monotone-set-fixpoint No No 45 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 37 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 36 1 1 0
natstream No No 71 0 0 1
oarray No No 8 0 0 1
oarray-sort No No 70 0 0 0
oelem No No 21 3 1 0
oelem-min-max No No 34 4 2 0
olist No No 56 11 4 0
olist-act No No 8 0 0 1
olist-min-max No No 61 12 8 0
olist-sort No No 22 2 1 0
oset No No 47 8 2 0
ostore No No 38 4 1 0
pair Yes No 11 5 3 1
path-reachable No No 51 9 5 0
putoutside-id No No 20 2 0 0
real-abs No No 47 6 5 0
real-basic No No 54 11 4 1
real-floor-ceil No No 25 4 2 0
real-limit No No 47 7 6 0
real-min-max No No 27 4 2 0
real-multdiv No No 47 8 1 0
real-supinf No No 66 9 4 0
reflist No No 47 0 0 1
ring No No 64 9 5 0
rowcol-upd No No 73 12 4 0
rtc No No 23 3 2 0
rtc-rel No No 29 5 4 0
set-basic No No 48 6 5 1
set-union No No 42 6 6 0
setelems No No 8 0 0 1
store No No 67 11 6 1
store+set No No 50 8 5 0
store-map No No 28 4 2 0
stream No No 130 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 2 1 0
string No No 43 0 0 1
string-less No No 66 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