---

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