\begin{frame}{Encoding a PCP-Instance into a Formula}
  \begin{goal}{}
    Now given a PCP instance
    \begin{talign}
      \forestgreen{I} =
      \tuple{\pair{\forestgreen{w_1}}{\forestgreen{v_1}},
             \pair{\forestgreen{w_2}}{\forestgreen{v_2}},
             \ldots,
             \pair{\forestgreen{w_k}}{\forestgreen{v_k}}}
    \end{talign}
    \pause
    we encode $\forestgreen{I}$ into a formula $\aformi{\!\forestgreen{I}}$ of predicate logic as follows:
    \pause{}
    %
    \begin{align*}
      \aformi{\!\forestgreen{I}} 
        & \:\defdby\: 
        \formula{\logimp{\logand{\aformi{1}}{\aformi{2}}}{\aformi{3}}}
      \\[2ex]
      \mpause[1]{
        \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}}}}
      } \\
      \mpause{
        \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) }}}
      } \\
      \mpause{
        \aformi{3}
        & \:\defdby\:
        \formula{\existsst{z}{\:\binpred{P}{z}{z}}}
      }
    \end{align*}
  \end{goal}
  \smallskip\updatepause
  
  The idea behind $\sbinpred{P}$ is:
  \begin{talign}
    \binpred{P}{x}{y} \;\iff\; \text{$\pair{x}{y}$ can be constructed using dominos in $\forestgreen{I}$}
  \end{talign}
\end{frame}