Nuprl - Proof: flip adjacent 1 1

(24steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

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

1. k :

k
3.

, x,y:

k. y-x = n

(

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

By:	Analyze 0 THEN NatInd -1

Generated subgoals:

1 4. x1 : k
5. y1 : k
6. y1-x1 = 0
  L:(k-1) List. (x1, y1) = compose_flips(L)
3 steps

2 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
  L:(k-1) List. (x1, y1) = compose_flips(L)
13 steps

About:

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

(24steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

1	4. x1 : k 5. y1 : k 6. y1-x1 = 0 L:(k-1) List. (x1, y1) = compose_flips(L)	3 steps
2	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 L:(k-1) List. (x1, y1) = compose_flips(L)	13 steps