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