\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{2} \defdby \formula{\forallst{x}{\forallst{y}{ \bigl( \binpred{P}{x}{y} \logimpinf 
       \bigwedge_{i=1,\ldots,k} \binpred{P}{\unfunci{f}{\forestgreen{w_i}}{x}}{\unfunci{f}{\forestgreen{v_i}}{y}}
     \bigr) }}}$:
    \pause\vspace{-.5ex}
    \begin{talign}
      & \amodel \satisfieslookup{\saluf} \aformi{2} 
      \mpause[1]{
      \;\;\Longleftrightarrow\;\; \ldots\\[-.25ex]
      & \Longleftrightarrow\;\;
        \Big( \text{$\forall w,v \in \model{{B}}\,$:
            $\pair{w}{v} \in \intin{\sbinpred{P}}{\amodel} \Longrightarrow
             \textstyle\bigwedge_{i=1,\ldots,k} 
             \pair{\forestgreen{w_i}w}{\forestgreen{v_i}v} \in \intin{\sbinpred{P}}{\amodel}$}
        \Big)
      } \\[-.25ex]
      \mpause{
      & \Longleftrightarrow\;\;
        \Big(
        \begin{aligned}[t]  
          &
          \pair{\forestgreen{w}_{i_1}\cdots \forestgreen{w}_{i_n}}
               {\forestgreen{v}_{i_1}\cdots \forestgreen{v}_{i_n}}
            \in\intin{\sbinpred{P}}{\amodel}
          \\[-1ex]
          &\quad\Longrightarrow
          \pair{\forestgreen{w_i}\forestgreen{w}_{i_1}\cdots \forestgreen{w}_{i_n}}
               {\forestgreen{v_i}\forestgreen{v}_{i_1}\cdots \forestgreen{v}_{i_n}}
            \in\intin{\sbinpred{P}}{\model{\amodeli{\!\forestgreen{I}}}}
          \;\;\Big)
          \mpause{ \hspace*{1.5ex}\alert{\checkmark} }
        \end{aligned}
      }
    \end{talign}
  \end{goal}
  \vspace{10cm}
\end{frame}