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

By:	p  otherPeg(p; q) | otherPeg(p; q)  q  Asserted THEN Inst: 3 Using:[p | otherPeg(p; q)]

1	p  otherPeg(p; q)	1 step
2	7. p  otherPeg(p; q)   otherPeg(p; q)  q	1 step
3	7. p  otherPeg(p; q) 8. otherPeg(p; q)  q 9. m : {1...} 10. s1 : {1...m}{1...n-1}Peg 11. s1 is a Hanoi(n-1 disk) seq on 1..m 12. s1(1) = (i.p) 13. s1(m) = (i.otherPeg(p; q))   z:{1...}, m:{1...z-1}, s1:({1...m}{1...n}Peg),   s2:({m+1...z}{1...n}Peg).   (s1 @(m) s2) is a Hanoi(n disk) seq on 1..z   & s1(1) = (i.p)  {1...n}Peg   & s2(z) = (i.q)	15 steps

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