---

Step * of Lemma cantor-to-fb_wf

∀[b:ℕ ⟶ ℕ+]. ∀[g:ℕ ⟶ 𝔹]. ∀[n:ℕ].  (cantor-to-fb(b;g;n) ∈ ℕb n)
BY
{ (Intros
   THEN Unfold `cantor-to-fb` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Unhide
   THEN (GenConcl ⌜Σ(b j | j < n) = k ∈ ℕ⌝⋅ THENA (Auto THEN (MemTypeCD THEN Auto) THEN BLemma `non_neg_sum` THEN Auto))
   THEN (GenConcl ⌜(b n) = bb ∈ ℕ⌝⋅ THENA Auto)) }

1
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

---

Latex:

---

Latex:
\mforall{}[b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}].  \mforall{}[g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}].    (cantor-to-fb(b;g;n)  \mmember{}  \mBbbN{}b  n)


By

---

Latex:
(Intros
  THEN  Unfold  `cantor-to-fb`  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Unhide
  THEN  (GenConcl  \mkleeneopen{}\mSigma{}(b  j  |  j  <  n)  =  k\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  (MemTypeCD  THEN  Auto)  THEN  BLemma  `non\_neg\_sum`  THEN  Auto)
              )
  THEN  (GenConcl  \mkleeneopen{}(b  n)  =  bb\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index