1. n : 
2. f : n
3. L : (n-1) List
  sum(f(compose_flips(L)(x)) | x < n) = sum(f(x) | x < n)

1	2. (n-1) List   f:(n). sum(f(compose_flips(nil)(x)) | x < n) = sum(f(x) | x < n)	1 step
2	2. (n-1) List 3. u : (n-1) 4. v : (n-1) List 5. f:(n). sum(f(compose_flips(v)(x)) | x < n) = sum(f(x) | x < n)   f:(n). sum(f(compose_flips([u / v])(x)) | x < n) = sum(f(x) | x < n)	11 steps

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