[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 specs5151564174
lib specs7957952788817
total8468463352991
bag-arrayNoNo16169538
gearrayNoNo0000
lrsNoNo11166
lrs-opsNoNo116216
nat-setNoNo0000
orderNoNo1120
sortNoNo11287
sortedNoNo885011
suffixNoNo9918450
suffix-arrayNoNo13137627
suffix-array-baseNoNo0000
suffix-array-opsNoNo115119
arrayNoYes1212256
array-copyNoYes363617155
array-spliceNoYes3838525228
bag-basicNoYes55144
bag-unionNoYes393920385
elemNoYes0000
gelemNoYes0000
lcpNoYes775718
min-maxNoYes1010170
natNoYes12112123971
nat-basic1YesYes6262984
nat-basic2NoYes666618756
oelemNoYes88113
osetNoYes10810822576
osetaNoYes2222
set-basicNoYes959538984
set-unionNoYes186186625125

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo737106768
all lib specsNoNo47788606
all nonlib specsNoNo26018162
all data specsNoNo121862
all nondata specsNoNo73197737
all data lib specsNoNo6931
all nondata lib specsNoNo47179575
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo26018162
bag-arrayNoNo15320
gearrayNoNo5000
lrsNoNo23220
lrs-opsNoNo44110
nat-setNoNo6001
orderNoNo24330
sortNoNo42220
sortedNoNo21220
suffixNoNo21220
suffix-arrayNoNo24320
suffix-array-baseNoNo17001
suffix-array-opsNoNo18000
arrayNoYes36541
array-copyNoYes8413100
array-spliceNoYes811280
bag-basicNoYes27331
bag-unionNoYes471170
elemNoYes6001
gelemNoYes8000
lcpNoYes25110
min-maxNoYes13220
natNoYes15540
nat-basic1YesYes6931
nat-basic2NoYes13510
oelemNoYes15310
osetNoYes36860
osetaNoYes1001
set-basicNoYes39651
set-unionNoYes25550