---

Step * of Lemma consensus-rcv-crosses-size

∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ+]. ∀[n:ℤ]. ∀[L:consensus-rcv(V;A) List]. ∀[r:consensus-rcv(V;A)].
  (||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(n;L @ [r])))|| = ((2 * t) + 1) ∈ ℤ) 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)
   THEN RepUR ``votes-from-inning`` 0
   THEN (RWO "mapfilter-append" 0 THENA Auto)
   THEN Fold `votes-from-inning` 0
   THEN (RWO "map_append_sq" 0 THENA Auto)) }

1
1. V : Type
2. A : Id List
3. t : ℕ+
4. n : ℤ
5. L : consensus-rcv(V;A) List
6. r : consensus-rcv(V;A)
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])))||
⊢ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(n;L)) @ map(λp.(fst(p));votes-from-inning(n;[r])))||
= ((2 * t) + 1)
∈ ℤ

---

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)].
    (||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(n;L  @  [r])))||
          =  ((2  *  t)  +  1))  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)
  THEN  RepUR  ``votes-from-inning``  0
  THEN  (RWO  "mapfilter-append"  0  THENA  Auto)
  THEN  Fold  `votes-from-inning`  0
  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto))

---

Home Index