\begin{frame}
\small

\begin{definitions}
\begin{itemize}[<+->]
\item 
\alert<1>{substitution} is mapping
$\alert<1>{\sigma}\colon \VV \to \TT(\FF,\VV)$ such that its domain
\vspace{-1ex}
\[
\alert<1>{\Dom(}\sigma\alert<1>{)} =
\{ x \in \VV \mid \sigma(x) \neq x \}
\]\\[-3ex]
is finite
%\item
%variables \alert<2>{introduced} by $\sigma$
%\[
%\alert<2>{\II(}\sigma\alert<2>{)} =
%\bigcup_{x \in \Dom(\sigma)} \Var(\sigma(x))
%\]
\item
\alert<2>{empty} substitution \alert<2>{$\varepsilon$}
\quad ($\Dom(\varepsilon) = \varnothing$)
\item
\alert<3>{application} of substitution $\sigma$ to term $t$
\vspace{-1ex}
\[
\alert<3>{t\sigma} =
\begin{cases}
\sigma(t) & \text{if $t \in \VV$} \\[.5ex]
f(t_1\sigma,\dots,t_n\sigma) & \text{if $t = f(\seq{t})$}
\end{cases}
\]
\vspace{-3ex}
%
\item
relation $R$ on terms is \alert<4>{closed under substitutions} if
$\forall$ terms $s, t$
\vspace{-1ex}
\[
s \mathrel{R} t \quad\Longrightarrow\quad
\text{$\forall$ substitutions $\sigma$\,:} \quad
\alert<4>{s\sigma \mathrel{R} t\sigma}
\]
\vspace{-3.5ex}
\end{itemize}
\end{definitions}

\begin{example}<5->
\smallskip
$t = \GREEN{x+\m{s}(y+z)}$ ~
$\sigma = \{ \GREEN{x} \mapsto \GREEN{\m{s}(y)},
\GREEN{y} \mapsto \GREEN{x + \m{s(0)}} \}$ ~
\onslide<6->{$t\sigma = \GREEN{\m{s}(y)+\m{s}((x+\ms{s}(0))+z)}$}
\smallskip
\end{example}

\end{frame}