(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
1
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). [u / v][i] = a-1)
u < a-1
By:
SupposeNot
THEN
Analyze -2
THEN
InstConcl [0]
THEN
Reduce 0
Generated subgoals:
None
About:
(99steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
(
i:
v 
u < a-1