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

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))
By:
Analyze -2
THEN
Try Trivial
THEN
ParallelOp -1
THEN
ExRepD
THEN
InstConcl [i+1]
THEN
Obvious
Generated subgoals:
None
About: