---

Step * of Lemma weakly-infinite-cases

∀[S:ℕ ⟶ ℙ]. (w∃∞x.S[x] ⇒ (∀[A:ℕ ⟶ ℙ]. ((∀n:ℕ. (A[n] ⇒ S[n])) ⇒ (¬¬(w∃∞n.A[n] ∨ w∃∞n.S[n] ∧ (¬A[n]))))))
BY
{ (Auto
   THEN DistinguishCases ⌜w∃∞n.A[n]⌝⋅
   THEN Auto
   THEN (NotAllElim (-1) THENA Auto)
   THEN (SupposeMore (-1) THENA Auto)
   THEN (RWO "not_over_exists" (-1) THENA Auto)) }

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]))
⊢ ¬¬(w∃∞n.A[n] ∨ w∃∞n.S[n] ∧ (¬A[n]))

---

Latex:

---

Latex:
\mforall{}[S:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}]
    (w\mexists{}\minfty{}x.S[x]  {}\mRightarrow{}  (\mforall{}[A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  S[n]))  {}\mRightarrow{}  (\mneg{}\mneg{}(w\mexists{}\minfty{}n.A[n]  \mvee{}  w\mexists{}\minfty{}n.S[n]  \mwedge{}  (\mneg{}A[n]))))))


By

---

Latex:
(Auto
  THEN  DistinguishCases  \mkleeneopen{}w\mexists{}\minfty{}n.A[n]\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (NotAllElim  (-1)  THENA  Auto)
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  (RWO  "not\_over\_exists"  (-1)  THENA  Auto))

---

Home Index