---

Step * 2 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) ∈ ℤ
⊢ poly-approx-aux(a;x;xM;M;n;k) ∈ ℤ
BY
{ (RecUnfold `poly-approx-aux` 0
   THEN (GenConcl ⌜poly-approx-aux(a;x;xM;M;n + 1;k - 1) = u ∈ ℤ⌝⋅ 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 ∈ ℤ
⊢ 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  ∈ ℤ

---

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{}
\mvdash{}  poly-approx-aux(a;x;xM;M;n;k)  \mmember{}  \mBbbZ{}


By

---

Latex:
(RecUnfold  `poly-approx-aux`  0
  THEN  (GenConcl  \mkleeneopen{}poly-approx-aux(a;x;xM;M;n  +  1;k  -  1)  =  u\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index