1. n : 
2. p : Peg
3. q : Peg
4. p  q
5. a : 
  HanoiSTD(n disks; from: p; to: q; indexing from: a)
  =
  (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>)

By:

Compute CoHanoiSTD(n disks; from: p; to: q; indexing from: a) Co* Coif n=0 <a,x,i. whatever> Coelse HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1. Coelse HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1) Coelse /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi THEN SplitITE Concl

1	6. n  0   p  otherPeg(p; q)	1 step
2	6. n  0 7. m : {a...} 8. s1 : {a...m}{1...n-1}Peg 9. HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) = <m,s1>   otherPeg(p; q)  q	1 step

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