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
6. L:(k-1) List. (y, x) = compose_flips(L)
  L:(k-1) List. (x, y) = compose_flips(L)

1

7. x1 : k   (x, y)(x1) = (y, x)(x1)

1 step

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