---

three-consensus-ts(V;A;t;f) ==
  <{a:Id| (a  A)}   (consensus-rcv(V;A) List)
  , a.[]
  , x,y.
     a:{a:Id| (a  A)} 
      e:consensus-rcv(V;A)
       ((b:{a:Id| (a  A)} . i:. v:V.
           ((e = Vote[b;i;v])
            ((L:consensus-rcv(V;A) List
                 (L  x b  archive-condition(V;A;t;f;i;v;L)))
               ((e  x a)))))
        (b:{a:Id| (a  A)} . (((b = a))  ((y b) = (x b))))
        ((y a) = ((x a) @ [e])))
  , x.v:V. a:{a:Id| (a  A)} . ((x a) = [Init[v]])>

---

Definitions :  function: x:A  B[x],  pair: <a, b>,  nat: ,  cs-rcv-vote: Vote[a;i;v],  iseg: l1  l2,  archive-condition: archive-condition(V;A;t;f;n;v;L),  and: P  Q,  implies: P  Q,  not: A,  append: as @ bs,  lambda: x.A[x],  exists: x:A. B[x],  all: x:A. B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  equal: s = t,  list: type List,  consensus-rcv: consensus-rcv(V;A),  apply: f a,  cons: [car / cdr],  cs-initial-rcv: Init[v],  nil: []
FDL editor aliases :  three-consensus-ts

---

three-consensus-ts(V;A;t;f)  ==
    <\{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List)
    ,  \mlambda{}a.[]
    ,  \mlambda{}x,y.
          \mexists{}a:\{a:Id|  (a  \mmember{}  A)\} 
            \mexists{}e:consensus-rcv(V;A)
              ((\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}v:V.
                      ((e  =  Vote[b;i;v])
                      {}\mRightarrow{}  ((\mexists{}L:consensus-rcv(V;A)  List.  (L  \mleq{}  x  b  \mwedge{}  archive-condition(V;A;t;f;i;v;L)))
                            \mwedge{}  (\mneg{}(e  \mmember{}  x  a)))))
              \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((\mneg{}(b  =  a))  {}\mRightarrow{}  ((y  b)  =  (x  b))))
              \mwedge{}  ((y  a)  =  ((x  a)  @  [e])))
    ,  \mlambda{}x.\mexists{}v:V.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  ((x  a)  =  [Init[v]])>


Date html generated: 2010_08_27-AM-01_01_57
Last ObjectModification: 2009_12_23-PM-03_34_26

Home Index