So, we are down to proving

(A) z:{a...}, m:{a...z-1}, s1:({a...m}{1...n}Peg),
(A) s2:({m+1...z}{1...n}Peg).
(A) (s1 @(m) s2) is a Hanoi(n disk) seq on a..z & s1(a) = f & s2(z) = g

Since f(n)  g(n), otherPeg(f(n); g(n)) is the remaining Peg. The stacking situation i.otherPeg(f(n); g(n)) has all it disks on that other Peg. Let's digress a moment. In the mathematical notation we are using, a notation for a function on one domain is automatically interpreted as well as a function over a smaller domain. Thus, since f, g  {1...n}Peg then also f, g  {1...n-1}Peg. This means we will able to apply our induction hypothesis on f and g. Application of the inductive hypothesis twice assures us there is a Hanoi sequence from f to i.otherPeg(f(n); g(n)) as well as one from i.otherPeg(f(n); g(n)) to g. Applying it first using

f, (i.otherPeg(f(n); g(n)))  {1...n-1}Peg, a  

gives us m  {a...} and s1  {a...m}{1...n-1}Peg such that

s1 is a Hanoi(n-1 disk) seq on a..m

s1(a) = f  {1...n-1}Peg

s1(m) = (i.otherPeg(f(n); g(n)))

Applying the inductive hypothesis further to (i.otherPeg(f(n); g(n))), g  {1...n-1}Peg, m+1   gives us z  {m+1...} and s2  {m+1...z}{1...n-1}Peg such that

s2 is a Hanoi(n-1 disk) seq on m+1..z

s2(m+1) = (i.otherPeg(f(n); g(n)))

s2(z) = g  {1...n-1}Peg

The principle for showing how to combine two such Hanoi sequences to show our goal has been isolated in a lemma:

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)

Gloss

Applying this special lemma here to show (A) from above reduces to establishing that for i  {1...n-1}

s1(m,i)  f(n), which follows from s1(m) = (i.otherPeg(f(n); g(n))) above, and

s2(m+1,i)  g(n), which follows from s2(m+1) = (i.otherPeg(f(n); g(n))) above.

QED

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