---

paxos-decide-relation(es; f; leader; Proposal; Vote; d; b) ==
  d is first@ leader b s.t.  q.||filter(e'.((snd(fst(Vote(e'))) = b)
                                             snd(Vote(e')) =b tt);
                                        (Vote)(q))||
  = (f + 1)
   ((d  (Proposal)')  ((fst((Proposal)'(d))) = b))
   e'<d.(e'  Vote)
     (((snd(fst(Vote(e'))))  b)
        (((snd(fst(Vote(e')))) = b)  ((snd(Vote(e'))) = tt)))

---

Definitions :  es-first-at: e is first@ i s.t.  e.P[e],  apply: f a,  length: ||as||,  filter: filter(P;l),  lambda: x.A[x],  band: p  q,  eq_int: (i = j),  eq_bool: p =b q,  es-interface-predecessors: (X)(e),  add: n + m,  natural_number: $n,  es-prior-val: (X)',  alle-lt: e<e'.P[e],  assert: b,  in-eclass: e  X,  and: P  Q,  le: A  B,  implies: P  Q,  int: ,  pi1: fst(t),  equal: s = t,  bool: ,  pi2: snd(t),  eclass-val: X(e),  btrue: tt

---

paxos-decide-relation(es;  f;  leader;  Proposal;  Vote;  d;  b)  ==
    d  is  first@  leader  b  s.t.    q.||filter(\mlambda{}e'.((snd(fst(Vote(e')))  =\msubz{}  b)  \mwedge{}\msubb{}  snd(Vote(e'))  =b  tt);
                                                                                \mleq{}(Vote)(q))||
    =  (f  +  1)
    \mwedge{}  ((\muparrow{}d  \mmember{}\msubb{}  (Proposal)')  \mwedge{}  ((fst((Proposal)'(d)))  =  b))
    \mwedge{}  \mforall{}e'<d.(\muparrow{}e'  \mmember{}\msubb{}  Vote)
        {}\mRightarrow{}  (((snd(fst(Vote(e'))))  \mleq{}  b)  \mwedge{}  (((snd(fst(Vote(e'))))  =  b)  {}\mRightarrow{}  ((snd(Vote(e')))  =  tt)))


Date html generated: 2010_08_28-PM-12_48_45
Last ObjectModification: 2010_04_16-PM-01_55_13

Home Index