Nuprl - Proof: Ramsey-recursion 1 2 1 1 2 1 1 1 1 3 2 2 1 2 2 1 1

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

At: Ramsey-recursion 1 2 1 1 2 1 1 1 1 3 2 2 1 2 2 1 1

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. R[c]- > L[c--]^k
18. (s. G(map(f;s))) {s:(R[c] List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L[c--]||
19. c@0: ||L[c--]||
20. f@0: (L[c]-1)R[c]
21. increasing(f@0;L[c]-1)
22. s:(L[c]-1) List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;map(f@0;s))) = c
23. increasing(f o f@0[L[c]-1:=n-1];L[c])
24. a:
25. L[c] = a

s:a List. (i:||s||. s[i] = a-1) (map(f o f@0[a-1:=n-1];s) ~ map(f;map(f@0;s)))

By: InductionOnList THEN Reduce 0 THEN Analyze 0 THEN Analyze

Generated subgoals:

1 26. s: a List
27. u: a
28. v: a List
29. (i:||v||. v[i] = a-1) (map(f o f@0[a-1:=n-1];v) ~ map(f;map(f@0;v)))
30. (i:(||v||+1). [u / v][i] = a-1)
(f o f@0[a-1:=n-1](u)) ~ (f(f@0(u))) 2 steps

2 26. s: a List
27. u: a
28. v: a List
29. (i:||v||. v[i] = a-1) (map(f o f@0[a-1:=n-1];v) ~ map(f;map(f@0;v)))
30. (i:(||v||+1). [u / v][i] = a-1)
map(f o f@0[a-1:=n-1];v) ~ map(f;map(f@0;v)) 1 step

About:

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

1	26. `s:` `a List` 27. `u:` `a` 28. `v:` `a List` 29. `(i:\|\|v\|\|. v[i] = a-1) (map(f o f@0[a-1:=n-1];v) ~ map(f;map(f@0;v)))` 30. `(i:(\|\|v\|\|+1). [u / v][i] = a-1)` `(f o f@0[a-1:=n-1](u)) ~ (f(f@0(u)))`	2 steps

2	26. `s:` `a List` 27. `u:` `a` 28. `v:` `a List` 29. `(i:\|\|v\|\|. v[i] = a-1) (map(f o f@0[a-1:=n-1];v) ~ map(f;map(f@0;v)))` 30. `(i:(\|\|v\|\|+1). [u / v][i] = a-1)` `map(f o f@0[a-1:=n-1];v) ~ map(f;map(f@0;v))`	1 step