---

Step * 1 1 of Lemma rng_lsum-partition


1. k : ℕ
2. A : Type
3. p : A ⟶ ℕk
4. r : Rng
5. f : A ⟶ |r|
6. u : A
⊢ f[u] = (Σ(r) 0 ≤ i < k. if (p u =z i) then f[u] else 0 fi ) ∈ |r|
BY
{ ((Assert p u < k BY
          Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜(p u) = m ∈ ℕ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN NatInd (-1)) }

1
.....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|)

2
.....upcase..... 
1. k : ℕ
2. A : Type
3. p : A ⟶ ℕk
4. r : Rng
5. f : A ⟶ |r|
6. u : A
7. m : ℤ
8. 0 < m
9. m - 1 < k ⇒ (f[u] = (Σ(r) 0 ≤ i < k. if (m - 1 =z i) then f[u] else 0 fi ) ∈ |r|)
⊢ m < k ⇒ (f[u] = (Σ(r) 0 ≤ i < k. if (m =z i) then f[u] else 0 fi ) ∈ |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
\mvdash{}  f[u]  =  (\mSigma{}(r)  0  \mleq{}  i  <  k.  if  (p  u  =\msubz{}  i)  then  f[u]  else  0  fi  )


By

---

Latex:
((Assert  p  u  <  k  BY
                Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(p  u)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  NatInd  (-1))

---

Home Index