---

Step * of Lemma mu-bound-unique

∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹]. ∀[x:ℕb].  mu(f) = x ∈ ℤ supposing (↑(f x)) ∧ (∀y:ℕb. ((↑(f y)) ⇒ (y = x ∈ ℤ)))
BY
{ (Auto
   THEN AssertBY ⌜∃n:ℕb. (↑(f n))⌝ ((InstConcl [⌜x⌝])⋅ THEN Auto)⋅
   THEN (InstLemma `mu-bound-property` [⌜b⌝; ⌜f⌝])⋅
   THEN Auto) }

1
1. b : ℕ
2. f : ℕb ⟶ 𝔹
3. x : ℕb
4. ↑(f x)
5. ∀y:ℕb. ((↑(f y)) ⇒ (y = x ∈ ℤ))
6. ∃n:ℕb. (↑(f n))
7. ↑(f mu(f))
8. ∀[i:ℕb]. ¬↑(f i) supposing i < mu(f)
⊢ mu(f) = x ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[b:\mBbbN{}].  \mforall{}[f:\mBbbN{}b  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:\mBbbN{}b].    mu(f)  =  x  supposing  (\muparrow{}(f  x))  \mwedge{}  (\mforall{}y:\mBbbN{}b.  ((\muparrow{}(f  y))  {}\mRightarrow{}  (y  =  x)))


By

---

Latex:
(Auto
  THEN  AssertBY  \mkleeneopen{}\mexists{}n:\mBbbN{}b.  (\muparrow{}(f  n))\mkleeneclose{}  ((InstConcl  [\mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THEN  Auto)\mcdot{}
  THEN  (InstLemma  `mu-bound-property`  [\mkleeneopen{}b\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}])\mcdot{}
  THEN  Auto)

---

Home Index