Thm*  n:, p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:, 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)
Thm*  (
Thm*  ((2^n)z-a+1)

(Note that a sequence with index range {a...z} has length z-a+1.)

Our proof will depend on the key lemma for analyzing Hanoi sequences:

(A) Thm*  n:, p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:, 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)
Thm*  (
Thm*  ((x:{a...z-1}, y:{x+1...z}, p',q':Peg.
Thm*  (((u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)
Thm*  ((& s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg
Thm*  ((& p  p'
Thm*  ((& q  q'))

Gloss

which says that a solution (s indexed {a...z}) to the standard problem can be broken into two parts ({a...x} and {y...z}), the first of which keeps the largest disk (n) on the starting peg (p), removing smaller disks ({1...n-1}) to another peg (p'), and the second of which keeps it on the ending peg (q), removing all smaller disks from another peg (q').

The proof that 2^n states is minimal is by induction, with inductive hypothesis

(B) n1:. 
(B) n1<n
(B) 
(B) (p,q:Peg.
(B) (p  q
(B) (
(B) ((a:, z:{a...}, s:({a...z}{1...n1}Peg).
(B) ((s is a Hanoi(n1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)
(B) ((
(B) (((2^n1)z-a+1))

and assuming

p  q

(C) s is a Hanoi(n disk) seq on a..z

(D) s(a) = (i.p)  {1...n}Peg

(E) s(z) = (i.q)  {1...n}Peg

n  0

we aim to show

(*) 2(2^(n-1))z-a+1

Continued at hanoi sol2 lb gloss cont

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