Step
*
2
2
2
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
⊢ ∃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
{ ((InstHyp [⌜λa,b. if g a b <z 2 then 0 else (g a b) - 1 fi ⌝] (-2)⋅ THENA Auto)
THEN D -1
THEN (SplitOnHypITE -1 THENA Auto)
THEN Reduce -2) }
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
(Inj(ℕN;ℕM;f) ∧ (∀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 ∈ ℤ))))
14. 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 ∈ ℤ))))
2
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:ℕs (i + 1) ⟶ ℕM
(Inj(ℕs (i + 1);ℕM;f)
∧ (∀a,b:ℕs (i + 1). (f a < f b ⇒ (if g (f a) (f b) <z 2 then 0 else (g (f a) (f b)) - 1 fi = i ∈ ℤ))))
14. ¬(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 ∈ ℤ))))
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
\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:
((InstHyp [\mkleeneopen{}\mlambda{}a,b. if g a b <z 2 then 0 else (g a b) - 1 fi \mkleeneclose{}] (-2)\mcdot{} THENA Auto)
THEN D -1
THEN (SplitOnHypITE -1 THENA Auto)
THEN Reduce -2)
Home
Index