Nuprl - Proof: Ramsey-recursion 1 2 2 2

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

At: Ramsey-recursion 1 2 2 2

1. r:
2. k:
3. L: List
4. R: List
5. 2k
6. ||R|| = ||L||
7. i:||L||. 0 < L[i] R[i]- > L[i--]^k
8. r- > R^k-1
9. n:
10. r+1n
11. G: {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||
12. c: ||R||
13. f: R[c](n-1)
14. increasing(f;R[c])
15. s:R[c] List. ||s|| = k-1 (x,y:||s||. x < y s[x] < s[y]) G(map(f;s) @ [(n-1)]) = c
16. 0 < L[c]
17. c1: ||L||
18. f1: L[c1]n
19. increasing(f1;L[c1])
20. s: L[c1] List
21. ||s|| = k
22. x,y:||s||. x < y s[x] < s[y]

map(f1;s) {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }

By: Analyze THEN Try (Complete Auto)

Generated subgoal:

1 ||map(f1;s)|| = k & (x,y:||map(f1;s)||. x < y map(f1;s)[x] < map(f1;s)[y]) 2 steps

About:

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