---

Step * 1 1 1 2 2 1 of Lemma cantor-to-interval-onto-proper


1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. a ≤ x
6. x ≤ b
7. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
     ∃g:{g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} . (g = f ∈ (ℕn ⟶ 𝔹)\000C)
8. g : n:ℕ
⟶ f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} 
⟶ {g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} 
9. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .  ((g n f) = f ∈ (ℕn ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
11. λn.(primrec(n + 1;λx.ff;g) n) ∈ ℕ ⟶ 𝔹
12. n : ℕ
13. primrec(n;λx.ff;g) = primrec(n;λx.ff;g) ∈ (ℕn ⟶ 𝔹)
14. x ∈ [fst(cantor-interval(a;b;primrec(n;λx.ff;g);n)), snd(cantor-interval(a;b;primrec(n;λx.ff;g);n))]
⊢ x ∈ [fst(cantor-interval(a;b;λn.(primrec(n + 1;λx.ff;g) n);n)), snd(cantor-interval(a;b;λn.(primrec(n + 1;λx.ff;g) 
                                                                                              n);n))]
BY
{ ((Assert ⌜(λn.(primrec(n + 1;λx.ff;g) n)) = primrec(n;λx.ff;g) ∈ (ℕn ⟶ 𝔹)⌝⋅ THENM (HypSubst' (-1) 0 THEN Auto))
   THEN (FunExt THENA Auto)
   THEN Reduce 0) }

1
1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. a ≤ x
6. x ≤ b
7. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
     ∃g:{g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} . (g = f ∈ (ℕn ⟶ 𝔹)\000C)
8. g : n:ℕ
⟶ f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} 
⟶ {g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} 
9. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .  ((g n f) = f ∈ (ℕn ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
11. λn.(primrec(n + 1;λx.ff;g) n) ∈ ℕ ⟶ 𝔹
12. n : ℕ
13. primrec(n;λx.ff;g) = primrec(n;λx.ff;g) ∈ (ℕn ⟶ 𝔹)
14. x ∈ [fst(cantor-interval(a;b;primrec(n;λx.ff;g);n)), snd(cantor-interval(a;b;primrec(n;λx.ff;g);n))]
15. x1 : ℕn
⊢ primrec(x1 + 1;λx.ff;g) x1 = primrec(n;λx.ff;g) x1

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  <  b
4.  x  :  \mBbbR{}
5.  a  \mleq{}  x
6.  x  \mleq{}  b
7.  \mforall{}n:\mBbbN{}.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  .
          \mexists{}g:\{g:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;g;n  +  1)),  snd(cantor-interval(a;b;g;n  +  1))]\} 
            (g  =  f)
8.  g  :  n:\mBbbN{}
{}\mrightarrow{}  f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\} 
{}\mrightarrow{}  \{g:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;g;n  +  1)),  snd(cantor-interval(a;b;g;n  +  1))]\} 
9.  \mforall{}n:\mBbbN{}.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  .
          ((g  n  f)  =  f)
10.  \mforall{}n:\mBbbN{}
            (primrec(n;\mlambda{}x.ff;g)  \mmember{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}| 
                                                          x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  )
11.  \mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g)  n)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
12.  n  :  \mBbbN{}
13.  primrec(n;\mlambda{}x.ff;g)  =  primrec(n;\mlambda{}x.ff;g)
14.  x  \mmember{}  [fst(cantor-interval(a;b;primrec(n;\mlambda{}x.ff;g);n)),  snd(cantor-interval(a;b;primrec(n;\mlambda{}x.ff;
                                                                                                                                                                                  g);n))]
\mvdash{}  x  \mmember{}  [fst(cantor-interval(a;b;\mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g) 
                                                                      n);n)),  snd(cantor-interval(a;b;\mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g) 
                                                                                                                                              n);n))]


By

---

Latex:
((Assert  \mkleeneopen{}(\mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g)  n))  =  primrec(n;\mlambda{}x.ff;g)\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  Auto))
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0)

---

Home Index