n,k:
, c:(n
k).
Thm*
p:(k( List)).
Thm* sum(||p(j)|| | j < k) = n
Thm* & (
j:k, x,y:||p(j)||. x<y 
(p(j))[x]>(p(j))[y])
Thm* & (
j:k, x:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)n:, a:
. sum(a | x < n) = a
nn:, f,g:(n).
Thm* (
i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n)k:, f,g:(k), p:(k
).
Thm* sum(if p(i)
f(i)+g(i) else f(i) fi | i < k)
Thm* =
Thm* sum(f(i) | i < k)+sum(if p(i)
g(i) else 0 fi | i < k)n:, f:(n), m:n.
Thm* (
x:n. 
x = m f(x) = 0) sum(f(x) | x < n) = f(m)a:T, as:T List, i:. 0<i i
||as|| [a / as][i] = as[(i-1)]