---

Step * of Lemma mu-wf2

∀[P:ℕ ⟶ ℙ]. ∀[d:∀n:ℕ. Dec(P[n])].  mu(d) ∈ ℕ supposing ∃n:ℕ. P[n]
BY
{ TACTIC:((InstLemma `mu-ge_wf2` [⌜0⌝]⋅ THENA Auto)
          THEN Intro
          THEN ParallelOp -2
          THEN Fold `mu` (-1)
          THEN ParallelLast) }

1
.....antecedent..... 
1. ∀[f:{0...} ⟶ (Top + Top)]. mu-ge(f;0) ∈ {0...} supposing ∃m:{0...}. (↑isl(f m))
2. P : ℕ ⟶ ℙ
3. d : ∀n:ℕ. Dec(P[n])
4. ∃n:ℕ. P[n]
⊢ ∃m:{0...}. (↑isl(d m))

2
1. ∀[f:{0...} ⟶ (Top + Top)]. mu-ge(f;0) ∈ {0...} supposing ∃m:{0...}. (↑isl(f m))
2. P : ℕ ⟶ ℙ
3. d : ∀n:ℕ. Dec(P[n])
4. ∃n:ℕ. P[n]
5. mu(d) ∈ {0...}
⊢ mu(d) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}n:\mBbbN{}.  Dec(P[n])].    mu(d)  \mmember{}  \mBbbN{}  supposing  \mexists{}n:\mBbbN{}.  P[n]


By

---

Latex:
TACTIC:((InstLemma  `mu-ge\_wf2`  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  Intro
                THEN  ParallelOp  -2
                THEN  Fold  `mu`  (-1)
                THEN  ParallelLast)

---

Home Index