---

Step * 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. [%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)
BY
{ TACTIC:(InstLemma `mu-ge_wf2` [⌜0⌝;⌜d⌝]⋅ THENA Auto) }

1
.....antecedent..... 
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:ℕ. P[n]
6. P[mu-ge(d;0)]
7. ∀[i:ℕmu-ge(d;0)]. (¬P[i])
⊢ ∃m:{0...}. (↑isl(d m))

2
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])
8. mu-ge(d;0) ∈ {0...}
⊢ ∀i:ℕ. ¬P[i] supposing i < mu-ge(d;0)

---

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.  [\%5]  :  \mexists{}n:\mBbbN{}.  P[n]
6.  P[mu-ge(d;0)]
7.  \mforall{}[i:\mBbbN{}mu-ge(d;0)].  (\mneg{}P[i])
\mvdash{}  \mforall{}i:\mBbbN{}.  \mneg{}P[i]  supposing  i  <  mu-ge(d;0)


By

---

Latex:
TACTIC:(InstLemma  `mu-ge\_wf2`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index