| Rank | Theorem | Name |
| 6 | Thm*  k:  , L: List. 0 < ||L||   ( r:. r- > L^k) | [Ramsey] |
| cites |
| 4 | Thm* L: List. sum(L[i]-1 | i < ||L||)+1- > L^1 | [Ramsey-base-case] |
| 0 | Thm* k:, L: List, r1,r2: . r1 r2 r1- > L^k r2- > L^k | [arrows-monotone1] |
| 5 | Thm* k:, L: List. k-1- > L^k  (i:||L||. L[i] < k) | [trivial-arrows] |
| 0 | Thm* k,b:, f:(k  ). (x:k. bf(x)) b ksum(f(x) | x < k) | [sum_lower_bound] |
| 1 | Thm* n:, f,g:(n), d:. sum(f(x)-g(x) | x < n) = d sum(f(x) | x < n) = sum(g(x) | x < n)+d | [sum_difference] |
| 2 | Thm* n:, f:(n), m:n. (x:n.  x = m f(x) = 0) sum(f(x) | x < n) = f(m) | [singleton_support_sum] |
| 3 | 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] |
| 0 | Thm* n:, f:(n). (x:n. 0f(x)) 0sum(f(x) | x < n) | [non_neg_sum] |
| 2 | Thm* L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L||  | [list-dec-length] |
| 2 | Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i) | [mklist_select] |
| 1 | Thm* n:, f:(nT). ||mklist(n;f)|| = n | [mklist_length] |
| 4 | 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] |