\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{1} \defdby \formula{\bigwedge_{i=1,\ldots,k} \binpred{P}{\unfunci{f}{\forestgreen{w_i}}{\const{e}}}{\unfunci{f}{\forestgreen{v_i}}{\const{e}}}}$
  in $\amodel$ we find:
  \pause
  \begin{align*}
    \amodel \satisfieslookup{\saluf} \aformi{1} 
    \mpause[1]{
      \;\;&\Longleftrightarrow\;\;
      \text{$\forall i$ with $1\le i\le k$: 
            $\amodel \satisfieslookup{\saluf} 
             \formula{\binpred{P}{\unfunci{f}{\forestgreen{w_i}}{\const{e}}}{\unfunci{f}{\forestgreen{v_i}}{\const{e}}}}$}
    } \\
    \mpause{
      \;\;&\Longleftrightarrow\;\;
      \text{$\forall i$ with $1\le i\le k$: 
            $\pair{\intin{(\formula{\unfunci{f}{\forestgreen{w_i}}{\const{e}}})}{\amodel}}
                  {\intin{(\formula{\unfunci{f}{\forestgreen{v_i}}{\const{e}}})}{\amodel}} 
               \in \intin{\sbinpred{P}}{\amodel}$}
    } \\
    \mpause{
      \;\;&\Longleftrightarrow\;\;
      \text{$\forall i$ with $1\le i\le k$: 
            $\pair{\forestgreen{w_i}}{\forestgreen{v_i}}  \in \intin{\sbinpred{P}}{\amodel}$} 
    } 
    \hspace*{1.5ex} \mpause{\alert{\checkmark}}
  \end{align*}
  \end{goal}
  \vspace{10cm}
\end{frame}