---

Step * 1 of Lemma same-half-cube-of-compatible


1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. i : ℕk
⊢ (↑Inhabited(c i))
⇒ (↑is-half-interval(c i;a i))
⇒ (↑is-half-interval(c i;b i))
⇒ a i ⋂ b i ≤ a i
⇒ a i ⋂ b i ≤ b i
⇒ ((a i) = (b i) ∈ ℚInterval)
BY
{ (GenConclTerms Auto [⌜a i⌝;⌜b i⌝;⌜c i⌝]⋅
   THEN D -6
   THEN D -4
   THEN D -2
   THEN RepUR ``rat-interval-intersection inhabited-rat-interval`` 0
   THEN RepUR ``is-half-interval rat-interval-face`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN All Thin
   THEN ((Assert ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ)) BY
                (Unfold `rational-interval` 0 THEN Auto))
         THEN All (Unfold `rat-point-interval`)
         THEN (RWO "-1" 0 THENA Auto)
         THEN (All (RWO "qmax-eq-iff-1 qmax-eq-iff-2 qmin-eq-iff-1 qmin-eq-iff-2") THENA Auto)
         THEN (All (RWO "qmax-eq-iff qmin-eq-iff") THENA Auto))
   THEN skip{(RepeatFor 4 ((D 0 THENA Auto))
              THEN (SplitOrHyps THEN (ExRepD THENW Auto))
              THEN ((Eliminate ⌜v8⌝⋅ THENA Auto) THEN ThinVar `v8')
              THEN ((Eliminate ⌜v9⌝⋅ THENA Auto) THEN ThinVar `v9')
              THEN ((Eliminate ⌜v10⌝⋅ THENA Auto) THEN ThinVar `v10')
              THEN ((Eliminate ⌜v11⌝⋅ THENA Auto) THEN ThinVar `v11')
              THEN ∀h:hyp. (RWO "qle-qavg-iff-1 qavg-qle-iff-1" h THENA Auto) 
              THEN All (Unfold `rat-point-interval`)
              THEN (Assert ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ)) BY
                          (Unfold `rational-interval` 0 THEN Auto))
              THEN (RWO "-1" (-3) THENA Auto)
              THEN (RWO "-1" (-2) THENA Auto)
              THEN (RWO "-1" 0 THENA Auto)
              THEN (All (RWO "qmax-eq-iff-1 qmax-eq-iff-2 qmin-eq-iff-1 qmin-eq-iff-2") THENA Auto)
              THEN (All (RWO "qmax-eq-iff qmin-eq-iff") THENA Auto)
              THEN SplitOrHyps
              THEN ExRepD
              THEN Repeat ((ThinTrivial
                            THEN (RationalElim ⌜v6⌝⋅ ORELSE RationalElim ⌜v7⌝⋅ ORELSE RationalElim ⌜v5⌝⋅)
                            THEN All QavgSimp))
              THEN Try (QuickAuto))}) }

1
1. v3 : ℚ
2. v4 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. v7 : ℚ
6. v8 : ℚ
7. ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
⊢ (v7 ≤ v8)
⇒ (((v7 = v3 ∈ ℚ) ∧ (v8 = qavg(v3;v4) ∈ ℚ)) ∨ ((v7 = qavg(v3;v4) ∈ ℚ) ∧ (v8 = v4 ∈ ℚ)))
⇒ (((v7 = v5 ∈ ℚ) ∧ (v8 = qavg(v5;v6) ∈ ℚ)) ∨ ((v7 = qavg(v5;v6) ∈ ℚ) ∧ (v8 = v6 ∈ ℚ)))
⇒ (((v5 ≤ v3) ∧ ((v6 ≤ v4) ⇒ (v3 = v6 ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (v3 = v4 ∈ ℚ)))
   ∨ ((((v5 ≤ v3) ⇒ (v4 = v3 ∈ ℚ)) ∧ ((v3 ≤ v5) ⇒ (v4 = v5 ∈ ℚ))) ∧ (v4 ≤ v6))
   ∨ ((v5 ≤ v3) ∧ (v4 ≤ v6)))
⇒ (((v3 ≤ v5) ∧ ((v6 ≤ v4) ⇒ (v5 = v6 ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (v5 = v4 ∈ ℚ)))
   ∨ ((((v5 ≤ v3) ⇒ (v6 = v3 ∈ ℚ)) ∧ ((v3 ≤ v5) ⇒ (v6 = v5 ∈ ℚ))) ∧ (v6 ≤ v4))
   ∨ ((v3 ≤ v5) ∧ (v6 ≤ v4)))
⇒ ((v3 = v5 ∈ ℚ) ∧ (v4 = v6 ∈ ℚ))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbQ{}Cube(k)
3.  b  :  \mBbbQ{}Cube(k)
4.  c  :  \mBbbQ{}Cube(k)
5.  i  :  \mBbbN{}k
\mvdash{}  (\muparrow{}Inhabited(c  i))
{}\mRightarrow{}  (\muparrow{}is-half-interval(c  i;a  i))
{}\mRightarrow{}  (\muparrow{}is-half-interval(c  i;b  i))
{}\mRightarrow{}  a  i  \mcap{}  b  i  \mleq{}  a  i
{}\mRightarrow{}  a  i  \mcap{}  b  i  \mleq{}  b  i
{}\mRightarrow{}  ((a  i)  =  (b  i))


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};\mkleeneopen{}b  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  D  -6
  THEN  D  -4
  THEN  D  -2
  THEN  RepUR  ``rat-interval-intersection  inhabited-rat-interval``  0
  THEN  RepUR  ``is-half-interval  rat-interval-face``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  All  Thin
  THEN  ((Assert  \mforall{}a,b,c,d:\mBbbQ{}.    (<a,  b>  =  <c,  d>  \mLeftarrow{}{}\mRightarrow{}  (a  =  c)  \mwedge{}  (b  =  d))  BY
                            (Unfold  `rational-interval`  0  THEN  Auto))
              THEN  All  (Unfold  `rat-point-interval`)
              THEN  (RWO  "-1"  0  THENA  Auto)
              THEN  (All  (RWO  "qmax-eq-iff-1  qmax-eq-iff-2  qmin-eq-iff-1  qmin-eq-iff-2")  THENA  Auto)
              THEN  (All  (RWO  "qmax-eq-iff  qmin-eq-iff")  THENA  Auto))
  THEN  skip\{(RepeatFor  4  ((D  0  THENA  Auto))
                        THEN  (SplitOrHyps  THEN  (ExRepD  THENW  Auto))
                        THEN  ((Eliminate  \mkleeneopen{}v8\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v8')
                        THEN  ((Eliminate  \mkleeneopen{}v9\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v9')
                        THEN  ((Eliminate  \mkleeneopen{}v10\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v10')
                        THEN  ((Eliminate  \mkleeneopen{}v11\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v11')
                        THEN  \mforall{}h:hyp.  (RWO  "qle-qavg-iff-1  qavg-qle-iff-1"  h  THENA  Auto) 
                        THEN  All  (Unfold  `rat-point-interval`)
                        THEN  (Assert  \mforall{}a,b,c,d:\mBbbQ{}.    (<a,  b>  =  <c,  d>  \mLeftarrow{}{}\mRightarrow{}  (a  =  c)  \mwedge{}  (b  =  d))  BY
                                                (Unfold  `rational-interval`  0  THEN  Auto))
                        THEN  (RWO  "-1"  (-3)  THENA  Auto)
                        THEN  (RWO  "-1"  (-2)  THENA  Auto)
                        THEN  (RWO  "-1"  0  THENA  Auto)
                        THEN  (All  (RWO  "qmax-eq-iff-1  qmax-eq-iff-2  qmin-eq-iff-1  qmin-eq-iff-2")  THENA  Auto)
                        THEN  (All  (RWO  "qmax-eq-iff  qmin-eq-iff")  THENA  Auto)
                        THEN  SplitOrHyps
                        THEN  ExRepD
                        THEN  Repeat  ((ThinTrivial
                                                    THEN  (RationalElim  \mkleeneopen{}v6\mkleeneclose{}\mcdot{}
                                                                ORELSE  RationalElim  \mkleeneopen{}v7\mkleeneclose{}\mcdot{}
                                                                ORELSE  RationalElim  \mkleeneopen{}v5\mkleeneclose{}\mcdot{})
                                                    THEN  All  QavgSimp))
                        THEN  Try  (QuickAuto))\})

---

Home Index