Nuprl Definition : paxos_A5

paxos_A5{i:l}(es;Id-lt;accpts;AcceptorState) ==
  elist:E List. bsp:PValue().
    (at-majority-locs(es;elist;accpts;e.as:acceptor-state(). (as  AcceptorState(e)  (bsp  accepted(as))))
     let b = fst(bsp) in
        let s = fst(snd(bsp)) in
        let p = snd(snd(bsp)) in
        all-class-values+{i:l}(es;acceptor-state();AcceptorState;as.bsp':PValue()
                                                                      let b' = fst(bsp') in
                                                                       let s' = fst(snd(bsp')) in
                                                                       let p' = snd(snd(bsp')) in
                                                                       (((bsp'  accepted(as))  (s = s'))
                                                                        (ballot-lt(Id-lt) b b'))
                                                                        (p = p')))


Proof not projected



Definitions occuring in Statement :  accepted: accepted(astate),  acceptor-state: acceptor-state(),  PValue: PValue(),  Command: Command(),  ballot-lt: ballot-lt(Id-lt),  at-majority-locs: at-majority-locs(es;elist;locs;e.P[e]),  all-class-values+: all-class-values+{i:l}(es;T;A;t.P[t]),  classrel: v  X(e),  es-E: E,  let: let,  pi1: fst(t),  pi2: snd(t),  all: x:A. B[x],  implies: P  Q,  and: P  Q,  apply: f a,  list: type List,  int: ,  equal: s = t,  l_member: (x  l)
FDL editor aliases :  paxos_A5
paxos\_A5\{i:l\}(es;Id-lt;accpts;AcceptorState)  ==
    \mforall{}elist:E  List.  \mforall{}bsp:PValue().
        (at-majority-locs(es;elist;accpts;e.\mforall{}as:acceptor-state()
                                                                                    (as  \mmember{}  AcceptorState(e)  {}\mRightarrow{}  (bsp  \mmember{}  accepted(as))))
        {}\mRightarrow{}  let  b  =  fst(bsp)  in
                let  s  =  fst(snd(bsp))  in
                let  p  =  snd(snd(bsp))  in
                all-class-values+\{i:l\}(es;acceptor-state();AcceptorState;as.\mforall{}bsp':PValue()
                                                                                                                                            let  b'  =  fst(bsp')  in
                                                                                                                                              let  s'  =  fst(snd(bsp'))  in
                                                                                                                                              let  p'  =  snd(snd(bsp'))  in
                                                                                                                                              (((bsp'  \mmember{}  accepted(as))
                                                                                                                                              \mwedge{}  (s  =  s'))
                                                                                                                                              \mwedge{}  (ballot-lt(Id-lt)  b  b'))
                                                                                                                                              {}\mRightarrow{}  (p  =  p')))


Date html generated: 2011_10_20-PM-11_59_29
Last ObjectModification: 2011_06_22-PM-12_39_53

Home Index