is mentioned by

Thm* r,k:, L,R: List. 2k ||R|| = ||L|| (i:||L||. 0 < L[i] R[i]- > L[i--]^k) r- > R^k-1 r+1- > L^k	[Ramsey-recursion]
Thm* L: List, i,j:||L||. 0 < L[i] L[i--][j] = if j=i L[j]-1 else L[j] fi	[list-dec-select]
Thm* L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L||	[list-dec-length]
Thm* L: List, i:||L||. 0 < L[i] L[i--] List	[list-dec_wf]
Thm* L: List. sum(L[i]-1 | i < ||L||)+1- > L^1	[Ramsey-base-case]
Thm* k:, L: List. k-1- > L^k (i:||L||. L[i] < k)	[trivial-arrows]
Thm* n,k:, c:(nk). p:(k( List)). sum(||p(j)|| | j < k) = n & (j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x] < n & c((p(j))[x]) = j)	[finite-partition]
Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y	[connect]
Def path(the_graph;p) == 0 < ||p|| & (i:(||p||-1). p[i]-the_graph- > p[(i+1)])	[path]
Def L[i--] == mklist(||L||;j.if j=i L[j]-1 else L[j] fi)	[list-dec]
Def r- > L^k == n:. rn (G:({s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||). c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c))	[arrows]

In prior sections: list 1 mb basic mb list 1 mb list 2 graph 1 1

Try larger context: Graphs