---

Step * 1 2 3 of Lemma sum-unroll


1. f : Base
2. n : Base
3. (n ∈ ℤ) ⇒ (Σ(f[x] | x < n) ~ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0)
4. (if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0)↓
⊢ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0 ≤ Σ(f[x] | x < n)
BY
{ TACTIC:((RWO "-2" 0 THEN Auto) THEN HasValueD (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Base
2.  n  :  Base
3.  (n  \mmember{}  \mBbbZ{})  {}\mRightarrow{}  (\mSigma{}(f[x]  |  x  <  n)  \msim{}  if  (0)  <  (n)    then  \mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]    else  0)
4.  (if  (0)  <  (n)    then  \mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]    else  0)\mdownarrow{}
\mvdash{}  if  (0)  <  (n)    then  \mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]    else  0  \mleq{}  \mSigma{}(f[x]  |  x  <  n)


By

---

Latex:
TACTIC:((RWO  "-2"  0  THEN  Auto)  THEN  HasValueD  (-1)  THEN  Auto)

---

Home Index