---

Step * 1 2 of Lemma rng_lsum-partition


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|
9. f[u] = (Σ(r) 0 ≤ i < k. if (p u =z i) then f[u] else 0 fi ) ∈ |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|
BY
{ (((RWO "-1" 0 THENA Auto) THEN (RWO "rng_sum_plus<" 0 THENA Auto)) THEN EqCDA) }

1
.....subterm..... T:t
4:n
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|
9. f[u] = (Σ(r) 0 ≤ i < k. if (p u =z i) then f[u] else 0 fi ) ∈ |r|
10. i : ℕk
⊢ (if (p u =z i) then f[u] else 0 fi  +r Σ{r} x ∈ filter(λa.(p a =z i);v). f[x])
= Σ{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:

1.  k  :  \mBbbN{}
2.  A  :  Type
3.  p  :  A  {}\mrightarrow{}  \mBbbN{}k
4.  r  :  Rng
5.  f  :  A  {}\mrightarrow{}  |r|
6.  u  :  A
7.  v  :  A  List
8.  \mSigma{}\{r\}  x  \mmember{}  v.  f[x]  =  (\mSigma{}(r)  0  \mleq{}  i  <  k.  \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}a.(p  a  =\msubz{}  i);v).  f[x])
9.  f[u]  =  (\mSigma{}(r)  0  \mleq{}  i  <  k.  if  (p  u  =\msubz{}  i)  then  f[u]  else  0  fi  )
\mvdash{}  (f[u]  +r  (\mSigma{}(r)  0  \mleq{}  i  <  k.  \mSigma{}\{r\}  x  \mmember{}  filter(\mlambda{}a.(p  a  =\msubz{}  i);v).  f[x]))
=  (\mSigma{}(r)  0 
                \mleq{}  i 
                <  k
        \mSigma{}\{r\}  x  \mmember{}  if  (p  u  =\msubz{}  i)
        then  [u  /  filter(\mlambda{}a.(p  a  =\msubz{}  i);v)]
        else  filter(\mlambda{}a.(p  a  =\msubz{}  i);v)
        fi  .  f[x])


By

---

Latex:
(((RWO  "-1"  0  THENA  Auto)  THEN  (RWO  "rng\_sum\_plus<"  0  THENA  Auto))  THEN  EqCDA)

---

Home Index