--- a/Paper/Paper.thy	Thu Jan 24 12:01:44 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 15:04:11 2013 +0100
@@ -26,6 +26,8 @@
   tcopy_init ("copy\<^bsub>begin\<^esub>") and
   tcopy_loop ("copy\<^bsub>loop\<^esub>") and
   tcopy_end ("copy\<^bsub>end\<^esub>") and
+  step0 ("step") and
+  steps0 ("steps") and
 (*  abc_lm_v ("lookup") and
   abc_lm_s ("set") and*)
   haltP ("stdhalt") and 
@@ -210,7 +212,7 @@
 it harder to design programs for these Turing machines. In order
 to construct a universal Turing machine we therefore do not follow 
 \cite{AspertiRicciotti12}, instead follow the proof in
-\cite{Boolos87} by relating abacus machines to Turing machines and in
+\cite{Boolos87} by translating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
 machine can then be constructed as a recursive function.
 
@@ -242,11 +244,11 @@
   or occupied, which we represent by a datatype having two
   constructors, namely @{text Bk} and @{text Oc}.  One way to
   represent such tapes is to use a pair of lists, written @{term "(l,
-  r)"}, where @{term l} stands for the tape on the left-hand side of the
-  head and @{term r} for the tape on the right-hand side. We have the
-  convention that the head, abbreviated @{term hd}, of the right-list is
-  the cell on which the head of the Turing machine currently operates. This can
-  be pictured as follows:
+  r)"}, where @{term l} stands for the tape on the left-hand side of
+  the head and @{term r} for the tape on the right-hand side. We have
+  the convention that the head, abbreviated @{term hd}, of the
+  right-list is the cell on which the head of the Turing machine
+  currently scannes. This can be pictured as follows:
   %
   \begin{center}
   \begin{tikzpicture}
@@ -427,7 +429,7 @@
   \end{center}
 
   \noindent
-  The first says that @{text p} must have at least an instruction for the starting 
+  The first states that @{text p} must have at least an instruction for the starting 
   state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 
   state, and the third that every next-state is one of the states mentioned in
   the program or being the @{text 0}-state.
@@ -524,10 +526,9 @@
   Turing machines, we need to analyse two concrete Turing machine
   programs and establish that they are correct, that is they are
   ``doing what they are supposed to be doing''.  This is usually left
-  out in the informal computability literature, for example
-  \cite{Boolos87}.  One program we prove correct is the @{term dither}
-  program shown in \eqref{dither} and the other program @{term
-  "tcopy"} is defined as
+  out in the informal literature, for example \cite{Boolos87}.  One program 
+  we prove correct is the @{term dither} program shown in \eqref{dither} 
+  and the other program @{term "tcopy"} is defined as
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -536,7 +537,12 @@
   \end{center}
 
   \noindent
-  whose three components are given in Figure~\ref{copy}.
+  whose three components are given in Figure~\ref{copy}. 
+  
+
+
+
+
   To prove the correctness, we derive some Hoare-style reasoning rules for 
   Turing machine programs. A \emph{Hoare-triple} for a terminating Turing 
   machine program is defined as
@@ -545,10 +551,16 @@
   @{thm Hoare_halt_def}
   \end{center}
 
+  A \emph{Hoare-pair} for a non-terminating Turing machine program is defined 
+  as
+
   \begin{center}
   @{thm Hoare_unhalt_def}
   \end{center}
 
+
+
+
   In the following we will consider the following Turing machine program
   that makes a copies a value on the tape.