---

Step * of Lemma vote-crosses-threshold

∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ+]. ∀[n1:ℕ]. ∀[n2:ℤ]. ∀[v1:V]. ∀[L1:consensus-rcv(V;A) List]. ∀[a:{a:Id| (a ∈ A)} ].
  ({(n1 = n2 ∈ ℤ) ∧ (¬↑null(filter(λr.n1 - 1 <z inning(r);L1)))}) supposing 
     ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n2;L1 @ [Vote[a;n1;v1]]))||) and 
     (||values-for-distinct(IdDeq;votes-from-inning(n2;L1))|| ≤ (2 * t)))
BY
{ (Auto
   THEN (FLemma `consensus-rcv-crosses-threshold` [-1;-2] THENA Auto)
   THEN ExRepD
   THEN Subst ⌜n1 = n2 ∈ ℤ⌝ 0⋅
   THEN Auto) }

1
.....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 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[n1:\mBbbN{}].  \mforall{}[n2:\mBbbZ{}].  \mforall{}[v1:V].  \mforall{}[L1:consensus-rcv(V;A)  List].
\mforall{}[a:\{a:Id|  (a  \mmember{}  A)\}  ].
    (\{(n1  =  n2)  \mwedge{}  (\mneg{}\muparrow{}null(filter(\mlambda{}r.n1  -  1  <z  inning(r);L1)))\})  supposing 
          ((((2  *  t)  +  1)  \mleq{}  ||values-for-distinct(IdDeq;votes-from-inning(n2;L1
              @  [Vote[a;n1;v1]]))||)  and 
          (||values-for-distinct(IdDeq;votes-from-inning(n2;L1))||  \mleq{}  (2  *  t)))


By

---

Latex:
(Auto
  THEN  (FLemma  `consensus-rcv-crosses-threshold`  [-1;-2]  THENA  Auto)
  THEN  ExRepD
  THEN  Subst  \mkleeneopen{}n1  =  n2\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index