\begin{frame}
  \small
  
  %\begin{example}
  %\[
  %\GREEN{\begin{array}{r@{~}c@{~}l@{\qquad\qquad}r@{~}c@{~}l}
  %\m{f}(\m{g}(x),y) & \to & \m{f}(\m{h}(x),y) &
  %\m{g}(x) & \to & \m{h}(x) \\[.5ex]
  %\m{f}(x,\m{g}(y)) & \to & \m{f}(x,\m{h}(y)) &
  %\m{h}(x) & \to & \m{g}(x)
  %\end{array}}
  %\]
  %\end{example}
  %
  %\medskip
  
  \begin{theorem}[Huet 1980]
  \smallskip
  $\,\text{\alert<1>{linearity}}
  \quad\&\quad
  {\cp} \:\subseteq\: (\to^= \cdot \FromP{*}) \cap (\to^* \cdot \FromP{=})
  \quad\Longrightarrow\quad \text{CR}$
  \end{theorem}
  
  \bigskip
  
  %\begin{example}
  %\[
  %\GREEN{\begin{array}{r@{~}c@{~}l}
  %\m{f}(\m{g}(x,y)) & \to & \m{g}(\m{f}(\m{j}(x)),y)
  %\\[.5ex]
  %\m{f}(\m{h}(x,y)) & \to & \m{h}(x,\m{f}(y))
  %\end{array}
  %\qquad\qquad
  %\begin{array}{r@{~}c@{~}l}
  %\m{g}(x,\m{k}(y,z)) & \to & \m{h}(\m{l}(y),\m{i}(z,x))
  %\\[.5ex]
  %\m{i}(x,\m{f}(\m{j}(y))) & \fromto & \m{f}(\m{i}(x,y))
  %\end{array}}
  %\]
  %\end{example}
  
  \begin{notation}<2->
  \begin{itemize}
    \item $s \overlay t$ for critical pair originating from overlap
          $\langle l_1 \to r_1, \alert<3>{\epsilon}, l_2 \to r_2 \rangle$
    \item ${\icp} \:=\: {\cp \setminus \overlay}$
  \end{itemize}
  \end{notation}
  
  \medskip
  
  \begin{theorem}<3->[Toyama 1988]
  \smallskip
  $\,\text{left-linearity} \quad\&\quad
  {\icp} \:\subseteq\: \smash{\parr}
  \quad\&\quad
  \alert<3>{{\overlay} \:\subseteq\: {\parr \cdot \FromP{*}}}
  \quad\Longrightarrow\quad \text{CR}$
  \end{theorem}
  
  \medskip
  
  %\begin{example}
  %\[
  %\GREEN{\begin{array}{r@{~}c@{~}l}
  %\m{f}(x) & \to & \m{g}(x)
  %\\[.5ex]
  %\m{f}(x) & \to & \m{h}(x)
  %\end{array}
  %\qquad
  %\begin{array}{r@{~}c@{~}l}
  %\m{g}(x) & \to & \m{i}(\m{f}(x))
  %\\[.5ex]
  %\m{h}(x) & \to & \m{i}(\m{f}(x))
  %\end{array}
  %\qquad
  %\begin{array}{r@{~}c@{~}l}
  %\m{i}(x) & \to & \m{j}(x,x)
  %\end{array}}
  %\]
  %\end{example}
  
  \begin{theorem}<4->[van Oostrom 1996]
  \smallskip
  $\,\text{left-linearity} \quad\&\quad
  {\icp} \:\subseteq\: \alert<4>{\dev}
  \quad\&\quad
  {\overlay} \:\subseteq\: {\dev \cdot \FromP{*}}
  \quad\Longrightarrow\quad \text{CR}$
  \end{theorem}
  
  %\begin{example}
  %\[
  %\GREEN{\begin{array}{r@{~}c@{~}l}
  %\m{a} & \to & \m{f}(\m{b})
  %\\[.5ex]
  %\m{a} & \to & \m{g}(\m{a},\m{a})
  %\end{array}
  %\qquad
  %\begin{array}{r@{~}c@{~}l}
  %\m{f}(x) & \to & \m{g}(x,x)
  %\\[.5ex]
  %\m{g}(x,y) & \to & x
  %\end{array}
  %\qquad
  %\begin{array}{r@{~}c@{~}l}
  %\m{b} & \to & \m{a}
  %\end{array}}
  %\]
  %\end{example}
\end{frame}