---

Step * of Lemma sum_functionality_wrt_sqequal

∀[n:ℕ]. ∀[f,g:Base].  Σ(f[x] | x < n) ~ Σ(g[x] | x < n) supposing ∀i:ℕn. (f[i] ~ g[i])
BY
{ (InductionOnNat
   THEN (UnivCD THENA Auto)
   THEN Reduce 0
   THEN Try (Trivial)
   THEN (RWO "sum-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN EqCD
   THEN BackThruSomeHyp) }

1
1. n : ℤ
2. 0 < n
3. ∀[f,g:Base].  Σ(f[x] | x < n - 1) ~ Σ(g[x] | x < n - 1) supposing ∀i:ℕn - 1. (f[i] ~ g[i])
4. f : Base
5. g : Base
6. ∀i:ℕn. (f[i] ~ g[i])
7. 0 < n
⊢ ∀i:ℕn - 1. (f[i] ~ g[i])

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,g:Base].    \mSigma{}(f[x]  |  x  <  n)  \msim{}  \mSigma{}(g[x]  |  x  <  n)  supposing  \mforall{}i:\mBbbN{}n.  (f[i]  \msim{}  g[i])


By

---

Latex:
(InductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  (RWO  "sum-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  EqCD
  THEN  BackThruSomeHyp)

---

Home Index