Step
*
1
2
2
of Lemma
lsum-split
1. T : Type
2. L : T List
3. P : {x:T| (x ∈ L)} ⟶ 𝔹
4. f : {x:T| (x ∈ L)} ⟶ ℤ
5. l_sum(map(f;L)) = (l_sum(map(f;filter(P;L))) + l_sum(map(f;filter(λx.(¬b(P x));L)))) ∈ ℤ
⊢ l_sum(map(λx.f[x];filter(λx.(¬bP[x]);L))) = l_sum(map(f;filter(λx.(¬b(P x));L))) ∈ ℤ
BY
{ ((Assert L ∈ {x:T| (x ∈ L)} List BY Auto) THEN RepeatFor 2 (EqCDA) THEN Try ((FunExt THEN Auto))) }
1
.....subterm..... T:t
2:n
1. T : Type
2. L : T List
3. P : {x:T| (x ∈ L)} ⟶ 𝔹
4. f : {x:T| (x ∈ L)} ⟶ ℤ
5. l_sum(map(f;L)) = (l_sum(map(f;filter(P;L))) + l_sum(map(f;filter(λx.(¬b(P x));L)))) ∈ ℤ
6. L ∈ {x:T| (x ∈ L)} List
⊢ filter(λx.(¬bP[x]);L) = filter(λx.(¬b(P x));L) ∈ ({x:T| (x ∈ L)} List)
Latex:
Latex:
1. T : Type
2. L : T List
3. P : \{x:T| (x \mmember{} L)\} {}\mrightarrow{} \mBbbB{}
4. f : \{x:T| (x \mmember{} L)\} {}\mrightarrow{} \mBbbZ{}
5. l\_sum(map(f;L)) = (l\_sum(map(f;filter(P;L))) + l\_sum(map(f;filter(\mlambda{}x.(\mneg{}\msubb{}(P x));L))))
\mvdash{} l\_sum(map(\mlambda{}x.f[x];filter(\mlambda{}x.(\mneg{}\msubb{}P[x]);L))) = l\_sum(map(f;filter(\mlambda{}x.(\mneg{}\msubb{}(P x));L)))
By
Latex:
((Assert L \mmember{} \{x:T| (x \mmember{} L)\} List BY Auto) THEN RepeatFor 2 (EqCDA) THEN Try ((FunExt THEN Auto)))
Home
Index