---

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


1. b : ℕ ⟶ ℕ+
2. g : ℕ ⟶ 𝔹
3. n : ℕ
4. k : ℕ
5. Σ(b j | j < n) = k ∈ ℕ
6. bb : ℕ
7. (b n) = bb ∈ ℕ
8. ↑(bb - 2 <z mu(λi.(bb - 2 <z i ∨b(g (k + i)))) ∨b(g (k + mu(λi.(bb - 2 <z i ∨b(g (k + i)))))))
9. v : ℤ
10. 0 ≤ v
11. mu(λi.(bb - 2 <z i ∨b(g (k + i)))) = v ∈ ℕ
12. ∀[i:ℕ]. ¬↑(bb - 2 <z i ∨b(g (k + i))) supposing i < v
⊢ v < bb
BY
{ xxx(SupposeNot THEN Auto)xxx }

1
1. b : ℕ ⟶ ℕ+
2. g : ℕ ⟶ 𝔹
3. n : ℕ
4. k : ℕ
5. Σ(b j | j < n) = k ∈ ℕ
6. bb : ℕ
7. (b n) = bb ∈ ℕ
8. ↑(bb - 2 <z mu(λi.(bb - 2 <z i ∨b(g (k + i)))) ∨b(g (k + mu(λi.(bb - 2 <z i ∨b(g (k + i)))))))
9. v : ℤ
10. 0 ≤ v
11. mu(λi.(bb - 2 <z i ∨b(g (k + i)))) = v ∈ ℕ
12. ∀[i:ℕ]. ¬↑(bb - 2 <z i ∨b(g (k + i))) supposing i < v
13. ¬v < bb
⊢ v < bb

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
3.  n  :  \mBbbN{}
4.  k  :  \mBbbN{}
5.  \mSigma{}(b  j  |  j  <  n)  =  k
6.  bb  :  \mBbbN{}
7.  (b  n)  =  bb
8.  \muparrow{}(bb  -  2  <z  mu(\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i))))  \mvee{}\msubb{}(g  (k  +  mu(\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i)))))))
9.  v  :  \mBbbZ{}
10.  0  \mleq{}  v
11.  mu(\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i))))  =  v
12.  \mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i)))  supposing  i  <  v
\mvdash{}  v  <  bb


By

---

Latex:
xxx(SupposeNot  THEN  Auto)xxx

---

Home Index