---

Step * of Lemma rat-int-part_wf

∀q:ℤ ⋃ (ℤ × ℤ-o). (rat-int-part(q) ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} )
BY
{ (Auto THEN Unfold `rat-int-part` 0) }

1
1. q : ℤ ⋃ (ℤ × ℤ-o)
⊢ if q is an integer then <q, 0>
  else let n,m = q 
       in eval a = n ÷ m in
          eval b = n rem m in
            if (b =z 0) then <a, 0>
            if 0 <z m then if 0 ≤z n then <a, (b/m)> else <a - 1, (b + m/m)> fi 
            if 0 ≤z n then <a - 1, (b + m/m)>
            else <a, (b/m)>
            fi  ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} 

---

Latex:

---

Latex:
\mforall{}q:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{}).  (rat-int-part(q)  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  \{r:\mBbbQ{}|  (0  \mleq{}  r)  \mwedge{}  r  <  1\}  |  let  x,r  =  p  in  q  =  (x  +  r)\}  )


By

---

Latex:
(Auto  THEN  Unfold  `rat-int-part`  0)

---

Home Index