---

Step * 1 2 2 of Lemma member-votes-from-inning


1. V : Type
2. A : Id List@i
3. L : consensus-rcv(V;A) List@i
4. i : ℕ@i
5. b : Id@i
6. (b ∈ A)@i
7. v : V@i
8. (Vote[b;i;v] ∈ L)@i
9. y : consensus-rcv(V;A)
10. (y ∈ L)
11. ↑inning(y) =z i
⊢ let a,j,v = rcvd-vote(y) in 
  <a, v> ∈ {b:Id| (b ∈ A)}  × V
BY
{ (Thin (-2)
   THEN D -2
   THEN RepUR ``rcvd-inning-eq rcv-vote?`` -1
   THEN Auto
   THEN RepeatFor 2 (D -2)
   THEN All (RepUR ``rcvd-vote``)
   THEN Auto)⋅ }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List@i
3.  L  :  consensus-rcv(V;A)  List@i
4.  i  :  \mBbbN{}@i
5.  b  :  Id@i
6.  (b  \mmember{}  A)@i
7.  v  :  V@i
8.  (Vote[b;i;v]  \mmember{}  L)@i
9.  y  :  consensus-rcv(V;A)
10.  (y  \mmember{}  L)
11.  \muparrow{}inning(y)  =\msubz{}  i
\mvdash{}  let  a,j,v  =  rcvd-vote(y)  in 
    <a,  v>  \mmember{}  \{b:Id|  (b  \mmember{}  A)\}    \mtimes{}  V


By

(Thin  (-2)
  THEN  D  -2
  THEN  RepUR  ``rcvd-inning-eq  rcv-vote?``  -1
  THEN  Auto
  THEN  RepeatFor  2  (D  -2)
  THEN  All  (RepUR  ``rcvd-vote``)
  THEN  Auto)\mcdot{}

---

Home Index