---

Step * of Lemma not-not-Ramsey

∀[R:ℕ ⟶ ℕ ⟶ ℙ]. (¬(∀s:StrictInc. ∃n:ℕ. (¬homogeneous(R;n;s))))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (InstLemma `monotone-bar-induction-strict` [⌜λ2n s.¬homogeneous(R;n;s)⌝;⌜λ2n s.¬weakly-safe-seq(R;n;s)⌝]⋅
         THENA Auto
         )) }

1
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. ∀s:StrictInc. ∃n:ℕ. (¬homogeneous(R;n;s))
3. n : ℕ
4. s : {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} 
5. ¬homogeneous(R;n;s)
6. m : ℕ
7. strictly-increasing-seq(n + 1;s.m@n)
⊢ ¬homogeneous(R;n + 1;s.m@n)

2
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. ∀s:StrictInc. ∃n:ℕ. (¬homogeneous(R;n;s))
3. n : ℕ
4. s : {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} 
5. ¬homogeneous(R;n;s)
⊢ ↓¬weakly-safe-seq(R;n;s)

3
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. ∀s:StrictInc. ∃n:ℕ. (¬homogeneous(R;n;s))
3. n : ℕ
4. s : {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} 
5. ∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ (↓¬weakly-safe-seq(R;n + 1;s.m@n)))
⊢ ↓¬weakly-safe-seq(R;n;s)

4
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. ∀s:StrictInc. ∃n:ℕ. (¬homogeneous(R;n;s))
3. ↓¬weakly-safe-seq(R;0;λx.⊥)
⊢ False

---

Latex:

---

Latex:
\mforall{}[R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (\mneg{}(\mforall{}s:StrictInc.  \mexists{}n:\mBbbN{}.  (\mneg{}homogeneous(R;n;s))))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (InstLemma  `monotone-bar-induction-strict`  [\mkleeneopen{}\mlambda{}\msubtwo{}n  s.\mneg{}homogeneous(R;n;s)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}n  s.\mneg{}weakly-safe-seq(R;n;s)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index