---

Step * 1 1 of Lemma weakly-infinite-cases


1. S : ℕ ⟶ ℙ
2. w∃∞x.S[x]
3. A : ℕ ⟶ ℙ
4. ∀n:ℕ. (A[n] ⇒ S[n])
5. ¬w∃∞n.A[n]
6. n : ℕ
7. ∀q:ℕ. (¬(n < q ∧ A[q]))
8. n1 : ℕ
⊢ ¬¬(∃q:ℕ. (n1 < q ∧ S[q] ∧ (¬A[q])))
BY
{ ((Assert ∃m:ℕ. ((n ≤ m) ∧ (n1 ≤ m)) BY ( Decide ⌜n ≤ n1⌝⋅ THEN Auto)) THEN D (-1)⋅) }

1
1. S : ℕ ⟶ ℙ
2. w∃∞x.S[x]
3. A : ℕ ⟶ ℙ
4. ∀n:ℕ. (A[n] ⇒ S[n])
5. ¬w∃∞n.A[n]
6. n : ℕ
7. ∀q:ℕ. (¬(n < q ∧ A[q]))
8. n1 : ℕ
9. m : ℕ
10. (n ≤ m) ∧ (n1 ≤ m)
⊢ ¬¬(∃q:ℕ. (n1 < q ∧ S[q] ∧ (¬A[q])))

---

Latex:

---

Latex:

1.  S  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  w\mexists{}\minfty{}x.S[x]
3.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  S[n])
5.  \mneg{}w\mexists{}\minfty{}n.A[n]
6.  n  :  \mBbbN{}
7.  \mforall{}q:\mBbbN{}.  (\mneg{}(n  <  q  \mwedge{}  A[q]))
8.  n1  :  \mBbbN{}
\mvdash{}  \mneg{}\mneg{}(\mexists{}q:\mBbbN{}.  (n1  <  q  \mwedge{}  S[q]  \mwedge{}  (\mneg{}A[q])))


By

---

Latex:
((Assert  \mexists{}m:\mBbbN{}.  ((n  \mleq{}  m)  \mwedge{}  (n1  \mleq{}  m))  BY  (  Decide  \mkleeneopen{}n  \mleq{}  n1\mkleeneclose{}\mcdot{}  THEN  Auto))  THEN  D  (-1)\mcdot{})

---

Home Index