The Towers of Hanoi Problem is soluble.

At: hanoi sol2 via general

  n:, p,q:Peg.
  p  q
  
  (a:. 
  (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))

1

1. n :  2. p : Peg 3. q : Peg 4. p  q 5. a :    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)

1 step

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