\begin{frame}{Encoding a PCP-Instance into a Formula}
  \begin{center}
    \scalebox{.8}{
    \begin{minipage}{\textwidth}
      \understandmodel{}
    \end{minipage}
    }
  \end{center}
  \pause\smallskip
  
  \begin{goal}{}
  Interpreting $\aformi{3} \defdby \formula{\existsst{z}{\:\binpred{P}{z}{z}}}$ in $\amodel$ we find:
  \pause
  \begin{align*}
    \amodel \satisfieslookup{\saluf} \aformi{3}
    \mpause[1]{
      \;\;&\Longleftrightarrow\;\;
      \text{there is a $w\in\model{B}$ such that $\pair{w}{w} \in \intin{\sbinpred{P}}{\amodel}$}
    } \\
    \mpause{
      \;\;&\Longleftrightarrow\;\;
      \parbox[t]{0.7\textwidth}{
        there is a sequence \!$\tuple{i_1,i_2,\ldots,i_n}$\! of indices\\
        such that $\forestgreen{w}_{i_1}\forestgreen{w}_{i_2}\cdots \forestgreen{w}_{i_n} =
                   \forestgreen{v}_{i_1}\forestgreen{v}_{i_2}\cdots \forestgreen{v}_{i_n}$}  
    } \\
    \mpause{
      \;\;&\Longleftrightarrow\;\;
      \text{PCP instance $\forestgreen{I}$ is solvable}
    }
  \end{align*}
  \end{goal}
  \vspace{10cm}
\end{frame}