---

Step * 1 4 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. -any : (Vote[b;i;v] ∈ L)@i
9. ∃y:consensus-rcv(V;A). ((y ∈ L) ∧ ((↑((λr.inning(r) =z i) y)) c∧ (<b, v> = ((λr.let a,j,v = rcvd-vote(r) in <a, v>) y\000C) ∈ ({b:Id| (b ∈ A)}  × V))))@i
10. ∀x:consensus-rcv(V;A). ((x ∈ L) c∧ (↑inning(x) =z i) ∈ Type)
11. r : consensus-rcv(V;A)@i
12. (r ∈ L) c∧ (↑inning(r) =z i)@i
13. (Vote[b;i;v] ∈ L)@i
⊢ let a,j,v = rcvd-vote(r) in 
  <a, v> ∈ {b:Id| (b ∈ A)}  × V
BY
{ (D -2
   THEN DVar `r'⋅
   THEN All (RepUR ``rcvd-inning-eq rcv-vote? rcvd-vote``)
   THEN Try (Trivial)
   THEN RepeatFor 2 (D (-3))
   THEN All Reduce
   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.  -any  :  (Vote[b;i;v]  \mmember{}  L)@i
9.  \mexists{}y:consensus-rcv(V;A)
        ((y  \mmember{}  L)  \mwedge{}  ((\muparrow{}((\mlambda{}r.inning(r)  =\msubz{}  i)  y))  c\mwedge{}  (<b,  v>  =  ((\mlambda{}r.let  a,j,v  =  rcvd-vote(r)  in  <a,  v>)  y))\000C))@i
10.  \mforall{}x:consensus-rcv(V;A).  ((x  \mmember{}  L)  c\mwedge{}  (\muparrow{}inning(x)  =\msubz{}  i)  \mmember{}  Type)
11.  r  :  consensus-rcv(V;A)@i
12.  (r  \mmember{}  L)  c\mwedge{}  (\muparrow{}inning(r)  =\msubz{}  i)@i
13.  (Vote[b;i;v]  \mmember{}  L)@i
\mvdash{}  let  a,j,v  =  rcvd-vote(r)  in 
    <a,  v>  \mmember{}  \{b:Id|  (b  \mmember{}  A)\}    \mtimes{}  V


By

(D  -2
  THEN  DVar  `r'\mcdot{}
  THEN  All  (RepUR  ``rcvd-inning-eq  rcv-vote?  rcvd-vote``)
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  (D  (-3))
  THEN  All  Reduce
  THEN  Auto)

---

Home Index