---

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

.....subterm..... T:t
2:n
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)
13. k : ℕ
14. p : ℕ ⟶ 𝔹
15. q : ℕ ⟶ 𝔹
16. p = q ∈ (ℕg k ⟶ 𝔹)
17. n : ℕk
⊢ p = q ∈ ({g n..g (n + 1)-} ⟶ 𝔹)
BY
{ (SubsumeC ⌜ℕg k ⟶ 𝔹⌝⋅ THENL [Auto; (Assert ⌜(g (n + 1)) ≤ (g k)⌝⋅ THEN Auto)]) }

1
1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. (g 0) = 0 ∈ ℤ
6. ∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ)
7. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
8. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
9. h : k:ℕ ⟶ ℕ
10. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
11. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
12. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
13. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
14. k : ℕ
15. p : ℕ ⟶ 𝔹
16. q : ℕ ⟶ 𝔹
17. p = q ∈ (ℕg k ⟶ 𝔹)
18. n : ℕk
19. p = q ∈ (ℕg k ⟶ 𝔹)
⊢ (g (n + 1)) ≤ (g k)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{}\})
10.  \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)
11.  F  :  n:\mBbbN{}  {}\mrightarrow{}  (\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B  n
12.  \mforall{}n:\mBbbN{}.  Surj(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{};\mBbbN{}B  n;F  n)
13.  k  :  \mBbbN{}
14.  p  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
15.  q  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
16.  p  =  q
17.  n  :  \mBbbN{}k
\mvdash{}  p  =  q


By

---

Latex:
(SubsumeC  \mkleeneopen{}\mBbbN{}g  k  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}\mcdot{}  THENL  [Auto;  (Assert  \mkleeneopen{}(g  (n  +  1))  \mleq{}  (g  k)\mkleeneclose{}\mcdot{}  THEN  Auto)])

---

Home Index