Nuprl Definition : paxos_C2

paxos_C2{i:l}(Id-lt;accpts;AcceptorState;es) ==
  elist:E List. bsp:PValue().
    (at-majority-locs(es;elist;accpts;e.[v:acceptor-state()]. (bsp  accepted(v)) supposing v  AcceptorState(e))
     all-class-values+{i:l}(es;Id  PValue();BaseClass(pax_p2a();Id
        PValue())@accpts;v.supercompat-pvals(Id-lt;bsp;snd(v))))


Proof not projected



Definitions occuring in Statement :  accepted: accepted(astate),  acceptor-state: acceptor-state(),  pax_p2a: pax_p2a(),  supercompat-pvals: supercompat-pvals(Id-lt;bsp;bsp'),  PValue: PValue(),  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]),  restricted-baseclass: BaseClass(h;T)@locs,  classrel: v  X(e),  es-E: E,  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  pi2: snd(t),  all: x:A. B[x],  implies: P  Q,  product: x:A  B[x],  list: type List,  l_member: (x  l)
FDL editor aliases :  paxos_C2
paxos\_C2\{i:l\}(Id-lt;accpts;AcceptorState;es)  ==
    \mforall{}elist:E  List.  \mforall{}bsp:PValue().
        (at-majority-locs(es;elist;accpts;e.\mforall{}[v:acceptor-state()]
                                                                                    (bsp  \mmember{}  accepted(v))  supposing  v  \mmember{}  AcceptorState(e))
        {}\mRightarrow{}  all-class-values+\{i:l\}(es;Id  \mtimes{}  PValue();BaseClass(pax\_p2a();Id
              \mtimes{}  PValue())@accpts;v.supercompat-pvals(Id-lt;bsp;snd(v))))


Date html generated: 2011_10_21-AM-00_00_18
Last ObjectModification: 2011_06_23-PM-12_33_53

Home Index