\begin{frame}{Encoding a PCP-Instance into a Formula}
  So we have shown:
  \begin{talign}
     \amodel &\satisfies \aformi{1} \\  
     \amodel &\satisfies \aformi{2} \\
     \amodel &\satisfies \aformi{3} \;\;\Longleftrightarrow\;\; \text{$\forestgreen{I}$ is solvable}  
  \end{talign}
  \pause
  
  Hence we conclude:
  \pause
  \begin{talign}
     \amodel \satisfies \aformi{\!\forestgreen{I}}
     \mpause[1]{
       & \;\;\Longleftrightarrow\;\; 
       \amodel \satisfies \formula{\logimp{\logand{\aformi{1}}{\aformi{2}}}{\aformi{3}}}
     } \\
     \mpause{
       & \;\;\Longleftrightarrow\;\;
       \text{$\forestgreen{I}$ is solvable}
     }
  \end{talign}
  \updatepause
  
  and furthermore:
  \pause
  \begin{talign}
    \text{$\aformi{\!\forestgreen{I}}$ is valid}
    \mpause[1]{
      & \;\;\Longrightarrow\;\; 
      \amodel \satisfies \aformi{\forestgreen{I}}
    } \\ 
    \mpause{
      & \;\;\Longrightarrow\;\;
      \text{$\forestgreen{I}$ is solvable}
    }
  \end{talign}
\end{frame}