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