---

Step * 1 1 of Lemma Process-apply_wf


1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. P : Process(P.M[P])
4. m : pMsg(P.M[P])
5. P = P ∈ Process(P.M[P])
⊢ Continuous+(P.Com(P.M[P]) P)
BY
{ (RepUR ``Com tagged+`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  P  :  Process(P.M[P])
4.  m  :  pMsg(P.M[P])
5.  P  =  P
\mvdash{}  Continuous+(P.Com(P.M[P])  P)


By

---

Latex:
(RepUR  ``Com  tagged+``  0  THEN  Auto)\mcdot{}

---

Home Index