---

Step * of Lemma enumerate_wf

∀[P:ℕ ⟶ 𝔹]. ∀[n:ℕ].  enumerate(P;n) ∈ {k:ℕ| ↑(P k)}  supposing ∀n:ℕ. ∃k:ℕ. ((↑(P k)) ∧ (n ≤ k))
BY
{ ((Unfold `enumerate` 0 THEN InductionOnNat) THEN Reduce 0) }

1
1. P : ℕ ⟶ 𝔹
2. n : ℤ
⊢ mu(P) ∈ {k:ℕ| ↑(P k)}  supposing ∀n:ℕ. ∃k:ℕ. ((↑(P k)) ∧ (n ≤ k))

2
.....upcase..... 
1. P : ℕ ⟶ 𝔹
2. n : ℤ
3. 0 < n
4. primrec(n - 1;mu(P);λi,r. eval r' = r + 1 in r' + mu(λk.(P (r' + k)))) ∈ {k:ℕ| ↑(P k)}  supposing ∀n:ℕ. ∃k:ℕ. ((↑(P k\000C)) ∧ (n ≤ k))
⊢ primrec(n;mu(P);λi,r. eval r' = r + 1 in r' + mu(λk.(P (r' + k)))) ∈ {k:ℕ| ↑(P k)}  supposing ∀n:ℕ. ∃k:ℕ. ((↑(P k)) ∧ \000C(n ≤ k))

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}].    enumerate(P;n)  \mmember{}  \{k:\mBbbN{}|  \muparrow{}(P  k)\}    supposing  \mforall{}n:\mBbbN{}.  \mexists{}k:\mBbbN{}.  ((\muparrow{}(P  k))  \mwedge{}  (n  \mleq{}  k))


By

---

Latex:
((Unfold  `enumerate`  0  THEN  InductionOnNat)  THEN  Reduce  0)

---

Home Index