\documentclass[12pt,final,notitlepage,onecolumn,german]{article}%
\usepackage[all,cmtip]{xy}
\usepackage{lscape}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{amsmath}%
\setcounter{MaxMatrixCols}{30}
%TCIDATA{OutputFilter=latex2.dll}
%TCIDATA{Version=5.50.0.2960}
%TCIDATA{LastRevised=Sunday, June 05, 2011 22:42:57}
%TCIDATA{}
%TCIDATA{}
%TCIDATA{BibliographyScheme=Manual}
%BeginMSIPreambleData
\providecommand{\U}[1]{\protect\rule{.1in}{.1in}}
%EndMSIPreambleData
\voffset=-2.5cm
\hoffset=-0.5cm
\setlength\textheight{23cm}
\setlength\textwidth{14.5cm}
\begin{document}
\begin{center}
\textbf{Remarks on Krivine's "Lambda-calculus, types and models", Chapter 1,
\S 2}
Darij Grinberg, 5 June 2011
\textbf{1. Introduction}
\end{center}
The point of this note is to
\textbf{1)} add some lemmata to Chapter 1 \S 2 of [1] (lemmata that are used
in [1] without mention, due to their intuitive obviousness);
\textbf{2)} show that the definition of $\alpha$-equivalence given in [1] is
equivalent to the definition of $\alpha$-equivalence given in some other sources;
\textbf{3)} prove some rules for substitution (in order to answer a
MathOverflow question of myself).
We are going to use the notations and the results of Chapter 1 of [1]. In
particular, the sign $\equiv$ will stand for the $\alpha$-equivalence defined
in [1]. The different notion of $\alpha$-equivalence that we consider will be
denoted by $=^{\alpha}$ (in order not to confuse it with $\equiv$ as long as
it is not yet proven that the two notions are equivalent).
\begin{center}
\textbf{2. Sidenotes to Chapter 1 \S 2 of [1]}
\end{center}
Here come several facts silently used in some proofs in \S 1.2 of [1]. These
facts are all pretty simple, intuitively clear and easy to prove, and I
suspect this is why they have not been explicitly stated in [1]. I am making
them explicit and proving them in detail in order to formalize the theory a
little bit more.
We begin with some properties of bound variables (and their behaviour under substitution).
\begin{quote}
\textbf{Definition:} If $u$ is a term in $L$, let $\operatorname*{BV}u$ denote
the set of bounded variables of the term $u$.
\end{quote}
Before we continue, let us give an inductive method to compute
$\operatorname*{BV}u$ for a term $u$:
If $u=x$ for a variable $x$, then $\operatorname*{BV}u=\varnothing$.
If $u=\left( v\right) w$ for terms $v$ and $w$, then $\operatorname*{BV}
u=\left( \operatorname*{BV}v\right) \cup\left( \operatorname*{BV}w\right)
$.
If $u=\lambda xv$ for some variable $x$ and some term $v$, then
$\operatorname*{BV}u=\left\{ x\right\} \cup\left( \operatorname*{BV}
v\right) $.
\begin{quote}
\textbf{Lemma 1.A.} Let $t$, $t_{1}$, $...$, $t_{m}$ be terms in $L$, and
$x_{1}$, $...$, $x_{m}$ be distinct variables. Then, $\operatorname*{BV}%
\left( t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right)
\subseteq\left( \operatorname*{BV}t\right) \cup\left( \operatorname*{BV}%
t_{1}\right) \cup...\cup\left( \operatorname*{BV}t_{m}\right) $.
\end{quote}
\textit{Proof of Lemma 1.A.} We proceed by induction over $t$:
If $t$ is a variable or a term of the form $\left( u\right) v$, the
induction step is clear.
Remains to consider the case when $t=\lambda xu$ for some variable $x$ and
some term $u$.
In this case, $\operatorname*{BV}t=\left\{ x\right\} \cup\left(
\operatorname*{BV}u\right) $. There are two subcases to consider: the subcase
when $x\in\left\{ x_{1},...,x_{m}\right\} $ and the subcase when
$x\notin\left\{ x_{1},...,x_{m}\right\} $.
\textit{First, let us consider the subcase when }$x\in\left\{ x_{1}%
,...,x_{m}\right\} $\textit{.} In this subcase, let us WLOG assume that
$x=x_{1}$. Thus, $t=\lambda x_{1}u$, so that $\operatorname*{BV}t=\left\{
x_{1}\right\} \cup\left( \operatorname*{BV}u\right) $.
Now, $t=\lambda x_{1}u$ and the definition of $t\left\langle t_{1}%
/x_{1},...,t_{m}/x_{m}\right\rangle $ result in \newline$t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle =\lambda x_{1}\left( u\left\langle
t_{2}/x_{2},...,t_{m}/x_{m}\right\rangle \right) $, so that%
\[
\operatorname*{BV}\left( t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}%
\right\rangle \right) =\left\{ x_{1}\right\} \cup\operatorname*{BV}\left(
u\left\langle t_{2}/x_{2},...,t_{m}/x_{m}\right\rangle \right) .
\]
Since $\operatorname*{BV}\left( u\left\langle t_{2}/x_{2},...,t_{m}%
/x_{m}\right\rangle \right) \subseteq\left( \operatorname*{BV}u\right)
\cup\left( \operatorname*{BV}t_{2}\right) \cup...\cup\left(
\operatorname*{BV}t_{m}\right) $ by the induction assumption, this becomes
\begin{align*}
& \operatorname*{BV}\left( t\left\langle t_{1}/x_{1},...,t_{m}%
/x_{m}\right\rangle \right) \\
& \subseteq\underbrace{\left\{ x_{1}\right\} \cup\left( \operatorname*{BV}%
u\right) }_{=\operatorname*{BV}t}\cup\left( \operatorname*{BV}t_{2}\right)
\cup...\cup\left( \operatorname*{BV}t_{m}\right) \\
& =\left( \operatorname*{BV}t\right) \cup\left( \operatorname*{BV}%
t_{2}\right) \cup...\cup\left( \operatorname*{BV}t_{m}\right)
\subseteq\left( \operatorname*{BV}t\right) \cup\left( \operatorname*{BV}%
t_{1}\right) \cup...\cup\left( \operatorname*{BV}t_{m}\right) .
\end{align*}
\textit{Now, let us consider the subcase when }$x\notin\left\{ x_{1}%
,...,x_{m}\right\} $. In this subcase, $t=\lambda xu$ and the definition of
$t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle $ result in
$t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle =\lambda x\left(
u\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right) $. Thus,
\[
\operatorname*{BV}\left( t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}%
\right\rangle \right) =\left\{ x\right\} \cup\operatorname*{BV}\left(
u\left\langle t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right) .
\]
Since $\operatorname*{BV}\left( u\left\langle t_{1}/x_{1},...,t_{m}%
/x_{m}\right\rangle \right) \subseteq\left( \operatorname*{BV}u\right)
\cup\left( \operatorname*{BV}t_{1}\right) \cup...\cup\left(
\operatorname*{BV}t_{m}\right) $ by the induction assumption, this becomes%
\begin{align*}
\operatorname*{BV}\left( t\left\langle t_{1}/x_{1},...,t_{m}/x_{m}%
\right\rangle \right) & \subseteq\underbrace{\left\{ x\right\}
\cup\left( \operatorname*{BV}u\right) }_{=\operatorname*{BV}t}\cup\left(
\operatorname*{BV}t_{1}\right) \cup...\cup\left( \operatorname*{BV}%
t_{m}\right) \\
& =\left( \operatorname*{BV}t\right) \cup\left( \operatorname*{BV}%
t_{1}\right) \cup...\cup\left( \operatorname*{BV}t_{m}\right) .
\end{align*}
In both subcases, we have proven that $\operatorname*{BV}\left( t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle \right) \subseteq\left(
\operatorname*{BV}t\right) \cup\left( \operatorname*{BV}t_{1}\right)
\cup...\cup\left( \operatorname*{BV}t_{m}\right) $. This completes the
induction and thus proves Lemma 1.A.
Lemma 1.A is used in the proof of Lemma 1.12 in [1]. (In fact, this proof
claims that "no bound variable of this term is free in $\underline{u}%
_{1},...,\underline{u}_{n}$"\ \ \ \ \footnote{Here, "this term" refers to the
term $\underline{t}\left\langle \underline{t}_{1}/x_{1},...,\underline{t}%
_{m}/x_{m}\right\rangle $.}. The reason why this is true is the following:
Lemma 1.A yields that $\operatorname*{BV}\left( \underline{t}\left\langle
\underline{t}_{1}/x_{1},...,\underline{t}_{m}/x_{m}\right\rangle \right)
\subseteq\left( \operatorname*{BV}\underline{t}\right) \cup\left(
\operatorname*{BV}\underline{t}_{1}\right) \cup...\cup\left(
\operatorname*{BV}\underline{t}_{m}\right) $, and we know that no bound
variable of any of the terms $\underline{t},\underline{t}_{1}%
,...,\underline{t}_{m}$ is free in $\underline{u}_{1},...,\underline{u}_{n}$.)
\begin{quote}
\textbf{Lemma 1.B.} Let $u$ be a term in $L$, and let $x$ and $y$ be two
variables. Then, $\operatorname*{BV}\left( u\left\langle y/x\right\rangle
\right) \subseteq\operatorname*{BV}u$.
\end{quote}
\textit{Proof of Lemma 1.B.} Apply Lemma 1.A to $m=1$, $t_{1}=y$, $x_{1}=x$
and $t=u$. This yields $\operatorname*{BV}\left( u\left\langle
y/x\right\rangle \right) \subseteq\left( \operatorname*{BV}u\right)
\cup\underbrace{\left( \operatorname*{BV}y\right) }_{=\varnothing
}=\operatorname*{BV}u$, and thus Lemma 1.B is proven.
Lemma 1.B is used in the proof of Proposition 1.6 in [1]. (Namely, when this
proof says "the induction hypothesis gives", it silently uses the fact that no
free variable in $t_{1},...,t_{k}$ is bound in $u\left\langle y/x\right\rangle
$ or $u^{\prime}\left\langle y/x^{\prime}\right\rangle $ (this must be
guaranteed, lest we could not apply the induction hypothesis!). This holds
because Lemma 1.B yields $\operatorname*{BV}\left( u\left\langle
y/x\right\rangle \right) \subseteq\operatorname*{BV}u\subseteq\left\{
x\right\} \cup\left( \operatorname*{BV}u\right) =\operatorname*{BV}t$
(since $t=\lambda xu$) and $\operatorname*{BV}\left( u^{\prime}\left\langle
y/x^{\prime}\right\rangle \right) \subseteq\operatorname*{BV}t^{\prime}$ (for
similar reasons), and because we know that no free variable in $t_{1}%
,...,t_{k}$ is bound in $t$ or $t^{\prime}$.)
Next some lemmata about free variables:
\begin{quote}
\textbf{Definition:} If $u$ is a term in $L$, let $\operatorname*{FV}u$ denote
the set of free variables of the term $u$.
\end{quote}
Before we continue, let us give an inductive method to compute
$\operatorname*{FV}u$ for a term $u$:
If $u=x$ for a variable $x$, then $\operatorname*{FV}u=\left\{ x\right\} $.
If $u=\left( v\right) w$ for terms $v$ and $w$, then $\operatorname*{FV}
u=\left( \operatorname*{FV}v\right) \cup\left( \operatorname*{FV}w\right)
$.
If $u=\lambda xv$ for some variable $x$ and some term $v$, then
$\operatorname*{FV}u=\left( \operatorname*{FV}v\right) \setminus\left\{
x\right\} $.
\begin{quote}
\textbf{Lemma 1.C.} Let $u$ be a term in $L$, and let $y$ be a variable which
does not appear in $u$. Let $x$ be a variable. Then, $\operatorname*{FV}%
\left( u\left\langle y/x\right\rangle \right) =\operatorname*{map}%
\nolimits_{x,y}\left( \operatorname*{FV}u\right) $. Here,
$\operatorname*{map}\nolimits_{x,y}$ denotes the map $V\rightarrow V$ (where
$V$ is the set of variables) which maps $x$ to $y$ and maps $v$ to $v$ for
every variable $v\neq x$.
\end{quote}
\textit{Proof of Lemma 1.C.} We proceed by induction over $u$:
If $u$ is a variable, then everything is clear.
Consider the case when $u=\left( v\right) w$ for terms $v$ and $w$. In this
case, $u\left\langle y/x\right\rangle =\left( v\left\langle y/x\right\rangle
\right) \left( w\left\langle y/x\right\rangle \right) $, so that%
\begin{equation}
\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right) =\left(
\operatorname*{FV}\left( v\left\langle y/x\right\rangle \right) \right)
\cup\left( \operatorname*{FV}\left( w\left\langle y/x\right\rangle \right)
\right) . \label{1.c.pf.1}%
\end{equation}
By the induction assumption, $\operatorname*{FV}\left( v\left\langle
y/x\right\rangle \right) =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}v\right) $ and $\operatorname*{FV}\left( w\left\langle
y/x\right\rangle \right) =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}w\right) $. Thus (\ref{1.c.pf.1}) becomes%
\[
\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right) =\left(
\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}v\right) \right)
\cup\left( \operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}%
w\right) \right) =\operatorname*{map}\nolimits_{x,y}\left( \left(
\operatorname*{FV}v\right) \cup\left( \operatorname*{FV}w\right) \right)
.
\]
Since $\left( \operatorname*{FV}v\right) \cup\left( \operatorname*{FV}%
w\right) =\operatorname*{FV}u$ (due to $u=\left( v\right) w$), this becomes
$\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right)
=\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}u\right) $,
completing the induction (in the case $u=\left( v\right) w$).
It remains to complete the induction step in the case when $u=\lambda zv$ for
some variable $z$ and some term $v\in L$.
Consider this case. Clearly, $\operatorname*{FV}u=\left( \operatorname*{FV}
v\right) \setminus\left\{ z\right\} $ in this case.
Two subcases are possible: the subcase $z=x$ and the subcase $z\neq x$.
Consider the subcase $z=x$. In this subcase, $u=\lambda zv=\lambda xv$, thus
$u\left\langle y/x\right\rangle =\lambda xv=u$, so that $\operatorname*{FV}%
\left( u\left\langle y/x\right\rangle \right) =\operatorname*{FV}u$. But we
want to prove that $\operatorname*{FV}\left( u\left\langle y/x\right\rangle
\right) =\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}%
u\right) $. So we only need to check that $\operatorname*{map}\nolimits_{x,y}%
\left( \operatorname*{FV}u\right) =\operatorname*{FV}u$. But this is clear
because $x\notin\operatorname*{FV}u$ (since $u=\lambda xv$, so that
$\operatorname*{FV}u=\left( \operatorname*{FV}v\right) \setminus\left\{
x\right\} $) and because $\operatorname*{map}\nolimits_{x,y}$ leaves every
variable except of $x$ fixed.
Now consider the subcase $z\neq x$. In this subcase, $u=\lambda zv$ leads to
$u\left\langle y/x\right\rangle =\lambda z\left( v\left\langle
y/x\right\rangle \right) $, so that $\operatorname*{FV}\left( u\left\langle
y/x\right\rangle \right) =\left( \operatorname*{FV}\left( v\left\langle
y/x\right\rangle \right) \right) \setminus\left\{ z\right\} $. By the
induction hypothesis, $\operatorname*{FV}\left( v\left\langle
y/x\right\rangle \right) =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}v\right) $ (since $y$ does not appear in $v$, which is
because $y$ does not appear in $u$). Thus, $\operatorname*{FV}\left(
u\left\langle y/x\right\rangle \right) =\underbrace{\left(
\operatorname*{FV}\left( v\left\langle y/x\right\rangle \right) \right)
}_{=\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}v\right)
}\setminus\left\{ z\right\} =\left( \operatorname*{map}\nolimits_{x,y}%
\left( \operatorname*{FV}v\right) \right) \setminus\left\{ z\right\} $.
Let us now show that \newline$\left( \operatorname*{map}\nolimits_{x,y}%
\left( \operatorname*{FV}v\right) \right) \setminus\left\{ z\right\}
=\operatorname*{map}\nolimits_{x,y}\left( \left( \operatorname*{FV}v\right)
\setminus\left\{ z\right\} \right) $. In fact, $\operatorname*{FV}v$ does
not contain $y$ (because $y$ does not appear in $u$, and thus $y$ does not
appear in $v$ either), so that $\operatorname*{FV}v\subseteq V\diagdown
\left\{ y\right\} $ (where $V$ denotes the set of all variables). Also,
$\left\{ z\right\} \subseteq V\diagdown\left\{ y\right\} $ (since $z\neq
y$ (which is because $y$ does not appear in $u=\lambda zv$, while $z$ does
appear in $\lambda zv$)). Now, $\operatorname*{map}\nolimits_{x,y}$ is
injective on $V\diagdown\left\{ y\right\} $ (because $\left( x,y\right) $
is the only possible pair of distinct variables which have the same value
under $\operatorname*{map}\nolimits_{x,y}$, and therefore there is no such
pair inside $\left( V\diagdown\left\{ y\right\} \right) \times\left(
V\diagdown\left\{ x\right\} \right) $). Thus, $\operatorname*{map}%
\nolimits_{x,y}\left( \left( \operatorname*{FV}v\right) \setminus\left\{
z\right\} \right) =\left( \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}v\right) \right) \setminus\left( \operatorname*{map}%
\nolimits_{x,y}\left\{ z\right\} \right) $ (since $\operatorname*{FV}v$ and
$\left\{ z\right\} $ both are subsets of $V\diagdown\left\{ y\right\} $).
Since $\operatorname*{map}\nolimits_{x,y}\left\{ z\right\} =\left\{
z\right\} $ (because $z\neq x$, and thus $\operatorname*{map}\nolimits_{x,y}%
z=z$), this becomes $\operatorname*{map}\nolimits_{x,y}\left( \left(
\operatorname*{FV}v\right) \setminus\left\{ z\right\} \right) =\left(
\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}v\right) \right)
\setminus\left\{ z\right\} $. Now,%
\[
\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right) =\left(
\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}v\right) \right)
\setminus\left\{ z\right\} =\operatorname*{map}\nolimits_{x,y}\left(
\underbrace{\left( \operatorname*{FV}v\right) \setminus\left\{ z\right\}
}_{=\operatorname*{FV}u}\right) =\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right) .
\]
Thus, $\operatorname*{FV}\left( u\left\langle y / x\right\rangle \right)
=\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV} u\right) $ is
proven in every possible case and subcase. Lemma 1.C is proven.
\begin{quote}
\textbf{Lemma 1.D.} Let $x$ and $x^{\prime}$ be two variables, let $u$ and
$u^{\prime}$ be two terms in $L$, and let $y$ be a variable which does not
appear in any of the terms $u$ and $u^{\prime}$. Assume that
$\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right)
=\operatorname*{FV}\left( u^{\prime}\left\langle y/x^{\prime}\right\rangle
\right) $. Then, $\operatorname*{FV}\left( \lambda xu\right)
=\operatorname*{FV}\left( \lambda x^{\prime}u^{\prime}\right) $.
\end{quote}
\textit{Proof of Lemma 1.D.} Lemma 1.C yields $\operatorname*{FV}\left(
u\left\langle y/x\right\rangle \right) =\operatorname*{map}\nolimits_{x,y}%
\left( \operatorname*{FV}u\right) $ (where $\operatorname*{map}%
\nolimits_{x,y}$ is defined as in Lemma 1.C). But $y\notin\operatorname*{FV}u$
(because $y$ does not appear in $u$). Now we will prove that $\left(
\operatorname*{FV}u\right) \setminus\left\{ x\right\} =\left(
\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}u\right) \right)
\setminus\left\{ y\right\} $.
In fact, let $z$ be an arbitrary element of $\left( \operatorname*{FV}%
u\right) \setminus\left\{ x\right\} $. Then, $z\neq x$, but also
$z\in\operatorname*{FV}u$, so that $z\neq y$ (since $z\in\operatorname*{FV}u$
and $y\notin\operatorname*{FV}u$). Now, due to $z\neq x$, we have
$\operatorname*{map}\nolimits_{x,y}z=z$ (because $\operatorname*{map}%
\nolimits_{x,y}w=w$ for every variable $w\neq x$), and thus
$z=\operatorname*{map}\nolimits_{x,y}z\in\operatorname*{map}\nolimits_{x,y}%
\left( \operatorname*{FV}u\right) $ (since $z\in\operatorname*{FV}u$).
Together with $z\notin\left\{ y\right\} $ (since $z\neq y$), this yields
$z\in\left( \operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}%
u\right) \right) \setminus\left\{ y\right\} $. Thus we have shown that
every $z\in\left( \operatorname*{FV}u\right) \setminus\left\{ x\right\} $
satisfies $z\in\left( \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right) \right) \setminus\left\{ y\right\} $. In other
words, $\left( \operatorname*{FV}u\right) \setminus\left\{ x\right\}
\subseteq\left( \operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}%
u\right) \right) \setminus\left\{ y\right\} $.
Now, let $z^{\prime}$ be an arbitrary element of $\left( \operatorname*{map}%
\nolimits_{x,y}\left( \operatorname*{FV}u\right) \right) \setminus\left\{
y\right\} $. Then, $z^{\prime}\in\operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right) $, so that there exists some $w^{\prime}%
\in\operatorname*{FV}u$ such that $z^{\prime}=\operatorname*{map}%
\nolimits_{x,y}w^{\prime}$. Consider this $w^{\prime}$. Clearly, $w^{\prime
}\neq x$ (since $w^{\prime}=x$ would yield $z^{\prime}=\operatorname*{map}%
\nolimits_{x,y}\underbrace{w^{\prime}}_{=x}=\operatorname*{map}\nolimits_{x,y}%
x=y$, contradicting $z^{\prime}\in\left( \operatorname*{map}\nolimits_{x,y}%
\left( \operatorname*{FV}u\right) \right) \setminus\left\{ y\right\} $).
Thus, $\operatorname*{map}\nolimits_{x,y}w^{\prime}=w^{\prime}$ (since
$\operatorname*{map}\nolimits_{x,y}w=w$ for every variable $w\neq x$). Thus,
$z^{\prime}=\operatorname*{map}\nolimits_{x,y}w^{\prime}=w^{\prime}%
\in\operatorname*{FV}u$. Combined with $z^{\prime}\notin\left\{ x\right\} $
(since $z^{\prime}=w^{\prime}\neq x$), this yields $z^{\prime}\in\left(
\operatorname*{FV}u\right) \setminus\left\{ x\right\} $. Thus we have shown
that every $z^{\prime}\in\left( \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right) \right) \setminus\left\{ y\right\} $ satisfies
$z^{\prime}\in\left( \operatorname*{FV}u\right) \setminus\left\{ x\right\}
$. In other words, $\left( \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right) \right) \setminus\left\{ y\right\}
\subseteq\left( \operatorname*{FV}u\right) \setminus\left\{ x\right\} $.
Combined with $\left( \operatorname*{FV}u\right) \setminus\left\{
x\right\} \subseteq\left( \operatorname*{map}\nolimits_{x,y}\left(
\operatorname*{FV}u\right) \right) \setminus\left\{ y\right\} $, this
yields $\left( \operatorname*{FV}u\right) \setminus\left\{ x\right\}
=\left( \operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}u\right)
\right) \setminus\left\{ y\right\} $.
Thus,%
\[
\operatorname*{FV}\left( \lambda xu\right) =\left( \operatorname*{FV}%
u\right) \setminus\left\{ x\right\} =\underbrace{\left(
\operatorname*{map}\nolimits_{x,y}\left( \operatorname*{FV}u\right) \right)
}_{=\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right)
}\setminus\left\{ y\right\} =\left( \operatorname*{FV}\left( u\left\langle
y/x\right\rangle \right) \right) \diagdown\left\{ y\right\} .
\]
Similarly, $\operatorname*{FV}\left( \lambda x^{\prime}u^{\prime}\right)
=\left( \operatorname*{FV}\left( u^{\prime}\left\langle y/x^{\prime
}\right\rangle \right) \right) \setminus\left\{ y\right\} $. Therefore,
$\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right)
=\operatorname*{FV}\left( u^{\prime}\left\langle y/x^{\prime}\right\rangle
\right) $ yields%
\[
\operatorname*{FV}\left( \lambda xu\right) =\underbrace{\left(
\operatorname*{FV}\left( u\left\langle y/x\right\rangle \right) \right)
}_{=\operatorname*{FV}\left( u^{\prime}\left\langle y/x^{\prime}\right\rangle
\right) }\setminus\left\{ y\right\} =\left( \operatorname*{FV}\left(
u^{\prime}\left\langle y/x^{\prime}\right\rangle \right) \right)
\setminus\left\{ y\right\} =\operatorname*{FV}\left( \lambda x^{\prime
}u^{\prime}\right) .
\]
Lemma 1.D is proven.
Lemma 1.D is used in the proof that $t$ and $t^{\prime}$ have the same free
variables if $t\equiv t^{\prime}$ (this fact is given without proof on page 12
of [1]).
\begin{quote}
\textbf{Lemma 1.E.} Let $u$ be a term in $L$, and $x$ be a variable. Then,
$u\left\langle x/x\right\rangle =u$.
\end{quote}
\textit{Proof of Lemma 1.E.} This is a trivial induction proof (induction on
$u$), so we omit it.
Lemma 1.E is used in the proof of Proposition 1.14 in [1] (in fact, it is the
reason why $u^{\prime}\left[ x^{\prime}/x^{\prime}\right] =u^{\prime}$).
\begin{center}
\textbf{3. Equivalent definitions of }$\alpha$\textbf{-equivalence}
\end{center}
Not everybody defines the notion of $\alpha$-equivalence the same way as it is
done in [1]. In some other texts, $\alpha$-equivalence is defined in a
different way, which, instead of the substitution $\left\langle
t/x\right\rangle $ defined in [1], uses another notion of substitution:
\begin{quote}
\textbf{Definition.} For any term $t$ in $L$ and any variables $x_{1}$ and
$y_{1}$, we define the term $t\left\{ y_{1}/x_{1}\right\} $ as the result of
the replacement of \textit{every} occurence of $x_{1}$ in $t$ by $y_{1}$
(where "every occurence" really means "every occurence", including bounded and
free occurences and occurences in abstractions). The definition is by
induction on $t$, as follows:
if $t=x_{1}$, then $t\left\{ y_{1}/x_{1}\right\} =y_{1}$;
if $t$ is a variable $\neq x_{1}$, then $t\left\{ y_{1}/x_{1}\right\} =t$;
if $t=\left( u\right) v$ for some terms $u$ and $v$, then $t\left\{
y_{1}/x_{1}\right\} =\left( u\left\{ y_{1}/x_{1}\right\} \right) \left(
v\left\{ y_{1}/x_{1}\right\} \right) $;
if $t=\lambda xu$ for some variable $x$ and some term $u$, then $t\left\{
y_{1}/x_{1}\right\} =\lambda\left( x\left\{ y_{1}/x_{1}\right\} \right)
\left( u\left\{ y_{1}/x_{1}\right\} \right) $.
\end{quote}
Intuitively, this $\left\{ y_{1}/x_{1}\right\} $ substitution is a very
low-level kind of substitution, best understood as a blind find-replace
operation without regard to the meaning of the $x_{1}$'s which are being
replaced. Similarly one can define a substitution $\left\{ y_{1}%
/x_{1},...,y_{m}/x_{m}\right\} $ for $m$ variables $x_{1},...,x_{m}$ and $m$
variables $y_{1},...,y_{m}$, but I will not use it.\footnote{Note that
$t\left\{ s/x\right\} $ \textit{cannot} be defined if $s$ is just assumed to
be an arbitrary term (rather than a single variable).} Now here is the second
definition of $\alpha$-equivalence I am speaking about:
\begin{quote}
\textbf{Definition.} Let us define a relation $=^{\alpha}$ on terms in
$L$.\ \ \ \ \footnote{We denote this relation by $=^{\alpha}$, but later (in
Theorem 1.F) we will show that this relation is identical to the relation
$\equiv$ from [1].} Namely, we define $t=^{\alpha}t^{\prime}$ by induction on
the length of $t$ by the following clauses:
if $t$ is a variable, then $t=^{\alpha}t^{\prime}$ if and only if
$t=t^{\prime}$;
if $t=\left( u\right) v$ for some terms $u$ and $v$, then $t=^{\alpha
}t^{\prime}$ if and only if $t^{\prime}=\left( u^{\prime}\right) v^{\prime}$
for some terms $u^{\prime}$ and $v^{\prime}$ with $u=^{\alpha}u^{\prime}$ and
$v=^{\alpha}v^{\prime}$;
if $t=\lambda xu$ for some variable $x$ and some term $u$, then $t=^{\alpha
}t^{\prime}$ if and only if $t^{\prime}=\lambda x^{\prime}u^{\prime}$ for some
variable $x^{\prime}$ and some term $u^{\prime}$ such that all variables $y$
except a finite number satisfy $u\left\{ y/x\right\} =^{\alpha}u^{\prime
}\left\{ y/x^{\prime}\right\} $.
\end{quote}
We claim that the relation $=^{\alpha}$ defined by this definition is the
$\alpha$-equivalence defined in [1]; i. e., we claim that the following
theorem holds:
\begin{quote}
\textbf{Theorem 1.F.} The relations $\equiv$ and $=^{\alpha}$ are identical.
\end{quote}
We prove this using a lemma:
\begin{quote}
\textbf{Lemma 1.G.} Let $t$ be a term in $L$. Let $x$ and $y$ be two variables
such that $y$ does not occur in $t$. Then, $t\left\langle y/x\right\rangle
\equiv t\left\{ y/x\right\} $.
\end{quote}
\textit{Proof of Lemma 1.G.} We prove this by induction over $t$:
If $t$ is a variable, then everything is clear because the definitions of
$t\left\langle y / x\right\rangle $ and $t\left\{ y / x\right\} $ for $t$
being a variable are the same.
If $t=\left( u\right) v$ for some terms $u$ and $v$, then everything is
clear again because the definition of $t\left\langle y/x\right\rangle $ says%
\begin{align*}
t\left\langle y/x\right\rangle & =\underbrace{\left( u\left\langle
y/x\right\rangle \right) }_{\substack{\equiv u\left\{ y/x\right\}
\\\text{(by the induction}\\\text{assumption)}}}\underbrace{\left(
v\left\langle y/x\right\rangle \right) }_{\substack{\equiv v\left\{
y/x\right\} \\\text{(by the induction}\\\text{assumption)}}%
}\ \ \ \ \ \ \ \ \ \ \left( \text{since }t=\left( u\right) v\right) \\
& \equiv\left( u\left\{ y/x\right\} \right) \left( v\left\{
y/x\right\} \right) =t\left\{ y/x\right\} \\
& \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since the definition of }t\left\{ y/x\right\} \text{ says}\\
\text{ }t\left\{ y/x\right\} =\left( u\left\{ y/x\right\} \right)
\left( v\left\{ y/x\right\} \right) \text{ (since }t=\left( u\right)
v\text{)}%
\end{array}
\right) .
\end{align*}
So it only remains to consider the case when $t=\lambda zu$ for some variable
$z$ and some term $u$. By the induction assumption, $u\left\langle y /
x\right\rangle \equiv u\left\{ y / x\right\} $.
Two subcases are possible: the subcase $z\neq x$ and the subcase $z=x$.
First consider the subcase $z\neq x$. In this subcase, $t\left\langle
y/x\right\rangle =\lambda z\left( u\left\langle y/x\right\rangle \right)
\equiv\lambda z\left( u\left\{ y/x\right\} \right) $ (by Corollary 1.7,
since $u\left\langle y/x\right\rangle \equiv u\left\{ y/x\right\} $) and
\newline$t\left\{ y/x\right\} =\lambda\left( z\left\{ y/x\right\}
\right) \left( u\left\{ y/x\right\} \right) =\lambda z\left( u\left\{
y/x\right\} \right) $ (since $z\neq x$ and thus $z\left\{ y/x\right\}
=z$), so that $t\left\langle y/x\right\rangle \equiv\lambda z\left( u\left\{
y/x\right\} \right) =t\left\{ y/x\right\} $.
Now consider the subcase $z=x$. In this subcase, $t=\lambda zu=\lambda xu$, so
that $t\left\langle y/x\right\rangle =\lambda xu$, but on the other hand
$t=\lambda xu$ gives us $t\left\{ y/x\right\} =\lambda\underbrace{\left(
x\left\{ y/x\right\} \right) }_{=y}\left( u\left\{ y/x\right\} \right)
=\lambda y\left( u\left\{ y/x\right\} \right) \equiv\lambda y\left(
u\left\langle y/x\right\rangle \right) $ (by Corollary 1.7, since $u\left\{
y/x\right\} \equiv u\left\langle y/x\right\rangle $). Since $y$ does not
occur in $u$ (because $y$ does not occur in $t$), we have $\lambda
xu\equiv\lambda y\left( u\left\langle y/x\right\rangle \right) $ by Lemma
1.9, so that $t\left\langle y/x\right\rangle =\lambda xu\equiv\lambda y\left(
u\left\langle y/x\right\rangle \right) \equiv t\left\{ y/x\right\} $.
Hence, $t\left\langle y / x\right\rangle \equiv t\left\{ y / x\right\} $ is
proved in every case and every subcase. Lemma 1.G is thus proven.
\begin{quote}
\textbf{Lemma 1.H.} Let $t$ and $t^{\prime}$ be two terms in $L$ such that
$t=^{\alpha}t^{\prime}$. Then, $t\equiv t^{\prime}$.
\end{quote}
\textit{Proof of Lemma 1.H.} We proceed by induction over the length of $t$.
There are three cases to consider: the case when $t$ is a variable; the case
when $t=\left( u\right) v$ for some terms $u$ and $v$; the case when
$t=\lambda xu$ for some variable $x$ and some term $u$.
In the case when $t$ is a variable, the relation $t=^{\alpha}t^{\prime}$
yields that $t^{\prime}$ is the same variable as $t$. Thus, $t\equiv
t^{\prime}$.
In the case when $t=\left( u\right) v$ for some terms $u$ and $v$, the
relation $t=^{\alpha}t^{\prime}$ yields that $t^{\prime}=\left( u^{\prime
}\right) v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$ with
$u=^{\alpha}u^{\prime}$ and $v=^{\alpha}v^{\prime}$. By the induction
assumption, $u=^{\alpha}u^{\prime}$ yields $u\equiv u^{\prime}$, and
$v=^{\alpha}v^{\prime}$ yields $v\equiv v^{\prime}$. Thus, $t^{\prime}=\left(
u^{\prime}\right) v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$
with $u\equiv u^{\prime}$ and $v\equiv v^{\prime}$. This means that $t\equiv
t^{\prime}$.
Now let us consider the final remaining case: the case when $t=\lambda xu$ for
some variable $x$ and some term $u$. In this case, $t=^{\alpha}t^{\prime}$
means that $t^{\prime}=\lambda x^{\prime}u^{\prime}$ for some variable
$x^{\prime}$ and some term $u^{\prime}$ such that all variables $y$ except a
finite number satisfy $u\left\{ y/x\right\} =^{\alpha}u^{\prime}\left\{
y/x^{\prime}\right\} $. By the induction assumption, this yields that all
variables $y$ except a finite number satisfy $u\left\{ y/x\right\} \equiv
u^{\prime}\left\{ y/x^{\prime}\right\} $ (because the terms $u\left\{
y/x\right\} $ and $u^{\prime}\left\{ y/x^{\prime}\right\} $ are as long as
$u$ and $u^{\prime}$, respectively, and therefore shorter than $t$ and
$t^{\prime}$, respectively). Thus, all variables $y$ except a finite number
and except those which occur in $u$ or $u^{\prime}$ satisfy $u\left\langle
y/x\right\rangle \equiv u^{\prime}\left\langle y/x^{\prime}\right\rangle $
(because Lemma 1.G yields that these variables satisfy $u\left\langle
y/x\right\rangle \equiv u\left\{ y/x\right\} $ and $u^{\prime}\left\langle
y/x^{\prime}\right\rangle \equiv u^{\prime}\left\{ y/x^{\prime}\right\} $,
so that they satisfy $u\left\langle y/x\right\rangle \equiv u\left\{
y/x\right\} \equiv u^{\prime}\left\{ y/x^{\prime}\right\} \equiv u^{\prime
}\left\langle y/x^{\prime}\right\rangle $). But "all variables $y$ except a
finite number and except those which occur in $u$ or $u^{\prime}$ " can be
rewritten as "all variables $y$ except a finite number", because only finitely
many variables occur in $u$ or $u^{\prime}$. Thus, all variables $y$ except a
finite number satisfy $u\left\langle y/x\right\rangle \equiv u^{\prime
}\left\langle y/x^{\prime}\right\rangle $. Hence, $t\equiv t^{\prime}$ (by the
definition of $\equiv$).
Thus we have proven that $t\equiv t^{\prime}$ in all possible cases. The proof
of Lemma 1.H is complete.
\begin{quote}
\textbf{Lemma 1.I.} Let $t$ and $t^{\prime}$ be two terms in $L$ such that
$t\equiv t^{\prime}$. Then, $t=^{\alpha}t^{\prime}$.
\end{quote}
\textit{Proof of Lemma 1.I.} We proceed by induction over the length of $t$.
There are three cases to consider: the case when $t$ is a variable; the case
when $t=\left( u\right) v$ for some terms $u$ and $v$; the case when
$t=\lambda xu$ for some variable $x$ and some term $u$.
In the case when $t$ is a variable, the relation $t\equiv t^{\prime}$ yields
that $t^{\prime}$ is the same variable as $t$. Thus, $t=^{\alpha}t^{\prime}$.
In the case when $t=\left( u\right) v$ for some terms $u$ and $v$, the
relation $t\equiv t^{\prime}$ yields that $t^{\prime}=\left( u^{\prime
}\right) v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$ with
$u\equiv u^{\prime}$ and $v\equiv v^{\prime}$. By the induction assumption,
$u\equiv u^{\prime}$ yields $u=^{\alpha}u^{\prime}$, and $v\equiv v^{\prime}$
yields $v=^{\alpha}v^{\prime}$. Thus, $t^{\prime}=\left( u^{\prime}\right)
v^{\prime}$ for some terms $u^{\prime}$ and $v^{\prime}$ with $u=^{\alpha
}u^{\prime}$ and $v=^{\alpha}v^{\prime}$. This means that $t=^{\alpha
}t^{\prime}$.
Now let us consider the final remaining case: the case when $t=\lambda xu$ for
some variable $x$ and some term $u$. In this case, $t\equiv t^{\prime}$ means
that $t^{\prime}=\lambda x^{\prime}u^{\prime}$ for some variable $x^{\prime}$
and some term $u^{\prime}$ such that all variables $y$ except a finite number
satisfy $u\left\langle y/x\right\rangle \equiv u^{\prime}\left\langle
y/x^{\prime}\right\rangle $. Thus, all variables $y$ except a finite number
and except those which occur in $u$ or $u^{\prime}$ satisfy $u\left\{
y/x\right\} \equiv u^{\prime}\left\{ y/x^{\prime}\right\} $ (because Lemma
1.G yields that these variables satisfy $u\left\langle y/x\right\rangle \equiv
u\left\{ y/x\right\} $ and $u^{\prime}\left\langle y/x^{\prime}\right\rangle
\equiv u^{\prime}\left\{ y/x^{\prime}\right\} $, so that they satisfy
$u\left\{ y/x\right\} \equiv u\left\langle y/x\right\rangle \equiv
u^{\prime}\left\langle y/x^{\prime}\right\rangle \equiv u^{\prime}\left\{
y/x^{\prime}\right\} $). But "all variables $y$ except a finite number and
except those which occur in $u$ or $u^{\prime}$ " can be rewritten as "all
variables $y$ except a finite number", because only finitely many variables
occur in $u$ or $u^{\prime}$. Thus, all variables $y$ except a finite number
satisfy $u\left\{ y/x\right\} \equiv u^{\prime}\left\{ y/x^{\prime
}\right\} $. By the induction assumption, this yields that all variables $y$
except a finite number satisfy $u\left\{ y/x\right\} =^{\alpha}u^{\prime
}\left\{ y/x^{\prime}\right\} $ (because the terms $u\left\{ y/x\right\} $
and $u^{\prime}\left\{ y/x^{\prime}\right\} $ are as long as $u$ and
$u^{\prime}$, respectively, and therefore shorter than $t$ and $t^{\prime}$,
respectively). Hence, $t=^{\alpha}t^{\prime}$ (by the definition of
$=^{\alpha}$).
Thus we have proven that $t=^{\alpha}t^{\prime}$ in all possible cases. The
proof of Lemma 1.I is complete.
\textit{Proof of Theorem 1.F.} Theorem 1.F follows directly from Lemma 1.H and
Lemma 1.I.
\begin{center}
\textbf{4. Some rules for substitution}
\end{center}
Now we are going to prove the following properties of the substitution defined
in Chapter 1 \S 2 of [1]:
\begin{quote}
\textbf{Lemma 1.J.} Any variable $x$ and any $s\in\Lambda$ satisfy $x\left[
s/x\right] =s$.
\textbf{Lemma 1.K.} Any two distinct variables $x$ and $y$ and any
$s\in\Lambda$ satisfy $y\left[ s/x\right] =y$.
\textbf{Lemma 1.L.} If $t_{1}\in\Lambda$, $t_{2}\in\Lambda$ and $s\in\Lambda$
are three equivalence classes and $x$ is a variable, then $\left( t_{1}%
t_{2}\right) \left[ s/x\right] =\left( t_{1}\left[ s/x\right] \right)
\left( t_{2}\left[ s/x\right] \right) $.
\textbf{Lemma 1.M.} If $x$ and $y$ are two distinct variables, and
$s\in\Lambda$ and $r\in\Lambda$ are two equivalence classes, then $\left(
\lambda yr\right) \left[ s/x\right] =\lambda y^{\prime}\left( r\left[
y^{\prime}/y\right] \left[ s/x\right] \right) $, where $y^{\prime}$ is any
variable which is not free in $x$, $s$ or $r$.
\textbf{Lemma 1.N.} If $x$ and $y$ are two distinct variables, and
$s\in\Lambda$ and $r\in\Lambda$ are two equivalence classes such that $y$ is
not a free variable in $s$, then $\left( \lambda yr\right) \left[
s/x\right] =\lambda y\left( r\left[ s/x\right] \right) $.
\textbf{Lemma 1.O.} If $x$ is a variable, and $s\in\Lambda$ and $r\in\Lambda$
are two equivalence classes, then $\left( \lambda xr\right) \left[
s/x\right] =\lambda xr$.
\end{quote}
\textit{Proof of Lemma 1.J.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Clearly, $x$ is a representative of $x$, and no bound
variable of $x$ is free in $\underline{s}$ (since $x$ has no bound variable).
Therefore, by the definition of substitution, $x\left[ s/x\right] $ is the
equivalence class of $x\left\langle \underline{s}/x\right\rangle $. Since
$x\left\langle \underline{s}/x\right\rangle =\underline{s}$, this means that
$x\left[ s/x\right] $ is the equivalence class of $\underline{s}$. In other
words, $x\left[ s/x\right] =s$ (because $s$ is the equivalence class of
$\underline{s}$). This proves Lemma 1.J.
\textit{Proof of Lemma 1.K.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Clearly, $y$ is a representative of $y$, and no bound
variable of $y$ is free in $\underline{s}$ (since $y$ has no bound variable).
Therefore, by the definition of substitution, $y\left[ s/x\right] $ is the
equivalence class of $y\left\langle \underline{s}/x\right\rangle $. Since
$y\left\langle \underline{s}/x\right\rangle =y$, this means that $y\left[
s/x\right] $ is the equivalence class of $y$. In other words, $y\left[
s/x\right] =y$. This proves Lemma 1.K.
\textit{Proof of Lemma 1.L.} Let $\underline{s}$ be a representative of the
equivalence class $s$.
Let $\underline{t}_{1}$ be a representative of the equivalence class $t_{1}$
such that no bound variable of $\underline{t}_{1}$ is free in $s$%
.\ \ \ \ \footnote{Such a representative $\underline{t}_{1}$ exists due to
Lemma 1.10.} Let $\underline{t}_{2}$ be a representative of the equivalence
class $t_{2}$ such that no bound variable of $\underline{t}_{2}$ is free in
$s$.\ \ \ \ \footnote{Such a representative $\underline{t}_{2}$ exists due to
Lemma 1.10.} Then, clearly, no bound variable of $\underline{t}_{1}%
\underline{t}_{2}$ is free in $s$ (since $\operatorname*{BV}\left(
\underline{t}_{1}\underline{t}_{2}\right) =\left( \operatorname*{BV}%
\underline{t}_{1}\right) \cup\left( \operatorname*{BV}\underline{t}%
_{2}\right) $), and we know that $\underline{t}_{1}\underline{t}_{2}$ is a
representative of the equivalence class $t_{1}t_{2}$. Thus, the definition of
$\left( t_{1}t_{2}\right) \left[ s/x\right] $ says that $\left(
t_{1}t_{2}\right) \left[ s/x\right] $ is the equivalence class of $\left(
\underline{t}_{1}\underline{t}_{2}\right) \left\langle \underline{s}%
/x\right\rangle $. On the other hand, the definition of $t_{1}\left[
s/x\right] $ says that $t_{1}\left[ s/x\right] $ is the equivalence class
of $\underline{t}_{1}\left\langle \underline{s}/x\right\rangle $ (since no
bound variable of $\underline{t}_{1}$ is free in $s$), and the definition of
$t_{2}\left[ s/x\right] $ says that $t_{2}\left[ s/x\right] $ is the
equivalence class of $\underline{t}_{2}\left\langle \underline{s}%
/x\right\rangle $ (since no bound variable of $\underline{t}_{2}$ is free in
$s$). Since we know that $\left( \underline{t}_{1}\underline{t}_{2}\right)
\left\langle \underline{s}/x\right\rangle =\left( \underline{t}%
_{1}\left\langle \underline{s}/x\right\rangle \right) \left( \underline{t}%
_{2}\left\langle \underline{s}/x\right\rangle \right) $, we therefore
conclude that
\begin{align*}
\left( t_{1}t_{2}\right) \left[ s/x\right] & =\left( \text{equivalence
class of }\underbrace{\left( \underline{t}_{1}\underline{t}_{2}\right)
\left\langle \underline{s}/x\right\rangle }_{=\left( \underline{t}%
_{1}\left\langle \underline{s}/x\right\rangle \right) \left( \underline{t}%
_{2}\left\langle \underline{s}/x\right\rangle \right) }\right) \\
& =\left( \text{equivalence class of }\left( \underline{t}_{1}\left\langle
\underline{s}/x\right\rangle \right) \left( \underline{t}_{2}\left\langle
\underline{s}/x\right\rangle \right) \right) \\
& =\underbrace{\left( \text{equivalence class of }\underline{t}%
_{1}\left\langle \underline{s}/x\right\rangle \right) }_{=t_{1}\left[
s/x\right] }\underbrace{\left( \text{equivalence class of }\underline{t}%
_{2}\left\langle \underline{s}/x\right\rangle \right) }_{=t_{2}\left[
s/x\right] }\\
& =\left( t_{1}\left[ s/x\right] \right) \left( t_{2}\left[ s/x\right]
\right) .
\end{align*}
Lemma 1.L is proven.
\textit{Proof of Lemma 1.N.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Let $\underline{r}$ be a representative of the
equivalence class $r$ such that no bound variable of $\underline{r}$ is free
in $s$. \ \ \ \ \footnote{Such a representative $\underline{r}$ exists due to
Lemma 1.10.} Then, $\lambda y\underline{r}$ is a representative of $\lambda
yr$, and no bound variable of $\lambda y\underline{r}$ is free in $s$ (because
$\operatorname*{BV}\left( \lambda y\underline{r}\right) =\left\{ y\right\}
\cup\left( \operatorname*{BV}\underline{r}\right) $, but neither $y$ nor any
bound variable of $\underline{r}$ is free in $s$). Therefore, by the
definition of $\left( \lambda yr\right) \left[ s/x\right] $, we know that
$\left( \lambda yr\right) \left[ s/x\right] $ is the equivalence class of
$\left( \lambda y\underline{r}\right) \left\langle \underline{s}%
/x\right\rangle $. Since $\left( \lambda y\underline{r}\right) \left\langle
\underline{s}/x\right\rangle =\lambda y\left( \underline{r}\left\langle
\underline{s}/x\right\rangle \right) $ (because $x\neq y$), this rewrites as
follows: $\left( \lambda yr\right) \left[ s/x\right] $ is the equivalence
class of $\lambda y\left( \underline{r}\left\langle \underline{s}%
/x\right\rangle \right) $. But since $r\left[ s/x\right] $ is the
equivalence class of $\underline{r}\left\langle \underline{s}/x\right\rangle $
(by the definition of $r\left[ s/x\right] $, since no bound variable of
$\underline{r}$ is free in $s$), the class $\lambda y\left( r\left[
s/x\right] \right) $ is the equivalence class of $\lambda y\left(
\underline{r}\left\langle \underline{s}/x\right\rangle \right) $. So now we
know that both $\left( \lambda yr\right) \left[ s/x\right] $ and $\lambda
y\left( r\left[ s/x\right] \right) $ are the equivalence class of $\lambda
y\left( \underline{r}\left\langle \underline{s}/x\right\rangle \right) $.
Thus, $\left( \lambda yr\right) \left[ s/x\right] =\lambda y\left(
r\left[ s/x\right] \right) $. This proves Lemma 1.N.
\textit{Proof of Lemma 1.M.} Let $y^{\prime}$ be any variable which is not
free in $x$, $s$ or $r$. Then, $y^{\prime}$ is not free in $\lambda yr$
either. Proposition 1.14 (applied to $\lambda yr$, $y$, $r$ and $y^{\prime}$
instead of $t$, $x$, $u$ and $x^{\prime}$) yields $\lambda yr=\lambda
y^{\prime}\left( r\left[ y^{\prime}/y\right] \right) $. Lemma 1.N (applied
to $y^{\prime}$ and $r\left[ y^{\prime}/y\right] $ instead of $y$ and $r$)
yields $\left( \lambda y^{\prime}\left( r\left[ y^{\prime}/y\right]
\right) \right) \left[ s/x\right] =\lambda y^{\prime}\left( r\left[
y^{\prime}/y\right] \left[ s/x\right] \right) $ (here we use $y^{\prime
}\neq x$, which is because $y^{\prime}$ is not free in $x$). Thus,
$\underbrace{\left( \lambda yr\right) }_{=\lambda y^{\prime}\left( r\left[
y^{\prime}/y\right] \right) }\left[ s/x\right] =\left( \lambda y^{\prime
}\left( r\left[ y^{\prime}/y\right] \right) \right) \left[ s/x\right]
=\lambda y^{\prime}\left( r\left[ y^{\prime}/y\right] \left[ s/x\right]
\right) $. This proves Lemma 1.M.
\textit{Proof of Lemma 1.O.} Let $\underline{s}$ be a representative of the
equivalence class $s$. Let $\underline{p}$ be a representative of the
equivalence class $\lambda xr$ such that no bound variable of $\underline{p}$
is free in $s$.\ \ \ \ \footnote{Such a representative $\underline{p}$ exists
due to Lemma 1.10.} Then, the definition of $\left( \lambda xr\right)
\left[ s/x\right] $ yields that $\left( \lambda xr\right) \left[
s/x\right] $ is the equivalence class of $\underline{p}\left\langle
\underline{s}/x\right\rangle $. But $x$ is not a free variable in
$\underline{p}$ (because $x$ is not a free variable in $\lambda xr$), and
therefore $\underline{p}\left\langle \underline{s}/x\right\rangle
=\underline{p}$ (by Lemma 1.1 in [1]). Hence, $\left( \lambda xr\right)
\left[ s/x\right] $ is the equivalence class of $\underline{p}$ (since
$\left( \lambda xr\right) \left[ s/x\right] $ is the equivalence class of
$\underline{p}\left\langle \underline{s}/x\right\rangle $). In other words,
$\left( \lambda xr\right) \left[ s/x\right] =\lambda xr$ (since we know
that the equivalence class of $\underline{p}$ is $\lambda xr$). This proves
Lemma 1.O.
\begin{center}
\textbf{Appendix: Proof of Corollary 1.3 of [1], Chapter 1, \S 1}
\end{center}
Below is a writeup of the proof of Corollary 1.3 of [1]. I made this writeup
at a time when the proof given in [1] was wrong; now the proof in [1] was
corrected, so there is no use in this writeup anymore except for the little
bit of additional detail it gives.
\textit{Proof of Corollary 1.3:} WLOG assume that $x_{1},...,x_{u}$ are those
variables among the set $\left\{ x_{1},...,x_{m}\right\} $ which don't occur
in $t$. Then, $x_{1},...,x_{u}$ are not free in $t$, so that Lemma 1.1 yields
$t\left\langle y_{1}/x_{1},...,y_{m}/x_{m}\right\rangle =t\left\langle
y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle $. Now, the sets $\left\{
x_{u+1},...,x_{m}\right\} $ and $\left\{ y_{1},...,y_{m}\right\} $ have no
common elements (because every of the variables $x_{u+1},...,x_{m}$ occurs in
$t$, while none of the variables $y_{1},...,y_{m}$ does). The hypothesis of
Lemma 1.2 is satisfied (with $k=0$), because none of the $y_{i}$ is bound in
$t$. Thus,%
\[
t\left\langle y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle \left\langle
t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle =t\left\langle t_{u+1}/x_{u+1}%
,...,t_{m}/x_{m},t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle .
\]
But $y_{1},...,y_{m}$ are not free in $t$, and thus Lemma 1.1 yields%
\[
t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m},t_{1}/y_{1},...,t_{m}%
/y_{m}\right\rangle =t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m}%
\right\rangle .
\]
Finally, $x_{1},...,x_{u}$ are not free in $t$, so that Lemma 1.1 yields
(again)%
\[
t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m}\right\rangle =t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle .
\]
Altogether,%
\begin{align*}
& \underbrace{t\left\langle y_{1}/x_{1},...,y_{m}/x_{m}\right\rangle
}_{=t\left\langle y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle }\left\langle
t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle \\
& =t\left\langle y_{u+1}/x_{u+1},...,y_{m}/x_{m}\right\rangle \left\langle
t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle =t\left\langle t_{u+1}/x_{u+1}%
,...,t_{m}/x_{m},t_{1}/y_{1},...,t_{m}/y_{m}\right\rangle \\
& =t\left\langle t_{u+1}/x_{u+1},...,t_{m}/x_{m}\right\rangle =t\left\langle
t_{1}/x_{1},...,t_{m}/x_{m}\right\rangle ,
\end{align*}
qed.
\begin{center}
\textbf{References}
\end{center}
[1] Jean-Louis Krivine, \textit{Lambda-calculus, types and models}, 22 January
2009, updated version of 5 June 2011.\newline%
\texttt{http://www.pps.jussieu.fr/\symbol{126}krivine/articles/Lambda.pdf}
\end{document}