\begin{frame}[fragile]{Evaluation of Conditions in a State}
  \begin{exampleblock}{Example}  
  Let $\saluf$ a state with
  \begin{talign}
    \aluf{x} = -2 && \aluf{y} = 5 && \aluf{z} = -1
  \end{talign}
  \pause
  Then we find: 
  \begin{itemize}\vspace*{0.6ex}\setlength{\itemsep}{0.6ex}
    \item $\saluf \malt[1]{\gray{\satisfiesblack}}{\satisfies} \lognot{(x \mathrel{\dm{+}} y \mathrel{\dm{<}} z)}$
      \updatepause\; 
      since $(-2) + 5 = 3 \ge (-1)$.
  \pause\medskip
    \item $\saluf \malt[1]{\gray{\satisfiesblack}}{\satisfiesnot} y \mathrel{\dm{-}} x \mathrel{\dm{*}} z \mathrel{\dm{<}} z$
      \updatepause\; 
      since $5 - (-2)\cdot(-1) = 3 \ge -1\,$.
  \pause\medskip
    \item $\saluf \malt[1]{\gray{\satisfiesblack}}{\satisfiesnot} 
           \forallst{u}{\;(y \mathrel{\dm{<}} u \logimpinf y \mathrel{\dm{*}} z \mathrel{\dm{<}} u \mathrel{\dm{*}} z)}$
      \updatepause\\[.5ex]
      \hspace*{1.5ex} since: $\saluf[\freevar{u}\mapsto 6] \satisfiesnot \formula{{(y \mathrel{\dm{<}} \freevar{u} \logimpinf y \mathrel{\dm{*}} z \mathrel{\dm{<}} \freevar{u} \mathrel{\dm{*}} z)}}$
      \pause\\[.5ex]
      \hspace*{1.5ex} because: $5 < 6$, but $5\cdot(-1) = -5 \ge -6 = 6\cdot(-1)$. 
  \end{itemize}\onslide<8>{}
  \end{exampleblock}
\end{frame}