\begin{frame}[t]{
    $\formula{\forallst{x}{(\logimp{\unpred{LL}{x}}{\unpred{C}{x}})}}
     \;\lognotequiv\;
     \formula{\logimp{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$
  }

  \vspace{-1.5ex}
  \begin{exampleblock}{}
    Model $\model{\amodel}$ with
    $\model{\adomain} = \setexp{1,2}$, 
    $\intin{\sunpred{LL}}{\model{\amodel}} = \setexp{1}$,
    $\intin{\sunpred{C}}{\model{\amodel}} = \setexp{2}$    
  \end{exampleblock}
  \pause
  
  \begin{block}{$\model{\amodel} \satisfiesnot \formula{\forallst{x}{(\logimp{\unpred{LL}{x}}{\unpred{C}{x}})}}$}
    \begin{malign}
      &\mpause[1]{\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{(\logimp{\unpred{LL}{x}}{\unpred{C}{x}})}}}
        \;\;\mpause[7]{\alert{\xmark}} 
      \\[-.5ex]
      &\mpause[-5]{
        \iff\;\; \text{for all $\forestgreen{a}\in\model{\adomain}\,$: } \;  
          \model{\amodel} 
          \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} 
          \formula{\logimp{\unpred{LL}{\freevar{x}}}{\unpred{C}{\freevar{x}}}}}
      \\[-.5ex]
      &\mpause{
        \iff\;\; 
        \text{for all $\forestgreen{a}\in\model{\adomain}\,$:  
              if  $\,\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{LL}{\freevar{x}}}\,$,
              then $\,\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto \forestgreen{a}]} \formula{\unpred{C}{\freevar{x}}}\,$}}  
      \\[-.5ex]
      &\mpause{
        \iff\;\;
        \text{for all $\forestgreen{a}\in\model{\adomain}\,$:  
              if   $\forestgreen{a}\in\intin{\sunpred{LL}}{\model{\amodel}}$, 
              then $\forestgreen{a}\in\intin{\sunpred{C}}{\model{\amodel}}$}}  
      \\[-.5ex]
      &\mpause{
        \;\;\Longrightarrow\;\;\;
        \text{if $1\in\intin{\sunpred{LL}}{\model{\amodel}}$, 
              then $1\in\intin{\sunpred{C}}{\model{\amodel}}$}} \;\;\mpause{\alert{\xmark}}
    \end{malign}
  \end{block} 

  \begin{block}{$\model{\amodel} \satisfies \formula{\logimp{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$}
    \begin{malign}
      &\mpause[+2]{
         \model{\amodel} 
         \satisfieslookup{\saluf}
         \formula{\logimp{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}}
       \;\;\mpause[+6]{\alert{\checkmark}}
      \\[-.5ex]
      &\mpause[-5]{
        \iff\;\;
        \text{if } \model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\unpred{LL}{x}}}
        \text{ then } \model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\unpred{C}{x}}}}
      \\[-.5ex]
      &\mpause{
        \;\Longleftarrow\:\;\;\; 
          \text{not: } \;\; \model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\unpred{LL}{x}}}}
      \\[-.5ex]
      &\mpause{
        \iff\;\;
        \text{not for all $\forestgreen{a}\in\model{\adomain}\,$:} \;\;
         \model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto\forestgreen{a}]} \formula{\unpred{LL}{\freevar{x}}}} 
      \\[-.5ex]
      &\mpause{
        \iff\;\;
        \text{not for all $\forestgreen{a}\in\model{\adomain}\,$:} \;\;
        \forestgreen{a}\in\intin{\sunpred{LL}}{\model{\amodel}}} \;\;
        \mpause{\alert{\checkmark}}
    \end{malign}
  \end{block}
  \vspace{10cm}
\end{frame}