Nuprl Lemma : processChoose_wf
∀[l_comm:Id]. (processChoose(l_comm) ∈ Process(P.piM(P)))
Proof
Definitions occuring in Statement :
processChoose: processChoose(l_comm),
piM: piM(T),
Process: Process(P.M[P]),
Id: Id,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
processChoose_wf2,
pi-process_wf,
Id_wf
Latex:
\mforall{}[l$_{comm}$:Id]. (processChoose(l$_{comm}$) \mmember{} Process(P.piM\000C(P)))
Date html generated:
2015_07_23-AM-11_59_51
Last ObjectModification:
2015_01_29-AM-07_41_56
Home
Index