---

Step * 1 of Lemma mu'_wf

.....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}
BY
{ xxx(RW (SubC (ComputeToC []) ) 0 THEN Trivial)xxx }

---

Latex:

---

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


By

---

Latex:
xxx(RW  (SubC  (ComputeToC  [])  )  0  THEN  Trivial)xxx

---

Home Index