--- a/Paper/Paper.thy	Sun Jan 27 15:46:32 2013 +0000
+++ b/Paper/Paper.thy	Sun Jan 27 17:15:38 2013 +0000
@@ -34,7 +34,7 @@
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ \<oplus> _") and 
-  DUMMY  ("\<^raw:\mbox{$\_$}>")
+  DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>")
 
 declare [[show_question_marks = false]]
 
@@ -315,7 +315,8 @@
 
   \noindent
   We slightly deviate
-  from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
+  from the presentation in \cite{Boolos87} and \cite{AspertiRicciotti12} 
+  by using the @{term Nop} operation; however its use
   will become important when we formalise halting computations and also universal Turing 
   machines.  Given a tape and an action, we can define the
   following tape updating function:
@@ -522,9 +523,7 @@
   halts, then in our setting the @{term steps}-evaluation does not
   actually halt, but rather transitions to the @{text 0}-state (the
   final state) and remains there performing @{text Nop}-actions until
-  @{text n} is reached. This is different from the setup in 
-  \cite{AspertiRicciotti12} where an option is returned once a final 
-  state is reached.
+  @{text n} is reached. 
   
   \begin{figure}[t]
   \begin{center}
@@ -668,11 +667,11 @@
   we need to prove correct is the @{term dither} program shown in \eqref{dither} 
   and the other program is @{term "tcopy"} defined as
 
-  \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  \begin{equation}
+  \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}\label{tcopy}
+  \end{equation}
 
   \noindent
   whose three components are given in Figure~\ref{copy}. To the prove
@@ -776,7 +775,7 @@
   \end{center}
 
   \noindent
-  We can prove the following formal statements
+  We can prove the following Hoare-statements:
  
   \begin{center}
   \begin{tabular}{l}
@@ -786,19 +785,37 @@
   \end{center}
 
   \noindent
-  {\it unfold} The first states that on a tape @{term "(Bk \<up> n,  [Oc, Oc])"}
-  halts in tree steps leaving the tape unchanged. In the other states
-  that @{term dither} started with tape @{term "(Bk \<up> n,  [Oc])"} loops.
-  
+  The first is by a simple calculation. The second is by induction on the
+  number of steps we can perform starting from the input tape.
 
+  The purpose of the @{term tcopy} program defined in \eqref{tcopy} is
+  to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when
+  started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of
+  a value on the tape.  Reasoning about this program is substantially
+  harder than about @{term dither}. To ease the burden, we can prove
+  the following Hoare-rules for sequentially composed programs.
 
-  In the following we will consider the following Turing machine program
-  that makes a copies a value on the tape.
-
+  \begin{center}
+  \begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}}
+  @{thm[mode=Rule] 
+  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"]}
+  &
+  @{thm[mode=Rule] 
+  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"]}
+  \end{tabular}
+  \end{center}
    
-
+  \noindent
+  The first corresponds to the usual Hoare-rule for composition of imperative
+  programs, where @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for 
+  all tapes @{term "(l, r)"}. The second rule covers the case where rughly the 
+  first program terminates generating a tape for which the second program
+  loops. These are two cases we need in our proof for undecidability.
   
-  
+  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 
+  the program @{term "tcopy_begin"}. 
 
 
   assertion holds for all tapes
@@ -813,21 +830,10 @@
   measure for the copying TM, which we however omit.
 
   halting problem
+
+  Magnus: invariants -- Section 5.4.5 on page 75.
 *}
 
-text {*
-  \begin{center}
-  \begin{tabular}{@ {}p{3cm}p{3cm}@ {}}
-  @{thm[mode=Rule] 
-  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"]}
-  &
-  @{thm[mode=Rule] 
-  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"]}
-  \end{tabular}
-  \end{center}
-
-
-*}
 
 section {* Abacus Machines *}