--- a/Paper/Paper.thy	Mon Jan 28 02:38:57 2013 +0000
+++ b/Paper/Paper.thy	Tue Jan 29 12:37:06 2013 +0000
@@ -81,10 +81,10 @@
 done
 
 lemmas HR1 = 
-  Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
 
 lemmas HR2 =
-  Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"]
 
 (*>*)
 
@@ -180,7 +180,7 @@
 %Turing machines.
 
 We are not the first who formalised Turing machines: we are aware 
-of the preliminary work by Asperti and Ricciotti
+of the work by Asperti and Ricciotti
 \cite{AspertiRicciotti12}. They describe a complete formalisation of
 Turing machines in the Matita theorem prover, including a universal
 Turing machine. However, they do \emph{not} formalise the undecidability of the 
@@ -637,8 +637,8 @@
   \end{scope}
   \end{tikzpicture}\\[-8mm]\mbox{} 
   \end{center}
-  \caption{The components of the \emph{copy Turing machine} (above). If started 
-  with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at 
+  \caption{The three components of the \emph{copy Turing machine} (above). If started 
+  (below) with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at 
   the end of the right tape; the second then ``moves'' all @{term Oc}s except the 
   first from the beginning of the tape to the end; the third ``refills'' the original 
   block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}
@@ -662,8 +662,8 @@
   \noindent
   A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l} 
   and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 
-  leftmost @{term "Oc"} on the tape. Note also that @{text 0} is represented by
-  a single filled cell, @{text 1} by two filled cells and so on.
+  leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} 
+  is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
 
   Before we can prove the undecidability of the halting problem for our
   Turing machines, we need to analyse two concrete Turing machine
@@ -728,7 +728,8 @@
   It is realatively straightforward to prove that the Turing program 
   @{term "dither"} shown in \eqref{dither} is correct. This program
   should be the ``identity'' when started with a standard tape representing 
-  @{text "1"} but loop when started with @{text 0} instead.
+  @{text "1"} but loop when started with @{text 0} instead, as pictured 
+  below.
 
 
   \begin{center}
@@ -802,14 +803,14 @@
   the following two Hoare-rules for sequentially composed programs.
 
   \begin{center}
-  \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{9mm}}c@ {}}
-  $\inferrule*[Right=@{thm (prem 4) HR1}]
-  {@{thm (prem 1) HR1} \\ @{thm (prem 3) HR1} \\ @{thm (prem 2) HR1}}
+  \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
+  $\inferrule*[Right=@{thm (prem 3) HR1}]
+  {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
   {@{thm (concl) HR1}}
   $ &
   $
-  \inferrule*[Right=@{thm (prem 4) HR2}]
-  {@{thm (prem 1) HR2} \\ @{thm (prem 3) HR2} \\ @{thm (prem 2) HR2}}
+  \inferrule*[Right=@{thm (prem 3) HR2}]
+  {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
   {@{thm (concl) HR2}}
   $
   \end{tabular}
@@ -817,18 +818,16 @@
 
   \noindent
   The first corresponds to the usual Hoare-rule for composition of two
-  terminating programs. The premise @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means that
-  @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for all tapes @{term "(l,
-  r)"}. The second rule covers the case where the first program
+  terminating programs. The second rule is for cases where the first program
   terminates generating a tape for which the second program loops.
-  The side-condition about @{thm (prem 4) HR2} is needed in both rules
+  The side-condition about @{thm (prem 3) HR2} is needed in both rules
   in order to ensure that the redirection of the halting and initial
   state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
 
 
   The Hoare-rules above allow us to prove the correctness of @{term tcopy}
   by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"} 
-  and @{term "tcopy_end"} in isolation. We will show some details for the 
+  and @{term "tcopy_end"} in isolation. We will show the details for the 
   the program @{term "tcopy_begin"}.