\begin{frame}
  \small
  
  \begin{block}{Remark}
  \smallskip
  \begin{itemize}
  \item
  In non-left-linear TRS descendant of redex is not necessarily redex
  \[
  \GREEN{\begin{array}[t]{@{}r@{~}c@{~}l}
  \m{a} & \to & \m{b} \\[.5ex]
  \m{f}(x,x) & \to & \m{b}
  \end{array}
  \qquad\qquad
  \m{\alert<1>{f}(a,a)} \to \m{\alert<1>{f}(b,a)}}
  \]
  \item<2->
  In TRS with critical pairs descendant of redex is not necessarily redex
  \[
  \GREEN{\begin{array}[t]{@{}r@{~}c@{~}l}
  \m{a} & \to & \m{b} \\[.5ex]
  \m{f}(\m{a}) & \to & \m{b}
  \end{array}
  \qquad\qquad
  \m{\alert<2>{f}(a)} \to \m{\alert<2>{f}(b)}}
  \]
  \vspace{-2ex}
  \end{itemize}
  \end{block}
\end{frame}