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