(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
Ramsey
2
1
2
2
2
2
2
1
1.
k:
2.
0 < k
3.
0 < k-1
(
L:
List. 0 < ||L||
(
r:
. r- > L^k-1))
4.
k = 1
5.
0 < k
6.
d:
7.
d1:
. d1 < d
(
L:
List. sum(L[i] | i < ||L||) = d1
0 < ||L||
(
r:
. r- > L^k))
8.
L:
List
9.
sum(L[i] | i < ||L||) = d
10.
0 < ||L||
11.
(
i:
||L||. L[i] < k)
12.
i:
||L||. 2
L[i]
13.
L:
List. sum(L[i] | i < ||L||) = d-1
0 < ||L||
(
r:
. r- > L^k)
14.
i:
||L||.
r:
. r- > L[i--]^k
15.
R:
List
16.
||R|| = ||L||
17.
i:
||L||. 0 < L[i]
R[i]- > L[i--]^k
18.
r:
19.
r- > R^k-1
r:
. r- > L^k
By:
Inst
Thm*
Ramsey-recursion [r;k;L;R]
Generated subgoal:
1
20.
r+1- > L^k
r:
. r- > L^k
1
step
About:
(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc