\documentclass[10pt]{article}
\input{preambolo.tex}

% \usepackage{tikz}

\newcommand{\true}{\operatorname{tt}}
\newcommand{\false}{\operatorname{ff}}

\newcommand{\ddef}{\mathrel{::=}}
\newcommand{\semi}{\mathrel{;}}

\newtheorem{example}[theorem]{Example}



\begin{document}

Terms:
\[t, u \ddef x \mid t\,u \mid \lambda x.\, t\]

Fireballs, inerts and normal forms:

\[\begin{array}{lll}
f & \ddef & x \mid i \mid \lambda x.\, t \\
i & \ddef & x\,F_1\cdots F_n \\
F & \ddef & K\langle f\rangle \\
\end{array}\]

Contexts $K$:
\[K \ddef [\,] \mid i \semi K\]


\[\begin{array}{lll}
 K_1\langle\lambda x.\,t\rangle \, K_2\langle \lambda y.\, u\rangle &
 \mapsto_{\beta_\lambda} &
 K_1\langle K_2\langle t\{x\leftarrow \lambda y.\, u\}\rangle\rangle
\\
 K_1\langle\lambda x.\,t\rangle \, K_2\langle y \,\,\,\,\,\,\,\,\,\,\rangle &
 \mapsto_{\beta_v} &
 K_1\langle K_2\langle t\{x\leftarrow y\}\rangle\rangle
\\
 K_1\langle\lambda x.\,t\rangle \, K_2\langle i\,\,\,\,\,\,\,\,\,\,\,\rangle &
 \mapsto_{\beta_i} &
 \begin{cases}
  K_1\langle K_2\langle t\{x\leftarrow i\}\rangle\rangle &
  \text{ if } x \text{ occurs in } t \\
  K_1\langle K_2\langle i \semi t\rangle\rangle &
  \text{ otherwise } \\
 \end{cases}
\end{array}\]

Evaluation contexts $E$:
\[E \ddef [\,] \mid t\,E \mid E\,t\]

\end{document}
