Nuprl Definition : paxos_A1

paxos_A1(Id-lt;es;AcceptorState) ==
  e,e':E. b,b':Ballot_Num().
    (acceptor-adopts(es; e; b; AcceptorState)
     (acceptor-adopts(es; e'; b'; AcceptorState)  (e <loc e'))
     (ballot-lt(Id-lt) b b'))


Proof not projected



Definitions occuring in Statement :  acceptor-adopts: acceptor-adopts(es; e; b; AcceptorState),  ballot-lt: ballot-lt(Id-lt),  Ballot_Num: Ballot_Num(),  es-locl: (e <loc e'),  es-E: E,  all: x:A. B[x],  implies: P  Q,  apply: f a
FDL editor aliases :  paxos_A1
paxos\_A1(Id-lt;es;AcceptorState)  ==
    \mforall{}e,e':E.  \mforall{}b,b':Ballot\_Num().
        (acceptor-adopts(es;  e;  b;  AcceptorState)
        {}\mRightarrow{}  (acceptor-adopts(es;  e';  b';  AcceptorState)  {}\mRightarrow{}  (e  <loc  e'))
        {}\mRightarrow{}  (ballot-lt(Id-lt)  b  b'))


Date html generated: 2011_10_20-PM-11_57_28
Last ObjectModification: 2011_06_22-AM-11_50_39

Home Index