---

Step * 1 of Lemma rsub-rmin-rleq-rabs


1. a : ℝ
2. b : ℝ
3. n : ℕ+
⊢ ((b - rmin(a;b)) n) ≤ ((|a - b| n) + 4)
BY
{ (RepUR ``rsub rmin rabs rminus radd reg-seq-list-add accelerate`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RepeatFor 3 ((RecUnfold `cbv_list_accum` 0 THEN Reduce 0))
   THEN GenConclTerms Auto [⌜b (4 * n)⌝ ;⌜a (4 * n)⌝]⋅
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (RWO "imin_unfold" 0 THENA Auto)
   THEN AutoSplit) }

1
1. a : ℝ
2. b : ℝ
3. n : ℕ+
4. v : ℤ
5. (b (4 * n)) = v ∈ ℤ
6. v1 : ℤ
7. (a (4 * n)) = v1 ∈ ℤ
8. v1 ≤ v
⊢ (((0 + v) + (-v1)) ÷ 4) ≤ (|((0 + v1) + (-v)) ÷ 4| + 4)

2
1. a : ℝ
2. b : ℝ
3. n : ℕ+
4. v : ℤ
5. (b (4 * n)) = v ∈ ℤ
6. v1 : ℤ
7. ¬(v1 ≤ v)
8. (a (4 * n)) = v1 ∈ ℤ
⊢ (((0 + v) + (-v)) ÷ 4) ≤ (|((0 + v1) + (-v)) ÷ 4| + 4)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  ((b  -  rmin(a;b))  n)  \mleq{}  ((|a  -  b|  n)  +  4)


By

---

Latex:
(RepUR  ``rsub  rmin  rabs  rminus  radd  reg-seq-list-add  accelerate``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RepeatFor  3  ((RecUnfold  `cbv\_list\_accum`  0  THEN  Reduce  0))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}b  (4  *  n)\mkleeneclose{}  ;\mkleeneopen{}a  (4  *  n)\mkleeneclose{}]\mcdot{}
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (RWO  "imin\_unfold"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index