---

Step * 2 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)||
∈ ℤ
⊢ ||filter(λx.x ∈b firstn(||count-repeats(L,eq)||;map(λp.(fst(p));count-repeats(L,eq)));L)|| = ||L|| ∈ ℤ
BY
{ ((RWO "filter_trivial" 0 THEN Auto) THEN RepUR ``l_all so_apply`` 0 THEN Auto THEN RWO "firstn_all" 0 THEN Auto) }

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

---

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)||
\mvdash{}  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(||count-repeats(L,eq)||;map(\mlambda{}p.(fst(p));count-repeats(L,eq)));L)||  =  ||L||


By

---

Latex:
((RWO  "filter\_trivial"  0  THEN  Auto)
  THEN  RepUR  ``l\_all  so\_apply``  0
  THEN  Auto
  THEN  RWO  "firstn\_all"  0
  THEN  Auto)

---

Home Index