(99steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
Ramsey-recursion
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.
s:
{s:(
(n-1) List)| ||s|| = k-1
& (
x,y:
||s||. x < y
s[x] < s[y]) }
(s @ [(n-1)])
{s:(
n List)| ||s|| = k
& (
x,y:
||s||. x < y
s[x] < s[y]) }
By:
Analyze -1
THEN
Analyze
THEN
Try (Complete Auto)
Generated subgoal:
1
12.
s:
(n-1) List
13.
||s|| = k-1
& (
x,y:
||s||. x < y
s[x] < s[y])
||s @ [(n-1)]|| = k
& (
x,y:
||s @ [(n-1)]||. x < y
(s @ [(n-1)])[x] < (s @ [(n-1)])[y])
5
steps
About:
(99steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc