---

{ [V:Type]. [A:Id List]. [W:{a:Id| (a  A)}  List List]. [s:ConsensusState].
  [i:]. [v,v2:V].
    (v = v2) supposing 
       (in state s, inning i has committed v2 and 
       in state s, inning i could commit v  and 
       two-intersection(A;W)) }

{ 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,  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  set: {x:A| B[x]} ,  list: type List,  int: ,  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  member: t  T,  and: P  Q,  prop: ,  cs-inning-committable: in state s, inning i could commit v ,  cs-inning-committed: in state s, inning i has committed v,  exists: x:A. B[x],  two-intersection: two-intersection(A;W),  all: x:A. B[x],  implies: P  Q,  or: P  Q,  cs-archived: by state s, a archived v in inning i,  cs-not-completed: in state s, a has not completed inning i,  l_all: (xL.P[x]),  not: A,  false: False,  guard: {T}
Lemmas :  cs-inning-committed_wf,  cs-inning-committable_wf,  two-intersection_wf,  consensus-state4_wf,  Id_wf,  l_member_wf

---

\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].  \mforall{}[s:ConsensusState].  \mforall{}[i:\mBbbZ{}].  \mforall{}[v,v2:V].
    (v  =  v2)  supposing 
          (in  state  s,  inning  i  has  committed  v2  and 
          in  state  s,  inning  i  could  commit  v    and 
          two-intersection(A;W))


Date html generated: 2011_08_16-AM-10_01_26
Last ObjectModification: 2011_06_18-AM-08_58_54

Home Index