equal
deleted
inserted
replaced
|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{a{\isadigit{6}}}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{The towers of Hanoi% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 In section \ref{psv2000hanoi} we introduced the towers of Hanoi and |
|
12 defined a function \isa{moves} to generate the moves to solve the |
|
13 puzzle. Now it is time to show that \isa{moves} is correct. This |
|
14 means that |
|
15 \begin{itemize} |
|
16 \item when executing the list of moves, the result is indeed the |
|
17 intended one, i.e.\ all disks are moved from one peg to another, and |
|
18 \item all of the moves are legal, i.e.\ never place a larger disk |
|
19 on top of a smaller one. |
|
20 \end{itemize} |
|
21 Hint: this is a nontrivial undertaking. The complexity of your proofs |
|
22 will depend crucially on your choice of model and you may have to |
|
23 revise your model as you proceed with the proof.% |
|
24 \end{isamarkuptext}% |
|
25 \isamarkuptrue% |
|
26 \isamarkupfalse% |
|
27 \end{isabellebody}% |
|
28 %%% Local Variables: |
|
29 %%% mode: latex |
|
30 %%% TeX-master: "root" |
|
31 %%% End: |