(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
Ramsey
1
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 < 1
6.
L:
List
7.
0 < ||L||
8.
sum(L[i]-1 | i < ||L||)+1- > L^1
9.
0 < sum(L[i]-1 | i < ||L||)+1
1- > L^1
By:
BLemma'
Thm*
k:
, L:
List, r1,r2:
. r1
r2
r1- > L^k
r2- > L^k
Generated subgoals:
None
About:
(41steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
(
L:
List. 0 < ||L|| (
r:
. r- > L^k-1))
List
0 < sum(L[i]-1 | i < ||L||)+1
1- > L^1
k:, L: List, r1,r2:. r1
r2 r1- > L^k r2- > L^k