Definitions HanoiTowers Sections NuprlLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Standard Solution is Optimal

How short could a Hanoi sequence moving all disks from one peg to another be? The Standard Solution seems to be order 2^n, and doesn't seem to be wasting any moves.

Thm*  n:, p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:. 
Thm*  (1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1)

Gloss

Since the sequence HanoiSTD(n disks; from: p; to: q; indexing from: a) is indexed by {a...z} where

z = 1of(HanoiSTD(n disks; from: p; to: q; indexing from: a))

its length is z-a+1 (hence there are (2^n)-1 moves between situations). Is this really the best one can do? It is:

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)

Gloss

About:
intnatural_numberaddsubtractlambdaapplyfunctionequalimpliesandall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions HanoiTowers Sections NuprlLIB Search Doc