Step
*
1
of Lemma
rat-int-bound_wf
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)}
BY
{ (AutoSplit THEN MemTypeCD THEN Auto THEN SubstFor ⌜q⌝ 0⋅ THEN Auto) }
1
1. q : ℚ
2. v1 : ℤ
3. v2 : ℚ
4. 0 ≤ v2
5. v2 < 1
6. q = (v1 + v2) ∈ ℚ
7. rat-int-part(q) = <v1, v2> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ}
8. v2 = 0 ∈ ℚ
⊢ v1 - 1 < v1 + v2
2
1. q : ℚ
2. v1 : ℤ
3. v2 : ℚ
4. 0 ≤ v2
5. v2 < 1
6. q = (v1 + v2) ∈ ℚ
7. rat-int-part(q) = <v1, v2> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ}
8. v2 = 0 ∈ ℚ
9. v1 - 1 < q
⊢ (v1 + v2) ≤ v1
3
1. q : ℚ
2. v1 : ℤ
3. v2 : ℚ
4. ¬(v2 = 0 ∈ ℚ)
5. 0 ≤ v2
6. v2 < 1
7. q = (v1 + v2) ∈ ℚ
8. rat-int-part(q) = <v1, v2> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ}
⊢ (v1 + 1) - 1 < v1 + v2
4
1. q : ℚ
2. v1 : ℤ
3. v2 : ℚ
4. ¬(v2 = 0 ∈ ℚ)
5. 0 ≤ v2
6. v2 < 1
7. q = (v1 + v2) ∈ ℚ
8. rat-int-part(q) = <v1, v2> ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ}
9. (v1 + 1) - 1 < q
⊢ (v1 + v2) ≤ (v1 + 1)
Latex:
Latex:
1. q : \mBbbQ{}
2. v1 : \mBbbZ{}
3. v2 : \mBbbQ{}
4. (0 \mleq{} v2) \mwedge{} v2 < 1
5. q = (v1 + v2)
6. rat-int-part(q) = <v1, v2>
\mvdash{} if qeq(v2;0) then v1 else v1 + 1 fi \mmember{} \{n:\mBbbZ{}| n - 1 < q \mwedge{} (q \mleq{} n)\}
By
Latex:
(AutoSplit THEN MemTypeCD THEN Auto THEN SubstFor \mkleeneopen{}q\mkleeneclose{} 0\mcdot{} THEN Auto)
Home
Index