[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 141 141 3493 1910
lib specs 251 251 517 131
total 392 392 4010 2041
CSPAWN+Preds No No 0 0 0 0
IO No No 0 0 0 0
IOfun No No 0 0 0 0
Progress-I-2-Theory No No 14 14 284 165
RG-I-2-Theory No No 37 37 793 431
RG-I-n-Instance No No 0 0 0 0
RG-I-n-Theory No No 18 18 420 212
RG2+DF-Theory No No 43 43 1059 594
RG2+DF-Theory-Ext No No 20 20 380 218
RGI-Conds No No 0 0 0 0
RGn No No 0 0 0 0
RGn-Decomp-Partial No No 6 6 305 147
RGn-Decomp-Total No No 3 3 252 143
RGn-Total No No 0 0 0 0
SEQ No No 0 0 0 0
SPAWN No No 0 0 0 0
cstate No No 0 0 0 0
state No No 0 0 0 0
state+param No No 0 0 0 0
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 94 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 859 66 47 9
all lib specs No No 71 17 8 1
all nonlib specs No No 788 49 39 8
all data specs No No 32 18 6 2
all nondata specs No No 843 57 44 8
all data lib specs No No 16 9 3 1
all nondata lib specs No No 55 8 5 0
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 788 49 39 8
CSPAWN+Preds No No 97 7 7 0
IO No No 22 0 0 2
IOfun No No 29 0 0 2
Progress-I-2-Theory No No 40 3 3 0
RG-I-2-Theory No No 80 1 1 0
RG-I-n-Instance No No 32 0 0 0
RG-I-n-Theory No No 22 0 0 0
RG2+DF-Theory No No 69 1 1 0
RG2+DF-Theory-Ext No No 83 17 12 0
RGI-Conds No No 56 7 5 0
RGn No No 48 8 6 0
RGn-Decomp-Partial No No 30 4 4 0
RGn-Decomp-Total No No 23 0 0 0
RGn-Total No No 30 1 0 0
SEQ No No 28 0 0 0
SPAWN No No 33 0 0 0
cstate No No 20 0 0 1
state No No 24 0 0 1
state+param No No 22 0 0 2
nat No Yes 28 5 4 0
nat-basic1 Yes Yes 16 9 3 1
nat-basic2 No Yes 27 3 1 0