Nuprl Definition : paxos_A2

paxos_A2(es;AcceptorState) ==
  e:E(AcceptorState)
    let msg = info(e) in
        (msg-header(msg) = pax_p2a())
         (v:acceptor-state(). (v  AcceptorState(e)  ((fst(snd(msg-body(msg)))) = ballot_num(v))))


Proof not projected



Definitions occuring in Statement :  ballot_num: ballot_num(astate),  acceptor-state: acceptor-state(),  pax_p2a: pax_p2a(),  Ballot_Num: Ballot_Num(),  msg-header: msg-header(m),  msg-body: msg-body(msg),  es-E-interface: E(X),  classrel: v  X(e),  es-info: info(e),  name: Name,  let: let,  pi1: fst(t),  pi2: snd(t),  all: x:A. B[x],  implies: P  Q,  equal: s = t
FDL editor aliases :  paxos_A2
paxos\_A2(es;AcceptorState)  ==
    \mforall{}e:E(AcceptorState)
        let  msg  =  info(e)  in
                (msg-header(msg)  =  pax\_p2a())
                {}\mRightarrow{}  (\mforall{}v:acceptor-state()
                            (v  \mmember{}  AcceptorState(e)  {}\mRightarrow{}  ((fst(snd(msg-body(msg))))  =  ballot\_num(v))))


Date html generated: 2011_10_20-PM-11_57_53
Last ObjectModification: 2011_06_22-PM-12_30_59

Home Index