---

{ [V:Type]
    A:Id List. t:. f:V List  V. v0:V. L:consensus-rcv(V;A) List.
      let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in
       (((2 * t) + 1)  ||remove-repeats(IdDeq;map(p.(fst(p));
                                                   votes-from-inning(i 
                                                   - 2;L)))||) supposing 
          ((votes-from-inning(i - 1;L) = []) and 
          (1 < i)) }

{ Proof }

---

Definitions occuring in Statement :  consensus-accum-num-state: consensus-accum-num-state(t;f;v0;L),  votes-from-inning: votes-from-inning(i;L),  consensus-rcv: consensus-rcv(V;A),  id-deq: IdDeq,  Id: Id,  map: map(f;as),  length: ||as||,  nat_plus: ,  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  uimplies: b supposing a,  uall: [x:A]. B[x],  pi1: fst(t),  le: A  B,  all: x:A. B[x],  less_than: a < b,  set: {x:A| B[x]} ,  lambda: x.A[x],  function: x:A  B[x],  product: x:A  B[x],  nil: [],  list: type List,  multiply: n * m,  subtract: n - m,  add: n + m,  natural_number: $n,  universe: Type,  equal: s = t,  l_member: (x  l),  remove-repeats: remove-repeats(eq;L)
Definitions :  member: t  T,  votes-from-inning: votes-from-inning(i;L),  top: Top,  all: x:A. B[x],  subtype: S  T,  cs-initial-rcv: Init[v],  map: map(f;as),  mapfilter: mapfilter(f;P;L),  rcvd-inning-eq: inning(r) = i,  filter: filter(P;l),  band: p  q,  rcv-vote?: rcv-vote?(x),  reduce: reduce(f;k;as),  ifthenelse: if b then t else f fi ,  bfalse: ff,  ycomb: Y,  uimplies: b supposing a,  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  and: P  Q,  cand: A c B,  prop: ,  Id: Id,  so_lambda: x.t[x],  le: A  B,  pi1: fst(t),  cs-rcv-vote: Vote[a;i;v],  not: A,  spreadn: spread3,  rcvd-vote: rcvd-vote(x),  outr: outr(x),  btrue: tt,  implies: P  Q,  false: False,  uall: [x:A]. B[x],  nat_plus: ,  sq_type: SQType(T),  guard: {T},  unzip: unzip(as),  pi2: snd(t),  so_apply: x[s],  nat: ,  bool: ,  unit: Unit,  iff: P  Q,  it:
Lemmas :  mapfilter-append,  consensus-rcv_wf,  top_wf,  rcvd-inning-eq_wf,  l_member_wf,  map_append_sq,  votes-from-inning_wf,  Id_wf,  append-nil,  map_wf,  pi1_wf_top,  consensus-accum-num-property1,  filter_wf,  rcvd-inning-gt_wf,  length_wf1,  zip_wf,  le_wf,  not_wf,  assert_wf,  null_wf3,  values-for-distinct_wf,  nat_plus_properties,  subtype_base_sq,  int_subtype_base,  remove-repeats_wf,  append_wf,  cs-rcv-vote_wf,  unzip_zip,  pi2_wf,  list_subtype_base,  set_subtype_base,  atom2_subtype_base,  eq_int_wf,  bool_wf,  bnot_wf,  iff_weakening_uiff,  uiff_transitivity,  eqtt_to_assert,  assert_of_eq_int,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff

---

\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.
        let  b,i,as,vs,v  =  consensus-accum-num-state(t;f;v0;L)  in
          (((2  *  t)  +  1)  \mleq{}  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(i 
                                                                                                  -  2;L)))||)  supposing 
                ((votes-from-inning(i  -  1;L)  =  [])  and 
                (1  <  i))


Date html generated: 2011_08_16-AM-10_14_07
Last ObjectModification: 2011_06_18-AM-09_06_25

Home Index