(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
Ramsey
1
1.
k:
2.
0 < k
3.
0 < k-1
(
L:
List. 0 < ||L||
(
r:
. r- > L^k-1))
4.
k = 1
5.
0 < 1
6.
L:
List
7.
0 < ||L||
r:
. r- > L^1
By:
Inst
Thm*
L:
List. sum(L[i]-1 | i < ||L||)+1- > L^1 [L]
Generated subgoal:
1
8.
sum(L[i]-1 | i < ||L||)+1- > L^1
r:
. r- > L^1
4
steps
About:
(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
r:
. r- > L^1
(
L: List. 0 < ||L|| (r:. r- > L^k-1))
List
r:. r- > L^1
L: List. sum(L[i]-1 | i < ||L||)+1- > L^1
[L]
r:. r- > L^1
