---

Step * 2 1 1 of Lemma poly-approx-aux_wf


1. k : ℤ
2. 0 < k
3. a : ℕ ⟶ ℝ
4. x : ℝ
5. xM : ℤ
6. M : ℕ+
7. n : ℕ
8. poly-approx-aux(a;x;xM;M;n + 1;k - 1) ∈ ℤ
9. u : ℤ
10. poly-approx-aux(a;x;xM;M;n + 1;k - 1) = u ∈ ℤ
⊢ if (k =z 0)
  then a n M
  else eval b = ((2 * |u|) ÷ M) + 1 in
       eval z = if (b =z 1) then xM else x (b * M) fi  in
       eval v = (u * z) ÷ 2 * b * M in
       eval t = a n M in
         v + t
  fi  ∈ ℤ
BY
{ ((GenConcl ⌜(((2 * |u|) ÷ M) + 1) = b ∈ ℕ+⌝⋅ THENA Auto) THEN (CallByValueReduce 0 THENA Auto)) }

1
1. k : ℤ
2. 0 < k
3. a : ℕ ⟶ ℝ
4. x : ℝ
5. xM : ℤ
6. M : ℕ+
7. n : ℕ
8. poly-approx-aux(a;x;xM;M;n + 1;k - 1) ∈ ℤ
9. u : ℤ
10. poly-approx-aux(a;x;xM;M;n + 1;k - 1) = u ∈ ℤ
11. b : ℕ+
12. (((2 * |u|) ÷ M) + 1) = b ∈ ℕ+
⊢ if (k =z 0)
  then a n M
  else eval z = if (b =z 1) then xM else x (b * M) fi  in
       eval v = (u * z) ÷ 2 * b * M in
       eval t = a n M in
         v + t
  fi  ∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  0  <  k
3.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
4.  x  :  \mBbbR{}
5.  xM  :  \mBbbZ{}
6.  M  :  \mBbbN{}\msupplus{}
7.  n  :  \mBbbN{}
8.  poly-approx-aux(a;x;xM;M;n  +  1;k  -  1)  \mmember{}  \mBbbZ{}
9.  u  :  \mBbbZ{}
10.  poly-approx-aux(a;x;xM;M;n  +  1;k  -  1)  =  u
\mvdash{}  if  (k  =\msubz{}  0)
    then  a  n  M
    else  eval  b  =  ((2  *  |u|)  \mdiv{}  M)  +  1  in
              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  =  a  n  M  in
                  v  +  t
    fi    \mmember{}  \mBbbZ{}


By

---

Latex:
((GenConcl  \mkleeneopen{}(((2  *  |u|)  \mdiv{}  M)  +  1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index