Step * 1 1 2 1 1 of Lemma better-not-not-Ramsey


1. : ℕ ⟶ ℕ ⟶ ℙ
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])))
4. ∀s:StrictInc. ∃m:ℕ. ∃n,p:{m 1...}. (R[s m;s n] ∧ R[s m;s p]))
5. StrictInc
6. : ℕ
7. {m 1...}
8. {m 1...}
9. R[s m;s n]
10. homogeneous(R;imax(imax(m;n 1);p 1);s)
⊢ R[s m;s p]
BY
(D -1 THEN (InstHyp [⌜m⌝;⌜n⌝;⌜p⌝(-1)⋅ THENA (Auto THEN RWW "imax_strict_ub" THEN Auto))) }

1
1. : ℕ ⟶ ℕ ⟶ ℙ
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])))
4. ∀s:StrictInc. ∃m:ℕ. ∃n,p:{m 1...}. (R[s m;s n] ∧ R[s m;s p]))
5. StrictInc
6. : ℕ
7. {m 1...}
8. {m 1...}
9. R[s m;s n]
10. strictly-increasing-seq(imax(imax(m;n 1);p 1);s)
11. ∀m@0,i,j:ℕimax(imax(m;n 1);p 1).  (m@0 <  m@0 <  (R (s m@0) (s i) ⇐⇒ (s m@0) (s j)))
12. (s m) (s n) ⇐⇒ (s m) (s p)
⊢ R[s m;s p]


Latex:


Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \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])))
3.  \mforall{}s:StrictInc.  \00D9(\mexists{}m:\mBbbN{}.  \mexists{}n,p:\{m  +  1...\}.  (R[s  m;s  n]  \mwedge{}  (\mneg{}R[s  m;s  p])))
4.  \mforall{}s:StrictInc.  \mexists{}m:\mBbbN{}.  \mexists{}n,p:\{m  +  1...\}.  (R[s  m;s  n]  \mwedge{}  (\mneg{}R[s  m;s  p]))
5.  s  :  StrictInc
6.  m  :  \mBbbN{}
7.  n  :  \{m  +  1...\}
8.  p  :  \{m  +  1...\}
9.  R[s  m;s  n]
10.  homogeneous(R;imax(imax(m;n  +  1);p  +  1);s)
\mvdash{}  R[s  m;s  p]


By


Latex:
(D  -1  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  RWW  "imax\_strict\_ub"  0  THEN  Auto)))




Home Index