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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
pi-process: pi-process()
Latex:
\mforall{}[l$_{comm}$,l$_{choose}$:Id]. (processComm(l$_\mbackslash{}ff7\000Cbcomm}$;l$_{choose}$) \mmember{} Process(P.piM(P)))
Date html generated:
2016_05_17-AM-11_36_29
Last ObjectModification:
2015_12_29-PM-06_47_48
Theory : event-logic-applications
Home
Index