At:
Ramsey-recursion
1
2
2
2
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]
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]
23.
x:
||s||
24.
y:
||s||
25.
x < y
f1(s[x]) < f1(s[y])
By:
FwdThru
Thm*
k:
, f:(
k

). increasing(f;k) 
(
x,y:
k. x < y 
f(x) < f(y))
[-7]
THEN
BackThru -1
THEN
EasyHyp
Generated subgoals:
None
About: