At: hanoi seq deepen seq

  a,z:, n:, s:({a...z}{1...n}Peg), n':.
  nn'
  
  (h:({n+1...n'}Peg). 
  (s is a Hanoi(n disk) seq on a..z
  (
  ((s(?) {to n}  h {to n'}) is a Hanoi(n' disk) seq on a..z)

1

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

7 steps

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