---

Step * 1 of Lemma inhabited-intersection-half-cubes


1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. d : ℚCube(k)
6. ∀i:ℕk. (↑is-half-interval(c i;a i))
7. ∀i:ℕk. (↑is-half-interval(d i;b i))
8. ∀i:ℕk. (↑Inhabited(c i ⋂ d i))
⊢ ↑Inhabited(a ⋂ b)
BY
{ ((RWO "assert-inhabited-rat-cube" 0 THENA Auto)
   THEN RepUR ``rat-cube-intersection`` 0
   THEN ParallelLast
   THEN (Assert (↑is-half-interval(c i;a i)) ∧ (↑is-half-interval(d i;b i)) BY
               Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜a i⌝;⌜b i⌝;⌜c i⌝;⌜d i⌝]⋅
   THEN D -8
   THEN D -6
   THEN D -4
   THEN D -2
   THEN RepUR ``rat-interval-intersection inhabited-rat-interval`` 0
   THEN RepUR ``is-half-interval`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "qmax_lb" 0 THENA Auto)
   THEN (RWO "qmin_ub" 0 THENA Auto)
   THEN All Thin
   THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. v4 : ℚ
2. v5 : ℚ
3. v6 : ℚ
4. v7 : ℚ
5. v8 : ℚ
6. v9 : ℚ
7. v10 : ℚ
8. v11 : ℚ
9. ((v8 ≤ v9) ∧ (v8 ≤ v11)) ∧ (v10 ≤ v9) ∧ (v10 ≤ v11)
10. (((v8 = v4 ∈ ℚ) ∧ (v9 = qavg(v4;v5) ∈ ℚ)) ∨ ((v8 = qavg(v4;v5) ∈ ℚ) ∧ (v9 = v5 ∈ ℚ)))
∧ (((v10 = v6 ∈ ℚ) ∧ (v11 = qavg(v6;v7) ∈ ℚ)) ∨ ((v10 = qavg(v6;v7) ∈ ℚ) ∧ (v11 = v7 ∈ ℚ)))
⊢ ((v4 ≤ v5) ∧ (v4 ≤ v7)) ∧ (v6 ≤ v5) ∧ (v6 ≤ v7)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbQ{}Cube(k)
3.  b  :  \mBbbQ{}Cube(k)
4.  c  :  \mBbbQ{}Cube(k)
5.  d  :  \mBbbQ{}Cube(k)
6.  \mforall{}i:\mBbbN{}k.  (\muparrow{}is-half-interval(c  i;a  i))
7.  \mforall{}i:\mBbbN{}k.  (\muparrow{}is-half-interval(d  i;b  i))
8.  \mforall{}i:\mBbbN{}k.  (\muparrow{}Inhabited(c  i  \mcap{}  d  i))
\mvdash{}  \muparrow{}Inhabited(a  \mcap{}  b)


By

---

Latex:
((RWO  "assert-inhabited-rat-cube"  0  THENA  Auto)
  THEN  RepUR  ``rat-cube-intersection``  0
  THEN  ParallelLast
  THEN  (Assert  (\muparrow{}is-half-interval(c  i;a  i))  \mwedge{}  (\muparrow{}is-half-interval(d  i;b  i))  BY
                          Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};\mkleeneopen{}b  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{};\mkleeneopen{}d  i\mkleeneclose{}]\mcdot{}
  THEN  D  -8
  THEN  D  -6
  THEN  D  -4
  THEN  D  -2
  THEN  RepUR  ``rat-interval-intersection  inhabited-rat-interval``  0
  THEN  RepUR  ``is-half-interval``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "qmax\_lb"  0  THENA  Auto)
  THEN  (RWO  "qmin\_ub"  0  THENA  Auto)
  THEN  All  Thin
  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index