equal
deleted
inserted
replaced
607 @{thm tcontra_def} |
607 @{thm tcontra_def} |
608 \end{textblock} |
608 \end{textblock} |
609 |
609 |
610 \only<2>{ |
610 \only<2>{ |
611 \begin{itemize} |
611 \begin{itemize} |
612 \item Suppose @{text H} decides @{text contra} called with code |
612 \item Suppose @{text H} decides @{text contra} called with the code |
613 of @{text contra} halts, then\smallskip |
613 of @{text contra} halts, then\smallskip |
614 |
614 |
615 \begin{center}\small |
615 \begin{center}\small |
616 \begin{tabular}{@ {}l@ {}} |
616 \begin{tabular}{@ {}l@ {}} |
617 \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}} |
617 \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}} |
632 \end{tabular} |
632 \end{tabular} |
633 \end{center} |
633 \end{center} |
634 \end{itemize}} |
634 \end{itemize}} |
635 \only<3>{ |
635 \only<3>{ |
636 \begin{itemize} |
636 \begin{itemize} |
637 \item Suppose @{text H} decides @{text contra} called with code |
637 \item Suppose @{text H} decides @{text contra} called with the code |
638 of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{} |
638 of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{} |
639 |
639 |
640 \begin{center}\small |
640 \begin{center}\small |
641 \begin{tabular}{@ {}l@ {}} |
641 \begin{tabular}{@ {}l@ {}} |
642 \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}} |
642 \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}} |
717 \item sizes |
717 \item sizes |
718 |
718 |
719 \begin{center} |
719 \begin{center} |
720 \begin{tabular}{ll} |
720 \begin{tabular}{ll} |
721 & sizes:\smallskip\\ |
721 & sizes:\smallskip\\ |
722 UF & 140843 constructors\\ |
722 UF & @{text 140843} constructors\\ |
723 URM & @{text 2} Mio instructions\\ |
723 URM & @{text 2} Mio instructions\\ |
724 UTM & @{text 38} Mio states\\ |
724 UTM & @{text 38} Mio states\\ |
725 \end{tabular} |
725 \end{tabular} |
726 \end{center}\smallskip\pause |
726 \end{center}\smallskip\pause |
727 |
727 |
889 \begin{center} |
889 \begin{center} |
890 \begin{tabular}{l@ {\hspace{-10mm}}l} |
890 \begin{tabular}{l@ {\hspace{-10mm}}l} |
891 @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\ |
891 @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\ |
892 & @{text "\<forall> cf r."}\\ |
892 & @{text "\<forall> cf r."}\\ |
893 & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\ |
893 & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\ |
894 & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (run k cf)"} |
894 & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (steps k cf)"} |
895 \end{tabular} |
895 \end{tabular} |
896 \end{center}\bigskip\bigskip |
896 \end{center}\bigskip\bigskip |
897 |
897 |
898 \normalsize |
898 \normalsize |
899 @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"} |
899 @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"} |