---

Step * 1 1 2 of Lemma sum-unroll


1. f : Base
2. n : Base
3. ¬0 < n
4. n ∈ ℤ
⊢ Σ(f[x] | x < n) ~ 0
BY
{ TACTIC:((Unfold `sum` 0 THEN RecUnfold `sum_aux` 0) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  f  :  Base
2.  n  :  Base
3.  \mneg{}0  <  n
4.  n  \mmember{}  \mBbbZ{}
\mvdash{}  \mSigma{}(f[x]  |  x  <  n)  \msim{}  0


By

---

Latex:
TACTIC:((Unfold  `sum`  0  THEN  RecUnfold  `sum\_aux`  0)  THEN  AutoSplit)

---

Home Index