1. n' : 
2. n : {n'...}
3. a : 
4. z : 
5. s : {a...z}{1...n}Peg
6. s is a Hanoi(n disk) seq on a..z
7. a' : {a...z}
8. z' : {a...z}
9. x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i)
10. x : {a'...z'}
11. x' : {a'...z'}
12. x+1 = x'
13. k : {1...n}
14. Moving disk k of n takes s(x) to s(x')
  k  {1...n'}

By:	FwdThru:  Thm*  n:, f,g:({1...n}Peg), k:{1...n}. Thm*  Moving disk k of n takes f to g  f(k)  g(k) on [ Hyp:-1 ]

1

15. s(x,k)  s(x',k)   k  {1...n'}

3 steps

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