--- a/Paper/Paper.thy	Thu Feb 14 09:31:19 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 14 12:11:40 2013 +0000
@@ -1258,7 +1258,7 @@
   register (the one with the highest register). That means we have to append a Turing machine that
   ``mops up'' the tape (cleaning all @{text Oc}s) except for the
   @{term Oc}s of the last register represented on the tape. This needs
-  a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R}
+  a Turing machine program with @{text "2 * R + 6"} states, assuming @{text R}
   is the number of registers to be ``cleaned''.
 
   While generating the Turing machine program for an abacus program is
@@ -1563,7 +1563,7 @@
   involved with constructing a universal Turing machine via recursive
   functions and abacus machines, we agree, is not a project
   one wants to undertake too many times (our formalisation of abacus
-  machines and their correct translation is approximately 4300 loc;
+  machines and their correct translation is approximately 4600 loc;
   recursive functions 5000 loc and the universal Turing machine 10000 loc).
   
   Our work is also very much inspired by the formalisation of Turing