---

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 (∀h:hyp. ((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  (\mforall{}h:hyp.  ((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