---

Step * 1 1 of Lemma mu-wf2


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 : ℕ
5. P[n]
⊢ ↑isl(d n)
BY
{ TACTIC:((GenConclTerm ⌜d n⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}[f:\{0...\}  {}\mrightarrow{}  (Top  +  Top)].  mu-ge(f;0)  \mmember{}  \{0...\}  supposing  \mexists{}m:\{0...\}.  (\muparrow{}isl(f  m))
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  d  :  \mforall{}n:\mBbbN{}.  Dec(P[n])
4.  n  :  \mBbbN{}
5.  P[n]
\mvdash{}  \muparrow{}isl(d  n)


By

---

Latex:
TACTIC:((GenConclTerm  \mkleeneopen{}d  n\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index