---

Step * 1 1 1 of Lemma mu-property2


1. ∀[P:{0...} ⟶ ℙ]. ∀d:∀n:{0...}. Dec(P[n]). {P[mu-ge(d;0)] ∧ (∀[i:ℕmu-ge(d;0)]. (¬P[i]))} supposing ∃m:{0...}. P[m]
2. P : ℕ ⟶ ℙ
3. ∀d:∀n:{0...}. Dec(P[n]). {P[mu-ge(d;0)] ∧ (∀[i:ℕmu-ge(d;0)]. (¬P[i]))} supposing ∃m:{0...}. P[m]
4. d : ∀n:ℕ. Dec(P[n])
5. n : ℕ
6. P[n]
7. P[mu-ge(d;0)]
8. ∀[i:ℕmu-ge(d;0)]. (¬P[i])
⊢ ↑isl(d n)
BY
{ TACTIC:((GenConclTerm ⌜d n⌝⋅ THEN Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}[P:\{0...\}  {}\mrightarrow{}  \mBbbP{}]
          \mforall{}d:\mforall{}n:\{0...\}.  Dec(P[n])
              \{P[mu-ge(d;0)]  \mwedge{}  (\mforall{}[i:\mBbbN{}mu-ge(d;0)].  (\mneg{}P[i]))\}  supposing  \mexists{}m:\{0...\}.  P[m]
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}d:\mforall{}n:\{0...\}.  Dec(P[n]).  \{P[mu-ge(d;0)]  \mwedge{}  (\mforall{}[i:\mBbbN{}mu-ge(d;0)].  (\mneg{}P[i]))\}  supposing  \mexists{}m:\{0...\}.  P[m]
4.  d  :  \mforall{}n:\mBbbN{}.  Dec(P[n])
5.  n  :  \mBbbN{}
6.  P[n]
7.  P[mu-ge(d;0)]
8.  \mforall{}[i:\mBbbN{}mu-ge(d;0)].  (\mneg{}P[i])
\mvdash{}  \muparrow{}isl(d  n)


By

---

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

---

Home Index