---

Step * of Lemma rat-int-bound_wf

∀[q:ℚ]. (rat-int-bound(q) ∈ {n:ℤ| n - 1 < q ∧ (q ≤ n)} )
BY
{ xxx((D 0 THENA Auto)
      THEN Unfold `rat-int-bound` 0
      THEN GenConclAtAddr [2;1]
      THEN RepeatFor 2 (D 2)
      THEN D 3
      THEN All Reduce)xxx }

1
1. q : ℚ
2. v1 : ℤ
3. v2 : ℚ
4. (0 ≤ v2) ∧ v2 < 1
5. q = (v1 + v2) ∈ ℚ
6. rat-int-part(q) = <v1, v2> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} 
⊢ if qeq(v2;0) then v1 else v1 + 1 fi  ∈ {n:ℤ| n - 1 < q ∧ (q ≤ n)} 

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  (rat-int-bound(q)  \mmember{}  \{n:\mBbbZ{}|  n  -  1  <  q  \mwedge{}  (q  \mleq{}  n)\}  )


By

---

Latex:
xxx((D  0  THENA  Auto)
        THEN  Unfold  `rat-int-bound`  0
        THEN  GenConclAtAddr  [2;1]
        THEN  RepeatFor  2  (D  2)
        THEN  D  3
        THEN  All  Reduce)xxx

---

Home Index