r,k:
, L,R: List. 2
k 
||R|| = ||L|| 
(i:||L||. 0 < L[i] R[i]- > L[i--]^k) r- > R^k-1 r+1- > L^kL: List, i,j:||L||. 0 < L[i] L[i--][j] = if j=
i
L[j]-1 else L[j] fiL: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L|| 
j.if j=i L[j]-1 else L[j] fi)
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] |
Try larger context:
Graphs