---

Step * 1 of Lemma sum-count-repeats

.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
⊢ ∀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)||
       ∈ ℤ))
BY
{ InductionOnNat }

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

2
.....upcase..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. j : ℤ
5. 0 < j
6. ((j - 1) ≤ ||count-repeats(L,eq)||)
⇒ (Σ(snd(count-repeats(L,eq)[i]) | i < j - 1)
   = ||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq)));L)||
   ∈ ℤ)
⊢ (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)|| ∈ ℤ)

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
\mvdash{}  \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)||))


By

---

Latex:
InductionOnNat

---

Home Index