529 \end{figure} |
529 \end{figure} |
530 |
530 |
531 We often need to restrict tapes to be in \emph{standard form}, which means |
531 We often need to restrict tapes to be in \emph{standard form}, which means |
532 the left list of the tape is either empty or only contains @{text "Bk"}s, and |
532 the left list of the tape is either empty or only contains @{text "Bk"}s, and |
533 the right list contains some ``clusters'' of @{text "Oc"}s separted by single |
533 the right list contains some ``clusters'' of @{text "Oc"}s separted by single |
534 blanks and can be followed by some blanks. To make this formal we define the |
534 blanks. To make this formal we define the following function |
535 following function |
535 |
536 |
536 \begin{center} |
537 \begin{center} |
537 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
538 foo |
538 @{thm (lhs) tape_of_nat_list.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(1)}\\ |
539 \end{center} |
539 @{thm (lhs) tape_of_nat_list.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(2)}\\ |
540 |
540 @{thm (lhs) tape_of_nat_list.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(3)} |
541 \noindent |
541 \end{tabular} |
542 A standard tape is then of the form @{text "(Bk\<^isup>k,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle> @ Bk\<^isup>l)"} for some @{text k}, |
542 \end{center} |
543 @{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the |
543 |
|
544 \noindent |
|
545 A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle>)"} for some @{text l} |
|
546 and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the |
544 leftmost @{term "Oc"} on the tape. |
547 leftmost @{term "Oc"} on the tape. |
545 |
548 |
546 |
549 |
547 Before we can prove the undecidability of the halting problem for our |
550 Before we can prove the undecidability of the halting problem for our |
548 Turing machines, we need to analyse two concrete Turing machine |
551 Turing machines, we need to analyse two concrete Turing machine |