[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 theorems.
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 6 6 86 16
lib specs 1814 1814 6492 2427
total 1820 1820 6578 2443
challenge2 No No 6 6 86 16
int-tree No No 0 0 0 0
elem No Yes 0 0 0 0
gref No Yes 0 0 0 0
heap No Yes 47 47 236 107
heap-sep No Yes 49 49 211 110
int-abs No Yes 276 276 505 107
int-basic1 No Yes 51 51 120 40
int-basic2 No Yes 55 55 164 40
int-div No Yes 439 439 2416 1148
int-min No Yes 34 34 82 9
int-mult No Yes 291 291 953 429
linked-tree No Yes 5 5 19 8
maplet No Yes 29 29 181 90
nat No Yes 119 119 227 66
nat-basic1 Yes Yes 64 64 105 4
nat-basic2 No Yes 65 65 182 56
node Yes Yes 0 0 0 0
node-heap No Yes 0 0 0 0
obj No Yes 0 0 0 0
ops No Yes 0 0 35 3
ref No Yes 0 0 0 0
refobj No Yes 0 0 0 0
refset No Yes 0 0 0 0
separation No Yes 10 10 24 10
set-basic No Yes 95 95 428 88
set-union No Yes 185 185 604 112
tree Yes Yes 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 592 158 89 11
all lib specs No No 537 152 87 11
all nonlib specs No No 55 6 2 0
all data specs No No 46 96 38 6
all nondata specs No No 569 110 70 8
all data lib specs No No 23 48 19 3
all nondata lib specs No No 514 104 68 8
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 55 6 2 0
challenge2 No No 48 6 2 0
int-tree No No 7 0 0 0
elem No Yes 6 0 0 1
gref No Yes 8 0 0 0
heap No Yes 99 21 11 1
heap-sep No Yes 66 14 14 0
int-abs No Yes 27 7 6 0
int-basic1 No Yes 29 6 3 1
int-basic2 No Yes 9 3 1 0
int-div No Yes 24 4 2 0
int-min No Yes 31 8 5 0
int-mult No Yes 15 3 1 0
linked-tree No Yes 15 2 1 0
maplet No Yes 33 6 6 0
nat No Yes 15 5 4 0
nat-basic1 Yes Yes 6 9 3 1
nat-basic2 No Yes 13 5 1 0
node Yes Yes 7 18 7 1
node-heap No Yes 6 0 0 1
obj No Yes 6 0 0 1
ops No Yes 18 7 0 0
ref No Yes 8 0 1 1
refobj No Yes 2 0 0 0
refset No Yes 7 0 0 1
separation No Yes 13 2 2 0
set-basic No Yes 39 6 5 1
set-union No Yes 25 5 5 0
tree Yes Yes 10 21 9 1