1. k : 
2. x : k
3. y : k
4. n:, x,y:k. y-x = n  (L:(k-1) List. (x, y) = compose_flips(L))
5. xy
  L:(k-1) List. (x, y) = compose_flips(L)

1

6. L:(k-1) List. (y, x) = compose_flips(L)   L:(k-1) List. (x, y) = compose_flips(L)

2 steps

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