---

Step * 1 1 1 of Lemma rng_lsum-partition

.....basecase..... 
1. k : ℕ
2. A : Type
3. p : A ⟶ ℕk
4. r : Rng
5. f : A ⟶ |r|
6. u : A
7. m : ℤ
⊢ 0 < k ⇒ (f[u] = (Σ(r) 0 ≤ i < k. if (0 =z i) then f[u] else 0 fi ) ∈ |r|)
BY
{ (((RWO "rng_sum_unroll_lo" 0 THENA Auto) THEN Reduce 0)
   THEN (Subst' (Σ(r) 1 ≤ i < k. if (0 =z i) then f[u] else 0 fi ) = (Σ(r) 1 ≤ i < k. 0) ∈ |r| 0
         THENA ((Auto THEN EqCDA) THEN AutoSplit)
         )
   ) }

1
1. k : ℕ
2. A : Type
3. p : A ⟶ ℕk
4. r : Rng
5. f : A ⟶ |r|
6. u : A
7. m : ℤ
⊢ 0 < k ⇒ (f[u] = (f[u] +r (Σ(r) 1 ≤ i < k. 0)) ∈ |r|)

---

Latex:

---

Latex:
.....basecase..... 
1.  k  :  \mBbbN{}
2.  A  :  Type
3.  p  :  A  {}\mrightarrow{}  \mBbbN{}k
4.  r  :  Rng
5.  f  :  A  {}\mrightarrow{}  |r|
6.  u  :  A
7.  m  :  \mBbbZ{}
\mvdash{}  0  <  k  {}\mRightarrow{}  (f[u]  =  (\mSigma{}(r)  0  \mleq{}  i  <  k.  if  (0  =\msubz{}  i)  then  f[u]  else  0  fi  ))


By

---

Latex:
(((RWO  "rng\_sum\_unroll\_lo"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (Subst'  (\mSigma{}(r)  1  \mleq{}  i  <  k.  if  (0  =\msubz{}  i)  then  f[u]  else  0  fi  )  =  (\mSigma{}(r)  1  \mleq{}  i  <  k.  0)  0
              THENA  ((Auto  THEN  EqCDA)  THEN  AutoSplit)
              )
  )

---

Home Index