diff -r ff6787d730d5 -r 260090b54ef9 doc-src/Exercises/2002/a6/generated/a6.tex --- a/doc-src/Exercises/2002/a6/generated/a6.tex Fri Apr 29 18:13:28 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{a{\isadigit{6}}}% -\isamarkupfalse% -% -\isamarkupsubsection{The towers of Hanoi% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -In section \ref{psv2000hanoi} we introduced the towers of Hanoi and -defined a function \isa{moves} to generate the moves to solve the -puzzle. Now it is time to show that \isa{moves} is correct. This -means that -\begin{itemize} -\item when executing the list of moves, the result is indeed the -intended one, i.e.\ all disks are moved from one peg to another, and -\item all of the moves are legal, i.e.\ never place a larger disk -on top of a smaller one. -\end{itemize} -Hint: this is a nontrivial undertaking. The complexity of your proofs -will depend crucially on your choice of model and you may have to -revise your model as you proceed with the proof.% -\end{isamarkuptext}% -\isamarkuptrue% -\isamarkupfalse% -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: