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
Latex:
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:
2016_05_16-AM-10_58_48
Last ObjectModification:
2012_02_25-AM-10_53_34
Theory : event-ordering
Home
Index