IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Permuting the pegs throughout a Hanoi sequence results in a Hanoi sequence.
At:
hanoi seq permutepegs n:, a,z:, s:({a...z}{1...n}Peg).
s is a Hanoi(n disk) seq on a..z (f:(PegPeg).
(Inj(Peg; Peg; f) (x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z)
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. f : PegPeg
7. Inj(Peg; Peg; f)
(x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z
6 steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html