[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem ks-TOPRED
⊦ 〈TOPRED(ks(n); tn)〉 (tn ≠ none → n = 2 ∧ tn = some(K))
Type: A user defined theorem
Validity: The proof is valid.
Features:
Comment:
Used by:
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 2
Proof steps: 25
Used lemmas:
decl-04
,
Used spec theorems:
termfuns
/
ks-rec-01
Used simplifier rules:
termfuns
/
ks-not-S
term
/
disj-01
termfuns
/
ks-zero
term
/
sel-01
term
/
inj
value
/
val-K
termfuns
/
ks-K
term
/
test-03
term
/
elim
term_or_none
/
inj
term_or_none
/
disj