[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 55 18
lib specs 293 293 692 180
total 298 298 747 198
lcp No No 5 5 55 18
array No Yes 11 11 21 4
array-copy No Yes 33 33 155 51
elem No Yes 0 0 0 0
nat No Yes 119 119 223 64
nat-basic1 Yes Yes 64 64 105 4
nat-basic2 No Yes 66 66 188 57
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 185 38 23 3
all lib specs No No 160 37 22 3
all nonlib specs No No 25 1 1 0
all data specs No No 12 18 6 2
all nondata specs No No 179 29 20 2
all data lib specs No No 6 9 3 1
all nondata lib specs No No 154 28 19 2
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 25 1 1 0
lcp No No 25 1 1 0
array No Yes 36 5 4 1
array-copy No Yes 84 13 10 0
elem No Yes 6 0 0 1
nat No Yes 15 5 4 0
nat-basic1 Yes Yes 6 9 3 1
nat-basic2 No Yes 13 5 1 0