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

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