---

Step * of Lemma member-votes-from-inning

∀[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))
BY
{ ((UnivCD THENA Auto) THEN Unfold `votes-from-inning` 0) }

1
1. [V] : Type
2. A : Id List@i
3. L : consensus-rcv(V;A) List@i
4. i : ℕ@i
5. b : {b:Id| (b ∈ A)} @i
6. v : V@i
⊢ (<b, v> ∈ mapfilter(λr.let a,j,v = rcvd-vote(r) in <a, v>;λr.inning(r) =z i;L)) ⇐⇒ (Vote[b;i;v] ∈ L)

---

Latex:


\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))


By

((UnivCD  THENA  Auto)  THEN  Unfold  `votes-from-inning`  0)

---

Home Index