---

Step * 1 of Lemma rational-truncate

.....wf..... 
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
⊢ if q_less(e;1) then TERMOF{rational-truncate1:o, 1:l} q e else integer-part(q) fi  ∈ ℚ
BY
{ (BoolCase ⌜q_less(e;1)⌝⋅ THENA Auto) }

1
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. e < 1
⊢ TERMOF{rational-truncate1:o, 1:l} q e ∈ ℚ

2
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. ¬e < 1
⊢ integer-part(q) ∈ ℚ

---

Latex:

---

Latex:
.....wf..... 
1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
\mvdash{}  if  q\_less(e;1)  then  TERMOF\{rational-truncate1:o,  1:l\}  q  e  else  integer-part(q)  fi    \mmember{}  \mBbbQ{}


By

---

Latex:
(BoolCase  \mkleeneopen{}q\_less(e;1)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index