(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

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


By: InstConcl [nil] THEN Unfold `compose_flips` 0 THEN Unfold `compose_list` 0
THEN
Reduce 0


Generated subgoal:

1   (x1y1) = (x.x)
2 steps

About:
listnilintnatural_numbersubtractlambdafunctionequalexists
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