Step
*
2
1
1
of Lemma
compatible-half-cubes
.....assertion.....
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))
9. ∀i:ℕk. (↑Inhabited(a i ⋂ b i))
10. ∀i:ℕk. a i ⋂ b i ≤ a i
11. ∀i:ℕk. a i ⋂ b i ≤ b i
⊢ ∀i:ℕk. (c i ⋂ d i ≤ c i ∧ c i ⋂ d i ≤ d i)
BY
{ ((D 0 THENA Auto)
THEN ∀h:hyp. ((InstHyp [⌜i⌝] h⋅ THENA Complete (Auto)) THEN Thin h THEN 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 rat-interval-face`` 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 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)
THEN Try (Try (((Assert (v4 ≤ v4) ∧ (v4 ≤ v7) BY Complete (Auto)) THEN D 0 THEN Auto)))) }
1
1. v5 : ℚ
2. v6 : ℚ
3. v4 : ℚ
4. v4 ≤ v5
5. v4 ≤ qavg(v6;v5)
6. v6 ≤ qavg(v4;v5)
7. v6 ≤ v5
8. v4 ≤ v5
9. v4 ≤ v5
10. v6 ≤ v5
11. v6 ≤ v5
12. (v6 ≤ v4) ⇒ (v5 = v4 ∈ ℚ)
13. (v4 ≤ v6) ⇒ (v5 = v6 ∈ ℚ)
14. v5 ≤ v5
15. (v6 ≤ v4) ⇒ (v5 = v4 ∈ ℚ)
16. (v4 ≤ v6) ⇒ (v5 = v6 ∈ ℚ)
17. v5 ≤ v5
18. ∀a,b,c,d:ℚ. (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
⊢ (((v6 ≤ v4) ∧ ((v6 ≤ v4) ⇒ (v4 = qavg(v6;v5) ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (v4 = v5 ∈ ℚ)))
∨ ((((v6 ≤ v4) ⇒ (v4 = v5 ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (qavg(v4;v5) = v6 ∈ ℚ))) ∧ (v4 ≤ v6))
∨ ((v6 ≤ v4) ∧ (v4 ≤ v6)))
∧ (((v4 ≤ v6) ∧ ((v6 ≤ v4) ⇒ (v6 = v5 ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (v6 = qavg(v4;v5) ∈ ℚ)))
∨ ((((v6 ≤ v4) ⇒ (qavg(v6;v5) = v4 ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (v6 = v5 ∈ ℚ))) ∧ (v6 ≤ v4))
∨ ((v4 ≤ v6) ∧ (v6 ≤ v4)))
2
1. v4 : ℚ
2. v5 : ℚ
3. v4 ≤ v5
4. v4 ≤ v4
5. v4 ≤ v5
6. v4 ≤ v4
7. v4 ≤ v5
8. v4 ≤ v4
9. v4 ≤ v5
10. v4 ≤ v4
11. v4 ≤ v4
12. (v5 ≤ v4) ⇒ (v4 = v5 ∈ ℚ)
13. v4 ≤ v4
14. (v5 ≤ v4) ⇒ (v4 = v5 ∈ ℚ)
15. ∀a,b,c,d:ℚ. (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
⊢ (((v4 ≤ v4) ∧ ((v4 ≤ v5) ⇒ (v4 = v4 ∈ ℚ)) ∧ ((v5 ≤ v4) ⇒ (v4 = v5 ∈ ℚ)))
∨ ((((v4 ≤ v4) ⇒ (v4 = v5 ∈ ℚ)) ∧ ((v4 ≤ v4) ⇒ (v5 = v4 ∈ ℚ))) ∧ (v5 ≤ v4))
∨ ((v4 ≤ v4) ∧ (v5 ≤ v4)))
∧ (((v4 ≤ v4) ∧ ((v4 ≤ v5) ⇒ (v4 = v4 ∈ ℚ)) ∧ ((v5 ≤ v4) ⇒ (v4 = v5 ∈ ℚ)))
∨ ((((v4 ≤ v4) ⇒ (v4 = v4 ∈ ℚ)) ∧ ((v4 ≤ v4) ⇒ (v4 = v4 ∈ ℚ))) ∧ (v4 ≤ v5))
∨ ((v4 ≤ v4) ∧ (v4 ≤ v5)))
3
1. v4 : ℚ
2. v7 : ℚ
3. v5 : ℚ
4. v4 ≤ v5
5. qavg(v4;v5) ≤ v7
6. qavg(v4;v7) ≤ v5
7. v4 ≤ v7
8. v4 ≤ v5
9. v4 ≤ v7
10. v4 ≤ v5
11. v4 ≤ v7
12. v4 ≤ v4
13. (v7 ≤ v5) ⇒ (v4 = v7 ∈ ℚ)
14. (v5 ≤ v7) ⇒ (v4 = v5 ∈ ℚ)
15. v4 ≤ v4
16. (v7 ≤ v5) ⇒ (v4 = v7 ∈ ℚ)
17. (v5 ≤ v7) ⇒ (v4 = v5 ∈ ℚ)
18. ∀a,b,c,d:ℚ. (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
19. v4 ≤ v4
20. v4 ≤ v7
⊢ ((v7 ≤ v5) ∧ ((v7 ≤ v5) ⇒ (qavg(v4;v5) = v7 ∈ ℚ)) ∧ ((v5 ≤ v7) ⇒ (v5 = v4 ∈ ℚ)))
∨ ((((v7 ≤ v5) ⇒ (v5 = v4 ∈ ℚ)) ∧ ((v5 ≤ v7) ⇒ (v5 = qavg(v4;v7) ∈ ℚ))) ∧ (v5 ≤ v7))
∨ ((v7 ≤ v5) ∧ (v5 ≤ v7))
4
1. v4 : ℚ
2. v7 : ℚ
3. v5 : ℚ
4. v4 ≤ v5
5. qavg(v4;v5) ≤ v7
6. qavg(v4;v7) ≤ v5
7. v4 ≤ v7
8. v4 ≤ v5
9. v4 ≤ v7
10. v4 ≤ v5
11. v4 ≤ v7
12. v4 ≤ v4
13. (v7 ≤ v5) ⇒ (v4 = v7 ∈ ℚ)
14. (v5 ≤ v7) ⇒ (v4 = v5 ∈ ℚ)
15. v4 ≤ v4
16. (v7 ≤ v5) ⇒ (v4 = v7 ∈ ℚ)
17. (v5 ≤ v7) ⇒ (v4 = v5 ∈ ℚ)
18. ∀a,b,c,d:ℚ. (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
19. v4 ≤ v4
20. v4 ≤ v7
⊢ ((v5 ≤ v7) ∧ ((v7 ≤ v5) ⇒ (v7 = v4 ∈ ℚ)) ∧ ((v5 ≤ v7) ⇒ (qavg(v4;v7) = v5 ∈ ℚ)))
∨ ((((v7 ≤ v5) ⇒ (v7 = qavg(v4;v5) ∈ ℚ)) ∧ ((v5 ≤ v7) ⇒ (v7 = v4 ∈ ℚ))) ∧ (v7 ≤ v5))
∨ ((v5 ≤ v7) ∧ (v7 ≤ v5))
Latex:
Latex:
.....assertion.....
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))
9. \mforall{}i:\mBbbN{}k. (\muparrow{}Inhabited(a i \mcap{} b i))
10. \mforall{}i:\mBbbN{}k. a i \mcap{} b i \mleq{} a i
11. \mforall{}i:\mBbbN{}k. a i \mcap{} b i \mleq{} b i
\mvdash{} \mforall{}i:\mBbbN{}k. (c i \mcap{} d i \mleq{} c i \mwedge{} c i \mcap{} d i \mleq{} d i)
By
Latex:
((D 0 THENA Auto)
THEN \mforall{}h:hyp. ((InstHyp [\mkleeneopen{}i\mkleeneclose{}] h\mcdot{} THENA Complete (Auto)) THEN Thin h THEN 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 rat-interval-face`` 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 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)
THEN Try (Try (((Assert (v4 \mleq{} v4) \mwedge{} (v4 \mleq{} v7) BY Complete (Auto)) THEN D 0 THEN Auto))))
Home
Index