Step
*
2
2
2
1
1
1
1
of Lemma
finite-Ramsey1
1. c : ℕ
2. ∀c:ℕc. ∀s:ℕc ⟶ ℕ.
∃N:ℕ+
∀g:ℕN ⟶ ℕN ⟶ ℕc. ∃i:ℕc. ∃f:ℕs i ⟶ ℕN. (Inj(ℕs i;ℕN;f) ∧ (∀a,b:ℕs i. (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
3. s : ℕc ⟶ ℕ
4. ¬(c = 0 ∈ ℤ)
5. ¬(c = 1 ∈ ℤ)
6. ¬(c = 2 ∈ ℤ)
7. N : ℕ+
8. ∀g:ℕN ⟶ ℕN ⟶ ℕ2
∃i:ℕ2
∃f:ℕ[s 0; s 1][i] ⟶ ℕN
(Inj(ℕ[s 0; s 1][i];ℕN;f) ∧ (∀a,b:ℕ[s 0; s 1][i]. (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
9. M : ℕ+
10. ∀g:ℕM ⟶ ℕM ⟶ ℕc - 1
∃i:ℕc - 1
∃f:ℕif (i =z 0) then N else s (i + 1) fi ⟶ ℕM
(Inj(ℕif (i =z 0) then N else s (i + 1) fi ;ℕM;f)
∧ (∀a,b:ℕif (i =z 0) then N else s (i + 1) fi . (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
11. g : ℕM ⟶ ℕM ⟶ ℕc
12. i : ℕc - 1
13. f : ℕN ⟶ ℕM
14. Inj(ℕN;ℕM;f)
15. ∀a,b:ℕN. (f a < f b ⇒ (if g (f a) (f b) <z 2 then 0 else (g (f a) (f b)) - 1 fi = i ∈ ℤ))
16. i = 0 ∈ ℤ
⊢ ∃i:ℕc. ∃f:ℕs i ⟶ ℕM. (Inj(ℕs i;ℕM;f) ∧ (∀a,b:ℕs i. (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
BY
{ (Assert ∀a,b:ℕN. (f a < f b ⇒ g (f a) (f b) < 2) BY
(ParallelOp -2 THEN RepeatFor 2 (ParallelLast) THEN SplitOnHypITE -1 THEN Auto)) }
1
1. c : ℕ
2. ∀c:ℕc. ∀s:ℕc ⟶ ℕ.
∃N:ℕ+
∀g:ℕN ⟶ ℕN ⟶ ℕc. ∃i:ℕc. ∃f:ℕs i ⟶ ℕN. (Inj(ℕs i;ℕN;f) ∧ (∀a,b:ℕs i. (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
3. s : ℕc ⟶ ℕ
4. ¬(c = 0 ∈ ℤ)
5. ¬(c = 1 ∈ ℤ)
6. ¬(c = 2 ∈ ℤ)
7. N : ℕ+
8. ∀g:ℕN ⟶ ℕN ⟶ ℕ2
∃i:ℕ2
∃f:ℕ[s 0; s 1][i] ⟶ ℕN
(Inj(ℕ[s 0; s 1][i];ℕN;f) ∧ (∀a,b:ℕ[s 0; s 1][i]. (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
9. M : ℕ+
10. ∀g:ℕM ⟶ ℕM ⟶ ℕc - 1
∃i:ℕc - 1
∃f:ℕif (i =z 0) then N else s (i + 1) fi ⟶ ℕM
(Inj(ℕif (i =z 0) then N else s (i + 1) fi ;ℕM;f)
∧ (∀a,b:ℕif (i =z 0) then N else s (i + 1) fi . (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
11. g : ℕM ⟶ ℕM ⟶ ℕc
12. i : ℕc - 1
13. f : ℕN ⟶ ℕM
14. Inj(ℕN;ℕM;f)
15. ∀a,b:ℕN. (f a < f b ⇒ (if g (f a) (f b) <z 2 then 0 else (g (f a) (f b)) - 1 fi = i ∈ ℤ))
16. i = 0 ∈ ℤ
17. ∀a,b:ℕN. (f a < f b ⇒ g (f a) (f b) < 2)
⊢ ∃i:ℕc. ∃f:ℕs i ⟶ ℕM. (Inj(ℕs i;ℕM;f) ∧ (∀a,b:ℕs i. (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
Latex:
Latex:
1. c : \mBbbN{}
2. \mforall{}c:\mBbbN{}c. \mforall{}s:\mBbbN{}c {}\mrightarrow{} \mBbbN{}.
\mexists{}N:\mBbbN{}\msupplus{}
\mforall{}g:\mBbbN{}N {}\mrightarrow{} \mBbbN{}N {}\mrightarrow{} \mBbbN{}c
\mexists{}i:\mBbbN{}c. \mexists{}f:\mBbbN{}s i {}\mrightarrow{} \mBbbN{}N. (Inj(\mBbbN{}s i;\mBbbN{}N;f) \mwedge{} (\mforall{}a,b:\mBbbN{}s i. (f a < f b {}\mRightarrow{} ((g (f a) (f b)) = i))))
3. s : \mBbbN{}c {}\mrightarrow{} \mBbbN{}
4. \mneg{}(c = 0)
5. \mneg{}(c = 1)
6. \mneg{}(c = 2)
7. N : \mBbbN{}\msupplus{}
8. \mforall{}g:\mBbbN{}N {}\mrightarrow{} \mBbbN{}N {}\mrightarrow{} \mBbbN{}2
\mexists{}i:\mBbbN{}2
\mexists{}f:\mBbbN{}[s 0; s 1][i] {}\mrightarrow{} \mBbbN{}N
(Inj(\mBbbN{}[s 0; s 1][i];\mBbbN{}N;f) \mwedge{} (\mforall{}a,b:\mBbbN{}[s 0; s 1][i]. (f a < f b {}\mRightarrow{} ((g (f a) (f b)) = i))))
9. M : \mBbbN{}\msupplus{}
10. \mforall{}g:\mBbbN{}M {}\mrightarrow{} \mBbbN{}M {}\mrightarrow{} \mBbbN{}c - 1
\mexists{}i:\mBbbN{}c - 1
\mexists{}f:\mBbbN{}if (i =\msubz{} 0) then N else s (i + 1) fi {}\mrightarrow{} \mBbbN{}M
(Inj(\mBbbN{}if (i =\msubz{} 0) then N else s (i + 1) fi ;\mBbbN{}M;f)
\mwedge{} (\mforall{}a,b:\mBbbN{}if (i =\msubz{} 0) then N else s (i + 1) fi . (f a < f b {}\mRightarrow{} ((g (f a) (f b)) = i))))
11. g : \mBbbN{}M {}\mrightarrow{} \mBbbN{}M {}\mrightarrow{} \mBbbN{}c
12. i : \mBbbN{}c - 1
13. f : \mBbbN{}N {}\mrightarrow{} \mBbbN{}M
14. Inj(\mBbbN{}N;\mBbbN{}M;f)
15. \mforall{}a,b:\mBbbN{}N. (f a < f b {}\mRightarrow{} (if g (f a) (f b) <z 2 then 0 else (g (f a) (f b)) - 1 fi = i))
16. i = 0
\mvdash{} \mexists{}i:\mBbbN{}c. \mexists{}f:\mBbbN{}s i {}\mrightarrow{} \mBbbN{}M. (Inj(\mBbbN{}s i;\mBbbN{}M;f) \mwedge{} (\mforall{}a,b:\mBbbN{}s i. (f a < f b {}\mRightarrow{} ((g (f a) (f b)) = i))))
By
Latex:
(Assert \mforall{}a,b:\mBbbN{}N. (f a < f b {}\mRightarrow{} g (f a) (f b) < 2) BY
(ParallelOp -2 THEN RepeatFor 2 (ParallelLast) THEN SplitOnHypITE -1 THEN Auto))
Home
Index