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(k; k; p)
6. x:k. p(x) = k-1
  L:(k-1) List. p = compose_flips(L)

By:	ExRepD THEN AssertBY Bij(k; k; p o (k-1, x)) (BackThru Thm* f,g:(TT). Bij(T; T; f)  Bij(T; T; g)  Bij(T; T; f o g) (THEN (BackThru Thm* k:, i,j:k. Bij(k; k; (i, j)))

1

6. x : k 7. p(x) = k-1 8. Bij(k; k; p o (k-1, x))   L:(k-1) List. p = compose_flips(L)

23 steps

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