---

Step * 1 2 1 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. \\%2 : (b ∈ A)@i
7. v : V@i
8. (Vote[b;i;v] ∈ L)@i
9. (Vote[b;i;v] ∈ L)
⊢ ↑inning(Vote[b;i;v]) =z i
BY
{ (RepUR ``rcvd-inning-eq rcv-vote? cs-rcv-vote rcvd-vote`` 0 THEN RW assert_pushdownC 0 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.  \mbackslash{}\mbackslash{}\%2  :  (b  \mmember{}  A)@i
7.  v  :  V@i
8.  (Vote[b;i;v]  \mmember{}  L)@i
9.  (Vote[b;i;v]  \mmember{}  L)
\mvdash{}  \muparrow{}inning(Vote[b;i;v])  =\msubz{}  i


By

(RepUR  ``rcvd-inning-eq  rcv-vote?  cs-rcv-vote  rcvd-vote``  0  THEN  RW  assert\_pushdownC  0  THEN  Auto)\mcdot{}

---

Home Index