[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 7 7 102 11
lib specs 935 935 2164 701
total 942 942 2266 712
matrix No No 0 0 0 0
matrix-dot No No 5 5 30 10
multiply No No 2 2 72 1
int-abs No Yes 281 281 436 65
int-basic1 No Yes 51 51 115 39
int-basic2 No Yes 55 55 167 45
int-mult No Yes 296 296 934 424
nat No Yes 121 121 233 68
nat-basic1 Yes Yes 63 63 95 4
nat-basic2 No Yes 68 68 184 56
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 398 48 26 3
all lib specs No No 192 36 19 2
all nonlib specs No No 206 12 7 1
all data specs No No 32 18 6 2
all nondata specs No No 382 39 23 2
all data lib specs No No 16 9 3 1
all nondata lib specs No No 176 27 16 1
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 206 12 7 1
matrix No No 47 7 5 1
matrix-dot No No 36 5 2 0
multiply No No 123 0 0 0
int-abs No Yes 36 7 6 0
int-basic1 No Yes 33 6 3 1
int-basic2 No Yes 24 3 1 0
int-mult No Yes 28 3 1 0
nat No Yes 28 5 4 0
nat-basic1 Yes Yes 16 9 3 1
nat-basic2 No Yes 27 3 1 0