---

Step * of Lemma mu-unique

∀[f:ℕ ⟶ 𝔹]. ∀[x:ℕ].  mu(f) = x ∈ ℤ supposing (↑(f x)) ∧ (∀y:ℕx. (¬↑(f y)))
BY
{ (Auto THEN (InstLemma `mu-bound-unique` [⌜x + 1⌝]⋅ THENA Auto) THEN BHyp -1  THEN Auto) }

1
1. f : ℕ ⟶ 𝔹
2. x : ℕ
3. ↑(f x)
4. ∀y:ℕx. (¬↑(f y))
5. ∀[f:ℕx + 1 ⟶ 𝔹]. ∀[x@0:ℕx + 1].  mu(f) = x@0 ∈ ℤ supposing (↑(f x@0)) ∧ (∀y:ℕx + 1. ((↑(f y)) ⇒ (y = x@0 ∈ ℤ)))
6. ↑(f x)
7. y : ℕx + 1@i
8. ↑(f y)@i
⊢ y = x ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `mu-bound-unique`  [\mkleeneopen{}x  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto)

---

Home Index