[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 4 9 105 25
lib specs 1315 1319 6498 1371
total 2638 2656 13206 2792
VerifyThis1 No No 4 9 105 25
natlist No No 0 0 0 0
elem No Yes 0 0 0 0
gelem No Yes 0 0 0 0
list No Yes 130 130 480 87
list-data Yes Yes 28 28 70 0
list-del No Yes 311 315 1809 340
list-dup No Yes 101 101 624 146
list-getput No Yes 9 9 58 15
list-last No Yes 163 163 644 156
list-perm No Yes 127 127 846 254
list-set No Yes 136 136 767 145
nat No Yes 120 120 327 61
nat-basic No Yes 125 125 386 39
oelem No Yes 8 8 19 3
olist No Yes 57 57 468 125
olist-act No Yes 0 0 0 0
VerifyThis1 4 9 105 25
natlist 0 0 0 0
elem 0 0 0 0
gelem 0 0 0 0
list 130 130 480 87
list-data 28 28 70 0
list-del 311 315 1809 340
list-dup 101 101 624 146
list-getput 9 9 58 15
list-last 163 163 644 156
list-perm 127 127 846 254
list-set 136 136 767 145
nat 120 120 327 61
nat-basic 125 125 386 39
oelem 8 8 19 3
olist 57 57 468 125
olist-act 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 732 118 44 5
all lib specs No No 607 110 41 4
all nonlib specs No No 125 8 3 1
all data specs No No 50 24 8 2
all nondata specs No No 707 106 40 4
all data lib specs No No 25 12 4 1
all nondata lib specs No No 582 98 37 3
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 125 8 3 1
VerifyThis1 No No 92 8 3 0
natlist No No 33 0 0 1
elem No Yes 22 0 0 1
gelem No Yes 26 0 0 0
list No Yes 43 7 5 0
list-data Yes Yes 25 12 4 1
list-del No Yes 93 22 5 0
list-dup No Yes 43 7 4 0
list-getput No Yes 39 4 0 0
list-last No Yes 63 14 5 0
list-perm No Yes 38 5 3 0
list-set No Yes 48 8 4 0
nat No Yes 28 5 3 0
nat-basic No Yes 41 12 3 1
oelem No Yes 27 3 1 0
olist No Yes 62 11 4 0
olist-act No Yes 9 0 0 1