\begin{frame} \small \begin{definition} A critical pair $s \cp t$ is \alert{trivial} if $s = t$. \end{definition} \begin{definition} A \alert{weakly orthogonal} TRS is left-linear and has only trivial critical pairs. \end{definition} % overlay niet echt nodig ? %AM find overlays rather useful on this (modified) slide % \begin{definitions} % \begin{itemize} % \item % critical pair $s \cp t$ is \alert<1>{trivial} if $s = t$ % \item<2-> % \alert<2>{weakly orthogonal} TRS is left-linear and has only trivial % critical pairs % \item<5-> % \alert<5>{overlay} $s \alert<3>{\overlay} t$ is critical pair originating % from overlap % $\langle l_1 \to r_1, \alert<3>{\epsilon}, l_2 \to r_2 \rangle$ % \item<6-> % weakly orthogonal TRS is \alert<6>{almost orthogonal} if all % critical pairs are overlays % \end{itemize} % \end{definitions} \medskip \begin{examples}<2-> \[ \GREEN{ \begin{array}{c@{\:\vee\:}c@{~}c@{~}c} x & \m{T} & \to & \m{T} \\[.5ex] \m{T} & x & \to & \m{T} \\[.5ex] \m{F} & \m{F} & \to & \m{F} \end{array} \qquad\qquad\qquad\qquad \onslide<3-> \begin{array}{r@{~}c@{~}l} \m{p}(\m{s}(x)) & \to & x \\[.5ex] \m{s}(\m{p}(x)) & \to & x \end{array} } \] \end{examples} \end{frame}