---

paxos-new-ballot(n; np_or_2b_or_firstballot; d; prevb) ==
  case np_or_2b_or_firstballot
  of inl(x) => case x
               of inl(np) => case prevb
                             of inl(b) => if (np = b)
                                          then inl (b + n) 
                                          else ff
                                          fi 
                              | inr(x) => ff
                | inr(y) => case y
                            of inl(2b) => case prevb
                                          of inl(b) => let b',ok = 2b in
                                                         if ((ok)
                                                             (b' = b))
                                                             (isl(d))
                                                        then inl (b + n) 
                                                        else ff
                                                        fi 
                                           | inr(x) => ff
                             | inr(firstballot) => case prevb
                                                   of inl(b) => ff
                                                    | inr(x) => firstballot
   | inr(x) => ff

---

Definitions :  bfalse: ff,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  add: n + m,  inl: inl x ,  isl: isl(x),  bnot: b,  eq_int: (i = j),  band: p  q,  ifthenelse: if b then t else f fi ,  spread: spread def
FDL editor aliases :  paxos-new-ballot

---

paxos-new-ballot(n;  np\_or\_2b\_or$_{firstballot}$;  d;  prevb)  ==
    case  np\_or\_2b\_or$_{firstballot}$
    of  inl(x)  =>  case  x
                              of  inl(np)  =>  case  prevb
                                                          of  inl(b)  =>  if  (np  =\msubz{}  b)  then  inl  (b  +  n)    else  ff  fi 
                                                            |  inr(x)  =>  ff
                                |  inr(y)  =>  case  y
                                                        of  inl(2b)  =>  case  prevb
                                                                                    of  inl(b)  =>  let  b',ok  =  2b  in
                                                                                                                  if  ((\mneg{}\msubb{}ok)  \mwedge{}\msubb{}  (b'  =\msubz{}  b))  \mwedge{}\msubb{}  (\mneg{}\msubb{}isl(d))
                                                                                                                then  inl  (b  +  n) 
                                                                                                                else  ff
                                                                                                                fi 
                                                                                      |  inr(x)  =>  ff
                                                          |  inr(firstballot)  =>  case  prevb
                                                                                                      of  inl(b)  =>  ff
                                                                                                        |  inr(x)  =>  firstballot
      |  inr(x)  =>  ff


Date html generated: 2010_08_28-PM-01_58_24
Last ObjectModification: 2010_07_15-PM-02_26_48

Home Index