Nuprl Definition : graph-rcvset
graph-rcvset(a;b;S;G;k) ==
isrcv(k)
∧b tag(k) = b
∧b lname(lnk(k)) = a source(lnk(k)) destination(lnk(k))
∧b source(lnk(k)) ∈b S)
∧b destination(lnk(k)) ∈b G source(lnk(k)))
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
,
apply: f a
FDL editor aliases :
graph-rcvset
graph-rcvset(a;b;S;G;k) ==
isrcv(k)
\mwedge{}\msubb{} tag(k) = b
\mwedge{}\msubb{} lname(lnk(k)) = a source(lnk(k)) destination(lnk(k))
\mwedge{}\msubb{} source(lnk(k)) \mmember{}\msubb{} S)
\mwedge{}\msubb{} destination(lnk(k)) \mmember{}\msubb{} G source(lnk(k)))
Date html generated:
2015_07_17-AM-09_13_20
Last ObjectModification:
2012_02_25-AM-10_53_34
Home
Index