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