\begin{frame}{PCP is Undecidable}
  \begin{block}{Theorem}
    \emph{Post's Correspondence Problem} is \alert{undecidable}.
  \end{block}
  \pause
  
  \begin{proof}[Idea of the Proof]
    The termination problem can be \emph{reduced to} PCP.\pause{}
    
    \medskip
    
    More precisely, there is a computable function $\dm{r}$ that maps
    instances of the termination problem to instances of PCP:\vspace*{-1ex}
    \begin{align*}
      \dm{r} \funin \;\;
      \pair{\forestgreen{P}}{\forestgreen{w}} 
        \;\; & \longmapsto \;\; 
      \mediumblue{I_{\pair{\forestgreen{P}}{\forestgreen{w}}}}
      \\[-1ex]
    \intertext{such that it holds:}
      \\[-4ex]
      \text{$\forestgreen{P}$ terminates on input $\forestgreen{w}$}
      \;\; &\Longleftrightarrow \;\;
      \text{$\mediumblue{I_{\pair{\forestgreen{P}}{\forestgreen{w}}}}$ has a solution}
    \end{align*}
    \pause\vspace*{-3ex}
    
    Then if we had a \emph{PCP-solver} (decides solvability of PCP-inst.) % (a solver for PCP-instances),
    we would obtain a \alert{solver for the termination problem.} $\;$ \alert{$\xmark$}
  \end{proof} 
\end{frame}