---

{ [V:Type]
    ((v,v':V. ((v = v')))
     (v,v':V.  Dec(v = v'))
     (A:Id List. W:{a:Id| (a  A)}  List List.
          (two-intersection(A;W)
           {s:ConsensusState. i:.
                x:consensus-state3(V)
                 ((x = INITIAL
                   v,v':V
                       (((v = v'))
                        in state s, inning i could commit v 
                        in state s, inning i could commit v' ))
                  (x = WITHDRAWN
                    (v:V. in state s, inning i could commit v ))
                  (v:V
                      ((x = COMMITED[v]
                       in state s, inning i has committed v)
                       (x = 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)))))))}))) }

{ Proof }

---

Definitions occuring in Statement :  two-intersection: two-intersection(A;W),  cs-inning-committable: in state s, inning i could commit v ,  cs-inning-committed: in state s, inning i has committed v,  consensus-state4: ConsensusState,  cs-commited: COMMITED[v],  cs-considering: CONSIDERING[v],  cs-withdrawn: WITHDRAWN,  cs-initial: INITIAL,  consensus-state3: consensus-state3(T),  Id: Id,  decidable: Dec(P),  uall: [x:A]. B[x],  guard: {T},  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  not: A,  implies: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  list: type List,  int: ,  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  implies: P  Q,  exists: x:A. B[x],  all: x:A. B[x],  guard: {T},  one-intersection: one-intersection(A;W),  l_all: (xL.P[x]),  member: t  T,  prop: ,  not: A,  and: P  Q,  iff: P  Q,  rev_implies: P  Q,  false: False,  cand: A c B,  cs-inning-committable: in state s, inning i could commit v ,  or: P  Q,  two-intersection: two-intersection(A;W),  decidable: Dec(P),  uimplies: b supposing a,  consensus-state3: consensus-state3(T),  cs-commited: COMMITED[v],  cs-considering: CONSIDERING[v],  cs-withdrawn: WITHDRAWN,  cs-inning-committed: in state s, inning i has committed v
Lemmas :  l_member_wf,  two-intersection_wf,  Id_wf,  decidable_wf,  not_wf,  decidable__cs-inning-two-committable,  decidable__cs-inning-committed,  decidable__cs-inning-committable-some,  consensus-state4_wf,  consensus-state3-unequal,  cs-commited_wf,  consensus-state3_wf,  cs-initial_wf,  cs-inning-committable_wf,  cs-withdrawn_wf,  cs-inning-committed_wf,  cs-considering_wf,  iff_wf,  cs-inning-committed-single,  cs-not-completed_wf,  cs-archived_wf

---

\mforall{}[V:Type]
    ((\mexists{}v,v':V.  (\mneg{}(v  =  v')))
    {}\mRightarrow{}  (\mforall{}v,v':V.    Dec(v  =  v'))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
                (two-intersection(A;W)
                {}\mRightarrow{}  \{\mforall{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.
                            \mexists{}x:consensus-state3(V)
                              ((x  =  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{}  (x  =  WITHDRAWN  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(\mexists{}v:V.  in  state  s,  inning  i  could  commit  v  ))
                              \mwedge{}  (\mforall{}v:V
                                        ((x  =  COMMITED[v]  \mLeftarrow{}{}\mRightarrow{}  in  state  s,  inning  i  has  committed  v)
                                        \mwedge{}  (x  =  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: 2011_08_16-AM-10_02_31
Last ObjectModification: 2011_06_18-AM-09_00_39

Home Index