\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}