--- a/Paper/Paper.thy	Sat Jan 26 01:36:48 2013 +0000
+++ b/Paper/Paper.thy	Sat Jan 26 11:50:40 2013 +0000
@@ -21,7 +21,7 @@
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
   update2 ("update") and
   tm_wf0 ("wf") and
-  is_even ("iseven") and
+  (*is_even ("iseven") and*)
   tcopy_init ("copy\<^bsub>begin\<^esub>") and
   tcopy_loop ("copy\<^bsub>loop\<^esub>") and
   tcopy_end ("copy\<^bsub>end\<^esub>") and
@@ -32,7 +32,7 @@
   abc_lm_s ("set") and*)
   haltP ("stdhalt") and 
   tcopy ("copy") and 
-  tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 
+  tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ \<oplus> _") and 
   DUMMY  ("\<^raw:\mbox{$\_$}>")
 
@@ -70,7 +70,14 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
-
+lemma nats2tape:
+  shows "<([]::nat list)> = []"
+  and "<[n]> = Oc \<up> (n + 1)"
+  and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
+apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac ns)
+apply(auto)
+done
 
 (*>*)
 
@@ -256,7 +263,7 @@
   scannes. This can be pictured as follows:
   %
   \begin{center}
-  \begin{tikzpicture}
+  \begin{tikzpicture}[scale=0.9]
   \draw[very thick] (-3.0,0)   -- ( 3.0,0);
   \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
@@ -274,8 +281,8 @@
   \draw[fill]     (-1.65,0.1) rectangle (-1.35,0.4);
   \draw (-0.25,0.8) -- (-0.25,-0.8);
   \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
-  \node [anchor=base] at (-0.8,-0.5) {\small left list};
-  \node [anchor=base] at (0.35,-0.5) {\small right list};
+  \node [anchor=base] at (-0.85,-0.5) {\small left list};
+  \node [anchor=base] at (0.40,-0.5) {\small right list};
   \node [anchor=base] at (0.1,0.7) {\small head};
   \node [anchor=base] at (-2.2,0.2) {\ldots};
   \node [anchor=base] at ( 2.3,0.2) {\ldots};
@@ -516,14 +523,24 @@
   
   \begin{figure}[t]
   \begin{center}
-  \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
-  @{thm (lhs) tcopy_init_def} @{text "\<equiv>"} &
-  @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"} &
+  \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
+  \begin{tabular}{@ {}l@ {}}
+  @{thm (lhs) tcopy_init_def} @{text "\<equiv>"}\\
+  @{text "["}@{text "(W0, 0), (R, 2), (R, 3),"}\\
+  \phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
+  \phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
+  \end{tabular}
+  &
+  \begin{tabular}{@ {}p{3.6cm}@ {}}
+  @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
+  @{thm (rhs) tcopy_loop_def}\\
+  \end{tabular}
+  &
+  \begin{tabular}{@ {}p{3.6cm}@ {}}
   @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
-  @{thm (rhs) tcopy_init_def} &
-  @{thm (rhs) tcopy_loop_def} &
   @{thm (rhs) tcopy_end_def}
   \end{tabular}
+  \end{tabular}
   \end{center}
   \caption{Copy machine}\label{copy}
   \end{figure}
@@ -535,17 +552,17 @@
   
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{thm (lhs) tape_of_nat_list.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(1)}\\
-  @{thm (lhs) tape_of_nat_list.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(2)}\\
-  @{thm (lhs) tape_of_nat_list.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(3)}
+  @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
+  @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
+  @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
   \end{tabular}
   \end{center}
 
   \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} 
+  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.
-
+  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.
 
   Before we can prove the undecidability of the halting problem for our
   Turing machines, we need to analyse two concrete Turing machine
@@ -606,7 +623,7 @@
   \begin{tabular}{l@ {\hspace{3mm}}lcl}
   & \multicolumn{1}{c}{start tape}\\[1mm]
   \raisebox{2.5mm}{halting case:} &
-  \begin{tikzpicture}
+  \begin{tikzpicture}[scale=0.9]
   \draw[very thick] (-2,0)   -- ( 0.75,0);
   \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
@@ -620,7 +637,7 @@
   \node [anchor=base] at (-1.7,0.2) {\ldots};
   \end{tikzpicture} 
   & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
-  \begin{tikzpicture}
+  \begin{tikzpicture}[scale=0.9]
   \draw[very thick] (-2,0)   -- ( 0.75,0);
   \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
@@ -635,7 +652,7 @@
   \end{tikzpicture}\\
 
   \raisebox{2.5mm}{non-halting case:} &
-  \begin{tikzpicture}
+  \begin{tikzpicture}[scale=0.9]
   \draw[very thick] (-2,0)   -- ( 0.25,0);
   \draw[very thick] (-2,0.5) -- ( 0.25,0.5);
   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);