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')
15. s(x,k)  s(x',k)
  k  {1...n'}

By:	n'<k  Asserted

1

n'<k

2 steps

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