IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi seq deepen seq1 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
8. x : {a...z}
9. x' : {a...z}
10. x+1 = x' 11. k : {1...n}
12. Moving disk k of n takes s(x) to s(x')
Moving disk k of n' takes (s(?) {to n} h {to n'})(x) to (s(?) {to n} h {to n'})(x')
6 steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html