64/145
\begin{frame}
  \small
  
  \begin{definition}<1->%[Orthogonality]
  \smallskip
  A TRS is \alert{orthogonal} if it is \alert{left-linear} and has \alert{no criticial pairs}.
  \strut
  \end{definition}
  
  \bigskip
  
  \begin{examples}<2->%[Orthogonal TRSs]
  \vspace{-2ex}
  \GREEN{\begin{align*}
  \m{I} \cdot x &\to x & 
  \onslide<3-> \m{ack}(\m{0},y) &\onslide<3->\to \m{s}(y) \\[.5ex]
  (\m{K} \cdot x) \cdot y &\to x & 
  \onslide<3-> \m{ack}(\m{s}(x),\m{0}) &\onslide<3->\to \m{ack}(x,\m{s}(\m{0})) \\[.5ex]
  ((\m{S} \cdot x) \cdot y) \cdot z &\to (x \cdot z) \cdot (y \cdot z) &
  \onslide<3-> \m{ack}(\m{s}(x),\m{s}(y)) &\onslide<3->\to \m{ack}(x,\m{ack}(\m{s}(x),y))
  \end{align*}}
  \vspace{-3ex}
  \end{examples}
\end{frame}