---

Step * 2 1 1 of Lemma baire2cantor2baire


1. a : ℕ ⟶ ℕ
2. init0(a)
3. increasing-sequence(a)
4. x : ℤ
5. a x ≠ a (x - 1)
6. x ≠ 0
7. 0 < x
8. cantor2baire-aux(baire2cantor(a);x - 1) = (a (x - 1)) ∈ ℕ
⊢ ((a (x - 1)) + 1) = (a x) ∈ ℕ
BY
{ (Unfold `increasing-sequence` 3
   THEN (InstHyp [⌜x - 1⌝] 3⋅ THENA Auto)
   THEN (Subst ⌜(x - 1) + 1 ~ x⌝ (-1)⋅ THENA Auto)) }

1
1. a : ℕ ⟶ ℕ
2. init0(a)
3. ∀n:ℕ. (((a (n + 1)) = (a n) ∈ ℕ) ∨ ((a (n + 1)) = ((a n) + 1) ∈ ℕ))
4. x : ℤ
5. a x ≠ a (x - 1)
6. x ≠ 0
7. 0 < x
8. cantor2baire-aux(baire2cantor(a);x - 1) = (a (x - 1)) ∈ ℕ
9. ((a x) = (a (x - 1)) ∈ ℕ) ∨ ((a x) = ((a (x - 1)) + 1) ∈ ℕ)
⊢ ((a (x - 1)) + 1) = (a x) ∈ ℕ

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  init0(a)
3.  increasing-sequence(a)
4.  x  :  \mBbbZ{}
5.  a  x  \mneq{}  a  (x  -  1)
6.  x  \mneq{}  0
7.  0  <  x
8.  cantor2baire-aux(baire2cantor(a);x  -  1)  =  (a  (x  -  1))
\mvdash{}  ((a  (x  -  1))  +  1)  =  (a  x)


By

---

Latex:
(Unfold  `increasing-sequence`  3
  THEN  (InstHyp  [\mkleeneopen{}x  -  1\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(x  -  1)  +  1  \msim{}  x\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index