\begin{frame} \vspace{-1ex} {\renewcommand{\arraystretch}{0.7} \begin{example} \begin{minipage}{65mm} \[ \begin{array}[t]{c} \GREEN{x\alert<2,3>{+}(\m{0}+\m{s}(y)) \approx \m{s}(z)\alert<2,3>{+}(\m{0}+x)} \\[1ex] \onslide<3->\derive{d}{} \\[1ex] \GREEN{\alert<4>{x \approx \m{s}(z)},~\m{0}+\m{s}(y) \approx \m{0}+x} \\[1ex] \onslide<4->\derive{v}{\GREEN{\alert<4,10>{x \mapsto \m{s}(z)}}} \\[1ex] \GREEN{\m{0}\alert<5>{+}\m{s}(y) \approx \m{0}\alert<5>{+}\m{s}(z)} \\[1ex] \onslide<5->\derive{d}{} \\[1ex] \GREEN{\alert<6>{\m{0}} \approx \alert<6>{\m{0}},~\m{s}(y) \approx \m{s}(z)} \\[1ex] \onslide<6->\derive{d}{} \\[1ex] \GREEN{\alert<7>{\m{s}}(y) \approx \alert<7>{\m{s}}(z)} \\[1ex] \onslide<7->\derive{d}{} \\[1ex] \GREEN{\alert<8>{y \approx z}} \\[1ex] \onslide<8->\derive{v}{\GREEN{\alert<8,10>{y \mapsto z}}} \\[1ex] % \GREEN{\alert<9>{z \approx z}} % \\[1ex] % \onslide<9->\derive{t}{} % \\[1ex] \onslide<8->\GREEN{\alert<9>{\Box}} \end{array} \] \end{minipage} \onslide<10-> \begin{minipage}{40mm} mgu \quad \GREEN{$\{ x \mapsto \m{s}(z), y \mapsto z \}$} \end{minipage} \end{example} } \end{frame}