L:T List, P:(T
T
).
Thm* (
x,y:T. P(x,y) 
P(y,x))
Thm*
Thm* (
L':T List.
Thm* ((L guarded_permutation(T;
L,i. P(L[i],L[(i+1)])) L')
Thm* (& (
i:
(||L'||-1). P(L'[i],L'[(i+1)])))L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| 
P:(L:(T List)(||L||-1)), m:((T List)).
Thm* (
L:T List, i:(||L||-1).
Thm* (P(L,i)
P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L))
Thm*
Thm* (
L:T List.
Thm* (
L':T List.
Thm* ((L guarded_permutation(T;
L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i)))L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))]L:T List, P:(TT), 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 fi