\begin{frame}[t]{Example (2)}
  \examplemodel
  \pause\medskip
    
  We use the formal definition to check
  $\model{\amodel} \satisfies \lognot{\formula{\unpred{P}{\const{c}}}}$:
  \pause
  \begin{talign}
    \model{\amodel} &\satisfies \formula{\lognot{\unpred{P}{\const{c}}}} \;\;\mpause[6]{\alert{\checkmark}} 
    \\
    \mpause[-5]{
      &\iff \text{not: } \model{\amodel} \satisfies \formula{\unpred{P}{\const{c}}}
      &&\text{(by definition of $\satisfies$)}}
    \\
    \mpause{
      &\iff \text{not: } \intin{\const{c}}{\model{\amodel}} \in \intin{\sunpred{P}}{\model{\amodel}}
      &&\text{(by definition of $\satisfies$)}}
    \\
    \mpause{
      &\iff \intin{\const{c}}{\model{\amodel}} \notin \intin{\sunpred{P}}{\model{\amodel}}}
    \\
    \mpause{
      &\iff a_3 \notin \setexp{a_1,\,a_2} \;\;\mpause{\alert{\checkmark}}
      &&\text{(by definition of $\model{\amodel}$)}}
  \end{talign}%
  \updatepause\pause
  Hence we conclude: 
  $\model{\amodel} \satisfies \formula{\lognot{\unpred{P}{\const{c}}}}$.
\end{frame}