diff -r 6ffd6880dad7 -r 199cf7ce1169 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 03:19:36 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 03:33:32 2013 +0000
@@ -1367,7 +1367,13 @@
   @{thm (concl) UTM_unhalt_lemma2} 
   \end{center}
 
-  \noindent
+  Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully
+  we can strengthen this result slightly by observing that @{text m} is at most
+  2 in the output tape. This observation allows one to construct a UTM that works
+  entirely on the left-tape by composing it with a machine that drags the tape
+  two cells to the right. A corolary is that one-sided Turing machines (where the
+  tape only extends to the right) are as powerful as our two-sided Turing machines. 
+
   While formalising the chapter about universal Turing machines in \cite{Boolos87}
   we noticed that they use their definition about what function Turing machines
   calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}: