1. k : 
2. 0<k
3. p:((k-1)(k-1)). 
3. Bij((k-1); (k-1); p)  (L:(k-1-1) List. p = compose_flips(L))
4. p : kk
5. Bij(k; k; p)
6. x : k
7. p(x) = k-1
8. Bij(k; k; p o (k-1, x))
9. p o (k-1, x)  (k-1)(k-1)
10. Bij((k-1); (k-1); p o (k-1, x))
11. L : (k-1-1) List
12. p o (k-1, x) = compose_flips(L)
13. L1 : (k-1) List
14. (k-1, x) = compose_flips(L1)
15. x1 : k
16. x1 = k-1
17. k-1 = k-1
  compose_flips(L)(k-1) = k-1  k

1	2. (k-1-1) List 3. 0<k   compose_flips(nil)(k-1) = k-1  k	1 step
2	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  k   compose_flips([u / v])(k-1) = k-1  k	3 steps

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