---

{ [V:Type]
    A:Id List. t:. f:V List  V. v0:V. L:consensus-rcv(V;A) List. n:.
    v:V.
      (archive-condition(V;A;t;f;n;v;L)
       let b,i,as,vs,w = list_accum(s,r.consensus-accum-num((2 * t)
                                           + 1;f;s;r);
                                       <ff, 0, [], [], v0>;
                                       L) in (b)  ((n + 1) = i)  (v = w)) }

{ Proof }

---

Definitions occuring in Statement :  consensus-accum-num: consensus-accum-num(num;f;s;r),  archive-condition: archive-condition(V;A;t;f;n;v;L),  consensus-rcv: consensus-rcv(V;A),  Id: Id,  assert: b,  bfalse: ff,  nat_plus: ,  nat: ,  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  and: P  Q,  function: x:A  B[x],  pair: <a, b>,  nil: [],  list: type List,  multiply: n * m,  add: n + m,  natural_number: $n,  int: ,  universe: Type,  equal: s = t,  list_accum: list_accum(x,a.f[x; a];y;l)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  member: t  T,  implies: P  Q,  assert: b,  pi1: fst(t),  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  prop: ,  btrue: tt,  ifthenelse: if b then t else f fi ,  bfalse: ff,  uimplies: b supposing a,  true: True,  so_lambda: x.t[x],  iff: P  Q,  and: P  Q,  rev_implies: P  Q,  squash: T,  false: False,  bool: ,  unit: Unit,  so_apply: x[s],  nat: ,  guard: {T},  consensus-accum-num-state: consensus-accum-num-state(t;f;v0;L),  subtype: S  T,  it:
Lemmas :  consensus-accum-num-archives,  archive-consensus-accum-num,  consensus-rcv_wf,  nat_plus_wf,  Id_wf,  consensus-accum-num-state_wf,  nat_plus_inc,  bool_wf,  l_member_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  nat_wf,  true_wf,  archive-condition_wf,  uall_wf,  archive-condition-one-one,  squash_wf,  false_wf,  nat_properties

---

\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:V  List  {}\mrightarrow{}  V.  \mforall{}v0:V.  \mforall{}L:consensus-rcv(V;A)  List.  \mforall{}n:\mBbbN{}.  \mforall{}v:V.
        (archive-condition(V;A;t;f;n;v;L)
        \mLeftarrow{}{}\mRightarrow{}  let  b,i,as,vs,w  =  list\_accum(s,r.consensus-accum-num((2  *  t)  +  1;f;s;r);
                                                                          <ff,  0,  [],  [],  v0>
                                                                          L)  in  (\muparrow{}b)  \mwedge{}  ((n  +  1)  =  i)  \mwedge{}  (v  =  w))


Date html generated: 2011_08_16-AM-10_16_36
Last ObjectModification: 2011_06_18-AM-09_06_41

Home Index