--- a/Paper/Paper.thy	Tue Feb 05 08:58:30 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 09:17:06 2013 +0000
@@ -1170,7 +1170,9 @@
   Turing machines, we fetch instructions from an abacus program such
   that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
   this way it is easy to define a function @{term steps} that
-  executes @{term n} instructions of an abacus program.
+  executes @{term n} instructions of an abacus program. By convention
+  the value calculated by an abacus program is stored in the
+  last register (the register with the highest index).
   
   The main point of abacus programs is to be able to translate them to 
   Turing machine programs. Registers and their content are represented by
@@ -1229,8 +1231,13 @@
   Finally, having a turing machine for each abacus instruction we need
   to ``stitch'' the Turing machines together into one so that each
   Turing machine component transitions to next one, just like in
-  are needed to translate each abacus instructionabacus
-  programs. While generating the Turing machine program for an abacus
+  the abacus programs. One last problem to overcome is that an abacus
+  program is assumed to calculate a value stored in the last
+  register. That means we have to append a Turing machine that
+  ``mops up'' the tape (cleaning all @{text Oc}s) except for the
+  last number represented on the tape.
+
+  While generating the Turing machine program for an abacus
   program is not too difficult to formalise, the problem is that it
   contains @{text Goto}s all over the place. The unfortunate result is
   are needed to translate each abacus instructionthat we cannot

Binary file paper.pdf has changed