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 & s(a) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. 
8. p = otherPeg(p; q)
  otherPeg(p; q) = q

By:	BackThru: Thm*  x,y:Peg. x  y  otherPeg(x; y)  y

None

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