[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 1 1 39 5
lib specs 263 263 533 129
total 264 264 572 134
challenge1 No No 1 1 39 5
nat-array No No 0 0 0 0
array No Yes 15 15 19 3
elem No Yes 0 0 0 0
nat No Yes 119 119 227 66
nat-basic1 Yes Yes 64 64 105 4
nat-basic2 No Yes 65 65 182 56
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 110 28 14 4
all lib specs No No 87 26 13 3
all nonlib specs No No 23 2 1 1
all data specs No No 12 18 6 2
all nondata specs No No 104 19 11 3
all data lib specs No No 6 9 3 1
all nondata lib specs No No 81 17 10 2
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 23 2 1 1
challenge1 No No 18 2 1 0
nat-array No No 5 0 0 1
array No Yes 43 7 5 1
elem No Yes 6 0 0 1
nat No Yes 17 5 4 0
nat-basic1 Yes Yes 6 9 3 1
nat-basic2 No Yes 15 5 1 0