94/144
\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}