---

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


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. u : T × ℕ+
6. v : (T × ℕ+) List
7. filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) = [u / v] ∈ ((T × ℕ+) List)
8. ¬([u / v] = [] ∈ ((Top × ℤ) List))
9. (fst(u)) = x ∈ T
⊢ ||L|| < 2 * ||filter(λy.(eq y x);L)||
BY
{ ((Assert (u ∈ filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq))) BY
          (HypSubst' (-3) 0 THEN Auto THEN (BLemma `cons_member` THENM OrLeft) THEN Auto))
   THEN (RWO "member_filter" (-1) THENA Auto)
   )⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. u : T × ℕ+
6. v : (T × ℕ+) List
7. filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) = [u / v] ∈ ((T × ℕ+) List)
8. ¬([u / v] = [] ∈ ((Top × ℤ) List))
9. (fst(u)) = x ∈ T
10. (u ∈ count-repeats(L,eq)) ∧ (↑((λp.||L|| <z 2 * (snd(p))) u))
⊢ ||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.  u  :  T  \mtimes{}  \mBbbN{}\msupplus{}
6.  v  :  (T  \mtimes{}  \mBbbN{}\msupplus{})  List
7.  filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq))  =  [u  /  v]
8.  \mneg{}([u  /  v]  =  [])
9.  (fst(u))  =  x
\mvdash{}  ||L||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

Latex:
((Assert  (u  \mmember{}  filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq)))  BY
                (HypSubst'  (-3)  0  THEN  Auto  THEN  (BLemma  `cons\_member`  THENM  OrLeft)  THEN  Auto))
  THEN  (RWO  "member\_filter"  (-1)  THENA  Auto)
  )\mcdot{}

---

Home Index