---

Step * 1 1 1 2 1 of Lemma face-of-half-cube


1. v6 : ℚ
2. v : ℚInterval
3. v5 : ℚ
4. ↑is-half-interval(v;[v6])
5. v = [v6] ∈ ℚInterval
6. ↑is-half-interval(<qavg(v5;v6), v6>;<v5, v6>)
7. v ≤ <qavg(v5;v6), v6>
8. y1 : ℚ
9. y2 : ℚ
10. ↑is-half-interval(<y1, y2>;<v5, v6>)
11. ([v6] = [y1] ∈ ℚInterval) ∨ ([v6] = [y2] ∈ ℚInterval) ∨ ([v6] = <y1, y2> ∈ ℚInterval)
⊢ <y1, y2> = <qavg(v5;v6), v6> ∈ ℚInterval
BY
{ (MoveToConcl (-2)
   THEN Unfold `rat-point-interval` -1
   THEN SplitOrHyps
   THEN (EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN (RWO  "-1< -2<" 0 THENA Auto)
   THEN (RepUR ``is-half-interval`` 0 THEN (RW  assert_pushdownC 0 THENA Auto))
   THEN QavgSimp 0
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN Auto
   THEN RepeatFor 2 (((RWO "-1 -2" 0 THENA Auto) THEN QavgSimp 0 THEN Auto))) }

1
1. v6 : ℚ
2. v : ℚInterval
3. v5 : ℚ
4. ↑is-half-interval(v;[v6])
5. v = [v6] ∈ ℚInterval
6. ↑is-half-interval(<qavg(v5;v6), v6>;<v5, v6>)
7. v ≤ <qavg(v5;v6), v6>
8. y1 : ℚ
9. y2 : ℚ
10. v6 = y1 ∈ ℚ
11. v6 = y2 ∈ ℚ
12. v6 = v5 ∈ ℚ
13. v6 = v6 ∈ ℚ
⊢ <v6, v6> = <qavg(v5;v6), v6> ∈ ℚInterval

---

Latex:

---

Latex:

1.  v6  :  \mBbbQ{}
2.  v  :  \mBbbQ{}Interval
3.  v5  :  \mBbbQ{}
4.  \muparrow{}is-half-interval(v;[v6])
5.  v  =  [v6]
6.  \muparrow{}is-half-interval(<qavg(v5;v6),  v6><v5,  v6>)
7.  v  \mleq{}  <qavg(v5;v6),  v6>
8.  y1  :  \mBbbQ{}
9.  y2  :  \mBbbQ{}
10.  \muparrow{}is-half-interval(<y1,  y2><v5,  v6>)
11.  ([v6]  =  [y1])  \mvee{}  ([v6]  =  [y2])  \mvee{}  ([v6]  =  <y1,  y2>)
\mvdash{}  <y1,  y2>  =  <qavg(v5;v6),  v6>


By

---

Latex:
(MoveToConcl  (-2)
  THEN  Unfold  `rat-point-interval`  -1
  THEN  SplitOrHyps
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  (RWO    "-1<  -2<"  0  THENA  Auto)
  THEN  (RepUR  ``is-half-interval``  0  THEN  (RW    assert\_pushdownC  0  THENA  Auto))
  THEN  QavgSimp  0
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  RepeatFor  2  (((RWO  "-1  -2"  0  THENA  Auto)  THEN  QavgSimp  0  THEN  Auto)))

---

Home Index