[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 specs6363633248
lib specs1308130852391381
total1371137158721629
indexseqNoNo0000
solitaireNoNo6363633248
stackseqNoNo0000
elemNoYes0000
gelemNoYes0000
listNoYes13013035286
list-dataYesYes3030460
list-delNoYes3093091481330
list-dupNoYes104104574167
list-lastNoYes160160425130
list-permNoYes124124774265
list-setNoYes137137637145
natNoYes12112123971
nat-basic1YesYes6262984
nat-basic2NoYes666618756
oelemNoYes88113
olistNoYes5757415124
olistaNoYes0000

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo731139726
all lib specsNoNo425106544
all nonlib specsNoNo30633182
all data specsNoNo8442184
all nondata specsNoNo689118634
all data lib specsNoNo422192
all nondata lib specsNoNo38385452
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo30633182
indexseqNoNo117001
solitaireNoNo13133180
stackseqNoNo58001
elemNoYes18001
gelemNoYes22000
listNoYes26650
list-dataYesYes291261
list-delNoYes7226110
list-dupNoYes34740
list-lastNoYes391180
list-permNoYes25530
list-setNoYes35840
natNoYes24540
nat-basic1YesYes13931
nat-basic2NoYes23510
oelemNoYes20310
olistNoYes38940
olistaNoYes7001