---

Step * 1 of Lemma truncate-rational_wf

.....equality..... 
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
⊢ truncate-rational(q;e) ~ TERMOF{rational-truncate:o, \\v:l} q e
BY
{ (RW (AddrC [2] ((BasicSymbolicComputeC ``qeq qdiv q_less qmul qadd qsub integer-part rat-int-bound``)⋅)) 0⋅
   THEN Fold `truncate-rational` 0
   THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
\mvdash{}  truncate-rational(q;e)  \msim{}  TERMOF\{rational-truncate:o,  \mbackslash{}\mbackslash{}v:l\}  q  e


By

---

Latex:
(RW  (AddrC  [2]  ((BasicSymbolicComputeC 
  ``qeq  qdiv  q\_less  qmul  qadd  qsub  integer-part  rat-int-bound``)\mcdot{}))  0\mcdot{}
  THEN  Fold  `truncate-rational`  0
  THEN  Auto)

---

Home Index