---

Step * 2 1 1 2 1 1 1 1 of Lemma strict-majority-property


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. u1 : T
6. u2 : ℕ+
7. v : (T × ℕ+) List
8. filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) = [<u1, u2> / v] ∈ ((T × ℕ+) List)
9. ¬([<u1, u2> / v] = [] ∈ ((Top × ℤ) List))
10. u1 = x ∈ T
11. (<u1, u2> ∈ count-repeats(L,eq))
12. ||L|| < 2 * u2
13. u2 = ||filter(λy.(eq y u1);L)|| ∈ ℤ
⊢ ||L|| < 2 * ||filter(λy.(eq y x);L)||
BY
{ TACTIC:(HypSubst' (-4) (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
5.  u1  :  T
6.  u2  :  \mBbbN{}\msupplus{}
7.  v  :  (T  \mtimes{}  \mBbbN{}\msupplus{})  List
8.  filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq))  =  [<u1,  u2>  /  v]
9.  \mneg{}([<u1,  u2>  /  v]  =  [])
10.  u1  =  x
11.  (<u1,  u2>  \mmember{}  count-repeats(L,eq))
12.  ||L||  <  2  *  u2
13.  u2  =  ||filter(\mlambda{}y.(eq  y  u1);L)||
\mvdash{}  ||L||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

Latex:
TACTIC:(HypSubst'  (-4)  (-1)  THEN  Auto)

---

Home Index