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

By:	Compute CoHanoiSTD(0 disks; from: p; to: q; indexing from: a)/z,s. Cos is a Hanoi(0 disk) seq on a..z Co& s(a) = (i.p)  {1...0}Peg Co& s(z) = (i.q)  {1...0}Peg Co* Co(x,i. whatever) is a Hanoi(0 disk) seq on a..a Co& (x,i. whatever)(a) = (i.p)  {1...0}Peg Co& (x,i. whatever)(a) = (i.q)  {1...0}Peg

1	(x,i. whatever) is a Hanoi(0 disk) seq on a..a	1 step
2	(x,i. whatever)(a) = (i.p)  {1...0}Peg	1 step
3	(x,i. whatever)(a) = (i.q)  {1...0}Peg	1 step

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