1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (a:. 
3. (HanoiSTD(n-1 disks; from: p; to: q; indexing from: a)/z,s.
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 : 
8. p = otherPeg(p; q)
9. otherPeg(p; q) = q
  (HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1.
  (HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)/z,s2.
  (<z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>)
  /z,s.
  s is a Hanoi(n disk) seq on a..z
  & s(a) = (i.p)  {1...n}Peg
  & s(z) = (i.q)  {1...n}Peg

1

10. m : {a...} 11. s1 : {a...m}{1...n-1}Peg 12. <m,s1> = HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) 13. s1 is a Hanoi(n-1 disk) seq on a..m 14. s1(a) = (i.p) 15. s1(m) = (i.otherPeg(p; q))   (HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)/z,s2.   (<z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>)   /z,s.   s is a Hanoi(n disk) seq on a..z   & s(a) = (i.p)  {1...n}Peg   & s(z) = (i.q)  {1...n}Peg

9 steps

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