1. n : 
2. n1:. 
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:. 
2. ((HanoiSTD(n1 disks; from: p; to: q; indexing from: a)
2. (( z:{a...}({a...z}{1...n1}Peg)))
3. p : Peg
4. q : Peg
5. p  q
6. a : 
  HanoiSTD(n disks; from: p; to: q; indexing from: a)
   z:{a...}({a...z}{1...n}Peg)

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

1

if n=0 <a,x,i. whatever>   else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1.   else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)   else /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi    z:{a...}({a...z}{1...n}Peg)

8 steps

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