[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 290 290 5825 2763
lib specs 1720 1720 9983 3022
total 2010 2010 15808 5785
IO-Aut-data Yes No 0 0 0 0
IO-Automaton No No 1 1 4 2
IObackward-INV No No 8 8 210 88
IObackward-INV-is-leqstarrefine No No 5 5 94 42
IOrefine-conds No No 11 11 299 130
IOrefine-conds-imply-IOrefine No No 19 19 695 330
IOrefine-def No No 7 7 75 16
IOtrace No No 92 92 1119 499
IOtrace-lift No No 8 8 121 54
Koenigs-Lemma-gen No No 10 10 497 214
funops No No 3 3 9 0
infgraph-gen No No 0 0 0 0
infgraph-gen-basic No No 0 0 0 0
list-to-set No No 1 1 8 0
min-of-Pnat No No 2 2 8 2
product No No 6 6 152 79
product-refine No No 32 32 1141 620
project-right No No 38 38 759 396
remtau No No 43 43 319 136
remtau-cont No No 3 3 32 16
weakfin-startfin-IObackward-INV-is-leqrefine No No 1 1 283 139
contfun-lim No Yes 18 18 1336 686
infinite-append No Yes 12 12 772 365
list No Yes 139 139 505 85
list-data Yes Yes 30 30 77 2
list-del No Yes 318 318 1855 351
list-dup No Yes 101 101 624 146
list-getput No Yes 9 9 58 15
list-last No Yes 161 161 602 136
nat No Yes 120 120 327 61
nat-basic No Yes 125 125 386 39
nat-inf No Yes 73 73 243 77
option No Yes 2 2 6 0
set-basic No Yes 101 101 489 90
set-union No Yes 213 213 878 148
stream No Yes 269 269 1035 409
stream-basic Yes Yes 4 4 8 0
streamseq-mon-lim No Yes 11 11 616 335
wellfounded No Yes 14 14 166 77
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 2640 322 186 8
all lib specs No No 1118 207 99 6
all nonlib specs No No 1522 115 87 2
all data specs No No 1118 207 99 6
all nondata specs No No 2582 294 175 5
all data lib specs No No 40 22 7 2
all nondata lib specs No No 1078 185 92 4
all data nonlib specs No No 18 6 4 1
all nondata nonlib specs No No 1504 109 83 1
IO-Aut-data Yes No 18 6 4 1
IO-Automaton No No 22 1 1 0
IObackward-INV No No 91 6 6 0
IObackward-INV-is-leqstarrefine No No 35 0 0 0
IOrefine-conds No No 194 16 16 0
IOrefine-conds-imply-IOrefine No No 82 0 0 0
IOrefine-def No No 63 6 6 0
IOtrace No No 82 10 10 0
IOtrace-lift No No 42 0 0 0
Koenigs-Lemma-gen No No 58 9 8 0
funops No No 33 4 4 0
infgraph-gen No No 32 3 3 0
infgraph-gen-basic No No 29 3 3 1
list-to-set No No 19 2 1 0
min-of-Pnat No No 17 2 1 0
product No No 191 13 9 0
product-refine No No 254 16 7 0
project-right No No 145 13 5 0
remtau No No 41 5 3 0
remtau-cont No No 28 0 0 0
weakfin-startfin-IObackward-INV-is-leqrefine No No 46 0 0 0
contfun-lim No Yes 248 32 24 0
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-inf No Yes 47 13 5 1
option No Yes 52 12 7 1
set-basic No Yes 47 6 5 1
set-union No Yes 69 13 10 0
stream No Yes 124 27 8 0
stream-basic Yes Yes 17 10 3 1
streamseq-mon-lim No Yes 39 2 1 0
wellfounded No Yes 61 5 5 0