Nuprl Definition : rcvset
rcvset(a;b;S;k) == isrcv(k) ∧b tag(k) = b ∧b lname(lnk(k)) = a ∧b source(lnk(k)) ∈b S ∧b destination(lnk(k)) ∈b S
Definitions occuring in Statement :
lname: lname(l),
ldst: destination(l),
lsrc: source(l),
tagof: tag(k),
lnk: lnk(k),
isrcv: isrcv(k),
eq_id: a = b,
id-deq: IdDeq,
deq-member: x ∈b L,
band: p ∧b q
FDL editor aliases :
rcvset
Latex:
rcvset(a;b;S;k) ==
isrcv(k) \mwedge{}\msubb{} tag(k) = b \mwedge{}\msubb{} lname(lnk(k)) = a \mwedge{}\msubb{} source(lnk(k)) \mmember{}\msubb{} S \mwedge{}\msubb{} destination(lnk(k)) \mmember{}\msubb{} S
Date html generated:
2016_05_16-AM-10_58_35
Last ObjectModification:
2012_02_25-AM-10_53_31
Theory : event-ordering
Home
Index