---

Step * 1 of Lemma do-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))))
⇒ {(↑(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)))}
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) }

1
1. A : Type
2. P : A ⟶ ℕ ⟶ 𝔹
3. d : ∀x:A. Dec(∃n:ℕ. (↑(P x n)))
4. x : A
5. x1 : ℕ
6. v2 : ↑(P x x1)
7. v3 : ∀i:ℕx1. (¬↑(P x i))
8. True
⊢ {(↑(P x x1)) ∧ (∀[i:ℕx1]. (¬↑(P x i)))}

---

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))))
{}\mRightarrow{}  \{(\muparrow{}(P  x  outl(fst((TERMOF\{p-mu-decider:o,  1:l,  i:l\}  P  d  x)))))
      \mwedge{}  (\mforall{}[i:\mBbbN{}outl(fst((TERMOF\{p-mu-decider:o,  1:l,  i:l\}  P  d  x)))].  (\mneg{}\muparrow{}(P  x  i)))\}


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)

---

Home Index