---

Step * 2 of Lemma strict-majority-property


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. strict-majority(eq;L) = (inl x) ∈ (T?)
⊢ ||L|| < 2 * ||filter(λy.(eq y x);L)||
BY
{ TACTIC:(RepUR ``strict-majority let`` -1
          THEN (SplitOnHypITE -1  THENA Auto)
          THEN Try ((RWO "filter_is_nil" (-1) THEN CompleteAuto))) }

1
.....falsecase..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. (inl (fst(hd(filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)))))) = (inl x) ∈ (T?)
6. ¬(filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) = [] ∈ ((Top × ℤ) List))
⊢ ||L|| < 2 * ||filter(λy.(eq y x);L)||

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
5.  strict-majority(eq;L)  =  (inl  x)
\mvdash{}  ||L||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

Latex:
TACTIC:(RepUR  ``strict-majority  let``  -1
                THEN  (SplitOnHypITE  -1    THENA  Auto)
                THEN  Try  ((RWO  "filter\_is\_nil"  (-1)  THEN  CompleteAuto)))

---

Home Index