Step
*
of Lemma
system-equiv-is-equiv
∀[M:Type ─→ Type]. EquivRel(System(P.M[P]);S1,S2.system-equiv(P.M[P];S1;S2)) supposing Continuous+(P.M[P])
BY
{ ((Auto THEN (InstLemma `process-equiv-is-equiv` [⌈M⌉]⋅ THENA Auto))
THEN RepeatFor 2 ((D 0 THEN Auto))
THEN DVar `a'
THEN Try (DVar `b')
THEN Try (DVar `c')
THEN All (RepUR ``system-equiv``)
THEN Auto
THEN (AllHyps h.((InstHyp [⌈k⌉] h⋅ THENA Auto) THEN MoveToConcl (-1))
THEN Try ((RepeatFor 2 ((GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0)) THEN (D 0 THENA Auto)))
THEN Try ((GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0 THEN Auto))
THEN Try ((GenConclAtAddr [1] THEN D -2 THEN Reduce 0))
THEN Auto
THEN Try ((BackThruSomeHyp THEN CompleteAuto))
THEN (D 3 THEN Auto)
THEN UseTrans ⌈v4⌉⋅)⋅) }
Latex:
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
EquivRel(System(P.M[P]);S1,S2.system-equiv(P.M[P];S1;S2)) supposing Continuous+(P.M[P])
By
Latex:
((Auto THEN (InstLemma `process-equiv-is-equiv` [\mkleeneopen{}M\mkleeneclose{}]\mcdot{} THENA Auto))
THEN RepeatFor 2 ((D 0 THEN Auto))
THEN DVar `a'
THEN Try (DVar `b')
THEN Try (DVar `c')
THEN All (RepUR ``system-equiv``)
THEN Auto
THEN (AllHyps h.((InstHyp [\mkleeneopen{}k\mkleeneclose{}] h\mcdot{} THENA Auto) THEN MoveToConcl (-1))
THEN Try ((RepeatFor 2 ((GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0))
THEN (D 0 THENA Auto)
))
THEN Try ((GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0 THEN Auto))
THEN Try ((GenConclAtAddr [1] THEN D -2 THEN Reduce 0))
THEN Auto
THEN Try ((BackThruSomeHyp THEN CompleteAuto))
THEN (D 3 THEN Auto)
THEN UseTrans \mkleeneopen{}v4\mkleeneclose{}\mcdot{})\mcdot{})
Home
Index