Proof of Nuprl Lemma : finite-Ramsey1

Step * 2 2 2 1 1 1 1 1 1 of Lemma finite-Ramsey1

.....wf.....
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)

⊢ λ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  ∈ ℕN ⟶ ℕN ⟶ ℕ2

BY
{ (RepeatFor 2 ((MemCD THENA Auto)) THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase.....
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:ℕN ⟶ ℕN ⟶ ℕc. ∃i:ℕc. ∃f:ℕs i ⟶ ℕN. (Inj(ℕs i;ℕN;f) ∧ (∀a,b:ℕs i.  (f a < f b

Latex:

Latex:
.....wf..... 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) \mvdash{} \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 \mmember{} \mBbbN{}N {}\mrightarrow{} \mBbbN{}N {}\mrightarrow{} \mBbbN{}\000C2 By Latex: (RepeatFor 2 ((MemCD THENA Auto)) THEN (SplitOnConclITE THENA Auto)) Home Index