---

Step * 1 1 2 of Lemma fb-to-cantor_wf


1. b : ℕ ⟶ ℕ+
2. f : n:ℕ ⟶ ℕb n
3. k : ℕ
4. m : ℕ
5. mu(λm.k <z Σ(b j | j < m)) = m ∈ ℕ
6. m = 0 ∈ ℤ
⊢ ∃n:ℕ. (↑k <z Σ(b j | j < n))
BY
{ xxx(With ⌜k + 1⌝ (D 0)⋅
      THEN Auto
      THEN (InstLemma `sum_lower_bound` [⌜k + 1⌝;⌜1⌝]⋅ THENA Auto)
      THEN RWO "-1<" 0
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  f  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}b  n
3.  k  :  \mBbbN{}
4.  m  :  \mBbbN{}
5.  mu(\mlambda{}m.k  <z  \mSigma{}(b  j  |  j  <  m))  =  m
6.  m  =  0
\mvdash{}  \mexists{}n:\mBbbN{}.  (\muparrow{}k  <z  \mSigma{}(b  j  |  j  <  n))


By

---

Latex:
xxx(With  \mkleeneopen{}k  +  1\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  (InstLemma  `sum\_lower\_bound`  [\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  RWO  "-1<"  0
        THEN  Auto)xxx

---

Home Index