---

Step * 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. ∀[i:ℕ]. ¬↑(bb - 2 <z i ∨b(g (k + i))) supposing i < mu(λi.(bb - 2 <z i ∨b(g (k + i))))
⊢ mu(λi.(bb - 2 <z i ∨b(g (k + i)))) ∈ ℕbb
BY
{ xxx(MoveToConcl (-1) THEN (GenConclTerm ⌜mu(λi.(bb - 2 <z i ∨b(g (k + i))))⌝⋅ THENA 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. mu(λi.(bb - 2 <z i ∨b(g (k + i)))) = v ∈ ℕ
⊢ (∀[i:ℕ]. ¬↑(bb - 2 <z i ∨b(g (k + i))) supposing i < v) ⇒ (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.  \mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i)))  supposing  i  <  mu(\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i))))
\mvdash{}  mu(\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i))))  \mmember{}  \mBbbN{}bb


By

---

Latex:
xxx(MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}mu(\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i))))\mkleeneclose{}\mcdot{}  THENA  Auto))xxx

---

Home Index