--- a/Paper/Paper.thy Sun Feb 03 12:24:28 2013 +0000
+++ b/Paper/Paper.thy Sun Feb 03 13:31:14 2013 +0000
@@ -1,6 +1,6 @@
(*<*)
theory Paper
-imports "../thys/uncomputable"
+imports "../thys/abacus"
begin
(*
@@ -1119,9 +1119,6 @@
to an contradiction, which means we have to abondon our assumption
that there exists a Turing machine @{term H} which can decide
whether Turing machines terminate.
-
-
-
*}
@@ -1135,22 +1132,22 @@
over an unlimited number of registers $R_0$, $R_1$, \ldots
each being able to hold an arbitrary large natural number.
We use natural numbers to refer to registers, but also
- to refer to \emph{opcodes} of abacus
- machines. Obcodes are given by the datatype
+ to refer to \emph{statements} of abacus programs. Statements
+ are given by the datatype
\begin{center}
- \begin{tabular}{rcll}
+ \begin{tabular}{rcl@ {\hspace{10mm}}l}
@{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\
& $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
& & & then decrement it by one\\
- & & & otherwise jump to opcode $o$\\
- & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
+ & & & otherwise jump to statement $o$\\
+ & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$
\end{tabular}
\end{center}
\noindent
A \emph{program} of an abacus machine is a list of such
- obcodes. For example the program clearing the register
+ statements. For example the program clearing the register
$R$ (setting it to 0) can be defined as follows:
\begin{center}