[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 5 5 123 41
lib specs 1133 1133 4080 1007
total 1138 1138 4203 1048
relaxed-prefix No No 5 5 123 41
elem No Yes 0 0 0 0
list No Yes 131 131 354 87
list-data Yes Yes 30 30 46 0
list-del No Yes 313 313 1489 334
list-dup No Yes 104 104 572 166
list-last No Yes 167 167 458 144
list-set No Yes 137 137 635 145
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 98 4
nat-basic2 No Yes 68 68 189 56
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 421 91 48 3
all lib specs No No 367 89 46 3
all nonlib specs No No 54 2 2 0
all data specs No No 90 42 18 4
all nondata specs No No 376 70 39 1
all data lib specs No No 45 21 9 2
all nondata lib specs No No 322 68 37 1
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 54 2 2 0
relaxed-prefix No No 54 2 2 0
elem No Yes 20 0 0 1
list No Yes 34 6 5 0
list-data Yes Yes 30 12 6 1
list-del No Yes 91 26 11 0
list-dup No Yes 35 7 4 0
list-last No Yes 52 11 8 0
list-set No Yes 39 8 4 0
nat No Yes 26 5 4 0
nat-basic1 Yes Yes 15 9 3 1
nat-basic2 No Yes 25 5 1 0