IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
This lemma says that given any two n-disk stacking situations f, g {1...n}Peg that locate the largest (n-th) disk on different pegs, one can compose an n-disk Hanoi sequence from two subsequences, the first starting at f and these second ending at g,
given one already has two n-1-disk Hanoi sequences, the first of which starts at f and the second of which ends at g (ignoring the largest disk), and which agree where they meet, ie, the second starts where the first ends.
Note that the two resulting sequences (for n disks) can be joined, but the two original sequences (for n-1 disks) cannot be joined since you can only join sequences by moving a disk, but the second orignal Hanoi sequence starts exactly where the first original sequence ends rather than a disk move later
The plan is to add the largest disk to peg f(n) throughout the first original n-1 disk Hanoi sequence, and add the largest disk to peg g(n) throughout the second original n-1 disk sequence, resulting in joinable Hanoi sequences.
Thm*n:, a:, z:{a...}, m:{a...z-1}, f,g:({1...n}Peg).
Thm* f(n) g(n)
Thm* Thm* (s1:({a...m}{1...n-1}Peg), s2:({m+1...z}{1...n-1}Peg).
Thm* (s1 is a Hanoi(n-1 disk) seq on a..m Thm* (& s1(a) = f {1...n-1}Peg
Thm* (& s2 is a Hanoi(n-1 disk) seq on m+1..z Thm* (& s2(z) = g {1...n-1}Peg
Thm* (& s1(m) = s2(m+1)
Thm* (& (i:{1...n-1}. s1(m,i) f(n) & s2(m+1,i) g(n)))
Thm* Thm* (r1:({a...m}{1...n}Peg), r2:({m+1...z}{1...n}Peg).
Thm* ((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g)
Our solution is to use
s1(?) {to n-1} f {to n} for r1 and
s2(?) {to n-1} g {to n} for r2
where s(?) {to n} h {to n'} is the operation for Deepening a sequence by adding larger disks to specified pegs throughout. We are left with three things to show
(A) (s1(?) {to n-1} f {to n})(a) = f
(B) (s2(?) {to n-1} g {to n})(z) = g
(C) ((s1(?) {to n-1} f {to n}) @(m) (s2(?) {to n-1} g {to n}))
(C) is a Hanoi(n disk) seq on a..z
First let's deal with (A). For x {1...n}, case split on whether x<n. If x<n then (s1(?) {to n-1} f {to n})(a,x) simplifies to s1(a,x), which equals f(x) by hypothesis. Otherwise (s1(?) {to n-1} f {to n})(a,x) simplifies directly to f(x). The reasoning establishing (B) is similar.
{1...n}
Peg
n:
, a:
, z:{a...}, m:{a...z-1}, f,g:({1...n}
g(n)
s1:({a...m}f {to n}
