---

Step * 1 of Lemma can-apply-mu'


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))
BY
{ (GenConclAtAddr [1;1;1;1]
   THEN Thin (-1)
   THEN (D -1 THEN Reduce 0)
   THEN (D -2 THEN Reduce 0)
   THEN RepUR ``p-mu`` -1
   THEN Auto
   THEN RWW "not_over_exists<" (-2)
   THEN 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)))
4.  x  :  A
\mvdash{}  \muparrow{}isl(fst((TERMOF\{p-mu-decider:o,  1:l,  i:l\}  P  d  x)))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (\muparrow{}(P  x  n))


By

---

Latex:
(GenConclAtAddr  [1;1;1;1]
  THEN  Thin  (-1)
  THEN  (D  -1  THEN  Reduce  0)
  THEN  (D  -2  THEN  Reduce  0)
  THEN  RepUR  ``p-mu``  -1
  THEN  Auto
  THEN  RWW  "not\_over\_exists<"  (-2)
  THEN  Auto)

---

Home Index