---

Step * of Lemma fast-rexp_wf

∀[x:ℝ]. (fast-rexp(x) ∈ {y:ℝ| y = e^x} )
BY
{ (Auto
   THEN Unfold `fast-rexp` 0
   THEN RepeatFor 4 ((CallByValueReduce 0⋅ THENA Auto))
   THEN Using [`f\'',⌜λ2x.e^x⌝] MemCD⋅
   THEN Auto) }

1
.....wf..... 
1. x : ℝ
⊢ (r((x 200) + 2))/400 ∈ {r:ℝ| (r((x 200) - 2))/400 < r} 

2
1. x : ℝ
⊢ d(λx.e^x[x])/dx = λx.e^x on [(r((x 200) - 2))/400, (r((x 200) + 2))/400]

3
1. x : ℝ
2. x1 : {x1:ℝ| x1 ∈ [(r((x 200) - 2))/400, (r((x 200) + 2))/400]} 
⊢ |e^x1| ≤ r(canonical-bound(e^(r((x 200) + 2))/400))

4
1. x : ℝ
⊢ x ∈ {x@0:ℝ| ((r((x 200) - 2))/400 ≤ x@0) ∧ (x@0 ≤ (r((x 200) + 2))/400)} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (fast-rexp(x)  \mmember{}  \{y:\mBbbR{}|  y  =  e\^{}x\}  )


By

---

Latex:
(Auto
  THEN  Unfold  `fast-rexp`  0
  THEN  RepeatFor  4  ((CallByValueReduce  0\mcdot{}  THENA  Auto))
  THEN  Using  [`f\mbackslash{}'',\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{}]  MemCD\mcdot{}
  THEN  Auto)

---

Home Index