---

Step * 1 of Lemma fast-rexp_wf

.....wf..... 
1. x : ℝ
⊢ (r((x 200) + 2))/400 ∈ {r:ℝ| (r((x 200) - 2))/400 < r} 
BY
{ ((MemTypeCD THEN Auto) THEN RWO "int-rdiv-req" 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  x  :  \mBbbR{}
\mvdash{}  (r((x  200)  +  2))/400  \mmember{}  \{r:\mBbbR{}|  (r((x  200)  -  2))/400  <  r\} 


By

---

Latex:
((MemTypeCD  THEN  Auto)  THEN  RWO  "int-rdiv-req"  0  THEN  Auto)

---

Home Index