(99steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
Ramsey-recursion
1
2
1
1
2
1
1
1
1
3
2
2
1
2
1
1
3
1.
a:
2.
s:
a List
3.
u:
a
4.
v:
a List
5.
(
i:
||v||. v[i] = a-1)
v
(a-1) List
6.
i:
(||v||+1)
i < ||[u / v]||
By:
Reduce 0
Generated subgoals:
None
About:
(99steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
(
i:
v 
i < ||[u / v]||