\begin{frame}[t]{Examle (3)}
  \examplemodel
  \pause\medskip

  We use the formal definition to check
  $\model{\amodel} \satisfies \formula{\binpred{R}{\const{c}}{\const{c}}}$:
  \pause
  \begin{talign}
    \model{\amodel} &\satisfies \formula{\binpred{R}{\const{c}}{\const{c}}} \;\;\mpause[4]{\alert{\checkmark}}
    \\
    \mpause[-3]{
      &\iff \pair{\intin{\const{c}}{\model{\amodel}}}{\intin{\const{c}}{\model{\amodel}}} 
             \in \intin{\sunpred{R}}{\model{\amodel}}
      && \hspace*{-15ex}\text{(by definition of $\satisfies$)}}     
    \\
    \mpause{
      &\iff \pair{a_3}{a_3} \in \setexp{\pair{a_1}{a_2}, \pair{a_1}{a_3}, \pair{a_3}{a_2}, \pair{a_3}{a_3} }
            \;\;\mpause{\alert{\checkmark}}
    \\[-0.25ex]    
    &&& \hspace*{-15ex}\text{(by definition of $\model{\amodel}$)}
    }
  \end{talign}
  \updatepause\pause
  Hence we conclude: 
  $\model{\amodel} \satisfies \formula{\binpred{R}{\const{c}}{\const{c}}}$.
\end{frame}