We can add any number of larger disks throughout a Hanoi sequence and it remains a Hanoi sequence. Let us call this operation "deepening" a sequence, the formulation of which will involve the auxilliary operation of "extending" a single stacking situation to larger disks:
Def (f {to n} f' {to n'})(i) == if in f(i) else f'(i) fi
Thm* n:, f:({1...n}Peg), n':.
Thm* nn' (f':({n+1...n'}Peg). (f {to n} f' {to n'}) {1...n'}Peg)
The operation
Def (s(?) {to n} h {to n'})(x) == s(x) {to n} h {to n'}
Thm* a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* nn'
Thm*
Thm* (h:({n+1...n'}Peg). (s(?) {to n} h {to n'}) {a...z}{1...n'}Peg)
Here are the basic rewrite lemmas for accessing the small and large disk positions from a deepened sequence:
Thm* a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* nn'
Thm*
Thm* (h:({n+1...n'}Peg), i:{1...n'}.
Thm* (in (x:{a...z}. (s(?) {to n} h {to n'})(x,i) = s(x,i)))
Thm* a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* nn'
Thm*
Thm* (h:({n+1...n'}Peg), i:{1...n'}.
Thm* (n<i (x:{a...z}. (s(?) {to n} h {to n'})(x,i) = h(i)))
Then deepening a Hanoi sequence produces a Hanoi sequence
Thm* a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* nn'
Thm*
Thm* (h:({n+1...n'}Peg).
Thm* (s is a Hanoi(n disk) seq on a..z
Thm* (
Thm* ((s(?) {to n} h {to n'}) is a Hanoi(n' disk) seq on a..z)
since each move of a disk in the original sequence corresponds to moving the same disk in the deepened sequence.
About: