1. k : 
2. (k-1-1) List
3. 0<k
4. u : (k-1-1)
5. v : (k-1-1) List
6. compose_flips(v)(k-1) = k-1
  (u, u+1)(compose_flips(v)(k-1)) = k-1  k

1

6. compose_flips(v)(k-1) = k-1 7. 0  compose_flips(v)(k-1) < k   (u, u+1)(k-1) = k-1  k

1 step

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