---

Step * of Lemma votes-from-inning_wf

∀[V:Type]. ∀[A:Id List]. ∀[L:consensus-rcv(V;A) List]. ∀[i:ℤ].  (votes-from-inning(i;L) ∈ ({b:Id| (b ∈ A)}  × V) List)
BY
{ (Auto THEN Unfold `votes-from-inning` 0 THEN Auto THEN All Reduce THEN Auto) }

1
1. V : Type
2. A : Id List
3. L : consensus-rcv(V;A) List
4. i : ℤ
5. ∀x:consensus-rcv(V;A). (↑inning(x) =z i ∈ Type)
6. r : consensus-rcv(V;A)@i
7. ↑inning(r) =z i@i
⊢ let a,j,v = rcvd-vote(r) in 
  <a, v> ∈ {b:Id| (b ∈ A)}  × V

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[L:consensus-rcv(V;A)  List].  \mforall{}[i:\mBbbZ{}].
    (votes-from-inning(i;L)  \mmember{}  (\{b:Id|  (b  \mmember{}  A)\}    \mtimes{}  V)  List)


By

(Auto  THEN  Unfold  `votes-from-inning`  0  THEN  Auto  THEN  All  Reduce  THEN  Auto)

---

Home Index