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
inning(r) =\msubz{} i == rcv-vote?(r) \mwedge{}\msubb{} let a,j,v = rcvd-vote(r) in (i =\msubz{} j)
Date html generated:
2015_07_17-AM-11_47_36
Last ObjectModification:
2012_02_25-AM-11_49_14
Home
Index