1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (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) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. a : 
  z:{a...}, s:({a...z}{1...n}Peg).
  s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)

By:	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) = (i.p) & s2(z) = (i.q) Asserted

1	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) = (i.p) & s2(z) = (i.q)	9 steps
2	8. z:{a...}, m:{a...z-1}, s1:({a...m}{1...n}Peg), 8. s2:({m+1...z}{1...n}Peg). 8. (s1 @(m) s2) is a Hanoi(n disk) seq on a..z & s1(a) = (i.p) & s2(z) = (i.q)   z:{a...}, s:({a...z}{1...n}Peg).   s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)	4 steps

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