\begin{frame} \begin{definitions} \begin{itemize}[<+->] \item \makebox[8mm][l]{\alert<1>{$\doteq$}} \alert<1>{literal similarity} \\[.5ex] \makebox[8mm][l]{$s \doteq t$} $~\iff~s \subsumes t ~\wedge~ t \subsumes s$ \item \alert<2>{variable substitution} is substitution from $\VV$ to $\VV$ \item \alert<3>{renaming} is bijective variable substitution \item terms $s$ and $t$ are \alert<4>{variants} if $s = t\sigma$ for some renaming $\sigma$ \smallskip \end{itemize} \end{definitions} \bigskip \begin{lemma}<5-> \smallskip terms $s$ and $t$ are variants \quad$\iff$\quad $s \doteq t$ \smallskip \end{lemma} \bigskip \begin{example}<6-> \smallskip $\GREEN{\m{s}(x)+\m{s}(y+\m{0})} \doteq \GREEN{\m{s}(y)+\m{s}(z+\m{0})}$ \qquad \onslide<7-> $\GREEN{\m{s}(x)+\m{s}(y+\m{0})} \not\doteq \GREEN{\m{s}(x)+\m{s}(x+\m{0})}$ \end{example} \end{frame}