\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}