---

Step * of Lemma better-not-not-Ramsey

∀[R:ℕ ⟶ ℕ ⟶ ℙ]. (¬(∀[s:StrictInc]. ⇃(∃n,m,p,q:ℕ. ((n < m ∧ R[s n;s m]) ∧ p < q ∧ (¬R[s p;s q])))))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN InstLemma `b-almost-full-intersection-lemma` [⌜λ2n m.R[n;m]⌝;⌜λ2n m.¬R[n;m]⌝]⋅
   THEN Auto
   THEN Try ((Unfold `b-almost-full` 0
              THEN ParallelLast
              THEN MoveToConcl (-1)
              THEN BLemma `implies-quotient-true`
              THEN Auto))) }

1
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. ∀[s:StrictInc]. ⇃(∃n,m,p,q:ℕ. ((n < m ∧ R[s n;s m]) ∧ p < q ∧ (¬R[s p;s q])))
3. ∀s:StrictInc. ⇃(∃m:ℕ. ∃n,p:{m + 1...}. (R[s m;s n] ∧ (¬R[s m;s p])))
⊢ False

---

Latex:

---

Latex:
\mforall{}[R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (\mneg{}(\mforall{}[s:StrictInc].  \00D9(\mexists{}n,m,p,q:\mBbbN{}.  ((n  <  m  \mwedge{}  R[s  n;s  m])  \mwedge{}  p  <  q  \mwedge{}  (\mneg{}R[s  p;s  q])))))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  InstLemma  `b-almost-full-intersection-lemma`  [\mkleeneopen{}\mlambda{}\msubtwo{}n  m.R[n;m]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n  m.\mneg{}R[n;m]\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((Unfold  `b-almost-full`  0
                        THEN  ParallelLast
                        THEN  MoveToConcl  (-1)
                        THEN  BLemma  `implies-quotient-true`
                        THEN  Auto)))

---

Home Index