---

Step * 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 ∈ ℕ
⊢ mu(λi.(bb - 2 <z i ∨b(g (k + i)))) ∈ ℕbb
BY
{ xxx((InstLemma `mu-property` [⌜λi.(bb - 2 <z i ∨b(g (k + i)))⌝]⋅ THENA Auto) THEN Reduce (-1) THEN D -1)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. ∀[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

---

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
\mvdash{}  mu(\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i))))  \mmember{}  \mBbbN{}bb


By

---

Latex:
xxx((InstLemma  `mu-property`  [\mkleeneopen{}\mlambda{}i.(bb  -  2  <z  i  \mvee{}\msubb{}(g  (k  +  i)))\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  D  -1)xxx

---

Home Index