Step
*
2
of Lemma
cantor-interval-req
.....upcase.....
1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
5. 0 < n
6. ((fst(cantor-interval(a;b;f;n - 1))) = (fst(cantor_ivl(a;b;f;n - 1))))
∧ ((snd(cantor-interval(a;b;f;n - 1))) = (snd(cantor_ivl(a;b;f;n - 1))))
⊢ ((fst(cantor-interval(a;b;f;n))) = (fst(cantor_ivl(a;b;f;n))))
∧ ((snd(cantor-interval(a;b;f;n))) = (snd(cantor_ivl(a;b;f;n))))
BY
{ (Unfold `cantor-interval` 0
THEN (UnrollPrimrec 0 THENA Auto)
THEN Fold `cantor-interval` 0
THEN (Unfold `cantor_ivl` 0 THEN Unfold `unit-interval-fan` 0)
THEN (UnrollPrimrec 0 THENA Auto)
THEN Fold `unit-interval-fan` 0
THEN (MoveToConcl (-1) THEN (GenConclTerm ⌜cantor-interval(a;b;f;n - 1)⌝⋅ THENA Auto))
THEN D -2
THEN Reduce 0
THEN Unfold `cantor_ivl` 0
THEN (GenConclTerm ⌜unit-interval-fan(f;n - 1)⌝⋅ THENA Auto)
THEN D -2
THEN Reduce 0
THEN (RWO "exp-fastexp<" 0 THENA Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN Reduce 0
THEN (BoolCase ⌜f (n - 1)⌝⋅ THENA Auto)
THEN (((CallByValueReduceOn ⌜3 * v4⌝ 0⋅ THENA Auto) THEN (CallByValueReduceOn ⌜v3 + (2 * v4)⌝ 0⋅ THENA Auto))
THEN Reduce 0
)
THEN (CallByValueReduce 0 THEN Auto)
THEN (RWO "int-rdiv-req" 0 THENA EAuto 2)
THEN (RWO "int-rmul-req" 0 THENA EAuto 2)
THEN (Assert (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ)) BY
EAuto 2)
THEN (Assert ⌜r(3^n) = (r(3^(n - 1)) * r(3))⌝⋅
THENA (RWO "rmul-int" 0 THEN Auto THEN RW (AddrC [2] (LemmaC `exp_step`)) 0 THEN Auto)
)) }
1
1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
5. 0 < n
6. v1 : ℝ
7. v2 : ℝ
8. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
9. v3 : ℤ
10. v4 : ℤ
11. unit-interval-fan(f;n - 1) = <v3, v4> ∈ (ℤ × ℤ)
12. ↑(f (n - 1))
13. v1 = (3^(n - 1) - v3 * a + v3 * b)/3^(n - 1)
14. v2 = (3^(n - 1) - v4 * a + v4 * b)/3^(n - 1)
15. (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ))
16. r(3^n) = (r(3^(n - 1)) * r(3))
⊢ ((r(2) * v1) + v2/r(3)) = ((r(3^n - (2 * v3) + v4) * a) + (r((2 * v3) + v4) * b)/r(3^n))
2
1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
5. 0 < n
6. v1 : ℝ
7. v2 : ℝ
8. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
9. v3 : ℤ
10. v4 : ℤ
11. unit-interval-fan(f;n - 1) = <v3, v4> ∈ (ℤ × ℤ)
12. ↑(f (n - 1))
13. v1 = (3^(n - 1) - v3 * a + v3 * b)/3^(n - 1)
14. v2 = (3^(n - 1) - v4 * a + v4 * b)/3^(n - 1)
15. (2 * v1 + v2)/3 = (3^n - (2 * v3) + v4 * a + (2 * v3) + v4 * b)/3^n
16. (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ))
17. r(3^n) = (r(3^(n - 1)) * r(3))
⊢ v2 = ((r(3^n - 3 * v4) * a) + (r(3 * v4) * b)/r(3^n))
3
1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
5. ¬↑(f (n - 1))
6. 0 < n
7. v1 : ℝ
8. v2 : ℝ
9. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
10. v3 : ℤ
11. v4 : ℤ
12. unit-interval-fan(f;n - 1) = <v3, v4> ∈ (ℤ × ℤ)
13. v1 = (3^(n - 1) - v3 * a + v3 * b)/3^(n - 1)
14. v2 = (3^(n - 1) - v4 * a + v4 * b)/3^(n - 1)
15. (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ))
16. r(3^n) = (r(3^(n - 1)) * r(3))
⊢ v1 = ((r(3^n - 3 * v3) * a) + (r(3 * v3) * b)/r(3^n))
4
1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
5. ¬↑(f (n - 1))
6. 0 < n
7. v1 : ℝ
8. v2 : ℝ
9. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
10. v3 : ℤ
11. v4 : ℤ
12. unit-interval-fan(f;n - 1) = <v3, v4> ∈ (ℤ × ℤ)
13. v1 = (3^(n - 1) - v3 * a + v3 * b)/3^(n - 1)
14. v2 = (3^(n - 1) - v4 * a + v4 * b)/3^(n - 1)
15. v1 = (3^n - 3 * v3 * a + 3 * v3 * b)/3^n
16. (¬(3^(n - 1) = 0 ∈ ℤ)) ∧ (¬(3^n = 0 ∈ ℤ))
17. r(3^n) = (r(3^(n - 1)) * r(3))
⊢ (v1 + (r(2) * v2)/r(3)) = ((r(3^n - v3 + (2 * v4)) * a) + (r(v3 + (2 * v4)) * b)/r(3^n))
Latex:
Latex:
.....upcase.....
1. a : \mBbbR{}
2. b : \mBbbR{}
3. f : \mBbbN{} {}\mrightarrow{} \mBbbB{}
4. n : \mBbbZ{}
5. 0 < n
6. ((fst(cantor-interval(a;b;f;n - 1))) = (fst(cantor\_ivl(a;b;f;n - 1))))
\mwedge{} ((snd(cantor-interval(a;b;f;n - 1))) = (snd(cantor\_ivl(a;b;f;n - 1))))
\mvdash{} ((fst(cantor-interval(a;b;f;n))) = (fst(cantor\_ivl(a;b;f;n))))
\mwedge{} ((snd(cantor-interval(a;b;f;n))) = (snd(cantor\_ivl(a;b;f;n))))
By
Latex:
(Unfold `cantor-interval` 0
THEN (UnrollPrimrec 0 THENA Auto)
THEN Fold `cantor-interval` 0
THEN (Unfold `cantor\_ivl` 0 THEN Unfold `unit-interval-fan` 0)
THEN (UnrollPrimrec 0 THENA Auto)
THEN Fold `unit-interval-fan` 0
THEN (MoveToConcl (-1) THEN (GenConclTerm \mkleeneopen{}cantor-interval(a;b;f;n - 1)\mkleeneclose{}\mcdot{} THENA Auto))
THEN D -2
THEN Reduce 0
THEN Unfold `cantor\_ivl` 0
THEN (GenConclTerm \mkleeneopen{}unit-interval-fan(f;n - 1)\mkleeneclose{}\mcdot{} THENA Auto)
THEN D -2
THEN Reduce 0
THEN (RWO "exp-fastexp<" 0 THENA Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN Reduce 0
THEN (BoolCase \mkleeneopen{}f (n - 1)\mkleeneclose{}\mcdot{} THENA Auto)
THEN (((CallByValueReduceOn \mkleeneopen{}3 * v4\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (CallByValueReduceOn \mkleeneopen{}v3 + (2 * v4)\mkleeneclose{} 0\mcdot{} THENA Auto)
)
THEN Reduce 0
)
THEN (CallByValueReduce 0 THEN Auto)
THEN (RWO "int-rdiv-req" 0 THENA EAuto 2)
THEN (RWO "int-rmul-req" 0 THENA EAuto 2)
THEN (Assert (\mneg{}(3\^{}(n - 1) = 0)) \mwedge{} (\mneg{}(3\^{}n = 0)) BY
EAuto 2)
THEN (Assert \mkleeneopen{}r(3\^{}n) = (r(3\^{}(n - 1)) * r(3))\mkleeneclose{}\mcdot{}
THENA (RWO "rmul-int" 0 THEN Auto THEN RW (AddrC [2] (LemmaC `exp\_step`)) 0 THEN Auto)
))
Home
Index