---

{ [V:Type]
    A:Id List. L:consensus-rcv(V;A) List. i:. b:{b:Id| (b  A)} . v:V.
      ((<b, v>  votes-from-inning(i;L))  (Vote[b;i;v]  L)) }

{ Proof }

---

Definitions occuring in Statement :  votes-from-inning: votes-from-inning(i;L),  cs-rcv-vote: Vote[a;i;v],  consensus-rcv: consensus-rcv(V;A),  Id: Id,  nat: ,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  set: {x:A| B[x]} ,  pair: <a, b>,  product: x:A  B[x],  list: type List,  universe: Type,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  votes-from-inning: votes-from-inning(i;L),  member: t  T,  prop: ,  spreadn: spread3,  rcvd-vote: rcvd-vote(x),  outr: outr(x),  exists: x:A. B[x],  and: P  Q,  cand: A c B,  iff: P  Q,  implies: P  Q,  rev_implies: P  Q,  le: A  B,  top: Top,  subtype: S  T,  so_lambda: x.t[x],  not: A,  false: False,  nat: ,  squash: T,  true: True,  cs-rcv-vote: Vote[a;i;v],  rcvd-inning-eq: inning(r) = i,  band: p  q,  rcv-vote?: rcv-vote?(x),  btrue: tt,  ifthenelse: if b then t else f fi ,  consensus-rcv: consensus-rcv(V;A),  assert: b,  bfalse: ff,  pi1: fst(t),  pi2: snd(t),  so_apply: x[s]
Lemmas :  Id_wf,  l_member_wf,  nat_wf,  consensus-rcv_wf,  mapfilter_wf,  rcvd-inning-eq_wf,  assert_wf,  cs-rcv-vote_wf,  iff_functionality_wrt_iff,  member-mapfilter,  iff_weakening_uiff,  eq_int_wf,  assert_of_eq_int,  pi1_wf_top,  pi2_wf,  le_wf,  squash_wf,  true_wf,  nat_properties

---

\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}L:consensus-rcv(V;A)  List.  \mforall{}i:\mBbbN{}.  \mforall{}b:\{b:Id|  (b  \mmember{}  A)\}  .  \mforall{}v:V.
        ((<b,  v>  \mmember{}  votes-from-inning(i;L))  \mLeftarrow{}{}\mRightarrow{}  (Vote[b;i;v]  \mmember{}  L))


Date html generated: 2011_08_16-AM-10_11_22
Last ObjectModification: 2011_06_18-AM-09_04_07

Home Index