---

Step * 1 of Lemma votes-from-inning_wf


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
BY
{ (D -2 THEN Try (RepeatFor 2 (D -2)) THEN All (RepUR ``rcvd-inning-eq rcv-vote? rcvd-vote``) THEN Auto) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  L  :  consensus-rcv(V;A)  List
4.  i  :  \mBbbZ{}
5.  \mforall{}x:consensus-rcv(V;A).  (\muparrow{}inning(x)  =\msubz{}  i  \mmember{}  Type)
6.  r  :  consensus-rcv(V;A)@i
7.  \muparrow{}inning(r)  =\msubz{}  i@i
\mvdash{}  let  a,j,v  =  rcvd-vote(r)  in 
    <a,  v>  \mmember{}  \{b:Id|  (b  \mmember{}  A)\}    \mtimes{}  V


By

(D  -2
  THEN  Try  (RepeatFor  2  (D  -2))
  THEN  All  (RepUR  ``rcvd-inning-eq  rcv-vote?  rcvd-vote``)
  THEN  Auto)

---

Home Index