---

Step * of Lemma mu-property2

∀[P:ℕ ⟶ ℙ]. ∀d:∀n:ℕ. Dec(P[n]). {P[mu(d)] ∧ (∀i:ℕ. ¬P[i] supposing i < mu(d))} supposing ∃n:ℕ. P[n]
BY
{ TACTIC:TACTIC:((InstLemma `mu-ge-property2` [⌜0⌝]⋅ THENA Auto)
                 THEN ParallelLast
                 THEN Unfold `mu` 0
                 THEN RepeatFor 4 (ParallelLast)) }

1
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. [%5] : ∃n:ℕ. P[n]
6. P[mu-ge(d;0)]
7. ∀[i:ℕmu-ge(d;0)]. (¬P[i])
⊢ ∀i:ℕ. ¬P[i] supposing i < mu-ge(d;0)

---

Latex:

---

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


By

---

Latex:
TACTIC:TACTIC:((InstLemma  `mu-ge-property2`  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  ParallelLast
                              THEN  Unfold  `mu`  0
                              THEN  RepeatFor  4  (ParallelLast))

---

Home Index