Thm*  n:, p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (z:{1...}, s:({1...z}{1...n}Peg).
Thm*  (s is a Hanoi(n disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q))

This proof is a variant of

Thm*  n:, p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:. 
Thm*  (z:{a...}, s:({a...z}{1...n}Peg).
Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))

Gloss

not only in its fixing the starting index at 1, but also in its use of index shifting and peg permutation to reduce the recursion. The base case (no disks) is the essentially the same, and the construction of the result from shorter Hanoi sequences for one few disks via the main lemma is the same. What's different is how those shorter Hanoi sequences are arrived at. In the earlier proof there are two applications of induction, the first to get s1  {a...m}{1...n-1}Peg, which is the same as done in the new proof except that s1  {1...m}{1...n-1}Peg (since we've fixed the starting index at 1), which moves the n-1 smaller disks from the source peg to the other peg that is not the destination peg for the n disk move.

What's different is how s2  {m+1...z}{1...n-1}Peg is arrived at. In the old proof it was gotten in the same way as s1, applying the inductive hypothesis again, but on different arguments. In the new proof s2 is instead derived directly from s1 by shifting the indices and permuting the pegs. First apply the lemma

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)

to "s1 is a Hanoi(n-1 disk) seq on 1..m", which was derived by applying the inductive hypothesis, and to the permutation function permute(p to otherPeg(p; q) ; otherPeg(p; q) to q), where p and q are supposed to be the source and destination pegs for the full n-disk move

Thm*  p,r,q,s:Peg. p  q  r  s  Inj(Peg; Peg; permute(p to r ; q to s))

giving us

(x,i. permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)(s1(x,i)))
is a Hanoi(n-1 disk) seq on 1..m

then shift the indexing by m (the length of the s1 sequence) using

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

to get

(x,i. permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)(s1(x-m,i)))
is a Hanoi(n-1 disk) seq on 1+m..m+m

These sequences can then be joined in the same way as in the original proof by using the 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)

QED

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