1. n : 
2. n1:. 
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:. 
2. ((1of(HanoiSTD(n1 disks; from: p; to: q; indexing from: a)) = a+(2^n1)-1))
3. p : Peg
4. q : Peg
5. p  q
6. a : 
7. n = 0
  1of(<a,x,i. whatever>) = a+1-1  

None

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