548 defined as |
548 defined as |
549 |
549 |
550 \begin{center} |
550 \begin{center} |
551 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
551 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
552 \begin{tabular}[t]{@ {}l@ {}} |
552 \begin{tabular}[t]{@ {}l@ {}} |
553 @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\ |
553 @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\[1mm] |
554 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
554 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
555 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
555 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
556 \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\ |
556 \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\ |
557 \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
557 \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
558 \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} |
558 \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} |
559 \end{tabular} & |
559 \end{tabular} & |
560 \begin{tabular}[t]{@ {}l@ {}} |
560 \begin{tabular}[t]{@ {}l@ {}} |
561 @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\ |
561 @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\[1mm] |
562 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
562 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
563 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
563 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
564 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
564 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
565 \end{tabular} |
565 \end{tabular} |
566 \end{tabular} |
566 \end{tabular} |
584 \end{center} |
584 \end{center} |
585 |
585 |
586 \noindent |
586 \noindent |
587 {\it unfold} The first states that on a tape @{term "(Bk \<up> n, [Oc, Oc])"} |
587 {\it unfold} The first states that on a tape @{term "(Bk \<up> n, [Oc, Oc])"} |
588 halts in tree steps leaving the tape unchanged. In the other states |
588 halts in tree steps leaving the tape unchanged. In the other states |
589 that @{term dither} started with tape @{term "(Bk \<up> n, [Oc, Oc])"} loops. |
589 that @{term dither} started with tape @{term "(Bk \<up> n, [Oc])"} loops. |
590 |
590 |
591 |
591 |
592 |
592 |
593 In the following we will consider the following Turing machine program |
593 In the following we will consider the following Turing machine program |
594 that makes a copies a value on the tape. |
594 that makes a copies a value on the tape. |