\begin{frame}[t]{Example (1)}
  \examplemodel
  \pause\medskip
       
  We use the formal definition to check
  $\model{\amodel} \satisfies \formula{\unpred{P}{\const{c}}}$
  or 
  $\model{\amodel} \satisfiesnot \formula{\unpred{P}{\const{c}}}$:
  \pause
  \begin{talign}
    \model{\amodel} &\satisfies \formula{\unpred{P}{\const{c}}}  \;\;\mpause[4]{\alert{\xmark}} 
    \\
    \mpause[-3]{
      &\iff \intin{\const{c}}{\model{\amodel}} \in \intin{\sunpred{P}}{\model{\amodel}}
      && \text{(by definition of $\satisfies$)} }
    \\
    \mpause{
      &\iff a_3 \in \setexp{a_1,\,a_2}}  \;\;\mpause{\alert{\xmark}}
      && \mpause[-1]{\text{(by definition of $\model{\amodel}$)}}
  \end{talign}
  \updatepause\pause\pause
  Hence we indeed conclude: 
  $\model{\amodel} \satisfiesnot \formula{\unpred{P}{\const{c}}}$.
\end{frame}