---

Step * 1 1 of Lemma approx-arg-interval_wf

.....assertion..... 
1. l : ℝ
2. r : {r:ℝ| l < r} 
3. f : [l, r] ⟶ℝ
4. f' : [l, r] ⟶ℝ
5. ∀x,y:{t:ℝ| t ∈ [l, r]} .  ((x = y) ⇒ (f'[x] = f'[y]))
6. d(f[x])/dx = λx.f'[x] on [l, r]
7. B : ℕ
8. ∀x:{x:ℝ| x ∈ [l, r]} . (|f'[x]| ≤ r(B))
9. ∀x,y:{x:ℝ| x ∈ [l, r]} .  (|f[x] - f[y]| ≤ (r(B) * |x - y|))
10. x : {x:ℝ| x ∈ [l, r]} 
⊢ accelerate(1 + (2 * B);λn.eval a = x n in
                            eval m = 2 * n in
                            eval x' = if (a * 2) < ((l m) + 2)
                                         then l
                                         else if ((r m) - 2) < (a * 2)  then r  else (r(a))/m in
                              f x' n)
= accelerate(1 + (2 * B);λn.(f approx-in-interval(l;r;x;n) n))
∈ (ℕ+ ⟶ ℤ)
BY
{ ((FunExt THENA Auto)
   THEN Reduce 0
   THEN RenameVar `n' (-1)
   THEN RepUR ``accelerate`` 0
   THEN (GenConcl ⌜(2 * (1 + (2 * B))) = k2 ∈ ℕ+⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN Reduce 0
   THEN (GenConcl ⌜(k2 * n) = m ∈ ℕ+⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN (Subst' eval a = x m in
                eval m@0 = 2 * m in
                eval x' = if (a * 2) < ((l m@0) + 2)
                             then l
                             else if ((r m@0) - 2) < (a * 2)  then r  else (r(a))/m@0 in
                  f x' m ~ f approx-in-interval(l;r;x;m) m 0
   THENM Auto
   )
   THEN RepUR ``approx-in-interval`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 ⋅ THENA Auto))
   THEN AutoSplit
   THEN (AutoSplit ORELSE (CallByValueReduce 0 ⋅ THEN Auto))
   THEN (CallByValueReduce 0 THEN Try (Fold `member` 0) THEN Auto)
   ⋅) }

---

Latex:

---

Latex:
.....assertion..... 
1.  l  :  \mBbbR{}
2.  r  :  \{r:\mBbbR{}|  l  <  r\} 
3.  f  :  [l,  r]  {}\mrightarrow{}\mBbbR{}
4.  f'  :  [l,  r]  {}\mrightarrow{}\mBbbR{}
5.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  [l,  r]\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y]))
6.  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  [l,  r]
7.  B  :  \mBbbN{}
8.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [l,  r]\}  .  (|f'[x]|  \mleq{}  r(B))
9.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [l,  r]\}  .    (|f[x]  -  f[y]|  \mleq{}  (r(B)  *  |x  -  y|))
10.  x  :  \{x:\mBbbR{}|  x  \mmember{}  [l,  r]\} 
\mvdash{}  accelerate(1  +  (2  *  B);\mlambda{}n.eval  a  =  x  n  in
                                                        eval  m  =  2  *  n  in
                                                        eval  x'  =  if  (a  *  2)  <  ((l  m)  +  2)
                                                                                  then  l
                                                                                  else  if  ((r  m)  -  2)  <  (a  *  2)    then  r    else  (r(a))/m  in
                                                            f  x'  n)
=  accelerate(1  +  (2  *  B);\mlambda{}n.(f  approx-in-interval(l;r;x;n)  n))


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  RenameVar  `n'  (-1)
  THEN  RepUR  ``accelerate``  0
  THEN  (GenConcl  \mkleeneopen{}(2  *  (1  +  (2  *  B)))  =  k2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}(k2  *  n)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  eval  a  =  x  m  in
                            eval  m@0  =  2  *  m  in
                            eval  x'  =  if  (a  *  2)  <  ((l  m@0)  +  2)
                                                      then  l
                                                      else  if  ((r  m@0)  -  2)  <  (a  *  2)    then  r    else  (r(a))/m@0  in
                                f  x'  m  \msim{}  f  approx-in-interval(l;r;x;m)  m  0
  THENM  Auto
  )
  THEN  RepUR  ``approx-in-interval``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  \mcdot{}  THENA  Auto))
  THEN  AutoSplit
  THEN  (AutoSplit  ORELSE  (CallByValueReduce  0  \mcdot{}  THEN  Auto))
  THEN  (CallByValueReduce  0  THEN  Try  (Fold  `member`  0)  THEN  Auto)
  \mcdot{})

---

Home Index