---

Step * of Lemma cantor-to-general-cantor

∀B:ℕ ⟶ ℕ+
  ∃f:(ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]
   (Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕB[n];f)
   ∧ (∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))))
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∃C:ℕ ⟶ ℕ+. ∀n:ℕ. ((B n) ≤ 2^(C n)) BY
               (D 0 With ⌜λn.imax(log(2;B n);1)⌝ 
                THEN Reduce 0
                THEN Auto
                THEN (Assert (B n) ≤ 2^log(2;B n) BY
                            Auto)
                THEN (RWO "-1" 0 THENA Auto)
                THEN BLemma `exp_functionality_wrt_le_1`
                THEN Auto))
   THEN D -1
   THEN (Assert ∃g:ℕ ⟶ ℕ. (((g 0) = 0 ∈ ℤ) ∧ (∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ))) BY
               (D 0 With ⌜λi.primrec(i;0;λj,x. (x + (C j)))⌝ 
                THEN Reduce 0
                THEN Auto
                THEN RW (AddrC [2] (LemmaC `primrec-unroll`)) 0
                THEN Reduce 0
                THEN Auto))
   THEN D -1
   THEN (Assert ∀n,m:ℕ.  (n < m ⇒ g n < g m) BY
               ((Assert ∀d:ℕ+. ∀n:ℕ.  g n < g (n + d) BY
                       (InductionOnNat
                        THEN Auto
                        THEN ((RWO "-3" 0 THEN Auto)
                        ORELSE ((Subst' n + d + 1 ~ (n + d) + 1 0 THENA Auto)
                                THEN RWO  "-5"  0
                                THEN Auto
                                THEN D -2 With ⌜n⌝ 
                                THEN Auto)
                        )))
                THEN Auto
                THEN InstHyp [⌜m - n⌝;⌜n⌝] (-4)⋅
                THEN Auto))) }

1
1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. ((g 0) = 0 ∈ ℤ) ∧ (∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ))
6. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
⊢ ∃f:(ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]
   (Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕB[n];f)
   ∧ (∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))))

---

Latex:

---

Latex:
\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
    \mexists{}f:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n]
      (Surj(\mBbbN{}  {}\mrightarrow{}  \mBbbB{};n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n];f)  \mwedge{}  (\mforall{}k:\mBbbN{}.  \mexists{}j:\mBbbN{}.  \mforall{}p,q:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((p  =  q)  {}\mRightarrow{}  ((f  p)  =  (f  q)))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mexists{}C:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.  ((B  n)  \mleq{}  2\^{}(C  n))  BY
                          (D  0  With  \mkleeneopen{}\mlambda{}n.imax(log(2;B  n);1)\mkleeneclose{} 
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  (Assert  (B  n)  \mleq{}  2\^{}log(2;B  n)  BY
                                                    Auto)
                            THEN  (RWO  "-1"  0  THENA  Auto)
                            THEN  BLemma  `exp\_functionality\_wrt\_le\_1`
                            THEN  Auto))
  THEN  D  -1
  THEN  (Assert  \mexists{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (((g  0)  =  0)  \mwedge{}  (\mforall{}i:\mBbbN{}.  ((g  (i  +  1))  =  ((g  i)  +  (C  i)))))  BY
                          (D  0  With  \mkleeneopen{}\mlambda{}i.primrec(i;0;\mlambda{}j,x.  (x  +  (C  j)))\mkleeneclose{} 
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  RW  (AddrC  [2]  (LemmaC  `primrec-unroll`))  0
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  D  -1
  THEN  (Assert  \mforall{}n,m:\mBbbN{}.    (n  <  m  {}\mRightarrow{}  g  n  <  g  m)  BY
                          ((Assert  \mforall{}d:\mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.    g  n  <  g  (n  +  d)  BY
                                          (InductionOnNat
                                            THEN  Auto
                                            THEN  ((RWO  "-3"  0  THEN  Auto)
                                            ORELSE  ((Subst'  n  +  d  +  1  \msim{}  (n  +  d)  +  1  0  THENA  Auto)
                                                            THEN  RWO    "-5"    0
                                                            THEN  Auto
                                                            THEN  D  -2  With  \mkleeneopen{}n\mkleeneclose{} 
                                                            THEN  Auto)
                                            )))
                            THEN  Auto
                            THEN  InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  (-4)\mcdot{}
                            THEN  Auto)))

---

Home Index