n:, a,z:, s:({a...z}{1...n}Peg).
  s is a Hanoi(n disk) seq on a..z
  
  (a',z':{a...z}. s is a Hanoi(n disk) seq on a'..z')

1

1. n :  2. a :  3. z :  4. s : {a...z}{1...n}Peg 5. s is a Hanoi(n disk) seq on a..z 6. a' : {a...z} 7. z' : {a...z}   s is a Hanoi(n disk) seq on a'..z'

1 step

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