---

{ [L:simple-consensus-msg() List]. [s:simple-consensus-state()].
    (list_accum(s,v.inning_step() s v;s;L) 
    ~ <map(p.(snd(outr(p)));filter(is-vote-from-inning((snd(s)) - 1);rev(L)))
       @ (fst(s))
    , snd(s)
    >) }

{ Proof }

---

Definitions occuring in Statement :  is-vote-from-inning: is-vote-from-inning(i),  inning_step: inning_step(),  simple-consensus-msg: simple-consensus-msg(),  simple-consensus-state: simple-consensus-state(),  reverse: rev(as),  map: map(f;as),  append: as @ bs,  outr: outr(x),  uall: [x:A]. B[x],  pi1: fst(t),  pi2: snd(t),  apply: f a,  lambda: x.A[x],  pair: <a, b>,  list: type List,  subtract: n - m,  natural_number: $n,  sqequal: s ~ t,  list_accum: list_accum(x,a.f[x; a];y;l),  filter: filter(P;l)
Definitions :  uall: [x:A]. B[x],  list_accum: list_accum(x,a.f[x; a];y;l),  append: as @ bs,  map: map(f;as),  filter: filter(P;l),  reverse: rev(as),  member: t  T,  ycomb: Y,  reduce: reduce(f;k;as),  pi1: fst(t),  pi2: snd(t),  simple-consensus-state: simple-consensus-state(),  inning_step: inning_step(),  ifthenelse: if b then t else f fi ,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  prop: ,  bfalse: ff,  top: Top,  subtype: S  T,  suptype: suptype(S; T),  outr: outr(x),  is-vote-from-inning: is-vote-from-inning(i),  band: p  q,  bnot: b,  isl: isl(x),  simple-consensus-msg: simple-consensus-msg(),  nat: ,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  it:
Lemmas :  simple-consensus-state_wf,  simple-consensus-msg_wf,  inning_step_wf,  eq_int_wf,  bool_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_eq_int,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff,  filter_append_sq,  is-vote-from-inning_wf,  reverse_wf,  map_append_sq,  filter_wf_top,  l_member_wf,  append_assoc_sq,  map_wf,  top_wf,  filter_wf

---

\mforall{}[L:simple-consensus-msg()  List].  \mforall{}[s:simple-consensus-state()].
    (list\_accum(s,v.inning\_step()  s  v;s;L) 
    \msim{}  <map(\mlambda{}p.(snd(outr(p)));filter(is-vote-from-inning((snd(s))  -  1);rev(L)))  @  (fst(s)),  snd(s)>)


Date html generated: 2011_08_17-PM-06_32_26
Last ObjectModification: 2011_06_18-AM-11_55_26

Home Index