--- a/Paper/Paper.thy	Mon Feb 04 11:14:03 2013 +0000
+++ b/Paper/Paper.thy	Mon Feb 04 21:11:43 2013 +0000
@@ -151,6 +151,14 @@
 using assms by auto
 
 
+lemma layout:
+  shows "layout_of [] = []"
+  and   "layout_of ((Inc R\<iota>)#os) = (2 * R\<iota> + 9)#(layout_of os)"
+  and   "layout_of ((Dec R\<iota> o\<iota>)#os) = (2 * R\<iota> + 16)#(layout_of os)"
+  and   "layout_of ((Goto o\<iota>)#os) = 1#(layout_of os)"
+by(auto simp add: layout_of.simps length_of.simps)
+
+
 (*>*)
 
 section {* Introduction *}
@@ -1162,6 +1170,15 @@
   this way it is easy to define a function @{term steps} that
   executes @{term n} statements of an abacus program.
   
+  The main point of abacus programs is to be able to translate them to 
+  Turing machine programs. Because of the jumps in abacus programs, it
+  seems difficult to build Turing machine programs using @{text "\<oplus>"}.
+  To overcome this difficulty we calculate a \emph{layout} as follows
+
+  \begin{center}
+  @{thm layout}
+  \end{center}
+
 
 
   %Running an abacus program means to start