---

Step * 1 1 1 of Lemma sum-unroll


1. f : Base
2. n : Base
3. n ∈ ℤ
4. 0 < n
⊢ Σ(f[x] | x < n) ~ Σ(f[x] | x < n - 1) + f[n - 1]
BY
{ TACTIC:((GenConcl ⌜(n - 1) = m ∈ ℕ⌝⋅ THENA Auto)
          THEN (Subst' n ~ m + 1 0 THENA Auto)
          THEN ThinVar `n'
          THEN Unfold `sum` 0) }

1
1. f : Base
2. m : ℕ
⊢ sum_aux(m + 1;0;0;x.f[x]) ~ sum_aux(m;0;0;x.f[x]) + f[m]

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:((GenConcl  \mkleeneopen{}(n  -  1)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (Subst'  n  \msim{}  m  +  1  0  THENA  Auto)
                THEN  ThinVar  `n'
                THEN  Unfold  `sum`  0)

---

Home Index