---

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


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. u : T × ℕ+
7. v : (T × ℕ+) List
8. filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) = [u / v] ∈ ((T × ℕ+) List)
⊢ (¬([u / v] = [] ∈ ((Top × ℤ) List))) ⇒ ((fst(u)) = x ∈ T) ⇒ ||L|| < 2 * ||filter(λy.(eq y x);L)||
BY
{ TACTIC:(Thin (-4) THEN 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
⊢ ||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.  (inl  (fst(hd(filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq))))))  =  (inl  x)
6.  u  :  T  \mtimes{}  \mBbbN{}\msupplus{}
7.  v  :  (T  \mtimes{}  \mBbbN{}\msupplus{})  List
8.  filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq))  =  [u  /  v]
\mvdash{}  (\mneg{}([u  /  v]  =  []))  {}\mRightarrow{}  ((fst(u))  =  x)  {}\mRightarrow{}  ||L||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

Latex:
TACTIC:(Thin  (-4)  THEN  Auto)

---

Home Index