\begin{frame}
  \frametitle{Proving Semantic Entailment}
  
  \begin{exampleblock}{}
    \begin{malign}
      \formula{\existsst{y}{\forallst{x}{\,\binpred{R}{x}{y}}}}
      \satisfies
      \formula{\forallst{x}{\existsst{y}{\,\binpred{R}{x}{y}}}}
    \end{malign}
    \pause
    
    For all models $\model{\amodel}$ with domain $\model{\adomain}$ and environments $\saluf$ we find:
    \pause{}\vspace*{-1ex}
    \begin{align*}
      &
      \model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{y}{\forallst{x}{\,\binpred{R}{x}{y}}}}
      \\
      & \uncover<4->{%
        \hspace*{2ex} \;\;\Longleftrightarrow\;\;
        \text{there is $\forestgreen{b}\in\model{\adomain}$ such that
          $\model{\amodel} \satisfieslookup{\saluf[\freevar{y}\mapsto\forestgreen{b}]} \formula{\forallst{x}{\,\binpred{R}{x}{\freevar{y}}}}$}}
      \\
      & \uncover<5->{%
        \hspace*{2ex} \;\;\Longleftrightarrow\;\;
        \parbox[t]{0.75\textwidth}
                  {there is $\forestgreen{b}\in\model{\adomain}$ such that for all $\forestgreen{a}\in\model{\adomain}$:
                   \\[-0.2ex]\hspace*{\fill} 
                   $\model{\amodel} 
                      \satisfieslookup{\saluf[\freevar{y}\mapsto\forestgreen{b}][\freevar{x}\mapsto\forestgreen{a}]} 
                    \formula{\,\binpred{R}{\freevar{x}}{\freevar{y}}}$}}
      \\
      & \uncover<6->{%
        \hspace*{2ex} \;\;\:\Longrightarrow\;\;
        \parbox[t]{0.75\textwidth}
                  {for all $\forestgreen{a}\in\model{\adomain}$ there is $\forestgreen{b}\in\model{\adomain}$ such that:
                   \\[-0.2ex]\hspace*{\fill} 
                   $\model{\amodel} 
                      \satisfieslookup{\saluf[\freevar{y}\mapsto\forestgreen{b}][\freevar{x}\mapsto\forestgreen{a}]} 
                    \formula{\binpred{R}{\freevar{x}}{\freevar{y}}}$}}
      \\
      & \uncover<7->{%
        \hspace*{2ex} \;\;\Longleftrightarrow\;\;
        \parbox[t]{0.75\textwidth}
                  {for all $\forestgreen{a}\in\model{\adomain}$ there is $\forestgreen{b}\in\model{\adomain}$ such that:
                   \\[-0.2ex]\hspace*{\fill} 
                   $\model{\amodel} 
                      \satisfieslookup{\saluf[\freevar{x}\mapsto\forestgreen{a}][\freevar{y}\mapsto\forestgreen{b}]} 
                    \formula{\binpred{R}{\freevar{x}}{\freevar{y}}}$}}
      \\
      & \uncover<8->{%
        \hspace*{2ex} \;\;\:\Longleftrightarrow\;\;
        \parbox[t]{0.75\textwidth}
                  {for all $\forestgreen{a}\in\model{\adomain}$: $\,$
                   $\model{\amodel} 
                      \satisfieslookup{\saluf[\freevar{x}\mapsto\forestgreen{a}]} 
                    \formula{\existsst{y}{\,\binpred{R}{\freevar{x}}{y}}}$}}
      \\
      & \uncover<9->{%
        \hspace*{2ex} \;\;\:\Longleftrightarrow\;\;
        \parbox[t]{0.75\textwidth}
                  {$\model{\amodel} 
                      \satisfieslookup{\saluf} 
                    \formula{\forallst{x}{\existsst{y}{\,\binpred{R}{x}{y}}}}$}}
    \end{align*}
    
    \uncover<10->{%
    Hence we can conclude: $\,$
    $\formula{\existsst{y}{\forallst{x}{\,\binpred{R}{x}{y}}}}
     \satisfies
     \formula{\forallst{x}{\existsst{y}{\,\binpred{R}{x}{y}}}}$.}
  \end{exampleblock}  
\end{frame}