2. P : L:(T List)
(||L||-1)
3. m : (T List)
4.
L:T List, i:(||L||-1).
4. P(L,i)
P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)
5. L : T List
6. 0<||L||
7. f : (T List)
(T List)
8.
L:T List.
8. f(L)
8. =
8. if null(L)
L
8. else let i = search(||L||-1;P(L)) in if i=
0 L else swap(L;i-1;i) fi fi
9.
x:T List. 
n:. f(f^n(x)) = f^n(x)
10. n :
11. 0<n
12. L guarded_permutation(T;
L,i. P(L,i)) (f^n-1(L))
13. Trans x,y:T List. x guarded_permutation(T;
L,i. P(L,i)) y
14. L2 : T List
15. f^n-1(L) = L2
16. L2 guarded_permutation(T;
L,i. P(L,i)) L2
17.
L2 = nil
18. 0<||L2||
19.
search(||L2||-1;P(L2)) = 0
L2
((L1,L2. i:(||L1||-1).
(P(L1,i) & L2 = swap(L1;i;i+1) 
T List)^*) swap(L2;search(||L2||-1;P(L2))
(P(L1,i) & L2 = swap(L1;i;i+1) T List)^*) -1;search(||L2||-1;P(L2)))
