(31steps 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: permute by flips 2 2 1 2

1. k : 
2. 0<k
3. p:((k-1)(k-1)). 
3. Bij((k-1); (k-1); p (L:(k-1-1) List. p = compose_flips(L))
4. p : kk
5. Bij(kkp)
6. x : k
7. p(x) = k-1
8. Bij(kkp o (k-1, x))
9. p o (k-1, x (k-1)(k-1)
10. Bij((k-1); (k-1); p o (k-1, x))
  L:(k-1) List. p = compose_flips(L)


By: InstHyp [p o (k-1, x)] 3 THEN ExRepD


Generated subgoal:

1 11. L : (k-1-1) List
12. p o (k-1, x) = compose_flips(L)
  L:(k-1) List. p = compose_flips(L kk

20 steps

About:
listintnatural_numbersubtractless_thanapplyfunction
equalmemberimpliesallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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