[Imprint]
[Data Privacy Statement]
[E-Mail]
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 base summary for Specification unwinding
Status:
Proved!
Axioms: 5, User Theorems: (Proved: 13, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 160, Interactions: 75
isEqRel-def(0,0)
lemma-5-4-2(21,10)
osc-help(6,2)
unwind-SD-theorem(4,2)
xosc-def(0,0)
isEqRel-reflexive(4,1)
lrf-def(0,0)
osc-intro(4,2)
xlrf-def(0,0)
xosc-is-osc(5,3)
isEqRel-symmetric(4,1)
lrf-intro(4,1)
unwind-BSD-theorem(22,11)
xlrf-intro(4,2)
isEqRel-transitive(4,1)
osc-def(0,0)
unwind-BSRA-theorem(41,21)
xlrf-property(37,18)