---

Step * 2 1 2 1 1 1 of Lemma sum-has-value


1. f : Base
2. d : ℤ
3. 0 < d
4. ∀n,m:ℕ.  (((n - m) ≤ (d - 1)) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))
5. n : ℕ@i
6. m : ℕ@i
7. (n - m) ≤ d
8. v : ℤ@i
9. (if (m) < (n)  then eval v' = f[m] + v in eval i' = m + 1 in   sum_aux(n;v';i';x.f[x])  else v)↓
10. m ∈ ℤ
11. n ∈ ℤ
12. i : {m..n-}
13. m < n
⊢ f i ∈ ℤ
BY
{ ((Reduce 9 THENA Auto)
   THEN HasValueD 9
   THEN (Assert f[m] ∈ Base BY
               Auto)
   THEN HasValueD (-2)
   THEN (CallByValueReduce 9 THENA Auto)
   THEN (FHyp 4 [9] THENA Auto)) }

1
1. f : Base
2. d : ℤ
3. 0 < d
4. ∀n,m:ℕ.  (((n - m) ≤ (d - 1)) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))
5. n : ℕ@i
6. m : ℕ@i
7. (n - m) ≤ d
8. v : ℤ@i
9. (sum_aux(n;f[m] + v;m + 1;x.f[x]))↓
10. m ∈ ℤ
11. n ∈ ℤ
12. i : {m..n-}
13. m < n
14. (f[m] + v)↓
15. f[m] ∈ Base
16. f[m] ∈ ℤ
17. v ∈ ℤ
18. f ∈ {m + 1..n-} ⟶ ℤ
⊢ f i ∈ ℤ

---

Latex:

---

Latex:

1.  f  :  Base
2.  d  :  \mBbbZ{}
3.  0  <  d
4.  \mforall{}n,m:\mBbbN{}.    (((n  -  m)  \mleq{}  (d  -  1))  {}\mRightarrow{}  (\mforall{}v:\mBbbZ{}.  ((sum\_aux(n;v;m;x.f[x]))\mdownarrow{}  {}\mRightarrow{}  (f  \mmember{}  \{m..n\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}))))
5.  n  :  \mBbbN{}@i
6.  m  :  \mBbbN{}@i
7.  (n  -  m)  \mleq{}  d
8.  v  :  \mBbbZ{}@i
9.  (if  (m)  <  (n)    then  eval  v'  =  f[m]  +  v  in  eval  i'  =  m  +  1  in      sum\_aux(n;v';i';x.f[x])    else  v)\mdownarrow{}
10.  m  \mmember{}  \mBbbZ{}
11.  n  \mmember{}  \mBbbZ{}
12.  i  :  \{m..n\msupminus{}\}
13.  m  <  n
\mvdash{}  f  i  \mmember{}  \mBbbZ{}


By

---

Latex:
((Reduce  9  THENA  Auto)
  THEN  HasValueD  9
  THEN  (Assert  f[m]  \mmember{}  Base  BY
                          Auto)
  THEN  HasValueD  (-2)
  THEN  (CallByValueReduce  9  THENA  Auto)
  THEN  (FHyp  4  [9]  THENA  Auto))

---

Home Index