[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 12 12 292 58
lib specs 549 549 1575 352
total 561 561 1867 410
abs No No 12 12 292 58
cuckoo No No 0 0 0 0
slot Yes No 0 0 0 0
table No No 0 0 0 0
array No Yes 12 12 25 6
elem No Yes 0 0 0 0
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 98 4
nat-basic2 No Yes 66 66 187 56
set-basic No Yes 96 96 390 84
set-union No Yes 192 192 636 131
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 305 45 30 6
all lib specs No No 171 35 22 4
all nonlib specs No No 134 10 8 2
all data specs No No 26 18 6 2
all nondata specs No No 275 29 23 4
all data lib specs No No 13 9 3 1
all nondata lib specs No No 158 26 19 3
all data nonlib specs No No 17 7 4 1
all nondata nonlib specs No No 117 3 4 1
abs No No 35 3 4 0
cuckoo No No 63 0 0 0
slot Yes No 17 7 4 1
table No No 19 0 0 1
array No Yes 35 5 4 1
elem No Yes 18 0 0 1
nat No Yes 24 5 4 0
nat-basic1 Yes Yes 13 9 3 1
nat-basic2 No Yes 23 5 1 0
set-basic No Yes 32 6 5 1
set-union No Yes 26 5 5 0