---

Step * of Lemma canonical-bound-property

∀x:ℝ. ((r(-canonical-bound(x)) ≤ x) ∧ (x ≤ r(canonical-bound(x))))
BY
{ ((D 0 THENA Auto)
   THEN (GenConclTerm ⌜canonical-bound(x)⌝⋅ THENW Auto)
   THEN RepUR ``rleq rnonneg rsub radd rminus int-to-real accelerate`` 0
   THEN D 0
   THEN (D 0 THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto)
   THEN Reduce 0
   THEN Mul ⌜4⌝ 0⋅
   THEN RWO "div_rem_sum2" 0
   THEN Auto
   THEN GenRem
   THEN Auto
   THEN RW IntNormC 0
   THEN Auto
   THEN (Assert |x (4 * n)| ≤ (8 * n * v) BY
               (DVar `v' THEN (Unhide THENA Auto) THEN InstHyp [⌜4 * n⌝] 3⋅ THEN Auto))
   THEN (Assert |r| < 4 BY
               (DVar `r' THEN Unhide THEN Auto))
   THEN RepeatFor 2 (((RWO "absval_ifthenelse" (-2) THENA Auto) THEN SplitOnHypITE -2  THEN Auto))⋅) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  ((r(-canonical-bound(x))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r(canonical-bound(x))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}canonical-bound(x)\mkleeneclose{}\mcdot{}  THENW  Auto)
  THEN  RepUR  ``rleq  rnonneg  rsub  radd  rminus  int-to-real  accelerate``  0
  THEN  D  0
  THEN  (D  0  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Mul  \mkleeneopen{}4\mkleeneclose{}  0\mcdot{}
  THEN  RWO  "div\_rem\_sum2"  0
  THEN  Auto
  THEN  GenRem
  THEN  Auto
  THEN  RW  IntNormC  0
  THEN  Auto
  THEN  (Assert  |x  (4  *  n)|  \mleq{}  (8  *  n  *  v)  BY
                          (DVar  `v'  THEN  (Unhide  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}4  *  n\mkleeneclose{}]  3\mcdot{}  THEN  Auto))
  THEN  (Assert  |r|  <  4  BY
                          (DVar  `r'  THEN  Unhide  THEN  Auto))
  THEN  RepeatFor  2  (((RWO  "absval\_ifthenelse"  (-2)  THENA  Auto)  THEN  SplitOnHypITE  -2    THEN  Auto))\mcdot{})

---

Home Index