Nuprl - Proof: Ramsey-base-case 1 1 1 1 1 1

(30steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: Ramsey-base-case 1 1 1 1 1 1

1. L: List
2. n:
3. G: {s:(n List)| ||s|| = 1 & (x,y:||s||. x < y s[x] < s[y]) }||L||
4. c: ||L||
5. A: List
6. m:

m||A|| (x:||A||. A[x] < n & G([A[x]]) = c) (x,y:||A||. x < y A[x] > A[y]) (f:(mn). increasing(f;m) & (s:m. G([(f(s))]) = c))

By: Auto

Generated subgoals:

1 7. m||A||
8. x:||A||. A[x] < n & G([A[x]]) = c
9. x,y:||A||. x < y A[x] > A[y]
f:(mn). increasing(f;m) & (s:m. G([(f(s))]) = c) 7 steps

2 7. m||A||
8. x: ||A||
9. A[x] < n
[A[x]] {s:(n List)| ||s|| = 1 & (x,y:||s||. x < y s[x] < s[y]) } 2 steps

About:

(30steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc