1. k : 
2. k
3. k
4. n : 
5. 0<n
6. x,y:k. y-x = n-1  (L:(k-1) List. (x, y) = compose_flips(L))
7. x1 : k
8. y1 : k
9. y1-x1 = n
10. L : (k-1) List
11. (x1+1, y1) = compose_flips(L)
12. y1 = x1+1
13. (x1, y1) = compose_list([(x1, x1+1); (y1, x1+1); (x1, x1+1)])
  (x1, y1) = compose_flips([x1] @ L @ [x1])

By:

Inst Thm* k:, L1,L2:(k-1) List. Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2) [k;[x1];L @ [x1]] THEN RevHypSubst -1 0 THEN Thin -1 THEN Inst Thm* k:, L1,L2:(k-1) List. Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2) [k;L;[x1]] THEN RevHypSubst -1 0 THEN Thin -1

1

(x1, y1) = compose_flips([x1]) o compose_flips(L) o compose_flips([x1])

5 steps

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