---

Step * 2 1 of Lemma strict-majority-property

.....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)||
BY
{ TACTIC:(ReduceUnionEq⋅ (-2)⋅ THENA Auto) }

1
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))
7. (fst(hd(filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq))))) = x ∈ T
⊢ ||L|| < 2 * ||filter(λy.(eq y x);L)||

---

Latex:

---

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


By

---

Latex:
TACTIC:(ReduceUnionEq\mcdot{}  (-2)\mcdot{}  THENA  Auto)

---

Home Index