---

Step * 2 1 1 of Lemma sum-count-repeats


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀j:ℕ
     ((j ≤ ||count-repeats(L,eq)||)
     ⇒ (Σ(snd(count-repeats(L,eq)[i]) | i < j)
        = ||filter(λx.x ∈b firstn(j;map(λp.(fst(p));count-repeats(L,eq)));L)||
        ∈ ℤ))
5. Σ(snd(count-repeats(L,eq)[i]) | i < ||count-repeats(L,eq)||)
= ||filter(λx.x ∈b firstn(||count-repeats(L,eq)||;map(λp.(fst(p));count-repeats(L,eq)));L)||
∈ ℤ
6. i : ℕ||L||
⊢ (L[i] ∈ map(λp.(fst(p));count-repeats(L,eq)))
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  \mforall{}j:\mBbbN{}
          ((j  \mleq{}  ||count-repeats(L,eq)||)
          {}\mRightarrow{}  (\mSigma{}(snd(count-repeats(L,eq)[i])  |  i  <  j)
                =  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(j;map(\mlambda{}p.(fst(p));count-repeats(L,eq)));L)||))
5.  \mSigma{}(snd(count-repeats(L,eq)[i])  |  i  <  ||count-repeats(L,eq)||)
=  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(||count-repeats(L,eq)||;map(\mlambda{}p.(fst(p));count-repeats(L,eq)));L)||
6.  i  :  \mBbbN{}||L||
\mvdash{}  (L[i]  \mmember{}  map(\mlambda{}p.(fst(p));count-repeats(L,eq)))


By

---

Latex:
EAuto  1

---

Home Index