---

Step * 1 2 2 1 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. is-exception(sum_aux(n;0;0;x.f[x]))
⊢ Σ(f[x] | x < n) ≤ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0
BY
{ TACTIC:(RecUnfold `sum_aux` (-1) THEN ExceptionCases (-1)) }

1
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. is-exception(if (0) < (n)  then eval v' = f[0] + 0 in eval i' = 0 + 1 in   sum_aux(n;v';i';x.f[x])  else 0)
5. 0 ∈ ℤ
6. n ∈ ℤ
⊢ Σ(f[x] | x < n) ≤ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0

2
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. is-exception(if (0) < (n)  then eval v' = f[0] + 0 in eval i' = 0 + 1 in   sum_aux(n;v';i';x.f[x])  else 0)
5. 0 ∈ ℤ
6. is-exception(n)
⊢ Σ(f[x] | x < n) ≤ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0

3
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. is-exception(if (0) < (n)  then eval v' = f[0] + 0 in eval i' = 0 + 1 in   sum_aux(n;v';i';x.f[x])  else 0)
5. is-exception(0)
⊢ Σ(f[x] | x < n) ≤ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0

---

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.  is-exception(sum\_aux(n;0;0;x.f[x]))
\mvdash{}  \mSigma{}(f[x]  |  x  <  n)  \mleq{}  if  (0)  <  (n)    then  \mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]    else  0


By

---

Latex:
TACTIC:(RecUnfold  `sum\_aux`  (-1)  THEN  ExceptionCases  (-1))

---

Home Index