1. T : Type
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
  L2 
  guarded_permutation(T;L,i. P(L,i)) if null(L2) L2
  guarded_permutation(T;L,i. P(L,i)) else let i = search(||L2||-1;P(L2)) in 
  guarded_permutation(T;L,i. P(L,i)) else if i=0 L2
  guarded_permutation(T;L,i. P(L,i)) else else swap(L2;i-1;i) fi fi

By:	Assert (L2 guarded_permutation(T;L,i. P(L,i)) L2)

1	L2 guarded_permutation(T;L,i. P(L,i)) L2	1 step
2	16. L2 guarded_permutation(T;L,i. P(L,i)) L2   L2    guarded_permutation(T;L,i. P(L,i)) if null(L2) L2   guarded_permutation(T;L,i. P(L,i)) else let i = search(||L2||-1;P(L2)) in    guarded_permutation(T;L,i. P(L,i)) else if i=0 L2   guarded_permutation(T;L,i. P(L,i)) else else swap(L2;i-1;i) fi fi	6 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html