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


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

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