---

Step * 1 of Lemma enumerate_wf


1. P : ℕ ⟶ 𝔹
2. n : ℤ
⊢ mu(P) ∈ {k:ℕ| ↑(P k)}  supposing ∀n:ℕ. ∃k:ℕ. ((↑(P k)) ∧ (n ≤ k))
BY
{ xxx((D 0 THENA Auto)
      THEN InstHyp [⌜0⌝] (-1)⋅
      THEN Auto
      THEN Try ((ParallelLast THEN Auto))
      THEN InstLemma `mu-property` [⌜P⌝]⋅
      THEN Auto
      THEN ParallelLast
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  n  :  \mBbbZ{}
\mvdash{}  mu(P)  \mmember{}  \{k:\mBbbN{}|  \muparrow{}(P  k)\}    supposing  \mforall{}n:\mBbbN{}.  \mexists{}k:\mBbbN{}.  ((\muparrow{}(P  k))  \mwedge{}  (n  \mleq{}  k))


By

---

Latex:
xxx((D  0  THENA  Auto)
        THEN  InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}
        THEN  Auto
        THEN  Try  ((ParallelLast  THEN  Auto))
        THEN  InstLemma  `mu-property`  [\mkleeneopen{}P\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  ParallelLast
        THEN  Auto)xxx

---

Home Index