--- a/Paper/Paper.thy	Tue Jan 29 13:00:51 2013 +0000
+++ b/Paper/Paper.thy	Tue Jan 29 16:37:38 2013 +0000
@@ -719,13 +719,13 @@
   with total correctness and non-terminantion, rather than have
   notions for partial correctness and termination. Although the latter
   would allow us to reason more uniformly (only using Hoare-triples),
-  we prefer our definitions because we can derive simple
+  we prefer our definitions because we can derive below some simple
   Hoare-rules for sequentially composed Turing programs.  In this way
   we can reason about the correctness of @{term "tcopy_begin"}, for
   example, completely separately from @{term "tcopy_loop"} and @{term
   "tcopy_end"}.
 
-  It is realatively straightforward to prove that the Turing program 
+  It is realatively straightforward to prove that the small 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, as pictured 
@@ -795,12 +795,13 @@
   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 prove
-  the following two Hoare-rules for sequentially composed programs.
+  The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
+  its purpose 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 prove the following two Hoare-rules for sequentially
+  composed programs.
 
   \begin{center}
   \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
@@ -827,8 +828,17 @@
 
   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 the details for the 
-  the program @{term "tcopy_begin"}. 
+  and @{term "tcopy_end"} in isolation. We will show the details for 
+  the program @{term "tcopy_begin"}. We found the following invariants for each
+  state:
+
+  \begin{center}
+  @{thm inv_begin0.simps}\\
+  @{thm inv_begin1.simps}\\
+  @{thm inv_begin2.simps}\\
+  @{thm inv_begin3.simps}\\
+  @{thm inv_begin4.simps}
+  \end{center}
 
 
   measure for the copying TM, which we however omit.