---

Step * 2 1 1 2 1 1 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
10. (u ∈ count-repeats(L,eq))
11. ||L|| < 2 * (snd(u))
⊢ ||L|| < 2 * ||filter(λy.(eq y x);L)||
BY
{ TACTIC:(DVar `u' THEN All Reduce THEN FLemma `member-count-repeats3` [-2] THEN Auto) }

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


By

---

Latex:
TACTIC:(DVar  `u'  THEN  All  Reduce  THEN  FLemma  `member-count-repeats3`  [-2]  THEN  Auto)

---

Home Index