---

Step * 2 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)||
        ∈ ℤ))
⊢ Σ(snd(count-repeats(L,eq)[i]) | i < ||count-repeats(L,eq)||) = ||L|| ∈ ℤ
BY
{ ((InstHyp [⌜||count-repeats(L,eq)||⌝] (-1)⋅ THENA Auto') THEN HypSubst'  (-1) 0) }

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)||
∈ ℤ
⊢ ||filter(λx.x ∈b firstn(||count-repeats(L,eq)||;map(λp.(fst(p));count-repeats(L,eq)));L)|| = ||L|| ∈ ℤ

---

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)||))
\mvdash{}  \mSigma{}(snd(count-repeats(L,eq)[i])  |  i  <  ||count-repeats(L,eq)||)  =  ||L||


By

---

Latex:
((InstHyp  [\mkleeneopen{}||count-repeats(L,eq)||\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto')  THEN  HypSubst'    (-1)  0)

---

Home Index