\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}