---

Step * of Lemma member-count-repeats3

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. ∀[n:ℕ+].
  n = ||filter(λy.(eq y x);L)|| ∈ ℤ supposing (<x, n> ∈ count-repeats(L,eq))
BY
{ (Auto THEN RepeatFor 2 (D -1)) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. n : ℕ+
6. i : ℕ
7. i < ||count-repeats(L,eq)||
8. <x, n> = count-repeats(L,eq)[i] ∈ (T × ℕ+)
⊢ n = ||filter(λy.(eq y x);L)|| ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[x:T].  \mforall{}[n:\mBbbN{}\msupplus{}].
    n  =  ||filter(\mlambda{}y.(eq  y  x);L)||  supposing  (<x,  n>  \mmember{}  count-repeats(L,eq))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  -1))

---

Home Index