---

Step * of Lemma lsum-append

No Annotations
∀[T:Type]. ∀[L1,L2:T List]. ∀[f:{x:T| (x ∈ L1 @ L2)}  ⟶ ℤ].
  (Σ(f[x] | x ∈ L1 @ L2) = (Σ(f[x] | x ∈ L1) + Σ(f[x] | x ∈ L2)) ∈ ℤ)
BY
{ (Auto THEN Unfold `lsum` 0 THEN (RWO "map_append_sq" 0 THENA Auto)) }

1
1. T : Type
2. L1 : T List
3. L2 : T List
4. f : {x:T| (x ∈ L1 @ L2)}  ⟶ ℤ
⊢ l_sum(map(λx.f[x];L1) @ map(λx.f[x];L2)) = (l_sum(map(λx.f[x];L1)) + l_sum(map(λx.f[x];L2))) ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].  \mforall{}[f:\{x:T|  (x  \mmember{}  L1  @  L2)\}    {}\mrightarrow{}  \mBbbZ{}].
    (\mSigma{}(f[x]  |  x  \mmember{}  L1  @  L2)  =  (\mSigma{}(f[x]  |  x  \mmember{}  L1)  +  \mSigma{}(f[x]  |  x  \mmember{}  L2)))


By

---

Latex:
(Auto  THEN  Unfold  `lsum`  0  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto))

---

Home Index