Step
*
1
of Lemma
surjection-cantor-finite-branching
1. b : ℕ ⟶ ℕ+
2. f : n:ℕ ⟶ ℕb n
3. x : ℕ
⊢ cantor-to-fb(b;λk.fb-to-cantor(b;f;k);x) = (f x) ∈ ℕb x
BY
{ (RepUR ``cantor-to-fb`` 0
THEN (GenConcl ⌜Σ(b j | j < x) = k ∈ ℕ⌝⋅ THENA (Auto THEN (MemTypeCD THEN Auto) THEN BLemma `non_neg_sum` THEN Auto))
THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }
1
1. b : ℕ ⟶ ℕ+
2. f : n:ℕ ⟶ ℕb n
3. x : ℕ
4. k : ℕ
5. Σ(b j | j < x) = k ∈ ℕ
⊢ mu(λi.((b x) - 2 <z i ∨bfb-to-cantor(b;f;k + i))) = (f x) ∈ ℕb x
Latex:
Latex:
1. b : \mBbbN{} {}\mrightarrow{} \mBbbN{}\msupplus{}
2. f : n:\mBbbN{} {}\mrightarrow{} \mBbbN{}b n
3. x : \mBbbN{}
\mvdash{} cantor-to-fb(b;\mlambda{}k.fb-to-cantor(b;f;k);x) = (f x)
By
Latex:
(RepUR ``cantor-to-fb`` 0
THEN (GenConcl \mkleeneopen{}\mSigma{}(b j | j < x) = k\mkleeneclose{}\mcdot{}
THENA (Auto THEN (MemTypeCD THEN Auto) THEN BLemma `non\_neg\_sum` THEN Auto)
)
THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto)))
Home
Index