equal
deleted
inserted
replaced
581 @{thm dither_halts}\\ |
581 @{thm dither_halts}\\ |
582 @{thm dither_loops} |
582 @{thm dither_loops} |
583 \end{tabular} |
583 \end{tabular} |
584 \end{center} |
584 \end{center} |
585 |
585 |
586 \noindet |
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, Oc])"} loops. |
590 |
590 |
591 |
591 |