---

Step * 1 1 of Lemma rat-half-cube-diameter


1. v : ℚInterval
2. v1 : ℚInterval
⊢ (↑is-half-interval(v;v1))
⇒ (rmax(r0;rat2real(snd(v)) - rat2real(fst(v))) = ((r1/r(2)) * rmax(r0;rat2real(snd(v1)) - rat2real(fst(v1)))))
BY
{ ((D -1 THEN D 1 THEN RepUR ``is-half-interval`` 0)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN (RWW "-1 -2 rat2real-qavg rmul-rmax" 0 THENA Auto)
   THEN BLemma `rmax_functionality`
   THEN Auto) }

---

Latex:

---

Latex:

1.  v  :  \mBbbQ{}Interval
2.  v1  :  \mBbbQ{}Interval
\mvdash{}  (\muparrow{}is-half-interval(v;v1))
{}\mRightarrow{}  (rmax(r0;rat2real(snd(v))  -  rat2real(fst(v)))
      =  ((r1/r(2))  *  rmax(r0;rat2real(snd(v1))  -  rat2real(fst(v1)))))


By

---

Latex:
((D  -1  THEN  D  1  THEN  RepUR  ``is-half-interval``  0)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (RWW  "-1  -2  rat2real-qavg  rmul-rmax"  0  THENA  Auto)
  THEN  BLemma  `rmax\_functionality`
  THEN  Auto)

---

Home Index