\begin{frame}{Proving Semantic Entailment}
  \begin{exampleblock}
        {\begin{center}
          \black{%
          $\satstmt{%
           \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}}
            \satisfies
          \formula{\existsst{x}{\,\lognot{\unpred{P}{x}}}}}$}
         \end{center}}\pause{}
   
  \medskip       
  For all models $\model{\amodel}$ with domain $\model{\adomain}$ and environments $\saluf$ we find:\pause{}
  \begin{align*}
    &
    \model{\amodel} \satisfieslookup{\saluf} \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}}
    \\
    & \uncover<4->{%
      \hspace*{2ex} \;\;\Longleftrightarrow\;\;
      \text{not:} \;\;
        \model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\unpred{P}{x}}}}
    \\
    & \uncover<5->{%
      \hspace*{2ex} \;\;\Longleftrightarrow\;\;
      \text{not for all $\forestgreen{a}\in\model{\adomain}\,$:} \;\;
         \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
    \\
    & \uncover<6->{%
      \hspace*{2ex} \;\;\Longleftrightarrow\;\;
      \text{there exists $\forestgreen{a}\in\model{\adomain}$ such that not:} \;\;
         \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
    \\
    & \uncover<7->{%
      \hspace*{2ex} \;\;\Longleftrightarrow\;\;
      \text{there exists $\forestgreen{a}\in\model{\adomain}$ such that:} \;\;
         \model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
    \\
    & \uncover<8->{%
      \hspace*{2ex} \;\;\Longleftrightarrow\;\;
      \text{there exists $\forestgreen{a}\in\model{\adomain}$ such that:} \;\;
         \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\lognot{\unpred{P}{\freevar{x}}}}}
    \\
    & \uncover<9->{%
      \hspace*{2ex} \;\;\Longleftrightarrow\;\;
      \model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\lognot{\unpred{P}{x}}}}}
  \end{align*}
  
  \uncover<10->{%
  Hence we can conclude:
  $\satstmt{%
   \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}}
     \satisfies
   \formula{\existsst{x}{\,\lognot{\unpred{P}{x}}}}}$.}  
    
  \end{exampleblock}  
\end{frame}