---

Step * 1 1 of Lemma cantor-to-general-cantor


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)
7. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
8. h : k:ℕ ⟶ ℕ
9. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
⊢ ∃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
{ ((Assert ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f) BY
          (Auto
           THEN (Assert {g n..g (n + 1)-} ⟶ 𝔹 ~ ℕ2^(C n) BY
                       ((InstLemma `equipollent-exp` [⌜C n⌝;⌜2⌝]⋅ THENA Auto)
                        THEN (Assert {g n..g (n + 1)-} ⟶ 𝔹 ~ ℕC n ⟶ ℕ2 BY
                                    (BLemma `indep-function_functionality_wrt_equipollent` 
                                     THEN Auto
                                     THEN RWO "6" 0
                                     THEN Auto))
                        THEN RelRST
                        THEN Auto))
           THEN RepeatFor 2 (D -1)
           THEN (Assert ∃F:ℕ2^(C n) ⟶ ℕB n. Surj(ℕ2^(C n);ℕB n;F) BY
                       (D 0 With ⌜λi.if i <z B n then i else 0 fi ⌝ 
                        THEN Auto
                        THEN (D 0 THENA Auto)
                        THEN Reduce 0
                        THEN (D 3 With ⌜n⌝  THENA Auto)
                        THEN D 0 With ⌜b⌝ 
                        THEN Auto))
           THEN D -1
           THEN (D 0 With ⌜F o f⌝  THENW Auto)
           THEN RepeatFor 2 (ParallelLast)
           THEN D -1
           THEN (D -6 With ⌜a⌝  THENA Auto)
           THEN ParallelLast
           THEN Reduce 0
           THEN Auto))
   THEN (Skolemize (-1) `F' THENA 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)
7. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
8. h : k:ℕ ⟶ ℕ
9. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
10. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
11. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
12. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
⊢ ∃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:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  C  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
3.  \mforall{}n:\mBbbN{}.  ((B  n)  \mleq{}  2\^{}(C  n))
4.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
5.  ((g  0)  =  0)  \mwedge{}  (\mforall{}i:\mBbbN{}.  ((g  (i  +  1))  =  ((g  i)  +  (C  i))))
6.  \mforall{}n,m:\mBbbN{}.    (n  <  m  {}\mRightarrow{}  g  n  <  g  m)
7.  \mforall{}k:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (k  \mmember{}  \{g  n..g  (n  +  1)\msupminus{}\})
8.  h  :  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
9.  \mforall{}k:\mBbbN{}.  (k  \mmember{}  \{g  (h  k)..g  ((h  k)  +  1)\msupminus{}\})
\mvdash{}  \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:
((Assert  \mforall{}n:\mBbbN{}.  \mexists{}f:(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B  n.  Surj(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{};\mBbbN{}B  n;f)  BY
                (Auto
                  THEN  (Assert  \{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}  \msim{}  \mBbbN{}2\^{}(C  n)  BY
                                          ((InstLemma  `equipollent-exp`  [\mkleeneopen{}C  n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                            THEN  (Assert  \{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}  \msim{}  \mBbbN{}C  n  {}\mrightarrow{}  \mBbbN{}2  BY
                                                                    (BLemma  `indep-function\_functionality\_wrt\_equipollent` 
                                                                      THEN  Auto
                                                                      THEN  RWO  "6"  0
                                                                      THEN  Auto))
                                            THEN  RelRST
                                            THEN  Auto))
                  THEN  RepeatFor  2  (D  -1)
                  THEN  (Assert  \mexists{}F:\mBbbN{}2\^{}(C  n)  {}\mrightarrow{}  \mBbbN{}B  n.  Surj(\mBbbN{}2\^{}(C  n);\mBbbN{}B  n;F)  BY
                                          (D  0  With  \mkleeneopen{}\mlambda{}i.if  i  <z  B  n  then  i  else  0  fi  \mkleeneclose{} 
                                            THEN  Auto
                                            THEN  (D  0  THENA  Auto)
                                            THEN  Reduce  0
                                            THEN  (D  3  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)
                                            THEN  D  0  With  \mkleeneopen{}b\mkleeneclose{} 
                                            THEN  Auto))
                  THEN  D  -1
                  THEN  (D  0  With  \mkleeneopen{}F  o  f\mkleeneclose{}    THENW  Auto)
                  THEN  RepeatFor  2  (ParallelLast)
                  THEN  D  -1
                  THEN  (D  -6  With  \mkleeneopen{}a\mkleeneclose{}    THENA  Auto)
                  THEN  ParallelLast
                  THEN  Reduce  0
                  THEN  Auto))
  THEN  (Skolemize  (-1)  `F'  THENA  Auto)
  )

---

Home Index