1. T : Type
2. T List
3. P : TT
4. x,y:T. P(x,y)  P(y,x)
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))

By:

RWO Thm* L:T List, P:(TT), n:(||L||-1). Thm* count(x < y in swap(L;n;n+1) | P(x,y)) Thm* = Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)] Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P,L[n]) Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if 1 Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+else 0 fi 0 THEN Repeat SplitOnConclITE

1

8. P(L1[i],L1[(i+1)]) 9. P(L1[(i+1)],L1[i])   count(x < y in L1 | P(x,y))+-1+1<count(x < y in L1 | P(x,y))

1 step

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