Nuprl - Proof: permute by flips 2 2 1 2 1 1 1 1 1 1 1 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: permute by flips 2 2 1 2 1 1 1 1 1 1 1 1 1 2

1. k :

(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

compose_flips([u / v])(k-1) = k-1

By:	Unfold `compose_flips` 0 THEN Unfold `compose_list` 0 THEN Reduce 0 THEN Fold `compose_list` 0 THEN Fold `compose_flips` 0

Generated subgoal:

1 (u, u+1)(compose_flips(v)(k-1)) = k-1 k
2 steps

About:

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