---

Step * of Lemma sum-in-vs-shift

∀[k,n,m:ℤ]. ∀[f,vs:Top].  (Σ{f[i] | n≤i≤m} ~ Σ{f[i + k] | n - k≤i≤m - k})
BY
{ (Intros
   THEN Unfold `sum-in-vs` 0
   THEN Unfold `vs-bag-add` 0
   THEN (Subst' [n, m + 1) ~ bag-map(λi.(i + k);[n - k, (m - k) + 1)) 0
   THENM (RWO  "bag-summation-map" 0 THEN Reduce 0 THEN Auto)
   )) }

1
.....equality..... 
1. k : ℤ
2. n : ℤ
3. m : ℤ
4. f : Top
5. vs : Top
⊢ [n, m + 1) ~ bag-map(λi.(i + k);[n - k, (m - k) + 1))

---

Latex:

---

Latex:
\mforall{}[k,n,m:\mBbbZ{}].  \mforall{}[f,vs:Top].    (\mSigma{}\{f[i]  |  n\mleq{}i\mleq{}m\}  \msim{}  \mSigma{}\{f[i  +  k]  |  n  -  k\mleq{}i\mleq{}m  -  k\})


By

---

Latex:
(Intros
  THEN  Unfold  `sum-in-vs`  0
  THEN  Unfold  `vs-bag-add`  0
  THEN  (Subst'  [n,  m  +  1)  \msim{}  bag-map(\mlambda{}i.(i  +  k);[n  -  k,  (m  -  k)  +  1))  0
  THENM  (RWO    "bag-summation-map"  0  THEN  Reduce  0  THEN  Auto)
  ))

---

Home Index