63   tcopy_end ("cend") and

    63   tcopy_end ("cend") and

    64   step0 ("step") and

    64   step0 ("step") and

    65   tcontra ("contra") and

    65   tcontra ("contra") and

    66   code_tcontra ("code contra") and

    66   code_tcontra ("code contra") and

    67   steps0 ("steps") and

    67   steps0 ("steps") and

    68   exponent ("_\<^bsup>_\<^esup>") and

    69   exponent ("_\<^bsup>_\<^esup>") and

    69   tcopy ("copy") and 

    70   tcopy ("copy") and 

    70   tape_of ("\<langle>_\<rangle>") and 

    71   tape_of ("\<langle>_\<rangle>") and 

    71   tm_comp ("_ \<oplus> _") and 

    72   tm_comp ("_ \<oplus> _") and 

    72   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and

    73   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and

   160   shows "layout_of [] = []"

   161   shows "layout_of [] = []"

   161   and   "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"

   162   and   "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"

   162   and   "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"

   163   and   "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"

   163   and   "layout_of ((Goto l)#is) = 1#(layout_of is)"

   164   and   "layout_of ((Goto l)#is) = 1#(layout_of is)"

   164 by(auto simp add: layout_of.simps length_of.simps)

   165 by(auto simp add: layout_of.simps length_of.simps)

   165 

   171 

   166 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

   172 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

   167   where

   173   where

   168   "clear n e = [Dec n e, Goto 0]"

   174   "clear n e = [Dec n e, Goto 0]"

   169 (*>*)

   175 (*>*)

   550   slightly fiddly. We use the following two auxiliary functions:

   556   slightly fiddly. We use the following two auxiliary functions:

   551 

   557 

   552   \begin{center}

   558   \begin{center}

   553   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

   559   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

   554   @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\

   560   @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\

   556   \end{tabular}

   562   \end{tabular}

   557   \end{center}

   563   \end{center}

   558 

   564 

   559   \noindent

   565   \noindent

   560   The first adds @{text n} to all states, except the @{text 0}-state,

   566   The first adds @{text n} to all states, except the @{text 0}-state,