---

Step * 4 of Lemma fast-rexp_wf


1. x : ℝ
⊢ x ∈ {x@0:ℝ| ((r((x 200) - 2))/400 ≤ x@0) ∧ (x@0 ≤ (r((x 200) + 2))/400)} 
BY
{ (((Subst' (r((x 200) + 2))/400 ~ above x within 1/100 0
     THENA (Unfold `rational-upper-approx` 0 THEN Reduce 0 THEN CallByValueReduce 0 THEN Auto)
     )
    THEN (Subst' (r((x 200) - 2))/400 ~ (below x within 1/100) 0
          THENA (Unfold `rational-lower-approx` 0 THEN Reduce 0 THEN CallByValueReduce 0 THEN Auto)
          )
    )
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
\mvdash{}  x  \mmember{}  \{x@0:\mBbbR{}|  ((r((x  200)  -  2))/400  \mleq{}  x@0)  \mwedge{}  (x@0  \mleq{}  (r((x  200)  +  2))/400)\} 


By

---

Latex:
(((Subst'  (r((x  200)  +  2))/400  \msim{}  above  x  within  1/100  0
      THENA  (Unfold  `rational-upper-approx`  0  THEN  Reduce  0  THEN  CallByValueReduce  0  THEN  Auto)
      )
    THEN  (Subst'  (r((x  200)  -  2))/400  \msim{}  (below  x  within  1/100)  0
                THENA  (Unfold  `rational-lower-approx`  0  THEN  Reduce  0  THEN  CallByValueReduce  0  THEN  Auto)
                )
    )
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index