\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}