At:
Ramsey-recursion
1
2
2
1
1
3
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.
f1:
0

n
18.
increasing(f1;0)
19.
s:
0 List
20.
||s|| = k
21.
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:
Assert False
Generated subgoal:
1 | False | 2 steps |
About: