---

Step * 2 1 1 2 1 1 of Lemma poly-approx-aux-property


1. k : ℤ
2. k ≠ 0
3. 0 < k
4. a : ℕ ⟶ ℝ
5. x : ℝ
6. xM : ℤ
7. M : ℕ+
8. ∀[n:ℕ]
     ((|x| ≤ (r1/r(4)))
     ⇒ 1-approx(x;M;xM)
     ⇒ (k - 1) + 1-approx(Σ{(a (n + i)) * x^i | 0≤i≤k - 1};M;poly-approx-aux(a;x;xM;M;n;k - 1)))
9. n : ℕ
10. |x| ≤ (r1/r(4))
11. 1-approx(x;M;xM)
12. v : ℝ
13. Σ{(a ((n + 1) + i)) * x^i | 0≤i≤k - 1} = v ∈ ℝ
14. u : ℤ
15. poly-approx-aux(a;x;xM;M;n + 1;k - 1) = u ∈ ℤ
16. k-approx(v;M;u)
17. b : ℕ+
18. (((2 * |u|) ÷ M) + 1) = b ∈ ℕ+
19. t : ℤ
20. (a n M) = t ∈ ℤ
21. 1-approx(a n;M;t)
⊢ k + 1-approx((a n) + (x * v);M;eval z = if (b =z 1) then xM else x (b * M) fi  in
                                 eval v = (u * z) ÷ 2 * b * M in
                                 eval t = t in
                                   v + t)
BY
{ ((GenConcl ⌜if (b =z 1) then xM else x (b * M) fi  = z ∈ ℤ⌝⋅ THENA Auto)
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   ) }

1
1. k : ℤ
2. k ≠ 0
3. 0 < k
4. a : ℕ ⟶ ℝ
5. x : ℝ
6. xM : ℤ
7. M : ℕ+
8. ∀[n:ℕ]
     ((|x| ≤ (r1/r(4)))
     ⇒ 1-approx(x;M;xM)
     ⇒ (k - 1) + 1-approx(Σ{(a (n + i)) * x^i | 0≤i≤k - 1};M;poly-approx-aux(a;x;xM;M;n;k - 1)))
9. n : ℕ
10. |x| ≤ (r1/r(4))
11. 1-approx(x;M;xM)
12. v : ℝ
13. Σ{(a ((n + 1) + i)) * x^i | 0≤i≤k - 1} = v ∈ ℝ
14. u : ℤ
15. poly-approx-aux(a;x;xM;M;n + 1;k - 1) = u ∈ ℤ
16. k-approx(v;M;u)
17. b : ℕ+
18. (((2 * |u|) ÷ M) + 1) = b ∈ ℕ+
19. t : ℤ
20. (a n M) = t ∈ ℤ
21. 1-approx(a n;M;t)
22. z : ℤ
23. if (b =z 1) then xM else x (b * M) fi  = z ∈ ℤ
⊢ k + 1-approx((a n) + (x * v);M;((u * z) ÷ 2 * b * M) + t)

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  k  \mneq{}  0
3.  0  <  k
4.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
5.  x  :  \mBbbR{}
6.  xM  :  \mBbbZ{}
7.  M  :  \mBbbN{}\msupplus{}
8.  \mforall{}[n:\mBbbN{}]
          ((|x|  \mleq{}  (r1/r(4)))
          {}\mRightarrow{}  1-approx(x;M;xM)
          {}\mRightarrow{}  (k  -  1)  +  1-approx(\mSigma{}\{(a  (n  +  i))  *  x\^{}i  |  0\mleq{}i\mleq{}k  -  1\};M;poly-approx-aux(a;x;xM;M;n;k  -  1)))
9.  n  :  \mBbbN{}
10.  |x|  \mleq{}  (r1/r(4))
11.  1-approx(x;M;xM)
12.  v  :  \mBbbR{}
13.  \mSigma{}\{(a  ((n  +  1)  +  i))  *  x\^{}i  |  0\mleq{}i\mleq{}k  -  1\}  =  v
14.  u  :  \mBbbZ{}
15.  poly-approx-aux(a;x;xM;M;n  +  1;k  -  1)  =  u
16.  k-approx(v;M;u)
17.  b  :  \mBbbN{}\msupplus{}
18.  (((2  *  |u|)  \mdiv{}  M)  +  1)  =  b
19.  t  :  \mBbbZ{}
20.  (a  n  M)  =  t
21.  1-approx(a  n;M;t)
\mvdash{}  k  +  1-approx((a  n)  +  (x  *  v);M;eval  z  =  if  (b  =\msubz{}  1)  then  xM  else  x  (b  *  M)  fi    in
                                                                  eval  v  =  (u  *  z)  \mdiv{}  2  *  b  *  M  in
                                                                  eval  t  =  t  in
                                                                      v  +  t)


By

---

Latex:
((GenConcl  \mkleeneopen{}if  (b  =\msubz{}  1)  then  xM  else  x  (b  *  M)  fi    =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  )

---

Home Index