\begin{frame} \small \begin{definition} \smallskip \alert<1>{composition} of substitutions $\sigma$ and $\tau$: \[ \alert<1>{\sigma\tau} = \{ x \mapsto \sigma(x)\tau \mid x \in \VV \} \] \end{definition} \medskip \begin{example}<2-> \smallskip $\sigma = \{ \GREEN{x} \mapsto \GREEN{\m{s}(y)}, \GREEN{y} \mapsto \GREEN{x + \m{s(0)}} \}$ \quad $\tau = \{ \GREEN{x} \mapsto \GREEN{\m{s(0)}}, \GREEN{z} \mapsto \GREEN{\m{s}(\m{s}(y))} \}$ \begin{itemize} \item<3-> $\sigma\tau = \{ \GREEN{x} \mapsto \GREEN{\m{s}(y)}, \GREEN{y} \mapsto \GREEN{\m{s(0) + s(0)}}, \GREEN{z} \mapsto \GREEN{\m{s}(\m{s}(y))} \}$ \item<4-> $\tau\sigma = \{ \GREEN{x} \mapsto \GREEN{\m{s(0)}}, \GREEN{y} \mapsto \GREEN{x + \m{s(0)}}, \GREEN{z} \mapsto \GREEN{\m{s}(\m{s}(x + \m{s(0)}} \}$ \end{itemize} \end{example} \medskip \begin{lemma}<5-> \smallskip $(\rho\sigma)\tau = \rho(\sigma\tau)$ for all substitutions $\rho$, $\sigma$, $\tau$ \end{lemma} \end{frame}