---

Step * 1 1 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. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. (inr <y2, y4, y5>  ∈ L)@i
12. ↑(i =z y4)@i
13. <b, v> = <y2, y5> ∈ ({b:Id| (b ∈ A)}  × V)@i
⊢ (Vote[b;i;v] ∈ L)
BY
{ ((RW assert_pushdownC (-2) THENA Auto) THEN AutoSimpHyp Auto (-1) THEN All (Fold `cs-rcv-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.  \mbackslash{}\mbackslash{}\%2  :  (b  \mmember{}  A)@i
7.  v  :  V@i
8.  y2  :  \{b:Id|  (b  \mmember{}  A)\}  @i
9.  y4  :  \mBbbN{}@i
10.  y5  :  V@i
11.  (inr  <y2,  y4,  y5>    \mmember{}  L)@i
12.  \muparrow{}(i  =\msubz{}  y4)@i
13.  <b,  v>  =  <y2,  y5>@i
\mvdash{}  (Vote[b;i;v]  \mmember{}  L)


By

((RW  assert\_pushdownC  (-2)  THENA  Auto)
  THEN  AutoSimpHyp  Auto  (-1)
  THEN  All  (Fold  `cs-rcv-vote`)
  THEN  Auto)

---

Home Index