diff -r 839e37b75d9a -r 4b35e0e0784b Paper.thy
--- a/Paper.thy	Sat Jan 12 01:33:20 2013 +0000
+++ b/Paper.thy	Sat Jan 12 02:14:29 2013 +0000
@@ -73,7 +73,7 @@
 
 lemma change_termi_state_def2:
  "change_termi_state p  == 
-  (map (\<lambda> (a, s). (a, if s = 0 then Suc ((length s) div 2)) else s) t)"
+  (map (\<lambda> (a, s). (a, if s = 0 then ((length p) div 2) + 1 else s)) p)"
 apply(rule eq_reflection)
 apply(auto simp add: change_termi_state.simps)
 done
@@ -93,8 +93,10 @@
   abc_lm_v ("lookup") and
   abc_lm_s ("set") and
   haltP ("stdhalt") and 
+  tshift ("shift") and 
   change_termi_state ("adjust") and
   tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 
+  t_add ("_ \<oplus> _") and 
   DUMMY  ("\<^raw:\mbox{$\_$}>")
 
 declare [[show_question_marks = false]]
@@ -531,18 +533,29 @@
   clustered on the output tape).
 
   Before we can prove the undecidability of the halting problem for Turing machines, 
-  we have to define how to compose Turing machines. Given our setup, this is relatively 
-  straightforward, if slightly fiddly.
+  we have to define how to compose two Turing machines. Given our setup, this is 
+  relatively straightforward, if slightly fiddly. We have the following two
+  auxiliary functions:
 
   \begin{center}
-  @{thm tshift_def2}
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) tshift_def2} @{text "\<equiv>"}\\
+  \hspace{4mm}@{thm (rhs) tshift_def2}\\
+  @{thm (lhs) change_termi_state_def2} @{text "\<equiv>"}\\
+  \hspace{4mm}@{text "map (\<lambda> (a, s)."}\\
+  \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\
+  \end{tabular}
   \end{center}
 
-  (* HERE *)
+  \noindent
+  With this we can define the \emph{sequential composition} of two
+  Turing machines @{text "M\<^isub>1"} and @{text "M\<^isub>2"}
 
-  shift and change of a p
+  \begin{center}
+  @{thm t_add.simps[where ?t1.0="M\<^isub>1" and ?t2.0="M\<^isub>2", THEN eq_reflection]}
+  \end{center}
 
-  composition of two ps
+
 
   assertion holds for all tapes