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
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}$:Id]. (processChoose(l$_{comm}$) \mmember{} Process(P.piM\000C(P)))
Date html generated:
2016_05_17-AM-11_35_58
Last ObjectModification:
2015_12_29-PM-06_48_02
Theory : event-logic-applications
Home
Index