---

Step * 1 of Lemma votes-from-inning-is-nil


1. V : Type
2. A : Id List
3. L : consensus-rcv(V;A) List
4. i : ℤ
5. n : ℤ
6. filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)
7. n < i
8. i@0 : ℕ||L||@i
9. ↑inning(L[i@0]) =z i@i
⊢ False
BY
{ (RenameVar `j' (-2)
   THEN (Assert (L[j] ∈ filter(λr.n <z inning(r);L)) BY
               ((BLemma `member_filter` THEN Reduce 0) THEN Auto))
   ) }

1
1. V : Type
2. A : Id List
3. L : consensus-rcv(V;A) List
4. i : ℤ
5. n : ℤ
6. filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)
7. n < i
8. j : ℕ||L||@i
9. ↑inning(L[j]) =z i@i
10. (L[j] ∈ L)
⊢ ↑n <z inning(L[j])

2
1. V : Type
2. A : Id List
3. L : consensus-rcv(V;A) List
4. i : ℤ
5. n : ℤ
6. filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)
7. n < i
8. j : ℕ||L||@i
9. ↑inning(L[j]) =z i@i
10. (L[j] ∈ filter(λr.n <z inning(r);L))
⊢ False

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  L  :  consensus-rcv(V;A)  List
4.  i  :  \mBbbZ{}
5.  n  :  \mBbbZ{}
6.  filter(\mlambda{}r.n  <z  inning(r);L)  =  []
7.  n  <  i
8.  i@0  :  \mBbbN{}||L||@i
9.  \muparrow{}inning(L[i@0])  =\msubz{}  i@i
\mvdash{}  False


By

(RenameVar  `j'  (-2)
  THEN  (Assert  (L[j]  \mmember{}  filter(\mlambda{}r.n  <z  inning(r);L))  BY
                          ((BLemma  `member\_filter`  THEN  Reduce  0)  THEN  Auto))
  )

---

Home Index