---

Step * of Lemma rng_lsum-partition

∀[k:ℕ]. ∀[A:Type]. ∀[p:A ⟶ ℕk]. ∀[r:Rng]. ∀[f:A ⟶ |r|]. ∀[as:A List].
  (Σ{r} x ∈ as. f[x] = (Σ(r) 0 ≤ i < k. Σ{r} x ∈ filter(λa.(p a =z i);as). f[x]) ∈ |r|)
BY
{ (InductionOnList THEN Reduce 0 THEN (Auto THEN Try ((RWO "rng_sum_0" 0 THEN Auto))) THEN (RWO "-1" 0 THENA Auto)) }

1
1. k : ℕ
2. A : Type
3. p : A ⟶ ℕk
4. r : Rng
5. f : A ⟶ |r|
6. u : A
7. v : A List
8. Σ{r} x ∈ v. f[x] = (Σ(r) 0 ≤ i < k. Σ{r} x ∈ filter(λa.(p a =z i);v). f[x]) ∈ |r|
⊢ (f[u] +r (Σ(r) 0 ≤ i < k. Σ{r} x ∈ filter(λa.(p a =z i);v). f[x]))
= (Σ(r) 0 
        ≤ i 
        < k
    Σ{r} x ∈ if (p u =z i) then [u / filter(λa.(p a =z i);v)] else filter(λa.(p a =z i);v) fi . f[x])
∈ |r|

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[A:Type].  \mforall{}[p:A  {}\mrightarrow{}  \mBbbN{}k].  \mforall{}[r:Rng].  \mforall{}[f:A  {}\mrightarrow{}  |r|].  \mforall{}[as:A  List].
    (\mSigma{}\{r\}  x  \mmember{}  as.  f[x]  =  (\mSigma{}(r)  0  \mleq{}  i  <  k.  \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}a.(p  a  =\msubz{}  i);as).  f[x]))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  (Auto  THEN  Try  ((RWO  "rng\_sum\_0"  0  THEN  Auto)))
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index