\begin{frame} \small \begin{definition}<1->[Matching Problem] \smallskip \begin{tabular}{ll} instance: & terms $s$, $t$ \\[.5ex] question: & $\exists$ subsitution $\sigma\colon ~ s\sigma = t$ ? \qquad \onslide<2->{($s$ \alert<2>{matches} $t$)} \end{tabular} \end{definition} \bigskip \begin{block}<3->{Remarks} \smallskip \begin{itemize} \item term $t$ can be rewritten if left-hand side of rewrite rule matches subterm of $t$ \item<4-> matching problem is decidable (in linear time) \smallskip \end{itemize} \end{block} \end{frame}