Nuprl - Proof: flip adjacent 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: flip adjacent 1 2

1. k :

2. x :

k
3. y :

k
4.

, x,y:

k. y-x = n

(

(k-1) List. (x, y) = compose_flips(L))

(k-1) List. (x, y) = compose_flips(L)

By:	Decide (xy)

Generated subgoals:

1 5. xy
L:(k-1) List. (x, y) = compose_flips(L)
1 step

2 5. xy
L:(k-1) List. (x, y) = compose_flips(L)
3 steps

About:

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

1	5. xy L:(k-1) List. (x, y) = compose_flips(L)	1 step
2	5. xy L:(k-1) List. (x, y) = compose_flips(L)	3 steps