---

Step * 2 of Lemma mu'_wf


1. A : Type
2. P : A ⟶ ℕ ⟶ 𝔹
3. d : ∀x:A. Dec(∃n:ℕ. (↑(P x n)))
⊢ λx.(fst((TERMOF{p-mu-decider:o, 1:l, i:l} P d x))) ∈ A ⟶ (ℕ + Top)
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
3.  d  :  \mforall{}x:A.  Dec(\mexists{}n:\mBbbN{}.  (\muparrow{}(P  x  n)))
\mvdash{}  \mlambda{}x.(fst((TERMOF\{p-mu-decider:o,  1:l,  i:l\}  P  d  x)))  \mmember{}  A  {}\mrightarrow{}  (\mBbbN{}  +  Top)


By

---

Latex:
Auto

---

Home Index