[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 16 42 480 180
lib specs 748 754 3426 748
total 1528 1592 7812 1856
VF3conc No No 2 27 314 117
VerifyThis3-sequential No No 5 6 79 33
natpair Yes No 0 0 0 0
sparsearray No No 0 0 0 0
tidset-npset No No 9 9 87 30
array No Yes 21 21 97 25
data No Yes 0 0 0 0
elem No Yes 0 0 0 0
elemdata No Yes 0 0 0 0
matrix No Yes 29 29 249 0
matrix+array No Yes 0 0 0 0
matrixops No Yes 21 21 249 131
nat No Yes 120 120 327 61
nat-basic No Yes 125 125 386 39
natset No Yes 6 6 30 15
ring No Yes 6 12 53 37
set-basic No Yes 99 99 486 91
set-union No Yes 201 201 893 153
store No Yes 78 78 469 142
store+set No Yes 42 42 187 54
VF3conc 2 27 314 117
VerifyThis3-sequential 5 6 79 33
natpair 0 0 0 0
sparsearray 0 0 0 0
tidset-npset 9 9 87 30
array 21 21 97 25
data 0 0 0 0
elem 0 0 0 0
elemdata 0 0 0 0
matrix 29 29 249 0
matrix+array 0 0 0 0
matrixops 21 21 249 131
nat 120 120 327 61
nat-basic 125 125 386 39
natset 6 6 30 15
ring 6 12 53 37
set-basic 99 99 486 91
set-union 201 201 893 153
store 78 78 469 142
store+set 42 42 187 54
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 1295 331 107 14
all lib specs No No 672 94 41 7
all nonlib specs No No 623 237 66 7
all data specs No No 0 0 0 0
all nondata specs No No 1278 326 104 13
all data lib specs No No 0 0 0 0
all nondata lib specs No No 672 94 41 7
all data nonlib specs No No 17 5 3 1
all nondata nonlib specs No No 606 232 63 6
VF3conc No No 432 222 59 5
VerifyThis3-sequential No No 68 5 2 0
natpair Yes No 17 5 3 1
sparsearray No No 35 0 0 1
tidset-npset No No 71 5 2 0
array No Yes 40 5 2 1
data No Yes 20 0 0 1
elem No Yes 22 0 0 1
elemdata No Yes 23 0 0 0
matrix No Yes 58 9 3 1
matrix+array No Yes 35 4 0 0
matrixops No Yes 124 19 3 0
nat No Yes 28 5 3 0
nat-basic No Yes 41 12 3 1
natset No Yes 56 1 1 0
ring No Yes 52 9 5 0
set-basic No Yes 42 6 5 1
set-union No Yes 35 5 5 0
store No Yes 53 11 6 1
store+set No Yes 43 8 5 0