s(?) {to n}  h {to n'}

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 f {to n}  f' {to n'} extends a stacking situation f  {1...n}Peg to more disks beyond n as stipulated by f'  {n+1...n'}Peg. Deepening a sequence s  {a...z}{1...n}Peg of stacking situations is just extending every situation s(x) of the sequence in the same way (by some h).

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)

Gloss

since each move of a disk in the original sequence corresponds to moving the same disk in the deepened sequence.

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