---

Step * of Lemma comm-create_wf

∀[M:Type ─→ Type]. ∀[c:pCom(P.M[P])].  comm-create(c) ∈ Process(P.M[P]) supposing com-kind(c) = "create" ∈ Atom
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (GenConcl ⌈c = m ∈ "create":Process(P.M[P])⌉⋅ THENA Auto)) }

1
.....wf..... 
1. M : Type ─→ Type
2. c : pCom(P.M[P])
⊢ c ∈ "create":Process(P.M[P])

2
1. M : Type ─→ Type
2. c : pCom(P.M[P])
3. m : "create":Process(P.M[P])@i
4. c = m ∈ "create":Process(P.M[P])@i
⊢ comm-create(m) ∈ Process(P.M[P]) supposing com-kind(m) = "create" ∈ Atom

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[c:pCom(P.M[P])].
    comm-create(c)  \mmember{}  Process(P.M[P])  supposing  com-kind(c)  =  "create"


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  (GenConcl  \mkleeneopen{}c  =  m\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index