IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A Non-standard Recursive Solution
Our Standard Solution involved an inductive proof invoking the inductive hypothesis twice to move an extra disk, implicitly defining a recursive procedure that invokes itself twice. Here we consider exploiting other features of Hanoi sequences to get a procedure that only calls itself once for each disk. Here we make two observations. First, that shifting the indices of a Hanoi sequence leaves it a Hanoi sequence, the obviousness of which was assumed as part of our formulation of Hanoi sequences in the first place; after all the indices are only used to provide a notion of sequence length and consecutiveness.
Thm*n:, a,z,d:, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z Thm* Thm* (x.s(x-d)) is a Hanoi(n disk) seq on a+d..z+d
Consequently, one could always "normalize" Hanoi sequences to start at, say, 1. Second, if one permutes the three pegs throughout a Hanoi sequence the result is still a Hanoi sequence. By a permutation we just mean a one-one correspondence between the class of pegs and itself, i.e., a function f PegPeg which is an injection:
Thm*n:, a,z:, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z Thm* Thm* (f:(PegPeg).
Thm* (Inj(Peg; Peg; f) (x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z)
n:
, a,z,d:
, s:({a...z}
{1...n}
x.s(x-d)) is a Hanoi(n disk) seq on a+d..z+d
Pegq
z:{1...}, s:({1...z}
