(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
Ramsey
2
1
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)
i:
||L||. 2
L[i]
By:
Auto
THEN
SupposeNot
THEN
Analyze -3
THEN
InstConcl [i]
Generated subgoals:
None
About:
(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
(
L:
List. 0 < ||L|| (
r:
. r- > L^k-1))
k = 1
d1:. d1 < d (L: List. sum(L[i] | i < ||L||) = d1 
0 < ||L|| (r:. r- > L^k))
List
(i:||L||. L[i] < k)
i:||L||. 2
L[i]