[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 35 35 541 279
lib specs 811 811 2156 732
total 846 846 2697 1011
array-of-int No No 0 0 0 0
prefixsum No No 15 15 388 187
split-finalzeros No No 20 20 153 92
array No Yes 10 10 15 3
elem No Yes 0 0 0 0
int-basic1 No Yes 51 51 120 40
int-basic2 No Yes 55 55 164 40
nat No Yes 119 119 227 66
nat-basic1 Yes Yes 64 64 105 4
nat-basic2 No Yes 65 65 182 56
nat-div No Yes 138 138 395 155
nat-even No Yes 51 51 219 47
nat-mult No Yes 214 214 573 239
nat-pot No Yes 44 44 156 82
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 425 62 37 5
all lib specs No No 229 49 27 4
all nonlib specs No No 196 13 10 1
all data specs No No 12 18 6 2
all nondata specs No No 419 53 34 4
all data lib specs No No 6 9 3 1
all nondata lib specs No No 223 40 24 3
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 196 13 10 1
array-of-int No No 4 0 0 1
prefixsum No No 168 9 8 0
split-finalzeros No No 24 4 2 0
array No Yes 40 5 4 1
elem No Yes 6 0 0 1
int-basic1 No Yes 35 6 3 1
int-basic2 No Yes 12 3 1 0
nat No Yes 20 5 4 0
nat-basic1 Yes Yes 6 9 3 1
nat-basic2 No Yes 18 5 1 0
nat-div No Yes 15 2 2 0
nat-even No Yes 32 6 4 0
nat-mult No Yes 10 2 1 0
nat-pot No Yes 35 6 4 0