---

Step * 2 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)) = [] ∈ ((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)||
BY
{ ((RepeatFor 2 (MoveToConcl  (-1)) THEN (GenConclAtAddrType ⌜(T × ℕ+) List⌝ [1;1;2]⋅ THENA Auto))
   THEN D -2
   THEN Reduce 0)⋅ }

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)) = [] ∈ ((T × ℕ+) List)
⊢ (¬([] = [] ∈ ((Top × ℤ) List))) ⇒ ((fst(hd([]))) = x ∈ T) ⇒ ||L|| < 2 * ||filter(λy.(eq y x);L)||

2
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)||

---

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


By

---

Latex:
((RepeatFor  2  (MoveToConcl    (-1))  THEN  (GenConclAtAddrType  \mkleeneopen{}(T  \mtimes{}  \mBbbN{}\msupplus{})  List\mkleeneclose{}  [1;1;2]\mcdot{}  THENA  Auto))
  THEN  D  -2
  THEN  Reduce  0)\mcdot{}

---

Home Index