1. n : 
2. a : 
3. z : {a...}
4. m : {a...z-1}
5. f : {1...n}Peg
6. g : {1...n}Peg
7. f(n)  g(n)
8. s1 : {a...m}{1...n-1}Peg
9. s2 : {m+1...z}{1...n-1}Peg
10. s1 is a Hanoi(n-1 disk) seq on a..m
11. s1(a) = f
12. s2 is a Hanoi(n-1 disk) seq on m+1..z
13. s2(z) = g
14. s1(m) = s2(m+1)
15. i:{1...n-1}. s1(m,i)  f(n) & s2(m+1,i)  g(n)
  k:{1...n}. 
  Moving disk k of n
  takes (s1(?) {to n-1}  f {to n})(m) to (s2(?) {to n-1}  g {to n})(m+1)

1	16. i : {1...n}   (s1(?) {to n-1}  f {to n})(m,i) = (s2(?) {to n-1}  g {to n})(m+1,i)      i  n	9 steps
2	16. i : {1...n-1}   (s1(?) {to n-1}  f {to n})(m,i)  (s1(?) {to n-1}  f {to n})(m,n)   & (s2(?) {to n-1}  g {to n})(m+1,i)  (s2(?) {to n-1}  g {to n})(m+1,n)	3 steps

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