Nuprl Definition : rcvd-inning-eq
inning(r) =z i == rcv-vote?(r) ∧b let a,j,v = rcvd-vote(r) in (i =z j)
Definitions occuring in Statement :
rcvd-vote: rcvd-vote(x),
rcv-vote?: rcv-vote?(x),
band: p ∧b q,
eq_int: (i =z j),
spreadn: spread3
FDL editor aliases :
rcvd-inning-eq
Latex:
inning(r) =\msubz{} i == rcv-vote?(r) \mwedge{}\msubb{} let a,j,v = rcvd-vote(r) in (i =\msubz{} j)
Date html generated:
2016_05_16-PM-00_34_38
Last ObjectModification:
2012_02_25-AM-11_49_14
Theory : event-ordering
Home
Index