---

Step * 1 of Lemma comm-create_wf

.....wf..... 
1. M : Type ─→ Type
2. c : pCom(P.M[P])
⊢ c ∈ "create":Process(P.M[P])
BY
{ (RepUR ``pCom pMsg Com tagged+`` -1 THEN Isect2HD (-1) THEN RepeatFor 2 (Thin (-1)) THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  c  :  pCom(P.M[P])
\mvdash{}  c  \mmember{}  "create":Process(P.M[P])


By

---

Latex:
(RepUR  ``pCom  pMsg  Com  tagged+``  -1
  THEN  Isect2HD  (-1)
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  DoSubsume
  THEN  Auto)

---

Home Index