\begin{frame}
\small

\vspace{-1ex}

\begin{definitions}
\begin{itemize}
\item
\alert<-3>{context} is term with one \alert<-2>{hole $\Box$}\onslide<2->,\\ i.e.,
element of $\TT(\FF \cup \{ \alert<2>{\Box} \},\VV)$ that contains exactly
one occurrence of $\alert<2>{\Box}$
\item<4->
$\alert<-5>{C[}t\alert<-5>{]}$ denotes result of replacing hole in context
$C$ by term $t$
\item<6->
relation $R$ on terms is \alert<6>{closed under contexts} if
$\forall$ terms $s, t$
\vspace{-1ex}
\[
s \mathrel{R} t \quad\Longrightarrow\quad
\text{$\forall$ contexts $C$:} \quad \alert<6>{C[s] \mathrel{R} C[t]}
\]
\vspace{-3.5ex}
\end{itemize}
\end{definitions}

\smallskip

\begin{examples}<3->
\begin{itemize}
\item
\GREEN{$\BLACK{\Box}
\qquad \m{s}(\m{0})+\m{s}(\m{s}(\BLACK{\Box}))
\qquad \BLACK{\Box} + x$}
\item<5->
\GREEN{$\BLACK{\Box[}\m{s(0)}\BLACK{]} = \m{s(0)}
\qquad (\BLACK{\Box} + x)\BLACK{[}0+x\BLACK{]} = (\m{0}+x)+x$}
\smallskip
\end{itemize}
\end{examples}

\smallskip

\begin{lemmata}<7->
\begin{itemize}
\item
$s \subterm t$ \quad$\iff$\quad $\exists$ context
\makebox[15mm][l]{$C\colon$} $t = C[s]$
\item<8->
$s \prsubterm t$ \quad$\iff$\quad $\exists$ context
\makebox[15mm][l]{$C \neq \Box\colon$} $t = C[s]$
\end{itemize}
\end{lemmata}

\end{frame}