[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 44 208 1521 438
lib specs 1960 1960 9925 2887
total 2004 2168 11446 3325
Hashset No No 7 7 14 7
Hashset-proofs No No 0 85 205 16
Hashset-refines-Set No No 0 69 210 12
Hashset-refines-Set-Theory-Instance No No 3 3 56 26
Set No No 0 0 0 0
Set-Test-IOAut No No 14 14 834 325
Set-proofs No No 0 10 33 3
abs No No 2 2 42 0
elem No No 0 0 0 0
hashset-preds No No 18 18 127 49
tid No No 0 0 0 0
IO-Aut-data Yes Yes 0 0 0 0
IO-Automaton No Yes 1 1 4 2
IOforward No Yes 3 3 89 42
IOforward-is-leqrefine No Yes 2 2 98 49
IOrefine-def No Yes 7 7 75 16
IOtrace No Yes 91 91 1113 497
array No Yes 21 21 97 25
infinite-append No Yes 12 12 772 365
list No Yes 138 138 503 84
list-data Yes Yes 30 30 77 2
list-del No Yes 309 309 1789 338
list-dup No Yes 101 101 624 146
list-getput No Yes 9 9 58 15
list-last No Yes 165 165 632 149
nat No Yes 120 120 327 61
nat-basic No Yes 125 125 386 39
nat-div No Yes 143 143 535 168
nat-inf No Yes 73 73 243 77
nat-mult No Yes 213 213 700 200
opt Yes Yes 0 0 0 0
optfuns No Yes 2 2 6 0
remtau No Yes 43 43 338 148
set-basic No Yes 99 99 485 90
stream No Yes 249 249 966 374
stream-basic Yes Yes 4 4 8 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 2718 1447 230 22
all lib specs No No 1114 194 88 8
all nonlib specs No No 1604 1253 142 14
all data specs No No 1114 194 88 8
all nondata specs No No 2648 1414 217 18
all data lib specs No No 70 33 13 4
all nondata lib specs No No 1044 161 75 4
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 1604 1253 142 14
Hashset No No 949 1079 83 5
Hashset-proofs No No 3 0 0 0
Hashset-refines-Set No No 65 10 0 0
Hashset-refines-Set-Theory-Instance No No 68 8 2 0
Set No No 347 121 41 6
Set-Test-IOAut No No 61 26 7 1
Set-proofs No No 3 0 0 0
abs No No 21 1 1 0
elem No No 14 1 1 1
hashset-preds No No 61 7 6 0
tid No No 12 0 1 1
IO-Aut-data Yes Yes 18 6 4 1
IO-Automaton No Yes 22 1 1 0
IOforward No Yes 61 2 2 0
IOforward-is-leqrefine No Yes 45 0 0 0
IOrefine-def No Yes 63 6 6 0
IOtrace No Yes 82 10 10 0
array No Yes 49 7 3 1
infinite-append No Yes 23 0 0 0
list No Yes 58 11 7 0
list-data Yes Yes 23 12 4 1
list-del No Yes 103 22 5 0
list-dup No Yes 44 7 4 0
list-getput No Yes 35 4 0 0
list-last No Yes 75 14 5 0
nat No Yes 25 5 3 0
nat-basic No Yes 28 12 3 1
nat-div No Yes 19 2 0 0
nat-inf No Yes 47 13 5 1
nat-mult No Yes 18 2 1 0
opt Yes Yes 12 5 2 1
optfuns No Yes 35 5 4 0
remtau No Yes 41 5 3 0
set-basic No Yes 47 6 5 1
stream No Yes 124 27 8 0
stream-basic Yes Yes 17 10 3 1