[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 IOrefine-conds-imply-IOrefine
Status:
Proved!
Axioms: 0, User Theorems: 19 (Proved: 19, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 695, Interactions: 330
branchinfw-fw(10,5)
bw-leqstar(3,2)
forward-implies-leqrefine(86,45)
normedfw-branchingfw(10,5)
simpleforward-is-leqrefine(3,2)
branchinfw-fw-aux(22,9)
bwinv-leqstar(37,19)
forward-lem(12,4)
normedfw-branchingfw-aux(89,48)
triang-fin(25,10)
branchingfw-normedfw(10,5)
bwtrueinv(7,3)
imfiniobackwardinv-implies-leqrefine(8,4)
simpleforward-is-forward(5,2)
wbw-leqstar(31,13)
branchingfw-normedfw-aux(38,18)
bwtrueinv-aux(7,4)
imfiniobackwardinv-implies-leqrefine-aux(270,122)
simpleforward-is-forward-aux(22,10)