---

Step * of Lemma sum-count-repeats

No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  (Σ(snd(count-repeats(L,eq)[i]) | i < ||count-repeats(L,eq)||) = ||L|| ∈ ℤ)
BY
{ (Auto
   THEN TACTIC:Assert ⌜∀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)||
                            ∈ ℤ))⌝⋅
   ) }

1
.....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)||
       ∈ ℤ))

2
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|| ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].
    (\mSigma{}(snd(count-repeats(L,eq)[i])  |  i  <  ||count-repeats(L,eq)||)  =  ||L||)


By

---

Latex:
(Auto
  THEN  TACTIC:Assert  \mkleeneopen{}\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)||))\mkleeneclose{}\mcdot{}
  )

---

Home Index