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)
8. z : {a...}
9. s:({a...z}{1...n-1}Peg). 
9. s is a Hanoi(n-1 disk) seq on a..z & s(a) = f & s(z) = g
  s:({a...z}{1...n}Peg). 
  s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g

By:

BackThru:  Thm*  n:, f,g:({1...n}Peg). Thm*  f(n) = g(n) Thm*   Thm*  (a:, z:{a...}. Thm*  ((s:({a...z}{1...n-1}Peg).  Thm*  ((s is a Hanoi(n-1 disk) seq on a..z Thm*  ((& s(a) = f  {1...n-1}Peg Thm*  ((& s(z) = g  {1...n-1}Peg) Thm*  ( Thm*  ((s:({a...z}{1...n}Peg).  Thm*  ((s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g))

None

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