Step 
*
 of Lemma 
processChoose_wf
∀[l_comm:Id]. (processChoose(l_comm) ∈ Process(P.piM(P)))
BY
 
{ Auto }
 
Latex: 
Latex:
\mforall{}[l$_{comm}$:Id].  (processChoose(l$_{comm}$)  \mmember{}  Process(P.piM\000C(P)))
 By 
Latex:
Auto
Home
Index