---

Step * 1 of Lemma vote-crosses-threshold

.....equality..... 
1. V : Type
2. A : Id List
3. t : ℕ+
4. n1 : ℕ
5. n2 : ℤ
6. v1 : V
7. L1 : consensus-rcv(V;A) List
8. a : {a:Id| (a ∈ A)} 
9. ||values-for-distinct(IdDeq;votes-from-inning(n2;L1))|| ≤ (2 * t)
10. ((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n2;L1 @ [Vote[a;n1;v1]]))||
11. a1 : {a:Id| (a ∈ A)} 
12. v : V
13. Vote[a;n1;v1] = Vote[a1;n2;v] ∈ consensus-rcv(V;A)
14. ¬↑null(filter(λr.n2 - 1 <z inning(r);L1))
15. 0 ≤ n2
⊢ n1 = n2 ∈ ℤ
BY
{ (Thin (-2) THEN RepUR ``cs-rcv-vote consensus-rcv`` -2 THEN Auto)⋅ }

---

Latex:


.....equality..... 
1.  V  :  Type
2.  A  :  Id  List
3.  t  :  \mBbbN{}\msupplus{}
4.  n1  :  \mBbbN{}
5.  n2  :  \mBbbZ{}
6.  v1  :  V
7.  L1  :  consensus-rcv(V;A)  List
8.  a  :  \{a:Id|  (a  \mmember{}  A)\} 
9.  ||values-for-distinct(IdDeq;votes-from-inning(n2;L1))||  \mleq{}  (2  *  t)
10.  ((2  *  t)  +  1)  \mleq{}  ||values-for-distinct(IdDeq;votes-from-inning(n2;L1  @  [Vote[a;n1;v1]]))||
11.  a1  :  \{a:Id|  (a  \mmember{}  A)\} 
12.  v  :  V
13.  Vote[a;n1;v1]  =  Vote[a1;n2;v]
14.  \mneg{}\muparrow{}null(filter(\mlambda{}r.n2  -  1  <z  inning(r);L1))
15.  0  \mleq{}  n2
\mvdash{}  n1  =  n2


By

(Thin  (-2)  THEN  RepUR  ``cs-rcv-vote  consensus-rcv``  -2  THEN  Auto)\mcdot{}

---

Home Index