43/162
\begin{frame}[t]
\frametitle{Termination is Undecidable (Structure of Argument)}

\begin{block}{Theorem}
\end{block}
\vspace{-3ex}
\begin{talign}
\mhide[10]{
\mpause[1]{
\text{$\terminator$ outputs \alert{yes} on input $\pair{\forestgreen{P}}{\forestgreen{w}}$}
\;\;& \overset{ \mat{time:undefined:fail}{\mpause[?+1]{ \textcolor{red}{\huge\xmark} }} }{ \Longleftrightarrow } \;\;
\text{$\forestgreen{P}$ halts on input $\forestgreen{w}$}
} \\[-.95ex]
\mpause{ & \;\; \Downarrow } \\[-.95ex]
\mpause{
\text{$\terminatoronitself$ outputs \alert{yes} on input $\forestgreen{P}$}
\;\; & \Longleftrightarrow \;\;
\text{$\forestgreen{P}$ halts on input $\forestgreen{P}$}
} \\[-.95ex]
\mpause{& \;\; \Downarrow} \\[-2.45ex]
}
\mpause{
\text{$\diagonalisator$ halts on input $\forestgreen{P}$}
\;\; &  \overset{ \mpause[?+5]{ \textcolor{red}{\huge\xmark} } }{ \Longleftrightarrow } \;\;
\text{$\forestgreen{P}$ does \alert{not} halt on input $\forestgreen{P}$}
} \\[-.95ex]
\mpause{ & \;\; \Downarrow} \\[-.95ex]
\mpause{
\text{$\diagonalisator$ halts on input $\diagonalisator$}
\;\; & \underset{ \mpause[?+1]{\textcolor{red}{\huge\xmark}\mtime{time:undefined:fail}} }{ \Longleftrightarrow } \;\;
\text{$\diagonalisator$ does \alert{not} halt on input $\diagonalisator$}
}
\mpause[+3]{
\text{\firebrick{barber} shaves $\forestgreen{x}$}
\text{$\forestgreen{x}$ does \alert{not} shave $\forestgreen{x}$} \\[-.95ex]