---

Step * of Lemma process-subtype

∀[M,E:Type ─→ Type].
  (process(P.M[P];P.E[P]) ⊆r (M[process(P.M[P];P.E[P])]
     ─→ (process(P.M[P];P.E[P]) × E[process(P.M[P];P.E[P])]))) supposing 
     (Continuous+(P.E[P]) and 
     Continuous+(P.M[P]))
BY
{ (Auto THEN Unfold `process` 0 THEN BLemma `corec-subtype` THEN Auto) }

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].
    (process(P.M[P];P.E[P])  \msubseteq{}r  (M[process(P.M[P];P.E[P])]
          {}\mrightarrow{}  (process(P.M[P];P.E[P])  \mtimes{}  E[process(P.M[P];P.E[P])])))  supposing 
          (Continuous+(P.E[P])  and 
          Continuous+(P.M[P]))


By

(Auto  THEN  Unfold  `process`  0  THEN  BLemma  `corec-subtype`  THEN  Auto)

---

Home Index