--- a/Paper/Paper.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -65,6 +65,7 @@
   tcontra ("contra") and
   code_tcontra ("code contra") and
   steps0 ("steps") and
+  adjust0 ("adjust") and
   exponent ("_\<^bsup>_\<^esup>") and
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
@@ -163,6 +164,11 @@
   and   "layout_of ((Goto l)#is) = 1#(layout_of is)"
 by(auto simp add: layout_of.simps length_of.simps)
 
+
+lemma adjust_simps:
+  shows "adjust0 p = map (\<lambda>(a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
+by(simp add: adjust.simps)
+
 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
   "clear n e = [Dec n e, Goto 0]"
@@ -552,7 +558,7 @@
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
-  @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
+  @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\
   \end{tabular}
   \end{center}