---

{ [V:Type]
    ((v,v':V. ((v = v')))
     (v,v':V.  Dec(v = v'))
     (A:Id List. W:{a:Id| (a  A)}  List List.
          (one-intersection(A;W)
           (s:ConsensusState. i:.
                Dec(v,v':V
                     (((v = v'))
                      in state s, inning i could commit v 
                      in state s, inning i could commit v' )))))) }

{ Proof }

---

Definitions occuring in Statement :  one-intersection: one-intersection(A;W),  cs-inning-committable: in state s, inning i could commit v ,  consensus-state4: ConsensusState,  Id: Id,  decidable: Dec(P),  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  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],  member: t  T,  prop: ,  not: A,  decidable: Dec(P),  and: P  Q,  or: P  Q,  cand: A c B,  false: False,  guard: {T}
Lemmas :  decidable__cs-inning-committable-some,  consensus-state4_wf,  one-intersection_wf,  Id_wf,  l_member_wf,  decidable_wf,  not_wf,  decidable__cs-inning-committable-another,  cs-inning-committable_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.
                (one-intersection(A;W)
                {}\mRightarrow{}  (\mforall{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.
                            Dec(\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'  ))))))


Date html generated: 2011_08_16-AM-10_02_23
Last ObjectModification: 2011_06_18-AM-09_00_35

Home Index