Nuprl Lemma : processComm_wf
∀[l_comm,l_choose:Id]. (processComm(l_comm;l_choose) ∈ Process(P.piM(P)))
Proof
Definitions occuring in Statement :
processComm: processComm(l_comm;l_choose),
piM: piM(T),
Process: Process(P.M[P]),
Id: Id,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
processComm_wf2,
pi-process_wf,
Id_wf
Latex:
\mforall{}[l$_{comm}$,l$_{choose}$:Id]. (processComm(l$_\mbackslash{}ff7\000Cbcomm}$;l$_{choose}$) \mmember{} Process(P.piM(P)))
Date html generated:
2015_07_23-PM-00_00_05
Last ObjectModification:
2015_01_29-AM-07_42_02
Home
Index