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