---

cs-ref-map-constraints(V;A;W;f) ==
  s:ConsensusState. i:.
    ((i < ||f s||  a:{a:Id| (a  A)} . (i  Inning(s;a)))
     ((i < ||f s||)
       ((f s[i] = INITIAL
           v,v':V
               (((v = v'))
                in state s, inning i could commit v 
                in state s, inning i could commit v' ))
          (f s[i] = WITHDRAWN
            (v:V. in state s, inning i could commit v ))
          (v:V
              ((f s[i] = COMMITED[v]  in state s, inning i has committed v)
               (f s[i] = CONSIDERING[v]
                 in state s, inning i could commit v 
                     (in state s, inning i has committed v)
                     (v':V
                         (in state s, inning i could commit v' 
                          (v' = v)))))))))

---

Definitions :  consensus-state4: ConsensusState,  nat: ,  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  le: A  B,  cs-inning: Inning(s;a),  less_than: a < b,  length: ||as||,  cs-initial: INITIAL,  cs-withdrawn: WITHDRAWN,  exists: x:A. B[x],  cs-commited: COMMITED[v],  iff: P  Q,  consensus-state3: consensus-state3(T),  select: l[i],  apply: f a,  cs-considering: CONSIDERING[v],  and: P  Q,  not: A,  cs-inning-committed: in state s, inning i has committed v,  all: x:A. B[x],  implies: P  Q,  cs-inning-committable: in state s, inning i could commit v ,  equal: s = t
FDL editor aliases :  cs-ref-map-constraints

---

cs-ref-map-constraints(V;A;W;f)  ==
    \mforall{}s:ConsensusState.  \mforall{}i:\mBbbN{}.
        ((i  <  ||f  s||  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (i  \mleq{}  Inning(s;a)))
        \mwedge{}  ((i  <  ||f  s||)
            {}\mRightarrow{}  ((f  s[i]  =  INITIAL
                    \mLeftarrow{}{}\mRightarrow{}  \mexists{}v,v':V
                              ((\mneg{}(v  =  v'))
                              \mwedge{}  in  state  s,  inning  i  could  commit  v 
                              \mwedge{}  in  state  s,  inning  i  could  commit  v'  ))
                  \mwedge{}  (f  s[i]  =  WITHDRAWN  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(\mexists{}v:V.  in  state  s,  inning  i  could  commit  v  ))
                  \mwedge{}  (\mforall{}v:V
                            ((f  s[i]  =  COMMITED[v]  \mLeftarrow{}{}\mRightarrow{}  in  state  s,  inning  i  has  committed  v)
                            \mwedge{}  (f  s[i]  =  CONSIDERING[v]
                                \mLeftarrow{}{}\mRightarrow{}  in  state  s,  inning  i  could  commit  v 
                                        \mwedge{}  (\mneg{}in  state  s,  inning  i  has  committed  v)
                                        \mwedge{}  (\mforall{}v':V.  (in  state  s,  inning  i  could  commit  v'    {}\mRightarrow{}  (v'  =  v)))))))))


Date html generated: 2010_08_27-AM-12_51_48
Last ObjectModification: 2009_12_23-PM-03_27_34

Home Index