---

Step * of Lemma mu-dec_wf

∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ]. ∀[d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k])]. ∀[a:A].  mu-dec(d;a) ∈ ℕ supposing ↓∃k:ℕ. P[a;k]
BY
{ TACTIC:((UnivCD THENA Auto) THEN D -1 THEN RepUR ``decidable or mu-dec`` 0 THEN Auto THEN Reduce 0) }

1
1. A : Type
2. P : A ⟶ ℕ ⟶ ℙ
3. d : a:A ⟶ k:ℕ ⟶ Dec(P[a;k])
4. a : A
5. ∃k:ℕ. P[a;k]
⊢ ∃n:ℕ. (↑isl(d a n))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:a:A  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  Dec(P[a;k])].  \mforall{}[a:A].
    mu-dec(d;a)  \mmember{}  \mBbbN{}  supposing  \mdownarrow{}\mexists{}k:\mBbbN{}.  P[a;k]


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  D  -1  THEN  RepUR  ``decidable  or  mu-dec``  0  THEN  Auto  THEN  Reduce  0)

---

Home Index