Thm*  n':, n:{n'...}, a,z:, s:({a...z}{1...n}Peg).
Thm*  s is a Hanoi(n disk) seq on a..z
Thm*  
Thm*  (a',z':{a...z}.
Thm*  ((x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i))
Thm*  (
Thm*  (s is a Hanoi(n' disk) seq on a'..z')

Digression on polymorphism:

This formulation uses two different, but related, types for the sequence s, namely the type {a...z}{1...n}Peg which it needs to be a stacking sequence for n disks, but also the type {a'...z'}{1...n'}Peg which it needs to be a, possibly shorter, stacking sequence for n' disks.

Note that in general, the mathematical notation we are employing allows us to construe any notation for a function also as a notation for its restriction to a subtype of the domain, without any explicit notation for the conversion. The pertinent case here is that

n':, n:{n'...}, a,z:, a',z':{a...z}.
{a...z}{1...n}Peg  {a'...z'}{1...n'}Peg

since

n':, n:{n'...}. {1...n'}  {1...n}
and
a,z:, a',z':{a...z}. {a'...z'}  {a...z}

where the propositional form A  B expresses the fact that all the notations for values of one type A may be construed also as notations for values in type B (see Polymorphism).

Turning to the argument, under the assumption that s is a Hanoi(n disk) seq on a..z, the adjacent states within s are all moves of disks within {1...n}, i.e. for some k  {1...n}, and some x and x+1 in {a...z}

Moving disk k of n takes s(x) to s(x')

hence, by

Thm*  n:, f,g:({1...n}Peg), k:{1...n}.
Thm*  Moving disk k of n takes f to g  f(k)  g(k),

s(x,k)  s(x+1,k)

To establish that s is a Hanoi(n' disk) seq on a'..z' we just need to establish that, given x  {a'...z'}, any such k  {1...n} is actually in {1...n'}. But from our assumption x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i) it would follow that

n'<k  s(x,k) = s(x+1,k)

since both sides could be rewritten to s(a,i). Consequently n<k since, as already mentioned above, s(x,k)  s(x+1,k).

QED

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