L:T List, P:(T
T
), n:
(||L||-1).
Thm* count(x < y in swap(L;n;n+1) | P(x,y))
Thm* =
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)])
-1 else 0 fi+if P(L[(n+1)]
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)])
-1 else 0 fi+if P,L[n])
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)])
-1 else 0 fi+if 1
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)])
-1 else 0 fi+else 0 fiL:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| 
k:, i,j:k. Bij(k; k; (i, j))n,m:, f:(nm), p:(nn), q:(mm).
Thm* Bij(
n; n; p)
Thm*
Thm* Bij(
m; m; q)
Thm*
Thm* sum(f(p(x),q(y)) | x < n; y < m) = sum(f(x,y) | x < n; y < m)
n,m:, f,g:(nm), d:.
Thm* sum(f(x,y)-g(x,y) | x < n; y < m) = d
Thm*
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)+d
n,m:, f:(nm), x1,x2:n, y1,y2:m.
Thm*
x1 = x2 
y1 = y2
Thm*
Thm* (
x:n, y:m. (x = x1 & y = y1) (x = x2 & y = y2) f(x,y) = 0)
Thm*
Thm* sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2)
n,m:, f,g:(nm).
Thm* (
x:n, y:m. f(x,y) = g(x,y))
Thm*
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)
L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))]k:, x,y,i:k. (y, x)((y, x)(i)) = i