\begin{frame} \small \begin{definitions} \begin{itemize}[<+->] \item \makebox[12mm][l]{\alert<.>{$t|_{p}$}} subterm of $t$ at position $p$ \\[1ex] \( t|_p = \begin{cases} t & \text{if $p = \epsilon$} \\[.5ex] {t_i}|_q & \text{if $t = f(\seq{t})$ and $p = iq$} \end{cases} \) \bigskip \item \makebox[12mm][l]{\alert<.>{$t(p)$}} symbol in $t$ at position $p$ \\[1ex] \( t(p) = \begin{cases} \rt(t) & \text{if $p = \epsilon$} \\[.5ex] t_i(q) & \text{if $t = f(\seq{t})$ and $p = iq$} \end{cases} \) \bigskip \item \makebox[12mm][l]{\alert<.>{$t[s]_p$}} replace subterm in $t$ at position $p$ by $s$ \\[1ex] \( t[s]_p = \begin{cases} s & \text{if $p = \epsilon$} \\[.5ex] f(t_1, \dots, t_i[s]_q, \dots, t_n) & \text{if $t = f(\seq{t})$ and $p = iq$} \end{cases} \) \end{itemize} \end{definitions} \end{frame}