---

Step * of Lemma rsum-shift

No Annotations
∀[k,n,m:ℤ]. ∀[x:Top].  (Σ{x[i] | n≤i≤m} ~ Σ{x[i + k] | n - k≤i≤m - k})
BY
{ (((UnivCD THENA Auto) THEN Unfold `rsum` 0)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN EqCD
   THEN Try (Trivial)) }

1
1. k : ℤ
2. n : ℤ
3. m : ℤ
4. x : Top
⊢ map(λi.x[i];[n, m + 1)) ~ map(λi.x[i + k];[n - k, (m - k) + 1))

---

Latex:

---

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


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `rsum`  0)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index