Paper/Paper.thy
changeset 118 7d8a1bfb8925
parent 117 b27f4bd98078
child 119 892a3d7493aa
equal deleted inserted replaced
117:b27f4bd98078 118:7d8a1bfb8925
  1219   and adjust the following registers. By adjusting we only need to 
  1219   and adjust the following registers. By adjusting we only need to 
  1220   replace the first @{term Oc} of each number by @{term Bk} and the last
  1220   replace the first @{term Oc} of each number by @{term Bk} and the last
  1221   one from @{term Bk} to @{term Oc}.
  1221   one from @{term Bk} to @{term Oc}.
  1222   Finally we need to transition the head of the
  1222   Finally we need to transition the head of the
  1223   Turing machine back into the standard position. This requires a Turing machine
  1223   Turing machine back into the standard position. This requires a Turing machine
  1224   with 9 states. Similarly for the translation of @{term Dec}, where the 
  1224   with 9 states (we omit the details). Similarly for the translation of @{term Dec}, where the 
  1225   translated Turing machine needs to first check whether the content of the
  1225   translated Turing machine needs to first check whether the content of the
  1226   corresponding register is @{text 0}. For this we have a Turing machine program
  1226   corresponding register is @{text 0}. For this we have a Turing machine program
  1227   with @{text 16} states. 
  1227   with @{text 16} states. 
  1228 
  1228 
  1229   Finally, having a turing machine for each abacus instruction we need
  1229   Finally, having a turing machine for each abacus instruction we need