IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Nuprl Section: HanoiTowers - Towers of Hanoi: a thorough treatment.
The purpose of these notes is to exhibit the application of formal proof-oriented methods to a familiar non-trivial problem. A variety of informal explanations and executable solutions may be easily found on the WEB by
for "towers of hanoi". We formulate various aspects of the problem domain and prove various key claims about them.
Here are the main contents, both extant and planned: