---

paxos-spec1{i:l}(Info;es;T;Decide) ==
  Vote:EClass(  T)
   ((e1,e2:E(Vote).
       (((fst(Vote(e1))) = (fst(Vote(e2))))  (Vote(e1) = Vote(e2))))
    (W:Id List List
       ((ws1W.(ws2W.a:Id. ((a  ws1)  (a  ws2))))
        (b:. v:T.
            ((Q:Id List
               ((Q  W)
                (aQ.e:E(Vote). ((loc(e) = a)  (Vote(e) = <b, v>)))))
             (e:E(Vote). ((b < (fst(Vote(e))))  ((snd(Vote(e))) = v)))))
        (d:E(Decide)
            Q:Id List
             ((Q  W)
              (b:
                 (aQ.e:E(Vote)
                        ((loc(e) = a)  (Vote(e) = <b, Decide(d)>)))))))))

---

Definitions :  eclass: EClass(A[eo; e]),  int: ,  implies: P  Q,  less_than: a < b,  pi1: fst(t),  pi2: snd(t),  all: x:A. B[x],  l_member: (x  l),  list: type List,  l_all: (xL.P[x]),  exists: x:A. B[x],  es-E-interface: E(X),  and: P  Q,  Id: Id,  es-loc: loc(e),  equal: s = t,  product: x:A  B[x],  nat: ,  pair: <a, b>,  eclass-val: X(e)
FDL editor aliases :  paxos-spec1

---

paxos-spec1\{i:l\}(Info;es;T;Decide)  ==
    \mexists{}Vote:EClass(\mBbbN{}  \mtimes{}  T)
      ((\mforall{}e1,e2:E(Vote).    (((fst(Vote(e1)))  =  (fst(Vote(e2))))  {}\mRightarrow{}  (Vote(e1)  =  Vote(e2))))
      \mwedge{}  (\mexists{}W:Id  List  List
              ((\mforall{}ws1\mmember{}W.(\mforall{}ws2\mmember{}W.\mexists{}a:Id.  ((a  \mmember{}  ws1)  \mwedge{}  (a  \mmember{}  ws2))))
              \mwedge{}  (\mforall{}b:\mBbbN{}.  \mforall{}v:T.
                        ((\mexists{}Q:Id  List.  ((Q  \mmember{}  W)  \mwedge{}  (\mforall{}a\mmember{}Q.\mexists{}e:E(Vote).  ((loc(e)  =  a)  \mwedge{}  (Vote(e)  =  <b,  v>)))))
                        {}\mRightarrow{}  (\mforall{}e:E(Vote).  ((b  <  (fst(Vote(e))))  {}\mRightarrow{}  ((snd(Vote(e)))  =  v)))))
              \mwedge{}  (\mforall{}d:E(Decide)
                        \mexists{}Q:Id  List
                          ((Q  \mmember{}  W)  \mwedge{}  (\mexists{}b:\mBbbN{}.  (\mforall{}a\mmember{}Q.\mexists{}e:E(Vote).  ((loc(e)  =  a)  \mwedge{}  (Vote(e)  =  <b,  Decide(d)>)))))))))


Date html generated: 2010_08_28-AM-11_52_07
Last ObjectModification: 2010_04_16-AM-01_04_34

Home Index