[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 2 2 64 23
lib specs 749 749 3920 1844
total 751 751 3984 1867
implementation No No 0 0 0 0
instance No No 0 0 0 0
verification No No 2 2 64 23
RG2-Theory No Yes 42 42 1847 996
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 98 4
nat-basic2 No Yes 68 68 189 56
nat-div No Yes 139 139 390 160
nat-mult No Yes 214 214 570 240
nat-prime No Yes 103 103 587 317
state No Yes 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 319 31 18 2
all lib specs No No 225 29 16 2
all nonlib specs No No 94 2 2 0
all data specs No No 32 18 6 2
all nondata specs No No 303 22 15 1
all data lib specs No No 16 9 3 1
all nondata lib specs No No 209 20 13 1
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 94 2 2 0
implementation No No 35 0 0 0
instance No No 32 0 0 0
verification No No 27 2 2 0
RG2-Theory No Yes 61 1 1 0
nat No Yes 26 5 4 0
nat-basic1 Yes Yes 16 9 3 1
nat-basic2 No Yes 25 3 1 0
nat-div No Yes 24 2 2 0
nat-mult No Yes 21 2 1 0
nat-prime No Yes 30 7 4 0
state No Yes 22 0 0 1