\begin{frame}[t]{Example (4)}
  \examplemodel
  \pause\medskip

  We use the formal definition to check
  $\model{\amodel} \satisfies \formula{\logor{\binpred{R}{\const{c}}{\const{c}}}{\unpred{P}{\const{c}}}}$:
  \pause
  \begin{talign}
    \model{\amodel} &\satisfies \formula{\logor{\binpred{R}{\const{c}}{\const{c}}}{\unpred{P}{\const{c}}}}
      \;\;\mpause[7]{\alert{\checkmark}}
    \\
    \mpause[-6]{
      &\iff
        \model{\amodel} \satisfies \binpred{R}{\const{c}}{\const{c}}
        \;\text{ or }\;
        \model{\amodel} \satisfies \unpred{P}{\const{c}}
      && \hspace*{-13ex}\text{(by definition of $\satisfies$)} }
    \\
    \mpause{
      &\iff
        \pair{\intin{\const{c}}{\model{\amodel}}}{\intin{\const{c}}{\model{\amodel}}} 
        \in \intin{\sunpred{R}}{\model{\amodel}}  
        \;\text{ or }\;   
        \intin{\const{c}}{\model{\amodel}} \in \intin{\sunpred{P}}{\model{\amodel}}
      && \hspace*{-13ex}\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}}
      \\
      &\phantom{\iff\;}
        \text{ or } \; a_3 \in \setexp{a_1,\,a_2} \;\;\mpause{\alert{\xmark}}  
                                                   \hspace*{8ex}\mpause{\alert{\checkmark}}  
      && \hspace*{-13ex}\text{(by definition of $\model{\amodel}$)} }
  \end{talign}
  \updatepause\pause
  %
  Hence we conclude: 
  $\model{\amodel} \satisfies \formula{\logor{\binpred{R}{\const{c}}{\const{c}}}{\unpred{P}{\const{c}}}}$.
\end{frame}

\theme{Interpretation \\[1ex]
  {\large of formulas \alert{with} quantifiers and free variables}}