Step
*
2
2
2
1
1
1
1
1
2
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 ∈ ℤ
17. ∀a,b:ℕN. (f a < f b ⇒ g (f a) (f b) < 2)
18. ∃i:ℕ2
∃f@0:ℕ[s 0; s 1][i] ⟶ ℕN
(Inj(ℕ[s 0; s 1][i];ℕN;f@0)
∧ (∀a,b:ℕ[s 0; s 1][i].
(f@0 a < f@0 b
⇒ (((λa,b. if f a <z f b then g (f a) (f b) if f b <z f a then g (f b) (f a) else 0 fi ) (f@0 a) (f@0 b))
= i
∈ ℤ))))
⊢ ∃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
{ ParallelLast }
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)
18. i1 : ℕ2
19. ∃f@0:ℕ[s 0; s 1][i1] ⟶ ℕN
(Inj(ℕ[s 0; s 1][i1];ℕN;f@0)
∧ (∀a,b:ℕ[s 0; s 1][i1].
(f@0 a < f@0 b
⇒ (((λa,b. if f a <z f b then g (f a) (f b) if f b <z f a then g (f b) (f a) else 0 fi ) (f@0 a) (f@0 b))
= i1
∈ ℤ))))
⊢ ∃f:ℕs i1 ⟶ ℕM. (Inj(ℕs i1;ℕM;f) ∧ (∀a,b:ℕs i1. (f a < f b ⇒ ((g (f a) (f b)) = i1 ∈ ℤ))))
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
17. \mforall{}a,b:\mBbbN{}N. (f a < f b {}\mRightarrow{} g (f a) (f b) < 2)
18. \mexists{}i:\mBbbN{}2
\mexists{}f@0:\mBbbN{}[s 0; s 1][i] {}\mrightarrow{} \mBbbN{}N
(Inj(\mBbbN{}[s 0; s 1][i];\mBbbN{}N;f@0)
\mwedge{} (\mforall{}a,b:\mBbbN{}[s 0; s 1][i].
(f@0 a < f@0 b
{}\mRightarrow{} (((\mlambda{}a,b. if f a <z f b then g (f a) (f b) if f b <z f a then g (f b) (f a) else 0 fi )\000C
(f@0 a)
(f@0 b))
= i))))
\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:
ParallelLast
Home
Index