---

Step * of Lemma processComm_wf

∀[l_comm,l_choose:Id].  (processComm(l_comm;l_choose) ∈ Process(P.piM(P)))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[l$_{comm}$,l$_{choose}$:Id].    (processComm(l$_\mbackslash{}ff7\000Cbcomm}$;l$_{choose}$)  \mmember{}  Process(P.piM(P)))


By

---

Latex:
Auto

---

Home Index