IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
This proof shows that The Towers of Hanoi Problem is soluble. For any number of disks and any two pegs, there is a legitimate Hanoi sequence of stacking situations taking all the disks from one peg to the other (and the sequence numbering can start wherever you like).
Thm*n:, p,q:Peg.
Thm* pq 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))
The proof is by induction on n. For the base case of 0 disks, no moves are needed and the starting situation is the ending situation and is the only situation possible, namely, no disks on any Peg. There is exactly one function, however one may choose to describe it, with the empty domain (see Void).
Now taking as our inductive hypothesis
p,q:Peg.
pq (a:.
(z:{a...}, s:({a...z}{1...n-1}Peg).
(s is a Hanoi(n-1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))
and assuming pq and a, we need to show
(*) z:{a...}, s:({a...z}{1...n}Peg).
(*) s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)
We can (and shortly we will) show that
(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 (A) & s1(a) = (i.p)
(A) & s2(z) = (i.q)
where s1 @(m) s2 is simply a joining together of Hanoi sequences s1 and s2, which we will do below. And from (A) our conclusion (*) follows, by using s1 @(m) s2 for s, since (s1 @(m) s2)(a) and (s1 @(m) s2)(z) reduce to s1(a) and s2(z). See Joining.
n:
, p,q:Peg.
q
.
z:{a...}, s:({a...z}
{1...n}
i.p) & s(z) = (
s2:({m+1...z}
