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