---

Step * 2 1 1 1 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. filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) = [] ∈ ((T × ℕ+) List)
⊢ (¬([] = [] ∈ ((Top × ℤ) List))) ⇒ ((fst(hd([]))) = x ∈ T) ⇒ ||L|| < 2 * ||filter(λy.(eq y x);L)||
BY
{ TACTIC:TACTIC:(Thin (-1) THEN Auto) }

---

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.  filter(\mlambda{}p.||L||  <z  2  *  (snd(p));count-repeats(L,eq))  =  []
\mvdash{}  (\mneg{}([]  =  []))  {}\mRightarrow{}  ((fst(hd([])))  =  x)  {}\mRightarrow{}  ||L||  <  2  *  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

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

---

Home Index