---

Step * of Lemma do-apply-mu'

∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ 𝔹]. ∀[d:∀x:A. Dec(∃n:ℕ. (↑(P x n)))]. ∀[x:A].
  {(↑(P x do-apply(mu'(P);x))) ∧ (∀[i:ℕdo-apply(mu'(P);x)]. (¬↑(P x i)))} supposing ↑can-apply(mu'(P);x)
BY
{ xxx(Auto
      THEN (MoveToConcl (-1))
      THEN RepUR ``mu\' can-apply do-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))))
⇒ {(↑(P x outl(fst((TERMOF{p-mu-decider:o, 1:l, i:l} P d x)))))
   ∧ (∀[i:ℕoutl(fst((TERMOF{p-mu-decider:o, 1:l, i:l} P d x)))]. (¬↑(P x i)))}

---

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{}(P  x  do-apply(mu'(P);x)))  \mwedge{}  (\mforall{}[i:\mBbbN{}do-apply(mu'(P);x)].  (\mneg{}\muparrow{}(P  x  i)))\} 
    supposing  \muparrow{}can-apply(mu'(P);x)


By

---

Latex:
xxx(Auto
        THEN  (MoveToConcl  (-1))
        THEN  RepUR  ``mu\mbackslash{}'  can-apply  do-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