---

Step * of Lemma sum-unroll

∀[n,f:Top].  (Σ(f[x] | x < n) ~ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0)
BY
{ TACTIC:((UnivCD THENA Auto) THEN SqEqualTopToBase) }

1
1. f : Base
2. n : Base
⊢ Σ(f[x] | x < n) ~ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0

---

Latex:

---

Latex:
\mforall{}[n,f:Top].    (\mSigma{}(f[x]  |  x  <  n)  \msim{}  if  (0)  <  (n)    then  \mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]    else  0)


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  SqEqualTopToBase)

---

Home Index