122/145
\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}