8/183
\begin{frame}<10>
  \frametitle{Proving Logical Equivalence}
  
  \begin{exampleblock}
        {\begin{center}
          \black{%
          $\satstmt{%
           \formula{\lognot{\forallst{x}{\,\unpred{P}{x}}}}
            \logequiv
          \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}}}}
     \logequiv
   \formula{\existsst{x}{\,\lognot{\unpred{P}{x}}}}}$.}  
    
  \end{exampleblock}  
  
  Note that each step is a bi-implication, so we have $\reflectbox{$\satisfies$}$ and $\satisfies$.
%   \begin{exampleblock}
%         {\begin{center}
%           \black{%
%           $\satstmt{%
%            \formula{\lognot{\existsst{x}{\,\unpred{P}{x}}}}
%             \logequiv
%           \formula{\forallst{x}{\,\lognot{\unpred{P}{x}}}}}$}
%          \end{center}}
%    
%   \medskip       
%   For all models $\model{\amodel}$ with domain $\model{\adomain}$ and all environments $\saluf$ we find:
%   \begin{align*}
%     &
%     \model{\amodel} \satisfieslookup{\saluf} \formula{\lognot{\existsst{x}{\,\unpred{P}{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{not:} \;\;
%         \model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\unpred{P}{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{there does not exist $\forestgreen{a}\in\model{\adomain}\,$:} \;\;
%          \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{for all $\forestgreen{a}\in\model{\adomain}$ it holds:} \;\;
%          \model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{P}{\freevar{x}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \text{for all $\forestgreen{a}\in\model{\adomain}$ it holds:} \;\;
%          \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\lognot{\unpred{P}{\freevar{x}}}}}
%     \\
%     & \uncover<1->{%
%       \hspace*{2ex} \;\;\Longleftrightarrow\;\;
%       \model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\lognot{\unpred{P}{x}}}}}
%   \end{align*}
%   
%   \uncover<1->{%
%   Hence we can conclude:
%   $\satstmt{%
%    \formula{
%            \lognot{\existsst{x}{\,\unpred{P}{x}}}}
%              \logequiv
%           \formula{\forallst{x}{\,\lognot{\unpred{P}{x}}}}}$.} 
%     
%   \end{exampleblock}  
\end{frame}