[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 specs4444796283
lib specs1728174886631872
total35443584189184310
array-setNoNo0000
challenge1NoNo4444796283
list-of-natarrayNoNo0000
natarrayNoNo0000
arrayNoYes21219725
array-copyNoYes7575447122
array-listopsNoYes11189
elemNoYes0000
gelemNoYes0000
get-outsideNoYes0000
listNoYes13013046680
list-as-arrayinstanceNoYes018234108
list-dataYesYes2828700
list-delNoYes3153151809340
list-dupNoYes101101624146
list-getputNoYes995815
list-lastNoYes163163628148
list-permNoYes138138866259
list-setNoYes136136767145
natNoYes12012032761
nat-basicNoYes12512538639
oarrayNoYes0000
oarray-sortNoYes0232
oelemNoYes88193
olistNoYes5959470127
olist-actNoYes0000
set-basicNoYes999948691
set-unionNoYes200200888152
array-set0000
challenge14444796283
list-of-natarray0000
natarray0000
array21219725
array-copy7575447122
array-listops11189
elem0000
gelem0000
get-outside0000
list13013046680
list-as-arrayinstance018234108
list-data2828700
list-del3153151809340
list-dup101101624146
list-getput995815
list-last163163628148
list-perm138138866259
list-set136136767145
nat12012032761
nat-basic12512538639
oarray0000
oarray-sort0232
oelem88193
olist5959470127
olist-act0000
set-basic999948691
set-union200200888152

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo11981647010
all lib specsNoNo938144607
all nonlib specsNoNo26020103
all data specsNoNo482482
all nondata specsNoNo1174152669
all data lib specsNoNo241241
all nondata lib specsNoNo914132566
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo26020103
array-setNoNo19001
challenge1NoNo17820100
list-of-natarrayNoNo32001
natarrayNoNo31001
arrayNoYes41521
array-copyNoYes861240
array-listopsNoYes35530
elemNoYes10001
gelemNoYes6000
get-outsideNoYes15100
listNoYes45750
list-as-arrayinstanceNoYes53000
list-dataYesYes241241
list-delNoYes1032250
list-dupNoYes44740
list-getputNoYes35400
list-lastNoYes751450
list-permNoYes39530
list-setNoYes50840
natNoYes25530
nat-basicNoYes281231
oarrayNoYes8001
oarray-sortNoYes56000
oelemNoYes21310
olistNoYes551140
olist-actNoYes8001
set-basicNoYes47651
set-unionNoYes29550