At:
Ramsey-recursion
1
2
2
1
1
1
1.
r:
2.
k:
3.
L:
List
4.
R:
List
5.
2
k
6.
||R|| = ||L||
7.
i:
||L||. 0 < L[i] 
R[i]- > L[i--]^k
8.
r- > R^k-1
9.
n:
10.
r+1
n
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]
increasing(
x.
;0)
By:
Analyze 0
THEN
Reduce 0
THEN
Analyze -1
Generated subgoals:
None
About: