---

Step * 1 1 2 of Lemma Ramsey-n-3


1. n : ℕ
2. N : ℕ+
3. g : ℕN ⟶ ℕN ⟶ ℕn
4. f : ℕ3 ⟶ ℕN
5. ∀a1,a2:ℕ3.  (((f a1) = (f a2) ∈ ℕN) ⇒ (a1 = a2 ∈ ℕ3))
6. ∀a,b,c,d:ℕ3.  (f a < f b ⇒ f c < f d ⇒ ((g (f a) (f b)) = (g (f c) (f d)) ∈ ℤ))
7. f 1 < f 0
8. f 0 < f 2
9. f 1 < f 2
⊢ ∃i,j,k:ℕN. (i < j ∧ j < k ∧ ((g i j) = (g i k) ∈ ℤ) ∧ ((g i k) = (g j k) ∈ ℤ))
BY
{ (InstConcl [⌜f 1⌝;⌜f 0⌝;⌜f 2⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  N  :  \mBbbN{}\msupplus{}
3.  g  :  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}n
4.  f  :  \mBbbN{}3  {}\mrightarrow{}  \mBbbN{}N
5.  \mforall{}a1,a2:\mBbbN{}3.    (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))
6.  \mforall{}a,b,c,d:\mBbbN{}3.    (f  a  <  f  b  {}\mRightarrow{}  f  c  <  f  d  {}\mRightarrow{}  ((g  (f  a)  (f  b))  =  (g  (f  c)  (f  d))))
7.  f  1  <  f  0
8.  f  0  <  f  2
9.  f  1  <  f  2
\mvdash{}  \mexists{}i,j,k:\mBbbN{}N.  (i  <  j  \mwedge{}  j  <  k  \mwedge{}  ((g  i  j)  =  (g  i  k))  \mwedge{}  ((g  i  k)  =  (g  j  k)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}f  1\mkleeneclose{};\mkleeneopen{}f  0\mkleeneclose{};\mkleeneopen{}f  2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index