Step
*
of Lemma
mu'_wf
∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ 𝔹]. ∀[d:∀x:A. Dec(∃n:ℕ. (↑(P x n)))]. (mu'(P) ∈ A ⟶ (ℕ + Top))
BY
{ xxx((Auto THEN Unfold `mu\'` 0⋅)
THEN Subst' TERMOF{p-mu-decider:o, 1:l, 1:l} ~ TERMOF{p-mu-decider:o, 1:l, i:l} 0
)xxx }
1
.....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}
2
1. A : Type
2. P : A ⟶ ℕ ⟶ 𝔹
3. d : ∀x:A. Dec(∃n:ℕ. (↑(P x n)))
⊢ λx.(fst((TERMOF{p-mu-decider:o, 1:l, i:l} P d x))) ∈ A ⟶ (ℕ + Top)
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)))]. (mu'(P) \mmember{} A {}\mrightarrow{} (\mBbbN{} + Top))
By
Latex:
xxx((Auto THEN Unfold `mu\mbackslash{}'` 0\mcdot{})
THEN Subst' TERMOF\{p-mu-decider:o, 1:l, 1:l\} \msim{} TERMOF\{p-mu-decider:o, 1:l, i:l\} 0
)xxx
Home
Index