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||
  L':T List. 
  (L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i))

By:	Assert (f:((T List)(T List)).  (L:T List.  (f(L) (= (if null(L) L (else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi)

1	f:((T List)(T List)).    L:T List.    f(L)   =   if null(L) L   else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi	4 steps
2	7. f:((T List)(T List)).  7. L:T List.  7. f(L) 7. = 7. if null(L) L 7. else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi   L':T List.    (L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i))	56 steps

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