---

Step * of Lemma can-apply-mu'

∀[A:Type]. ∀P:A ⟶ ℕ ⟶ 𝔹. ∀d:∀x:A. Dec(∃n:ℕ. (↑(P x n))). ∀x:A.  (↑can-apply(mu'(P);x) ⇐⇒ ∃n:ℕ. (↑(P x n)))
BY
{ xxx((UnivCD THENA Auto)
      THEN RepUR ``mu\' can-apply`` 0
      THEN (Subst' TERMOF{p-mu-decider:o, 1:l, 1:l} ~ TERMOF{p-mu-decider:o, 1:l, i:l} 0
            THENL [((RW (SubC (ComputeToC [])) 0) THEN Trivial); Id]
      ))xxx }

1
1. [A] : Type
2. P : A ⟶ ℕ ⟶ 𝔹
3. d : ∀x:A. Dec(∃n:ℕ. (↑(P x n)))
4. x : A
⊢ ↑isl(fst((TERMOF{p-mu-decider:o, 1:l, i:l} P d x))) ⇐⇒ ∃n:ℕ. (↑(P x n))

---

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))).  \mforall{}x:A.    (\muparrow{}can-apply(mu'(P);x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (\muparrow{}(P  x  n)))


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  RepUR  ``mu\mbackslash{}'  can-apply``  0
        THEN  (Subst'  TERMOF\{p-mu-decider:o,  1:l,  1:l\}  \msim{}  TERMOF\{p-mu-decider:o,  1:l,  i:l\}  0
                    THENL  [((RW  (SubC  (ComputeToC  []))  0)  THEN  Trivial);  Id]
        ))xxx

---

Home Index