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