---

Step * of Lemma mu'_wf

∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ 𝔹]. ∀[d:∀x:A. Dec(∃n:ℕ. (↑(P x n)))].  (mu'(P) ∈ A ⟶ (ℕ + Top))
BY
{ xxx((Auto THEN Unfold `mu\'` 0⋅)
      THEN Subst' TERMOF{p-mu-decider:o, 1:l, 1:l} ~ TERMOF{p-mu-decider:o, 1:l, i:l} 0
      )xxx }

1
.....equality..... 
1. A : Type
2. P : A ⟶ ℕ ⟶ 𝔹
3. d : ∀x:A. Dec(∃n:ℕ. (↑(P x n)))
⊢ TERMOF{p-mu-decider:o, 1:l, 1:l} ~ TERMOF{p-mu-decider:o, 1:l, i:l}

2
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)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[d:\mforall{}x:A.  Dec(\mexists{}n:\mBbbN{}.  (\muparrow{}(P  x  n)))].    (mu'(P)  \mmember{}  A  {}\mrightarrow{}  (\mBbbN{}  +  Top))


By

---

Latex:
xxx((Auto  THEN  Unfold  `mu\mbackslash{}'`  0\mcdot{})
        THEN  Subst'  TERMOF\{p-mu-decider:o,  1:l,  1:l\}  \msim{}  TERMOF\{p-mu-decider:o,  1:l,  i:l\}  0
        )xxx

---

Home Index