--- 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}: