Step
*
1
1
2
1
2
1
of Lemma
cantor-to-interval-onto-common
1. a : ℝ
2. b : ℝ
3. [%] : a < b
4. x : ℝ
5. y : ℝ
6. x ∈ [a, b]
7. y ∈ [a, b]
8. n : ℕ
9. |x - y| ≤ (2^n * b - a)/6 * 3^n
10. ∀a,b:ℝ.
(((x ∈ [(2 * a + b)/3, b]) ∧ (y ∈ [(2 * a + b)/3, b]))
∨ ((x ∈ [a, (a + 2 * b)/3]) ∧ (y ∈ [a, (a + 2 * b)/3]))) supposing
(((x ∈ [a, b]) ∧ (y ∈ [a, b]) ∧ (|x - y| ≤ (b - a/r(6)))) and
(a < b))
11. ∀m:ℕ. ∀f:ℕm ⟶ 𝔹.
∃g:ℕm + 1 ⟶ 𝔹 [((g = f ∈ (ℕm ⟶ 𝔹))
∧ (x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))]))]
supposing (x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (m ≤ n)
12. ∀m:ℕn + 1. ∀f:{f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])} .
∃g:{g:ℕm + 1 ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])}
(g = f ∈ (ℕm ⟶ 𝔹))
13. g : m:ℕn + 1
⟶ f:{f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])}
⟶ {g:ℕm + 1 ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])}
14. ∀m:ℕn + 1. ∀f:{f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])} .
((g m f) = f ∈ (ℕm ⟶ 𝔹))
⊢ ∃f:ℕn ⟶ 𝔹
∀m:ℕn + 1
((x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))]))
BY
{ TACTIC:(Assert ⌜∀m:ℕn + 1
(primrec(m;λx.ff;g) ∈ {f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])} )⌝⋅
THENA ((D 0 THENA Auto)
THEN InstLemma `primrec-wf-nsub` [⌜n + 1⌝;
⌜λ2m.{f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])} ⌝
; ⌜λi.ff⌝;⌜g⌝;⌜m⌝]⋅
THEN Auto
THEN RepUR ``cantor-interval i-member`` 0
THEN MemTypeCD
THEN Auto)
) }
1
1. a : ℝ
2. b : ℝ
3. [%] : a < b
4. x : ℝ
5. y : ℝ
6. x ∈ [a, b]
7. y ∈ [a, b]
8. n : ℕ
9. |x - y| ≤ (2^n * b - a)/6 * 3^n
10. ∀a,b:ℝ.
(((x ∈ [(2 * a + b)/3, b]) ∧ (y ∈ [(2 * a + b)/3, b]))
∨ ((x ∈ [a, (a + 2 * b)/3]) ∧ (y ∈ [a, (a + 2 * b)/3]))) supposing
(((x ∈ [a, b]) ∧ (y ∈ [a, b]) ∧ (|x - y| ≤ (b - a/r(6)))) and
(a < b))
11. ∀m:ℕ. ∀f:ℕm ⟶ 𝔹.
∃g:ℕm + 1 ⟶ 𝔹 [((g = f ∈ (ℕm ⟶ 𝔹))
∧ (x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))]))]
supposing (x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (m ≤ n)
12. ∀m:ℕn + 1. ∀f:{f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])} .
∃g:{g:ℕm + 1 ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])}
(g = f ∈ (ℕm ⟶ 𝔹))
13. g : m:ℕn + 1
⟶ f:{f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])}
⟶ {g:ℕm + 1 ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
∧ (y ∈ [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])}
14. ∀m:ℕn + 1. ∀f:{f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])} .
((g m f) = f ∈ (ℕm ⟶ 𝔹))
15. ∀m:ℕn + 1
(primrec(m;λx.ff;g) ∈ {f:ℕm ⟶ 𝔹|
(x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])} )
⊢ ∃f:ℕn ⟶ 𝔹
∀m:ℕn + 1
((x ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
∧ (y ∈ [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))]))
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. [\%] : a < b
4. x : \mBbbR{}
5. y : \mBbbR{}
6. x \mmember{} [a, b]
7. y \mmember{} [a, b]
8. n : \mBbbN{}
9. |x - y| \mleq{} (2\^{}n * b - a)/6 * 3\^{}n
10. \mforall{}a,b:\mBbbR{}.
(((x \mmember{} [(2 * a + b)/3, b]) \mwedge{} (y \mmember{} [(2 * a + b)/3, b]))
\mvee{} ((x \mmember{} [a, (a + 2 * b)/3]) \mwedge{} (y \mmember{} [a, (a + 2 * b)/3]))) supposing
(((x \mmember{} [a, b]) \mwedge{} (y \mmember{} [a, b]) \mwedge{} (|x - y| \mleq{} (b - a/r(6)))) and
(a < b))
11. \mforall{}m:\mBbbN{}. \mforall{}f:\mBbbN{}m {}\mrightarrow{} \mBbbB{}.
\mexists{}g:\mBbbN{}m + 1 {}\mrightarrow{} \mBbbB{} [((g = f)
\mwedge{} (x \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m
+ 1))]))]
supposing (x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (m \mleq{} n)
12. \mforall{}m:\mBbbN{}n + 1. \mforall{}f:\{f:\mBbbN{}m {}\mrightarrow{} \mBbbB{}|
(x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])\} .
\mexists{}g:\{g:\mBbbN{}m + 1 {}\mrightarrow{} \mBbbB{}|
(x \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])\}
(g = f)
13. g : m:\mBbbN{}n + 1
{}\mrightarrow{} f:\{f:\mBbbN{}m {}\mrightarrow{} \mBbbB{}|
(x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])\}
{}\mrightarrow{} \{g:\mBbbN{}m + 1 {}\mrightarrow{} \mBbbB{}|
(x \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;g;m + 1)), snd(cantor-interval(a;b;g;m + 1))])\}
14. \mforall{}m:\mBbbN{}n + 1. \mforall{}f:\{f:\mBbbN{}m {}\mrightarrow{} \mBbbB{}|
(x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])\} .
((g m f) = f)
\mvdash{} \mexists{}f:\mBbbN{}n {}\mrightarrow{} \mBbbB{}
\mforall{}m:\mBbbN{}n + 1
((x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))]))
By
Latex:
TACTIC:(Assert \mkleeneopen{}\mforall{}m:\mBbbN{}n + 1
(primrec(m;\mlambda{}x.ff;g)
\mmember{} \{f:\mBbbN{}m {}\mrightarrow{} \mBbbB{}|
(x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])\} )\mkleeneclose{}\mcdot{}
THENA ((D 0 THENA Auto)
THEN InstLemma `primrec-wf-nsub` [\mkleeneopen{}n + 1\mkleeneclose{};
\mkleeneopen{}\mlambda{}\msubtwo{}m.\{f:\mBbbN{}m {}\mrightarrow{} \mBbbB{}|
(x \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])
\mwedge{} (y \mmember{} [fst(cantor-interval(a;b;f;m)), snd(cantor-interval(a;b;f;m))])\} \mkleeneclose{}
; \mkleeneopen{}\mlambda{}i.ff\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
THEN Auto
THEN RepUR ``cantor-interval i-member`` 0
THEN MemTypeCD
THEN Auto)
)
Home
Index