\begin{frame}{Checking Formula Satisfiability in a Model}
  \begin{exampleblock}{
      \black{$\model{\amodel} \satisfies \formula{\existsst{x}{\,\unpred{P}{x}}}$
      \hspace*{1.75ex} where \hspace*{1ex}
      \parbox[c]{0.3\textwidth}{
        \begin{tikzpicture}[dot/.style={minimum size=4mm, circle, draw=none, fill=black, inner sep=0, outer sep=1mm, text=white}]
          \node [dot,fill=forestgreen] (1) {1};
          \node [dot,below right of=1] (2) {2};
          \node [dot,above right of=2] (3) {3};
          %
          \draw [rounded corners=5mm,thick,dashed] 
                 ($(1) + (-6mm,7mm)$) rectangle ($(3) + (6mm,-13mm)$);
          \node [right of=3,node distance=9mm,yshift=6.5mm] {{$\model{\amodel}$}};  
          \node [right of=2,node distance=8.5mm,yshift=-2mm] {$\model{\adomain}$};     
        \end{tikzpicture}}
      \parbox[c]{0.21\textwidth}{%
        \mbox{}\\[0.5ex]
        $\model{\adomain} = \setexp{1,2,3}$\\[0.75ex]
        $\intin{\sunpred{P}}{\model{\amodel}} = \setexp{1}$} 
      }%
    }
  \pause{}     
      
  \begin{align*}
    &
    \model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\unpred{P}{x}}} \;\;\uncover<8->{\alert{\checkmark}}
    \\
    & \uncover<3->{
      \;\;\;\;\Longleftrightarrow\;\;
         \text{there is $\forestgreen{a}\in\model{\adomain}$ such that 
                        $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}$}}
    \\[-0.75ex]                    
    & & & \uncover<3->{\hspace*{-5ex}\text{(by def.\ of $\ssatisfies$)}}   
    \\
    & \uncover<4->{
      \;\;\;\;\Longleftrightarrow\;\;
         \parbox[t]{0.6\textwidth}
           {there is $\forestgreen{a}\in\model{\adomain}$ s.th.\ 
            $\intin{\freevar{x}}{\model{\amodel},\saluf[\freevar{x}\mapsto \forestgreen{a}]}\in\intin{\sunpred{P}}{\model{\amodel}}$
            %$\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}$
            }}                    
    & & \uncover<4->{\hspace*{-5ex}\text{(by def.\ of $\ssatisfies$)}}   
    \\
    & \uncover<5->{
      \;\;\;\;\Longleftrightarrow\;\;
         \text{there is $\forestgreen{a}\in\model{\adomain}$ such that 
                        $\forestgreen{a}\in\intin{\sunpred{P}}{\model{\amodel}}$}}
    & & \uncover<5->{\hspace*{-5ex}\text{(def.\ of $(\cdot)^{\model{\amodel},[\freevar{x}\mapsto \forestgreen{a}]}$)}}                 
    \\
    & \uncover<6->{%
      \;\;\;\;\Longleftarrow\;\;
        1\in\intin{\sunpred{P}}{\model{\amodel}}} \;\;\uncover<7->{\alert{\checkmark}}
    & & \hspace*{-5ex}
        \uncover<6->{\text{(by def.\ of $\model{\amodel}$)}}                    
  \end{align*}\pause{}%
  \uncover<9->{% 
  Hence we have formally established
  $\model{\amodel} \satisfies \formula{\existsst{x}{\,\unpred{P}{x}}}$.}
  %,\\ that is, $\model{\amodel},\saluf$ satisfies $\formula{\existsst{x}{\,\unpred{P}{x}}}$.}    
  \end{exampleblock}
\end{frame}