[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 6250 6276 36108 12379
lib specs 0 0 0 0
total 6250 6276 36108 12379
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-fsarray No No 0 0 0 0
array-listops No No 1 1 18 9
array-revin No No 6 6 46 14
assoclist No No 35 35 216 67
bag-basic No No 7 7 28 6
bag-union No No 46 46 290 97
bnat No No 1 1 2 0
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
fsarray No No 21 21 79 18
fsarray-copy No No 49 49 265 57
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 694 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 2764 1116
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 1207 437
int-pair No No 14 14 79 34
int-pot No No 153 153 1056 479
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 347
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 153 153 909 274
list-set No No 136 136 767 145
list-setequal No No 13 13 42 8
map No No 79 79 458 139
map+set No No 42 42 187 54
map-ops No No 0 0 0 0
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 146 146 544 170
nat-even No No 53 53 294 51
nat-inf No No 73 73 243 77
nat-mult No No 213 213 699 201
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
ofsarray No No 0 0 0 0
olist No No 86 86 580 177
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
omap No No 40 40 151 36
oset No No 111 111 347 79
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 229 229 828 340
real-square No No 0 0 0 0
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 101 101 491 91
set-union No No 227 227 944 155
setelems 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 4464 618 288 33
all lib specs No No 0 0 0 0
all nonlib specs No No 4464 618 288 33
all data specs No No 0 0 0 0
all nondata specs No No 4388 582 273 28
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 4388 582 273 28
Ref No No 10 0 1 1
approx-fixpoint No No 38 5 4 0
array No No 40 5 2 1
array-as-listinstance No No 13 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
array-revin No No 32 4 2 0
assoclist No No 100 11 3 0
bag-basic No No 31 3 3 1
bag-union No No 55 11 7 0
bnat No No 64 9 6 1
bool Yes No 10 2 2 1
celem No No 8 0 1 0
char No No 17 0 0 1
choice No No 23 0 3 0
data No No 7 0 0 1
elem No No 9 0 0 1
elem-rel No No 8 0 1 0
elemdata No No 6 0 0 0
filter-count No No 50 5 2 0
fsarray No No 40 4 3 1
fsarray-copy No No 80 11 4 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 14 1 0 0
hilbert-choice No No 13 1 1 1
inf-app-list No No 19 0 0 0
infinite-append No No 21 0 0 0
infset-basic No No 47 6 6 1
infset-union No No 34 5 5 0
int-abs No No 38 7 6 0
int-basic1 No No 33 6 3 1
int-basic2 No No 19 3 1 0
int-div No No 27 4 0 0
int-gcd No No 41 7 4 0
int-inf No No 28 5 1 0
int-inf-basic Yes No 14 7 3 1
int-min No No 43 8 5 0
int-mult No No 24 3 1 0
int-pair No No 59 11 7 0
int-pot No No 29 3 0 0
int-square No No 21 2 1 0
intnat No No 30 5 2 0
lexical No No 25 1 1 0
lexical-param No No 16 0 0 0
lincell No No 14 0 1 1
linheap No No 18 0 0 1
list No No 44 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 102 22 5 0
list-dup No No 43 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
list-setequal No No 20 1 1 0
map No No 66 11 6 1
map+set No No 49 8 5 0
map-ops No No 27 4 2 0
matrix No No 60 9 3 1
matrix+array No No 30 4 0 0
matrixops No No 97 19 3 0
mon-lim-filter-count No No 68 11 5 0
monotone-set-fixpoint No No 44 7 5 0
nat No No 24 5 3 0
nat-basic No No 27 12 3 1
nat-div No No 18 2 0 0
nat-even No No 36 6 4 0
nat-inf No No 46 13 5 1
nat-mult No No 17 2 1 0
nat-pair No No 34 6 5 0
nat-pot No No 35 6 2 0
nat-prime No No 28 7 4 0
nat-sgn No No 19 2 1 0
natset No No 35 1 1 0
natstream No No 74 0 0 1
oarray No No 8 0 0 1
oarray-sort No No 71 0 0 0
oelem No No 20 3 1 0
oelem-min-max No No 33 4 2 0
ofsarray No No 8 0 0 1
olist No No 55 11 4 0
olist-act No No 8 0 0 1
olist-min-max No No 60 12 8 0
olist-sort No No 21 2 1 0
omap No No 37 4 1 0
oset No No 46 8 2 0
pair Yes No 11 5 3 1
path-reachable No No 50 9 5 0
putoutside-id No No 20 2 0 0
real-abs No No 46 6 5 0
real-basic No No 53 11 4 1
real-floor-ceil No No 24 4 2 0
real-limit No No 46 7 6 0
real-min-max No No 26 4 2 0
real-multdiv No No 46 8 1 0
real-square No No 25 3 1 0
real-supinf No No 65 9 4 0
reflist No No 47 0 0 1
ring No No 63 9 5 0
rowcol-upd No No 78 12 4 0
rtc No No 22 3 2 0
rtc-rel No No 28 5 4 0
set-basic No No 47 6 5 1
set-union No No 41 6 6 0
setelems No No 7 0 0 1
stream No No 130 30 7 0
stream-basic Yes No 17 10 3 1
stream-of-streams No No 69 0 0 1
streamseq-mon-lim No No 34 2 1 0
string No No 43 0 0 1
string-less No No 65 11 3 0
stut-mon No No 74 7 5 0
wellfounded No No 18 2 1 1
wellfounded-TL No No 16 0 0 0