At:
Ramsey-base-case
1
2
1
2
1.
L: 
List
2.
n:
3.
sum(L[i]-1 | i < ||L||)+1
n
4.
G: {s:(n List)| ||s|| = 1 
& (
x,y:||s||. x < y 
s[x] < s[y]) }
||L||
5.
c: ||L||
6.
f: L[c]n
7.
increasing(f;L[c]) & (s:L[c]. G([(f(s))]) = c)
8.
f1: L[c]n
9.
increasing(f1;L[c])
10.
s: L[c] List
11.
||s|| = 1
12.
x,y:||s||. x < y s[x] < s[y]
map(f1;s) {s:(n List)| ||s|| = 1 & (x,y:||s||. x < y s[x] < s[y]) }
By:
Analyze
THEN
Try (Complete Auto)
THEN
Analyze -3
THEN
All Reduce
THEN
Try (Complete Auto)
Generated subgoals:
None
About:
