\begin{frame} \small \begin{definitions} \begin{itemize} \item \makebox[8mm][l]{\alert<1>{$\subsumes$}} \alert<1>{subsumption} \\[.5ex] \makebox[8mm][l]{$s \subsumes t$} $~\iff~\exists \sigma\colon s\sigma = t$ \qquad \onslide<2->``$s$ \alert<.>{subsumes} $t$'' \quad ``$t$ is \alert<.>{instance} of $s$'' \item<3-> \makebox[8mm][l]{\alert<3>{$\prsubsumes$}} \alert<3>{proper} subsumption \\[.5ex] \makebox[8mm][l]{$s \prsubsumes t$} $~\iff~s \subsumes t ~\wedge~ \neg (t \subsumes s)$ \end{itemize} \end{definitions} \pause\pause\pause \bigskip \begin{example} \smallskip $\GREEN{x+y} \subsumes \GREEN{\m{s}(y)+\m{s}(0)}$ \qquad $\GREEN{\m{s}(x)+y} \not\subsumes \GREEN{x+\m{s}(0)}$ \qquad $\GREEN{\m{s}(x)+y} \subsumes \GREEN{\m{s}(x)+x}$ \end{example} \pause \bigskip \begin{lemma} \smallskip $\prinstance$ is well-founded order on terms \smallskip \end{lemma} \end{frame}