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
10.
i:(||x||-1). P(x,i) P(swap(x;i;i+1),i) & m(swap(x;i;i+1))<m(x)
11. x = nil
f(x) = x m(f(x))
m(x) & (m(f(x)) = m(x) f(x) = x)
