(99steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
Ramsey-recursion
1
2
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]
c:
||L||, f:(
L[c]
n). increasing(f;L[c]) & (
s:
L[c] List. ||s|| = k
(
x,y:
||s||. x < y
s[x] < s[y])
G(map(f;s)) = c)
By:
InstConcl [c]
Generated subgoals:
1
f:(
L[c]
n). increasing(f;L[c]) & (
s:
L[c] List. ||s|| = k
(
x,y:
||s||. x < y
s[x] < s[y])
G(map(f;s)) = c)
9
steps
 
2
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]
map(f1;s)
{s:(
n List)| ||s|| = k
& (
x,y:
||s||. x < y
s[x] < s[y]) }
3
steps
About:
(99steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc