---

{ [V:Type]. [A:Id List]. [W:{a:Id| (a  A)}  List List].
  [f:ConsensusState  (consensus-state3(V) List)].
    [x,y:ConsensusState]. [i:||f x||].
      (f x[i] = f y[i]) supposing 
         ((v:V
             ((in state x, inning i could commit v 
              in state y, inning i could commit v )
              (in state x, inning i has committed v
                in state y, inning i has committed v))) and 
         (i < ||f y||)) 
    supposing cs-ref-map-constraints(V;A;W;f) }

{ Proof }

---

Definitions occuring in Statement :  cs-ref-map-constraints: cs-ref-map-constraints(V;A;W;f),  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,  consensus-state3: consensus-state3(T),  Id: Id,  select: l[i],  length: ||as||,  int_seg: {i..j},  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  and: P  Q,  less_than: a < b,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  list: type List,  natural_number: $n,  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  and: P  Q,  iff: P  Q,  member: t  T,  le: A  B,  not: A,  implies: P  Q,  false: False,  rev_implies: P  Q,  prop: ,  nat: ,  exists: x:A. B[x],  cand: A c B,  so_lambda: x.t[x],  cs-ref-map-constraints: cs-ref-map-constraints(V;A;W;f),  int_seg: {i..j},  lelt: i  j < k,  or: P  Q,  guard: {T},  so_apply: x[s]
Lemmas :  cs-inning-committable_wf,  cs-inning-committed_wf,  le_wf,  iff_wf,  length_wf1,  consensus-state3_wf,  int_seg_wf,  consensus-state4_wf,  cs-ref-map-constraints_wf,  Id_wf,  l_member_wf,  cs-inning_wf,  select_wf,  cs-initial_wf,  not_wf,  cs-withdrawn_wf,  cs-commited_wf,  cs-considering_wf,  consensus-state3-cases,  and_functionality_wrt_iff,  implies_functionality_wrt_iff,  iff_functionality_wrt_iff,  exists_functionality_wrt_iff,  not_functionality_wrt_iff,  all_functionality_wrt_iff

---

\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].
\mforall{}[f:ConsensusState  {}\mrightarrow{}  (consensus-state3(V)  List)].
    \mforall{}[x,y:ConsensusState].  \mforall{}[i:\mBbbN{}||f  x||].
        (f  x[i]  =  f  y[i])  supposing 
              ((\mforall{}v:V
                      ((in  state  x,  inning  i  could  commit  v    \mLeftarrow{}{}\mRightarrow{}  in  state  y,  inning  i  could  commit  v  )
                      \mwedge{}  (in  state  x,  inning  i  has  committed  v  \mLeftarrow{}{}\mRightarrow{}  in  state  y,  inning  i  has  committed  v)))  and 
              (i  <  ||f  y||)) 
    supposing  cs-ref-map-constraints(V;A;W;f)


Date html generated: 2011_08_16-AM-10_04_09
Last ObjectModification: 2011_06_18-AM-09_00_47

Home Index