1. n : 
2. 0<n
3. f,g:({1...n-1}Peg), a:.
3. z:{a...}, s:({a...z}{1...n-1}Peg).
3. s is a Hanoi(n-1 disk) seq on a..z & s(a) = f & s(z) = g
4. f : {1...n}Peg
5. g : {1...n}Peg
6. a : 
7. f(n) = g(n)
  z:{a...}, m:{a...z-1}, s1:({a...m}{1...n}Peg),
  s2:({m+1...z}{1...n}Peg).
  (s1 @(m) s2) is a Hanoi(n disk) seq on a..z & s1(a) = f & s2(z) = g

By:	Inst: 3 Using:[f | i.otherPeg(f(n); g(n)) | a] THEN Inst: 3 Using:[i.otherPeg(f(n); g(n)) | g | m+1] THEN Witness: z | m

1

8. m : {a...} 9. s1 : {a...m}{1...n-1}Peg 10. s1 is a Hanoi(n-1 disk) seq on a..m 11. s1(a) = f  {1...n-1}Peg 12. s1(m) = (i.otherPeg(f(n); g(n))) 13. z : {m+1...} 14. s2 : {m+1...z}{1...n-1}Peg 15. s2 is a Hanoi(n-1 disk) seq on m+1..z 16. s2(m+1) = (i.otherPeg(f(n); g(n))) 17. s2(z) = g  {1...n-1}Peg   s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg).   (s1 @(m) s2) is a Hanoi(n disk) seq on a..z   & s1(a) = f  {1...n}Peg   & s2(z) = g  {1...n}Peg

5 steps

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