IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip adjacent1121111 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
(x1, x1+1) = (x1, x1+1) o (x.x)
By:
Ext THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html