equal
deleted
inserted
replaced
1 (*<*) |
|
2 theory a6 = Main: |
|
3 (*>*) |
|
4 subsection {* The towers of Hanoi *} |
|
5 |
|
6 text{* |
|
7 In section \ref{psv2000hanoi} we introduced the towers of Hanoi and |
|
8 defined a function @{term moves} to generate the moves to solve the |
|
9 puzzle. Now it is time to show that @{term moves} is correct. This |
|
10 means that |
|
11 \begin{itemize} |
|
12 \item when executing the list of moves, the result is indeed the |
|
13 intended one, i.e.\ all disks are moved from one peg to another, and |
|
14 \item all of the moves are legal, i.e.\ never place a larger disk |
|
15 on top of a smaller one. |
|
16 \end{itemize} |
|
17 Hint: this is a nontrivial undertaking. The complexity of your proofs |
|
18 will depend crucially on your choice of model and you may have to |
|
19 revise your model as you proceed with the proof. |
|
20 *} |
|
21 |
|
22 (*<*) |
|
23 end |
|
24 (*>*) |
|