Paper/Paper.thy
changeset 123 d8f04ed7489e
parent 122 db518aba152a
child 124 bda714532263
equal deleted inserted replaced
122:db518aba152a 123:d8f04ed7489e
  1178   
  1178   
  1179   The main point of abacus programs is to be able to translate them to 
  1179   The main point of abacus programs is to be able to translate them to 
  1180   Turing machine programs. Registers and their content are represented by
  1180   Turing machine programs. Registers and their content are represented by
  1181   standard tapes. Because of the jumps in abacus programs, it
  1181   standard tapes. Because of the jumps in abacus programs, it
  1182   seems difficult to build a Turing machine programs out of components 
  1182   seems difficult to build a Turing machine programs out of components 
  1183   using our @{text "\<oplus>"}-operation.
  1183   using our @{text "\<oplus>"}-operation shown in the previous section.
  1184   To overcome this difficulty, we calculate a \emph{layout} as follows
  1184   To overcome this difficulty, we calculate a \emph{layout} as follows
  1185 
  1185 
  1186   \begin{center}
  1186   \begin{center}
  1187   \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  1187   \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
  1188   @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\
  1188   @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\