| Rank | Theorem | Name |
| 3 | Thm*  n,k: , c:(n  k).  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] |
| cites |
| 0 | Thm* n:, a: . sum(a | x < n) = a n | [sum_constant] |
| 0 | Thm* n:, f,g:(n). (i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n) | [sum_functionality] |
| 0 | Thm* k:, f,g:(k), p:(k ). sum(if p(i) f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k) | [sum-ite] |
| 2 | Thm* n:, f:(n), m:n. (x:n.  x = m f(x) = 0) sum(f(x) | x < n) = f(m) | [singleton_support_sum] |
| 0 | Thm* a:T, as:T List, i:. 0 < i i ||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |