[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 theorems.
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 specs1515719287
lib specs1576157660612010
total1591159167802297
challenge4NoNo22435155
cyclicNoNo1313284132
RefNoYes0000
dataNoYes0000
elemNoYes0000
elemdataNoYes0000
genRefNoYes0000
genlincellNoYes0000
lincellNoYes0000
linheapNoYes0000
listNoYes12812833671
list-dataYesYes3030460
list-delNoYes2692691109264
list-dupNoYes9999580161
list-lastNoYes156156391111
list-setNoYes116116464119
natNoYes11911922766
nat-basic1YesYes64641054
nat-basic2NoYes656518256
nat-divNoYes138138395155
nat-multNoYes214214573239
nat-potNoYes383813366
path-reachableNoYes69691164571
reflistNoYes0000
storeNoYes7171356127

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo5281227110
all lib specsNoNo4611206910
all nonlib specsNoNo67220
all data specsNoNo3042184
all nondata specsNoNo513101628
all data lib specsNoNo152192
all nondata lib specsNoNo44699608
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo67220
challenge4NoNo47000
cyclicNoNo20220
RefNoYes8011
dataNoYes6001
elemNoYes6001
elemdataNoYes2000
genRefNoYes8000
genlincellNoYes9000
lincellNoYes11011
linheapNoYes8001
listNoYes21650
list-dataYesYes91261
list-delNoYes6326110
list-dupNoYes27740
list-lastNoYes371180
list-setNoYes26840
natNoYes17540
nat-basic1YesYes6931
nat-basic2NoYes15510
nat-divNoYes15220
nat-multNoYes10210
nat-potNoYes21640
path-reachableNoYes60950
reflistNoYes15001
storeNoYes611292