---

Step * of Lemma consensus-rcv-crosses-threshold

∀[V:Type]
  ∀A:Id List. ∀t:ℕ+. ∀n:ℤ. ∀L:consensus-rcv(V;A) List. ∀r:consensus-rcv(V;A).
    (∃a:{a:Id| (a ∈ A)} 
      ∃v:V. ((r = Vote[a;n;v] ∈ consensus-rcv(V;A)) ∧ (¬↑null(filter(λr.n - 1 <z inning(r);L))) ∧ (0 ≤ n))) supposing 
       ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n;L @ [r]))||) and 
       (||values-for-distinct(IdDeq;votes-from-inning(n;L))|| ≤ (2 * t)))
BY
{ (Auto
   THEN AllHyps h.(RepUR ``values-for-distinct`` h THEN (RWO "length-map" h THENA Auto)) 
   THEN RepUR ``votes-from-inning`` -1
   THEN (RWO "mapfilter-append" (-1) THENA Auto)
   THEN Fold `votes-from-inning` (-1)
   THEN (RWO "map_append_sq" (-1) THENA Auto)) }

1
1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. n : ℤ@i
5. L : consensus-rcv(V;A) List@i
6. r : consensus-rcv(V;A)@i
7. ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(n;L)))|| ≤ (2 * t)
8. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(n;L))
   @ map(λp.(fst(p));votes-from-inning(n;[r])))||
⊢ ∃a:{a:Id| (a ∈ A)} 
   ∃v:V. ((r = Vote[a;n;v] ∈ consensus-rcv(V;A)) ∧ (¬↑null(filter(λr.n - 1 <z inning(r);L))) ∧ (0 ≤ n))

---

Latex:


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


By

(Auto
  THEN  AllHyps  h.(RepUR  ``values-for-distinct``  h  THEN  (RWO  "length-map"  h  THENA  Auto)) 
  THEN  RepUR  ``votes-from-inning``  -1
  THEN  (RWO  "mapfilter-append"  (-1)  THENA  Auto)
  THEN  Fold  `votes-from-inning`  (-1)
  THEN  (RWO  "map\_append\_sq"  (-1)  THENA  Auto))

---

Home Index