T:Type, L:T List, i:(||L||-1), a,b:T.
  a before b  swap(L;i;i+1)  a before b  L  a = L[(i+1)] & b = L[i]

By:

((Auto THEN All (Unfold `l_before`) THEN Unfold `sublist` -1 THEN ExRepD ((THEN ((All Reduce ((THEN ((Inst Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||   [T;L;i;i+1] ((THEN ((RWO Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))] -2 ((THEN ((InstHyp [0] -2 ((THEN ((Reduce -1 ((THEN ((InstHyp [1] -3 ((THEN ((Reduce -1 ((THEN ((Inst Thm* k:, i,j:k. (i, j)  kk [||L||;i;i+1] ((THEN ((WeakSubstFor a 0) (THEN ((WeakSubstFor b 0)) THEN Decide ((i, i+1)(f(0))<(i, i+1)(f(1))) THENL [OrLeft THEN (BackThru Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L) ;OrRight]

1

1. T : Type 2. L : T List 3. i : (||L||-1) 4. a : T 5. b : T 6. f : 2||swap(L;i;i+1)|| 7. increasing(f;2) 8. j:2. [a; b][j] = L[((i, i+1)(f(j)))] 9. ||swap(L;i;i+1)|| = ||L||   10. a = L[((i, i+1)(f(0)))] 11. b = L[((i, i+1)(f(1)))] 12. (i, i+1)  ||L||||L|| 13. (i, i+1)(f(0))<(i, i+1)(f(1))   L[((i, i+1)(f(0)))] = L[(i+1)] & L[((i, i+1)(f(1)))] = L[i]

1 step

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