1. T : Type
2. L : T List
3. P : TT
4. x,y:T. P(x,y)  P(y,x)
  L':T List. 
  (L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')
  & (i:(||L'||-1). P(L'[i],L'[(i+1)]))

By:	Inst Thm: partial sort exists [T;L,i. P(L[i],L[(i+1)]);L.count(x < y in L | P(x,y))] THEN All Reduce

1	5. L1 : T List 6. i : (||L1||-1) 7. P(L1[i],L1[(i+1)])   P(swap(L1;i;i+1)[i],swap(L1;i;i+1)[(i+1)])	2 steps
2	5. L1 : T List 6. i : (||L1||-1) 7. P(L1[i],L1[(i+1)])   count(x < y in swap(L1;i;i+1) | P(x,y))<count(x < y in L1 | P(x,y))	2 steps
3	5. L1 : T List 6. i : (||L1||-1)   P(L1[i],L1[(i+1)])	Auto
4	5. L:T List.  5. L':T List.  5. (L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L') 5. & (i:(||L'||-1). P(L'[i],L'[(i+1)]))   L':T List.    (L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')   & (i:(||L'||-1). P(L'[i],L'[(i+1)]))	1 step

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