85/144
\begin{frame}
\small

\begin{definition}[Positions]
\begin{itemize}
\item
\alert<1>{$\Pos(\:\cdot\:)$}, the set of \alert<1>{positions of a term}\\[1ex]
\(
\Pos(t) =
\begin{cases}
\{ \epsilon \} & \text{if $t \in \VV$} \\[.5ex]
\{ \epsilon \} \cup \{ ip \mid p \in \Pos(t_i) \} &
\text{if $t = f(\seq{t})$}
\end{cases}
\)
\end{itemize}
\end{definition}

\bigskip

\begin{example}<2->
\GREEN{$(2:x)+((1:x):y)$} \qquad
\GREEN{\begin{tikzpicture}[on grid,baseline=(1).baseline]
\matrix[ampersand replacement=\&,row sep=5mm,column sep=2mm]{
\& \& \& \node (1) {$+$}; \& \& \& \\
\& \node (2) {$:$}; \& \& \& \& \node (3) {$:$}; \& \\
\node (4) {$2$}; \& \& \node (5) {$x$}; \& \& \node (6) {$:$}; \& \&
\node (7) {$y$}; \\
\& \& \& \node (8) {$1$}; \& \& \node (9) {$x$}; \& \\};
\draw (1) -- (2) (1) -- (3);
\draw (2) -- (4) (2) -- (5);
\draw (3) -- (6) (3) -- (7);
\draw (6) -- (8) (6) -- (9);
\onslide<3->{
\draw (1) node[right] {\alert<3>{$\,{}^\epsilon$}};
\draw (2) node[left] {\alert<3>{${}^1\,$}};
\draw (3) node[right] {\alert<3>{$\,{}^2$}};
\draw (4) node[left] {\alert<3>{${}^{11}\,$}};
\draw (5) node[right] {\alert<3>{$\,{}^{12}$}};
\draw (6) node[left] {\alert<3>{${}^{21}\,$}};
\draw (7) node[right] {\alert<3>{$\,{}^{22}$}};
\draw (8) node[left] {\alert<3>{${}^{211}\,$}};
\draw (9) node[right] {\alert<3>{$\,{}^{212}$}};
}
\end{tikzpicture}}
\end{example}

\end{frame}