$M_{0}\twoheadrightarrow M_{0}^{\prime},\forall
j\in[1,n],M_{1j}\twoheadrightarrow M_{1j}^{\prime},M_{2j}\twoheadrightarrow
M_{2j}^{\prime},(M_{11}^{\prime}...,M_{1j-1}^{\prime},x_{j},M_{2j+1}^{\prime}...,M_{2n}^{\prime})is\leavevmode\nobreak\
written\leavevmode\nobreak\ as\leavevmode\nobreak\ M_{j*}^{\prime}$
$\int_{(M_{11},M_{12},...M_{1n})}^{(M_{21},M_{22},...,M_{2n})}M_{0}dx\leavevmode\nobreak\
\twoheadrightarrow\int_{M_{11}^{\prime}}^{M_{21}^{\prime}}\pi_{1}(M_{0}^{\prime}[M_{1*}^{\prime}/x])dx_{1}\oplus...\oplus\int_{M_{1n}^{\prime}}^{M_{2n}^{\prime}}\pi_{n}(M_{0}^{\prime}[M_{n*}^{\prime}/x])dx_{n}$

$M_{0}\twoheadrightarrow M_{0}^{\prime},M_{1}\twoheadrightarrow
M_{1}^{\prime},M_{2}\twoheadrightarrow M_{2}^{\prime},M_{1},M_{2}:\textsf{B}$
$\int_{M_{1}}^{M_{2}}\lambda y:T_{2}.M_{0}dx\leavevmode\nobreak\
\twoheadrightarrow\lambda
y:T_{2}.\int_{M_{1}^{\prime}}^{M_{2}^{\prime}}M_{0}^{\prime}dx$

$N\twoheadrightarrow N^{\prime},M\twoheadrightarrow
M^{\prime},M,N:\textsf{B},\forall j\in[1,n],M_{j}\twoheadrightarrow
M_{j}^{\prime}$
$\int_{M}^{N}(M_{1},M_{2},...M_{n})dx\twoheadrightarrow(\int_{M^{\prime}}^{N^{\prime}}M_{1}^{\prime}dx,\int_{M^{\prime}}^{N^{\prime}}M_{2}^{\prime}dx,...,\int_{M^{\prime}}^{N^{\prime}}M_{n}^{\prime}dx)$

$N\twoheadrightarrow N^{\prime},M\twoheadrightarrow M^{\prime},N:\textsf{B}$
$(\lambda x:T.M)*N\twoheadrightarrow\lambda x:T.(M^{\prime}*N^{\prime})$

$\forall j\in[1,n],M_{j}\twoheadrightarrow M_{j}^{\prime},N\twoheadrightarrow
N^{\prime},N:\textsf{B}$
$(M_{1},M_{2},...M_{n})*N\twoheadrightarrow(M_{1}^{\prime}*N^{\prime},M_{2}^{\prime}*N^{\prime},...M_{n}^{\prime}*N^{\prime})$

$\forall j\in[1,n],M_{1j}\twoheadrightarrow
M_{1j}^{\prime},M_{2j}\twoheadrightarrow M_{2j}^{\prime}$
$(M_{11},M_{12},...M_{1n})*(M_{21},M_{22},...M_{2n})\twoheadrightarrow
M_{11}^{\prime}*M_{21}^{\prime}\oplus
M_{12}^{\prime}*M_{22}^{\prime}\oplus...\oplus
M_{1n}^{\prime}*M_{2n}^{\prime}$

$M\twoheadrightarrow M^{\prime}$ $fix\leavevmode\nobreak\ M\twoheadrightarrow
M^{\prime}\leavevmode\nobreak\ (fix\leavevmode\nobreak\
M^{\prime}),fix\leavevmode\nobreak\ M\twoheadrightarrow
fix\leavevmode\nobreak\ M^{\prime}$

######  Lemma A.6 (Preservation of $\twoheadrightarrow$).

If $N:B,N\twoheadrightarrow N^{\prime}$, then $N^{\prime}:B$.

######  Proof A.7.

If we name the one-step relation of our calculus as $\rho$, and its transitive
closure as $\rho^{*}$, then we have $\twoheadrightarrow\subseteq\rho^{*}$. So
we have $N\rho^{*}N^{\prime}$. Notice that we have the preservation property
of our calculus, thus we have $N^{\prime}:B$.

######  Lemma A.8 ($\twoheadrightarrow$ under substitution).

$M\twoheadrightarrow M^{\prime}$, $N\twoheadrightarrow N^{\prime}$, then we
have $M[N/x]\twoheadrightarrow M^{\prime}[N^{\prime}/x]$

######  Proof A.9.

Induction on $M\twoheadrightarrow M^{\prime}$

  * •

Case $M\twoheadrightarrow M$, make induction on the form of M.

    * –

Subcase c, then c[N/x] = c = c[N’/x], using $M\twoheadrightarrow M$ we have
$M[N/x]\twoheadrightarrow M[N^{\prime}/x]$.

    * –

Subcase $(t_{1},t_{2},...,t_{n})$, using induction we have
$t_{i}[N/x]\twoheadrightarrow t_{i}[N^{\prime}/x]$, Then using $\forall
i,M_{i}\twoheadrightarrow
M_{i}^{\prime}\Rightarrow(M_{1},M_{2},..,M_{n})\twoheadrightarrow(M_{1}^{\prime},M_{2}^{\prime},..,M_{n}^{\prime})$
we have $M\twoheadrightarrow M$ we have $M[N/x]\twoheadrightarrow
M[N^{\prime}/x]$.

Using the same technique, we can prove the subcase of $t\oplus t$, $t\ominus
t$, $t*t$, $\lambda x:T.t$, $t\ t$ , $\frac{\partial t}{\partial x}|_{t}$,
$\int_{t}^{t}tdx$, $\pi_{j}(t)$,
$\int_{M_{1}}^{M_{2}}M_{3}dx\twoheadrightarrow\int_{M_{1}^{\prime}}^{M_{2}^{\prime}}M_{3}^{\prime}dx,inl/inr\leavevmode\nobreak\
M,case\leavevmode\nobreak\ inr\leavevmode\nobreak\ M_{1}\leavevmode\nobreak\
of\leavevmode\nobreak\ inl\leavevmode\nobreak\ x_{1}\Rightarrow
M_{2}|\leavevmode\nobreak\ inr\leavevmode\nobreak\ x_{2}\Rightarrow M_{3}$.

    * –

Subcase variable y, if y = x then y[N/x] = N, y[N’/x] = N’, then
$y[N/x]\twoheadrightarrow y[N^{\prime}/x]$, if y is not x then same as the
subcase c.

The rest cases can be divided into three categories.

  * •

Case relation based on the relation of subterms.

    * –

Subcase $M\leavevmode\nobreak\ N\twoheadrightarrow
M^{\prime}\leavevmode\nobreak\ N^{\prime}$, using induction we have
$M[K/x]\twoheadrightarrow M^{\prime}[K^{\prime}/x]$, $N[K/x]\twoheadrightarrow
N^{\prime}[K^{\prime}/x]$, using $M\twoheadrightarrow
M^{\prime},N\twoheadrightarrow N^{\prime}\Rightarrow M\leavevmode\nobreak\
N\twoheadrightarrow M^{\prime}\leavevmode\nobreak\ N^{\prime}$ we have
$(M\leavevmode\nobreak\
N)[K/x]\twoheadrightarrow(M^{\prime}\leavevmode\nobreak\
N^{\prime})[K^{\prime}/x]$.

    * –

Subcases $M\oplus N\twoheadrightarrow M^{\prime}\oplus N^{\prime}$, $M\ominus
N\twoheadrightarrow M^{\prime}\ominus N^{\prime}$, $M*N\twoheadrightarrow
M^{\prime}*N^{\prime}$, $\frac{\partial M}{\partial
x}|_{N}\twoheadrightarrow\frac{\partial M^{\prime}}{\partial
x}|_{N^{\prime}}$,
$(M_{1},M_{2},..,M_{n})\twoheadrightarrow(M_{1}^{\prime},M_{2}^{\prime},..,M_{n}^{\prime})$,
$\lambda x:T.M\twoheadrightarrow\lambda
x:T.M^{\prime},\pi_{j}(M)\twoheadrightarrow\pi_{j}(M^{\prime})$,
$fix\leavevmode\nobreak\ M\twoheadrightarrow fix\leavevmode\nobreak\
M^{\prime}$, $inl/inr\leavevmode\nobreak\ M\twoheadrightarrow
inl/inr\leavevmode\nobreak\ M^{\prime}$: same as $M\leavevmode\nobreak\
N\twoheadrightarrow M^{\prime}\leavevmode\nobreak\ N^{\prime}$.

  * •

Case reduction changes the structure

    * –

Subcase
$(M_{11},M_{12},...M_{1n})\oplus(M_{21},M_{22},...M_{2n})\twoheadrightarrow(M_{11}^{\prime}\oplus
M_{21}^{\prime},M_{12}^{\prime}\oplus M_{22}^{\prime},...M_{1n}^{\prime}\oplus
M_{2n}^{\prime})$, using induction we have $\forall i\in[1,2],\forall
j\in[1,n],M_{ij}[K/x]\twoheadrightarrow M_{ij}^{\prime}[K^{\prime}/x]$, so we
have

$((M_{11},M_{12},...M_{1n})\oplus(M_{21},M_{22},...M_{2n}))[K/x]\twoheadrightarrow(M_{11}^{\prime}\oplus
M_{21}^{\prime},M_{12}^{\prime}\oplus M_{22}^{\prime},...M_{1n}^{\prime}\oplus
M_{2n}^{\prime})[K^{\prime}/x]$.

    * –

Subcases
$(M_{11},M_{12},...M_{1n})\ominus(M_{21},M_{22},...M_{2n})\twoheadrightarrow(M_{11}^{\prime}\ominus
M_{21}^{\prime},M_{12}^{\prime}\ominus
M_{22}^{\prime},...M_{1n}^{\prime}\ominus M_{2n}^{\prime})$,
$\frac{\partial(M_{1},M_{2},..,M_{n})}{\partial
x}|_{N}\twoheadrightarrow(\frac{\partial M_{1}^{\prime}}{\partial
x}|_{N^{\prime}},\frac{\partial M_{2}^{\prime}}{\partial
x}|_{N^{\prime}},...,\frac{\partial M_{n}^{\prime}}{\partial
x}|_{N^{\prime}})$, $\frac{\partial\lambda y:T.M}{\partial
x}|_{N}\twoheadrightarrow\lambda y:T.\frac{\partial M^{\prime}}{\partial
x}|_{N^{\prime}}$, $\int_{M_{1}}^{M_{2}}\lambda
y:T_{2}.M_{0}dx\leavevmode\nobreak\ \twoheadrightarrow\lambda
y:T_{2}.\int_{M_{1}^{\prime}}^{M_{2}^{\prime}}M_{0}^{\prime}dx$,
$\int_{M}^{N}(M_{1},M_{2},...M_{n})dx\twoheadrightarrow(\int_{M^{\prime}}^{N^{\prime}}M_{1}^{\prime}dx,\int_{M^{\prime}}^{N^{\prime}}M_{2}^{\prime}dx,...,\int_{M^{\prime}}^{N^{\prime}}M_{n}^{\prime}dx)$,
$(\lambda x:T.M)*N\twoheadrightarrow\lambda x:T.(M^{\prime}*N^{\prime})$,
$(M_{1},M_{2},...M_{n})*N\twoheadrightarrow(M_{1}^{\prime}*N^{\prime},M_{2}^{\prime}*N^{\prime},...M_{n}^{\prime}*N^{\prime})$,
$(M_{11},M_{12},...M_{1n})*(M_{21},M_{22},...M_{2n})\twoheadrightarrow
M_{11}^{\prime}*M_{12}^{\prime}\oplus
M_{21}^{\prime}*M_{22}^{\prime}\oplus...\oplus
M_{1n}^{\prime}*M_{2n}^{\prime}$, $fix\leavevmode\nobreak\ M\twoheadrightarrow
M^{\prime}\leavevmode\nobreak\ (fix\leavevmode\nobreak\ M^{\prime})$: same as
$(M_{11},M_{12},...M_{1n})\oplus(M_{21},M_{22},...M_{2n})\twoheadrightarrow(M_{11}^{\prime}\oplus
M_{21}^{\prime},M_{12}^{\prime}\oplus M_{22}^{\prime},...M_{1n}^{\prime}\oplus
M_{2n}^{\prime})$.

  * •

Case reduction involves substitution

    * –

Subcase $(\lambda x:T.M)N\twoheadrightarrow M^{\prime}[N^{\prime}/x]$, by
induction hypothesis, we have $M[K/y]\twoheadrightarrow
M^{\prime}[K^{\prime}/y]$, $N[K/y]\twoheadrightarrow
N^{\prime}[K^{\prime}/y]$, thus $((\lambda x:T.M)N)[K/y]=((\lambda
x:T.M[K/y])N[K/y])\twoheadrightarrow
M^{\prime}[K^{\prime}/y]([(N^{\prime}[K^{\prime}/y])/x)$, and we have
$M^{\prime}[N^{\prime}/x][K^{\prime}/y]=M^{\prime}[K^{\prime}/y]([(N^{\prime}[K^{\prime}/y])/x)$,
Therefore we prove the case.

    * –

Subcase$\forall
i,(M_{1}^{\prime},M_{2}^{\prime}...,M_{i-1}^{\prime},x_{i},M_{i+1}^{\prime}...,M_{n}^{\prime})is\leavevmode\nobreak\
written\leavevmode\nobreak\ as\leavevmode\nobreak\
M_{i*}^{\prime},\frac{\partial M_{0}}{\partial
x}|_{(M_{1},M_{2},...,M_{n})}\twoheadrightarrow$

$(\frac{\partial M_{0}^{\prime}[M_{1*}^{\prime}/x]}{\partial
x_{1}}|_{M_{1}^{\prime}},\frac{\partial M_{0}[M_{2*}^{\prime}/x]}{\partial
x_{2}}|_{M_{2}^{\prime}},...,\frac{\partial t[M_{n*}^{\prime}/x]}{\partial
x_{n}}|_{M_{n}^{\prime}})$

Notice that

$\begin{array}[]{llll}\\\ M_{0}^{\prime}[M_{i*}^{\prime}/x][K^{\prime}/y]\\\
\quad=\quad M_{0}^{\prime}[K^{\prime}/y][(M_{i*}^{\prime}[K^{\prime}/y])/x]\\\
\quad=\quad(M_{0}^{\prime}[K^{\prime}/y])[(M_{1}^{\prime}[K^{\prime}/y],M_{2}^{\prime}[K^{\prime}/y],...,\\\
\phantom{\quad=\quad(M_{0}^{\prime}[K^{\prime}/y])[(}M_{i-1}^{\prime}[K^{\prime}/y],x_{i}[K^{\prime}/y],M_{i+1}^{\prime}[K^{\prime}/y],...,M_{n}^{\prime}[K^{\prime}/y])/x]\\\
\quad=\quad(M_{0}^{\prime}[K^{\prime}/y])[((M^{\prime}[K^{\prime}/y])_{i*}^{\prime})/x]\par\end{array}$

Using induction, we know that $M_{i}[K/y]\twoheadrightarrow
M_{i}^{\prime}[K^{\prime}/y]$, so we prove the case.

    * –

Subcase $(\lambda x:T.M)\oplus(\lambda y:T.N)\twoheadrightarrow\lambda
x:T.M^{\prime}\oplus N^{\prime}[y/x]$, $(\lambda x:T.M)\ominus(\lambda
y:T.N)\twoheadrightarrow\lambda x:T.M^{\prime}\ominus N^{\prime}[y/x]$: same
as $(\lambda x:T.M)N\twoheadrightarrow M^{\prime}[N^{\prime}/x]$.

    * –

Subcases
$\int_{(M_{11},M_{12},...M_{1n})}^{(M_{21},M_{22},...,M_{2n})}M_{0}dx\leavevmode\nobreak\
\twoheadrightarrow\int_{M_{11}^{\prime}}^{M_{21}^{\prime}}\pi_{1}(M_{0}^{\prime}[M_{1*}^{\prime}/x])dx_{1}\oplus...\oplus\int_{M_{1n}^{\prime}}^{M_{2n}^{\prime}}\pi_{n}(M_{0}^{\prime}[M_{n*}^{\prime}/x])dx_{n}$,
$case\leavevmode\nobreak\ inl\leavevmode\nobreak\ M_{1}\leavevmode\nobreak\
of\leavevmode\nobreak\ inl\leavevmode\nobreak\ x_{1}\Rightarrow
M_{2}|\leavevmode\nobreak\ inr\leavevmode\nobreak\ x_{2}\Rightarrow
M_{3}\twoheadrightarrow M_{2}^{\prime}[M_{1}^{\prime}/x_{1}]$
,$case\leavevmode\nobreak\ inr\leavevmode\nobreak\ M_{1}\leavevmode\nobreak\
of\leavevmode\nobreak\ inl\leavevmode\nobreak\ x_{1}\Rightarrow
M_{2}|\leavevmode\nobreak\ inr\leavevmode\nobreak\ x_{2}\Rightarrow
M_{3}\twoheadrightarrow M_{3}^{\prime}[M_{1}^{\prime}/x_{2}]$ : same as
$\forall
i,(M_{1}^{\prime},M_{2}^{\prime},M_{i-1}^{\prime},x_{i},M_{i+1}^{\prime}...,M_{n}^{\prime})$is
written as $M_{i*}^{\prime}$ ,$\frac{\partial M_{0}}{\partial
x}|_{(M_{1},M_{2},...,M_{n})}\twoheadrightarrow$ $(\frac{\partial
M_{0}^{\prime}[M_{1*}^{\prime}/x]}{\partial
x_{1}}|_{M_{1}^{\prime}},\frac{\partial M_{0}[M_{2*}^{\prime}/x]}{\partial
x_{2}}|_{M_{2}^{\prime}},...,\frac{\partial t[M_{n*}^{\prime}/x]}{\partial
x_{n}}|_{M_{n}^{\prime}})$.

Thus we complete the proof.

######  Lemma A.10 (diamond property).

For $M\twoheadrightarrow M_{1},M\twoheadrightarrow M_{2}$, there exists a
$M_{3}$, such that $M_{1}\twoheadrightarrow M_{3},M_{2}\twoheadrightarrow
M_{3}$

######  Proof A.11.

We do induction on the case of $M\twoheadrightarrow M_{1}$.

  * •

Case $M\twoheadrightarrow M$

Then we choose $M_{3}$ as $M_{2}$.

  * •

Case $M\leavevmode\nobreak\ N\twoheadrightarrow M^{\prime}\leavevmode\nobreak\
N^{\prime}$

    * –

Subcase $M\twoheadrightarrow M_{2}$ as $M\twoheadrightarrow M$

Then we choose $M_{3}$ as $M_{1}$.

    * –

Subcase $M\twoheadrightarrow M_{2}$ as $M\leavevmode\nobreak\
N\twoheadrightarrow M^{\prime\prime}\leavevmode\nobreak\ N^{\prime\prime}$ ①

Then we use the induction hypothesis, we have $M^{*}$ that
$M^{\prime}\twoheadrightarrow M^{*}$,$M^{\prime\prime}\twoheadrightarrow
M^{*}$,and we have $N^{*}$ that $N^{\prime}\twoheadrightarrow
N^{*}$,$N^{\prime\prime}\twoheadrightarrow N^{*}$, so we choose $M_{3}$ as
$M^{*}\leavevmode\nobreak\ N^{*}$.

    * –

Subcase $M\twoheadrightarrow M_{2}$ as $M=\lambda x:T.P$, $(\lambda
x:T.P)N\twoheadrightarrow P^{\prime\prime}[N^{\prime\prime}/x]$. ②

Then we first have that $M=\lambda x:T.P$ Then $M^{\prime}=\lambda
x:T.P^{\prime}$, so we choose $M_{3}=P^{*}[N^{*}/x]$.

  * •

Case $M\oplus N\twoheadrightarrow M^{\prime}\oplus N^{\prime}$

    * –

Subcase $M\twoheadrightarrow M_{2}$ as $M\twoheadrightarrow M$

Then we choose $M_{3}$ as $M_{1}$.

    * –

Subcase $M\twoheadrightarrow M_{2}$ as $M\twoheadrightarrow
M^{\prime\prime},N\twoheadrightarrow N^{\prime\prime}\Rightarrow M\oplus
N\twoheadrightarrow M^{\prime\prime}\oplus N^{\prime\prime}$: same as ①.

    * –

Subcase $M\twoheadrightarrow M_{2}$ as $(\lambda x:T.M)\oplus(\lambda
y:T.N)\twoheadrightarrow\lambda x:T.M^{\prime}\oplus N^{\prime}[y/x]$

Then $M\twoheadrightarrow M_{1}$ must be $(\lambda x:T.M)\oplus(\lambda
y:T.N)\twoheadrightarrow(\lambda x:T.M^{\prime\prime})\oplus(\lambda
y:T.N^{\prime\prime})$, Then we choose $M_{3}$ to be $\lambda x:T.M^{*}\oplus
N^{*}[y/x]$.

    * –

Subcase $M\twoheadrightarrow M_{2}$ as
$(M_{11},M_{12},...M_{1n})\oplus(M_{21},M_{22},...M_{2n})\twoheadrightarrow(M_{11}^{\prime}\oplus
M_{21}^{\prime},M_{12}^{\prime}\oplus M_{22}^{\prime},...M_{1n}^{\prime}\oplus
M_{2n}^{\prime})$: same as $(\lambda x:T.M)\oplus(\lambda
y:T.N)\twoheadrightarrow\lambda x:T.M^{\prime}\oplus N^{\prime}[y/x]$.

All the other cases are similar to the case of application and $\oplus$,
except that we may have more subcases on these cases, but the extra subcases
are all similar to ②.

######  Lemma A.12 (Confluence).

One term has at most one normal form.

######  Proof A.13.

The relation $\twoheadrightarrow$ has the diamond property, and reduction
relation $\rho$ satisfy that
$\rho\subseteq\twoheadrightarrow\subseteq\rho^{*}$. Also notice that
$\twoheadrightarrow^{*}$ has the diamond property, and
$\twoheadrightarrow^{*}=\rho^{*}$, so the relation $\rho^{*}$ has the diamond
property. This is what results in the confluence.

###  A.4 Strong normalization

Here we write $\rightsquigarrow$ as $\rho^{*}$. $t$ and $t^{\prime}$

######  Lemma A.14 (existence of $\nu$).

$t$ is strongly normalisable iff there is a number $\nu(t)$ which bounds the
length of every normalisation sequence beginning with $t$.

######  Proof A.15.

See P27 in Proofs and Types [12].

######  Definition A.16.

We define a set $\textbf{RED}_{T}$ by induction on the type $T$.

1\. For $t$ of base type, $t$ is reducible iff it is strongly normalisable.

2\. For $t$ of type $(T_{1},T_{2},...,T_{n})$ , $t$ is reducible iff $\forall
j,\pi_{j}(t)$ is reducible.

3\. For $t$ of type U$\rightarrow$V , $t$ is reducible iff, for all reducible
$u$ of type $U$, $t\leavevmode\nobreak\ u$ is reducible of type V .

4\. For $t$ of type $T_{1}+T_{2}$, $t$ is reducible iff,
$case\leavevmode\nobreak\ t\leavevmode\nobreak\ of\leavevmode\nobreak\
inl\leavevmode\nobreak\ x_{1}\Rightarrow 0\leavevmode\nobreak\
|\leavevmode\nobreak\ inr\leavevmode\nobreak\ x_{2}\Rightarrow 0$is reducible
term of base type.

######  Definition A.17.

$t$ is neutral if $t$ is not of the form $(t_{1},t_{2},...,t_{n})$ or $\lambda
x:T.t$ or $inl/inr\leavevmode\nobreak\ t$

We will verify the following 3 properties by induction on types.

(CR 1) If $t$ $\in$ $\textbf{RED}_{T}$ , then t is strongly normalisable.

(CR 2) If $t$ $\in$ $\textbf{RED}_{T}$ and $t$$\rightsquigarrow$$t^{\prime}$,
then $t^{\prime}$ $\in$ $\textbf{RED}_{T}$ .

(CR 3) If $t$ is neutral, and whenever we convert a redex of $t$ we obtain a
term t’$\in$ $\textbf{RED}_{T}$ , then t$\in$ $\textbf{RED}_{T}$ .

  * •

Case base type

(CR 1) is a tautology.

(CR 2) If $t$ is strongly normalisable then every term $t^{\prime}$ to which
$t$ reduces is also.

(CR 3) A reduction path leaving $t$ must pass through one of the terms
$t^{\prime}$ , which are strongly normalisable, and so is finite. In fact, it
is immediate that $\nu$(t) is equal to the greatest of the numbers
$\nu(t^{\prime})+1$, as $t^{\prime}$ varies over the (one-step) conversions of
$t$.

  * •

Case tuple type

(CR 1) Suppose that $t$, of type $(T_{1},T_{2},...,T_{n})$ , is reducible;
then $\pi_{1}(t)$ is reducible and by induction hypothesis (CR 1) for $T_{1}$,
$\pi_{1}(t)$ is strongly normalisable. Moreover, $\nu(t)\leq\nu(\pi_{1}(t))$.
Since to any reduction sequence $t$, $t_{1}$, $t_{2}$, . . ., one can apply
$\pi_{1}()$ to construct a reduction sequence $\pi_{1}(t)$, $\pi_{1}(t_{1})$,
$\pi_{1}(t_{2})$… (in which the $\pi_{1}()$ is not reduced). So $\nu(t)$ is
finite, and t is strongly normalisable.

(CR 2) If $t\rightsquigarrow t^{\prime}$, then $\forall
j,\pi_{j}(t)\rightsquigarrow\pi_{j}(t^{\prime})$. By the induction hypothesis
for type $T_{j}$ on (CR 2), we have $\forall j,\pi_{j}(t^{\prime})$ is
reducible, so $t^{\prime}$ is reducible

(CR 3) Let $t$ be neutral and suppose all the $t^{\prime}$ one step from t are
reducible. Applying a conversion inside $\pi_{j}(t)$, the result is a
$\pi_{j}(t^{\prime})$ , since $\pi_{j}(t)$ cannot itself be a redex ($t$ is
not a tuple), and $\pi_{j}(t^{\prime})$ is reducible, since $t^{\prime}$ is.
But as $\pi_{j}(t)$ is neutral, and all the terms one step from $\pi_{j}(t)$
are reducible, the induction hypothesis (CR 3) for $T_{j}$ ensures that
$\pi_{j}(t)$ is reducible. so $t$ is reducible.

  * •

Case arrow type

(CR 1) If $t$ is reducible of type $U\rightarrow V$ , let $x$ be a variable of
type $U$;: . $\Rightarrow$ And we have $\nu(t)\leq\nu(t\leavevmode\nobreak\
x)$

(CR 2) If $t\rightsquigarrow t^{\prime}$, and t is reducible, take u reducible
of type $U$; then $t\leavevmode\nobreak\ u$ is reducible and
$t\leavevmode\nobreak\ u\rightsquigarrow t^{\prime}\leavevmode\nobreak\ u$ The
induction hypothesis (CR 2) for $V$ gives that $t^{\prime}\leavevmode\nobreak\
u$ is reducible. So $t^{\prime}$ is reducible.

(CR 3) Let $t$ be neutral and suppose all the $t^{\prime}$ one step from $t$
are reducible. Let $u$ be a reducible term of type $U$; we want to show that
$t\leavevmode\nobreak\ u$ is reducible. By induction hypothesis (CR 1) for
$U$, we know that $u$ is strongly normalisable; so we can reason by induction
on $\nu(u)$.

In one step, $t\leavevmode\nobreak\ u$ converts to

    * –

1\. $t\leavevmode\nobreak\ u$ with $t^{\prime}$ one step from $t$; but
$t^{\prime}$ is reducible, so $t\leavevmode\nobreak\ u$ is.

    * –

2\. $t\leavevmode\nobreak\ u^{\prime}$, with $u^{\prime}$ one step from $u$.
$u^{\prime}$ is reducible by induction hypothesis(CR 2) for U, and
$\nu(u^{\prime})<\nu(u)$; so the induction hypothesis for $u^{\prime}$ tells
us that $t\leavevmode\nobreak\ u^{\prime}$ is reducible.

    * –

3\. There is no other possibility, for $t\leavevmode\nobreak\ u$ cannot itself
be a redex ($t$ is not of the form $\lambda x:T.t$).

  * •

Case sum type

(CR 1) If $t$ is reducible of type $T_{1}+T_{2}$ , Then we have
$\nu(t)\leq\nu(case\leavevmode\nobreak\ t\leavevmode\nobreak\
of\leavevmode\nobreak\ inl\leavevmode\nobreak\ x_{1}\Rightarrow
0|inr\leavevmode\nobreak\ x_{2}\Rightarrow 0)$

(CR 2) same as tuple type.

(CR 3) same as arrow type.

######  Lemma A.18.

If $t_{1},t_{2},...,t_{n}$ are reducible terms, then so is
$(t_{1},t_{2},...,t_{n})$

######  Proof A.19.

Because of (CR 1), we can reason by induction on
$\nu(t_{1})+\nu(t_{2})+...+\nu(t_{n})$ to show that
$\pi_{j}(t_{1},t_{2},...,t_{n})$, is reducible. This term converts to

  * •

1\. $t_{j}$, then it is reducible.

  * •

2.$(t_{1},...,t_{k-1},t_{k}^{\prime},t_{k+1},...,t_{n})$, based on induction,
it is reducible.

######  Lemma A.20.

If for all reducible u of type U, t[u/x] is reducible, then so is $\lambda
x:T.t$.

######  Proof A.21.

To show $\lambda x:T.t\leavevmode\nobreak\ u$ is reducible, we make reductions
on $\nu(u)+\nu(t)$, $\lambda x:T.t\leavevmode\nobreak\ u$ , which can be
reduced to

  * •

1\. $t[u/x]$, then it is reducible.

  * •

2\. $(\lambda x:T.t^{\prime})\leavevmode\nobreak\ u$ or $(\lambda
x:T.t)\leavevmode\nobreak\ u^{\prime}$, based on induction we know it is
reducible.

######  Lemma A.22.

If $t$ is reducible, then so is $inl/inr\leavevmode\nobreak\ t$.

######  Proof A.23.

Same as the case $\lambda x:T.t$.

######  Lemma A.24.

If for all reducible $t_{1}$ and $t_{2}$ of type $T_{1}$ and $T_{2}$, we have
$t_{3}[t_{1}/x_{1}]$ and $t_{4}[t_{2}/x_{2}]$ are reducible, and t is
reducible term of type $T_{1}+T_{2}$, then so is $case\leavevmode\nobreak\
t\leavevmode\nobreak\ of\leavevmode\nobreak\ inl\leavevmode\nobreak\
x_{1}\Rightarrow t_{3}\leavevmode\nobreak\ |\leavevmode\nobreak\
inr\leavevmode\nobreak\ x_{2}\Rightarrow t_{4}$.

######  Proof A.25.

Same as the case $\lambda x:T.t$.

######  Lemma A.26.

If $t_{1}$ and $t_{2}$ are reducible terms of T, then so is $t_{1}\oplus
t_{2}$.

######  Proof A.27.

We prove this by induction on type.

  * •

Case base type, then it can only be reduced to $t_{1}^{\prime}\oplus
t_{2}^{\prime}$, so $\nu(t_{1}\oplus t_{2})=\nu(t_{1})+\nu(t_{2})$, Therefore
it is strongly normalisable, and thus reducible.

  * •

Case $(T_{1},T_{2},...,T_{n})$, we make induction on $\nu(t_{1})+\nu(t_{2})$,
$t_{1}\oplus t_{2}$ can be reduced to.

    * –

1.Subcase
$(t_{11},t_{12},...t_{1n})\oplus(t_{21},t_{22},...t_{2n})\rightarrow(t_{11}\oplus
t_{21},t_{12}\oplus t_{22},...t_{1n}\oplus t_{2n})$. Because $t_{1}$ and
$t_{2}$ si reducible, then $\forall i\forall j,t_{ij}$ is reducible, based on
induction on types, we have $\forall j,t_{1j}\oplus t_{2j}$ Thus,
$(t_{11}\oplus t_{21},t_{12}\oplus t_{22},...t_{1n}\oplus t_{2n})$ is
reducible.

    * –

2.Subcase $(t_{1}^{\prime}\oplus t_{2})$ or $(t_{1}\oplus t_{2}^{\prime})$.
Based on induction, we know it is reducible.

  * •

Case $A\rightarrow B$ for all reducible term u of type A, we make induction on
$\nu(t_{1})+\nu(t_{2})+\nu(u)$.

    * –

1\. Subcase $(\lambda x:T.t_{1})\oplus(\lambda y:T.t_{2})\rightarrow\lambda
x:T.t_{1}\oplus(t_{2}[x/y])$ notice that for all reducible u of type A
$(t_{1}\oplus t_{2}[x/y])[u/x]$, notice that this term is equal to
$(t_{1}[u/x]\oplus t_{2}[u/y])$, because $(\lambda x:T.t_{1})$ is a reducible
term, then so is $t_{1}[u/x]$. Because $t_{1}[u/x]$ and $t_{2}[u/y]$ are
reducible terms based on induction. So we have $\lambda
x:T.t_{1}\oplus(t_{2}[x/y])$’s reducibility.

    * –

2 Subcase $(t_{1}^{\prime}\oplus t_{2})\leavevmode\nobreak\ u$ or
$(t_{1}\oplus t_{2}^{\prime})\leavevmode\nobreak\ u$ or $(t_{1}\oplus
t_{2})\leavevmode\nobreak\ u^{\prime}$, based on induction we can prove the
case.

######  Lemma A.28.

If $t_{1}$ and $t_{2}$ are reducible terms of T, then so is $t_{1}\ominus
t_{2}$.

######  Proof A.29.

Same as $\oplus$.

######  Lemma A.30.

If $t_{1}$ and $t_{2}$ are reducible terms of $\frac{\partial T_{1}}{\partial
T_{2}}$ and $T_{2}$, then so is $t_{1}*t_{2}$.

######  Proof A.31.

We prove this by induction on types.

  * •

Case $T_{1}$: base type, $T_{2}$: base type: same as the case of $\oplus$.

  * •

Case $T_{1}$: $(T_{1},T_{2},...,T_{n})$, $T_{2}$: base type: same as the case
of $\oplus$.

  * •

Case $T_{1}$: $A\rightarrow B$, $T_{2}$: base type: same as the case of
$\oplus$.

  * •

Case $T_{1}$: $(T_{1},T_{2},...,T_{n})$, $T_{2}$:
$(T_{1}^{\prime},T_{2}^{\prime},...,T_{n}^{\prime})$

Suppose $t_{1}:(t_{11},t_{12},...t_{1n}),t_{2}:(t_{21},t_{22},...t_{2n})$, we
do induction on $\nu(t_{1})+\nu(t_{2})$.

    * –

Subcase
$t_{1}*t_{2}\rightarrow(t_{11}*t_{21})\oplus(t_{12}*t_{22})\oplus...\oplus(t_{1n}*t_{2n})$:
Because $t_{1}$ and $t_{2}$ is reducible, then so is $\forall i\forall
j,t_{ij}$, based on induction on types we have $\forall j,t_{1j}*t_{2j}$ is
reducible, then so is
$(t_{11}*t_{21})\oplus(t_{12}*t_{22})\oplus...\oplus(t_{1n}*t_{2n})$.

    * –

Subcase $t_{1}^{\prime}*t_{2}$ or $t_{1}*t_{2}^{\prime}$, based on induction
we know it is reducible.

######  Lemma A.32.

If $t_{1}$ and $t_{2}$ are reducible terms of $T_{1}$ and $T_{2}$, and for all
reducible u of type $T_{2}$, we have that $t_{1}[u/x]$ is reducible then so is
$\frac{\partial t_{1}}{\partial x}|_{t_{2}}$.

######  Proof A.33.

we prove this by induction on types.

  * •

Case $T_{1}$: $(T_{1},T_{2},...,T_{n})$ or $A\rightarrow B$ or base type,
$T_{2}$:B. Same as the case $t_{1}\leavevmode\nobreak\ *\leavevmode\nobreak\
t_{2}$.

  * •

Case $T_{1}$: $(T_{1},T_{2},...,T_{n})$, $T_{2}$:
$(T_{1}^{\prime},T_{2}^{\prime},...,T_{n}^{\prime})$, we make induction on
$\nu(t_{1})+\nu(t_{2})$.

    * –

Subcase $\forall
i,(t_{1},t_{2}...,t_{i-1},x_{i},t_{i+1}...,t_{n})is\leavevmode\nobreak\
written\leavevmode\nobreak\ as\leavevmode\nobreak\ t_{i*}$,

$\frac{\partial t}{\partial
x}|_{(t_{1},t_{2},...,t_{n})}\rightarrow(\frac{\partial t[t_{1*}/x]}{\partial
x_{1}}|_{t_{1}},\frac{\partial t[t_{2*}/x]}{\partial
x_{2}}|_{t_{2}},...,\frac{\partial t[t_{n*}/x]}{\partial x_{n}}|_{t_{n}})$,
note that $t_{i*}$ is reducible so based on induction. We have that
$\frac{\partial t[t_{j*}/x]}{\partial x_{j}}|_{t_{j}}$ is reducible. Note that
this induction is based on the hypothesis $(t[t_{j*}/x])[u/x_{j}]$ is
reducible for all the reducible u of type $T_{j}^{\prime}$, and
$(t[t_{j*}/x])[u/x_{j}]=(t[(t_{j*}[u/x_{j}])/x])$ because t has no occurrence
of $x_{j}$, and it is easy to show that $(t_{j*}[u/x_{j}])$ is a reducible
term of type $T_{2}$, so we finish the induction, then we have

$(\frac{\partial t[t_{1*}/x]}{\partial x_{1}}|_{t_{1}},\frac{\partial
t[t_{2*}/x]}{\partial x_{2}}|_{t_{2}},...,\frac{\partial t[t_{n*}/x]}{\partial
x_{n}}|_{t_{n}})$ is reducible.

    * –

Subcase $\frac{\partial t_{1}^{\prime}}{\partial x}|_{t_{2}}$ or
$\frac{\partial t_{1}}{\partial x}|_{t_{2}^{\prime}}$, based on induction we
have the proof.

######  Lemma A.34.

If $t_{1}$,$t_{2}$ and $t_{3}$ are reducible terms of $T_{1}$, $T_{1}$ and
$T_{2}$, and for all reducible u of type $T_{1}$, we have $t_{3}[u/x]$ is
reducible then so is $\int_{t_{1}}^{t_{2}}t_{3}dx$.

######  Proof A.35.

Same as the case of $\frac{\partial}{\partial x}|_{...}$

######  Lemma A.36.

If $t_{1}$,$t_{2}$ and $t_{3}$ are reducible terms of $T_{1}+T_{2}$, $T$ and
$T$, and for all reducible $u_{1}$ of type $T_{1}$, $u_{2}$ of type $T_{2}$,
we have that $t_{2}[u_{1}/x_{1}]$ and $t_{3}[u_{2}/x_{2}]$ are reducible then
so is $case\leavevmode\nobreak\ t_{1}\leavevmode\nobreak\
of\leavevmode\nobreak\ inl\leavevmode\nobreak\ x_{1}\Rightarrow
t_{2}\leavevmode\nobreak\ |\leavevmode\nobreak\ inr\leavevmode\nobreak\
{x_{2}}\Rightarrow t_{3}$.

######  Proof A.37.

Same as the case of $\frac{\partial}{\partial x}|_{...}$

######  Lemma A.38.

Let $t$ be any term (not assumed to be reducible), and suppose all the free
variables of t are among $x_{1},...,x_{n}$ of types $U_{1},...,U_{n}$. If
$u_{1},...,u_{n}$ are reducible terms of types $U_{1},...,U_{n}$ then
$t[u_{1}/x_{1},...,u_{n}/x_{n}]$ is reducible.

######  Proof A.39.

By induction on $t$. We write t[u/x] for $t[u_{1}/x_{1},...,u_{n}/x_{n}]$.

  * •

1\. $t$ is $x_{i}$, then $t[u/x_{i}]$ is reducible.

  * •

2\. $t$ is $c$, then $t_{i}$ has no free variable, and $c$ itself is
reducible, so it is reducible.

  * •

3\. $t$ is $(t_{1},t_{2},...,t_{n})$, based on induction we prove $t_{j}$[u/x]
is reducible, based on the lemma we know it is reducible.

  * •

4\. $t$ is $t\oplus t$, $t\ominus t$, $t*t$,$inl/inr\leavevmode\nobreak\ t$ or
$\pi_{j}(t)$: same as the case $(t_{1},t_{2},...,t_{n})$.

  * •

5\. $t$ is $\lambda y:T.t$, by induction we have t[u/x,v/y] is reducible, then
by lemma we have $\lambda y:T.(t[\underline{u}/\underline{x}])$ is reducible,
so $(\lambda y:T.t)[\underline{u}/\underline{x}]$ is reducible.

  * •

6\. $t$ is $\frac{\partial t}{\partial x}|_{t}$, $case\leavevmode\nobreak\
t\leavevmode\nobreak\ of\leavevmode\nobreak\ inl\leavevmode\nobreak\
x_{1}\Rightarrow t_{1}\leavevmode\nobreak\ |\leavevmode\nobreak\
inr\leavevmode\nobreak\ {x_{2}}\Rightarrow t_{2}$ or $\int_{t}^{t}tdx$: same
as the case $\lambda y:T.t$.

######  Theorem A.40.

All terms are reducible.

######  Proof A.41.

For arbitrary term $t$, apply the Lemma A.38 to
$t[x_{1}/x_{1},...,x_{n}/x_{n}]$ and we get the result.

######  Corollary A.42.

All terms are strongly normalisable.

##  Appendix B Appendix-Lemmas

######  Lemma B.1.

If $t_{1}\rho^{*}t_{1}^{\prime},t_{2}\rho^{*}t_{2}^{\prime}$, then
$t_{1}[t_{2}/x]\rho^{*}t_{1}^{\prime}[t_{2}^{\prime}/x]$.

######  Proof B.2.

Using the confluence property, it is easy to see.

######  Lemma B.3.

If $t_{1}=t_{1}^{\prime}$, $t_{2}=t_{2}^{\prime}$, then $t_{1}\oplus
t_{2}=t_{1}^{\prime}\oplus t_{2}^{\prime}$.

######  Proof B.4.

if $t_{1}$ or $t_{2}$ is not closed, then we use the substitution
$[u_{1}/x_{1},...,u_{n}/x_{n}]$ to make it closed. For simplicity of notation,
we just use $t_{1}$ and $t_{2}$ to be the closed-term of themselves.

Based on the equality defintion, we can assume that $t_{1}$, $t_{2}$,
$t_{1}^{\prime}$, $t_{2}^{\prime}$ are all normal forms and we prove this by
induction on types.

  * •

Case $t_{1}$ is of base type. Then $t_{2}$, $t_{1}^{\prime}$ and
$t_{2}^{\prime}$ have to be base type to be well-typed. And for base type
normal forms, we have $t_{1}\oplus t_{2}=t_{1}^{\prime}\oplus t_{2}^{\prime}$.

  * •

Case $t_{1}$ is $A\rightarrow B$ type, let’s suppose $t_{1}:\lambda
x:T.t_{3}$, $t_{1}^{\prime}:\lambda x^{\prime}:T.t_{3}^{\prime}$,
$t_{2}:\lambda y:T.t_{4}$, $t_{2}^{\prime}:\lambda
y^{\prime}:T.t_{4}^{\prime}$.

If $t_{1}$ or $t_{2}$ or $t_{1}^{\prime}$ or $t_{2}^{\prime}$ ’s normal form
are not $\lambda x:T.t$, then we know their normal form are all interpretable
in base type, thus we have $t_{1}\oplus t_{2}=t_{1}^{\prime}\oplus
t_{2}^{\prime}$.

Else for all u

$\begin{array}[]{llll}(t_{1}\oplus t_{2})\leavevmode\nobreak\ u\\\
\qquad=(\lambda x:T.t_{3}\oplus\lambda y:T.t_{4})\leavevmode\nobreak\ u\\\
\qquad=(\lambda x:T.t_{3}\oplus t_{4}[x/y])\leavevmode\nobreak\ u\\\
\qquad=t_{3}[u/x]\oplus t_{4}[u/y]\end{array}$

Similarly, we have $(t_{1}^{\prime}\oplus t_{2}^{\prime})\leavevmode\nobreak\
u^{\prime}=t_{3}^{\prime}[u/x^{\prime}]\oplus t_{4}^{\prime}[u/y^{\prime}]$.

And notice that because $t_{1}=t_{1}^{\prime}$, so $t_{1}\leavevmode\nobreak\
u=t_{1}^{\prime}\leavevmode\nobreak\ u$, so
$t_{3}[u/x]=t_{3}^{\prime}[u/x^{\prime}]$, based on induction of type B, we
have $t_{3}[u/x]\oplus t_{4}[u/y]=t_{3}^{\prime}[u/x^{\prime}]\oplus
t_{4}^{\prime}[u/y^{\prime}]$, so we have proven the case.

  * •

Case $t_{1}$ is of type $(T_{1},T_{2},..,T_{n})$. Then we suppose
$t_{1}:(t_{11},t_{12},..,t_{1n})$,
$t_{1}^{\prime}:(t_{11}^{\prime},t_{12}^{\prime},..,t_{1n}^{\prime})$,
$t_{2}:(t_{21},t_{22},..,t_{2n})$,
$t_{2}^{\prime}:(t_{21}^{\prime},t_{22}^{\prime},..,t_{2n}^{\prime})$

Then

$\begin{array}[]{llll}t_{1}\oplus t_{2}\\\
=(t_{11},t_{12},..,t_{1n})\oplus(t_{21},t_{22},..,t_{2n})\\\ =(t_{11}\oplus
t_{21},t_{12}\oplus t_{22},..,t_{1n}\oplus t_{2n})\end{array}$

Similarly we have $t_{1}^{\prime}\oplus t_{2}^{\prime}=(t_{11}^{\prime}\oplus
t_{21}^{\prime},t_{12}^{\prime}\oplus t_{22}^{\prime},..,t_{1n}^{\prime}\oplus
t_{2n}^{\prime})$, and based on induction we have $\forall j,t_{1j}\oplus
t_{2j}=t_{1j}^{\prime}\oplus t_{2j}^{\prime}$, so we have $t_{1}\oplus t_{2}$
= $t_{1}^{\prime}\oplus t_{2}^{\prime}$.

  * •

Case $t_{1}$ is of type $T_{1}+T_{2}$. This case is impossible because it is
not well-typed.

######  Lemma B.5.

For a term t, for any subterm s, if the term s’=s, then t[s’/s]=t. (We only
substitute the subterm s, but not other subterms same as s)

######  Proof B.6.

We prove this by induction. We first substitute for all the free variables in
$t$. Then

$\begin{array}[]{llll}t[s^{\prime}/s][u_{1}/x_{1},...,u_{n}/x_{n}]\\\
\qquad=t[u_{1}/x_{1},...,u_{n}/x_{n}][s^{\prime}[u_{1}/x_{1},...,u_{n}/x_{n}]/s[u_{1}/x_{1},...,u_{n}/x_{n}]]\par\end{array}$

notice that
$s^{\prime}[u_{1}/x_{1},...,u_{n}/x_{n}]=s[u_{1}/x_{1},...,u_{n}/x_{n}]$
because $s^{\prime}=s$, and we just substitute for some of the free variables
in $s^{\prime}$ and $s$. So we only need to prove that for a closed-term $t$,
for any subterm $s$, if the term $s^{\prime}=s$, then $t[s^{\prime}/s]=t$.

And notice that if we choose the subterm $s$ to be the $t$ itself, then we
have $t[s^{\prime}/s]=s^{\prime}=s=t$, And we prove the case. So we next make
induction on the form of $t$.

  * •

Case $t$ is $(t_{1},t_{2},...,t_{n})$

Using induction, we know $t_{i}[s^{\prime}/s]=t_{i}$, and we want to prove

$\begin{array}[]{llll}(t_{1},t_{2},...,t_{n})\\\
\qquad=(t_{1}[s^{\prime}/s],t_{2}[s^{\prime}/s],...,t_{n}[s^{\prime}/s])\end{array}$

And because we have the transitive property of equality, then we just reduce
both of them to normal forms, then by definition we know they equal to each
other, thus we prove the case.

Using the same technique, we can prove the case $\lambda x:T.t$ and
$inl/int\leavevmode\nobreak\ t$.

  * •

Case $t$ is $c$

Then it has no subterm except $c$ itself, if $s^{\prime}=c$, then
$c[s^{\prime}/c]=s^{\prime}$, thus we prove the case.

Using the same technique, we can prove the case $x$.

  * •

Case $t$ is $t_{1}\oplus t_{2}$

Using induction we have
$t_{1}[s^{\prime}/s]=t_{1}$,$t_{2}[s^{\prime}/s]=t_{2}$, and we have proven
Lemma 2.14 that if $t_{1}=t_{1}^{\prime},t_{2}=t_{2}^{\prime}$, then
$t_{1}\oplus t_{2}=t_{1}^{\prime}\oplus t_{2}^{\prime}$, thus we have proven
the case.

Using the same technique, we can prove the case $t\ominus t$, $t*t$,
$\pi_{j}(t)$.

  * •

Case $t$ is $t_{1}\leavevmode\nobreak\ t_{2}$

We want to prove if $t_{1}=t_{1}^{\prime},t_{2}=t_{2}^{\prime}$, then
$t_{1}\leavevmode\nobreak\ t_{2}=t_{1}^{\prime}\leavevmode\nobreak\
t_{2}^{\prime}$.

By definition we know if $t_{1}=t_{1}^{\prime}$, then
$t_{1}\leavevmode\nobreak\ t_{2}^{\prime}=t_{1}^{\prime}\leavevmode\nobreak\
t_{2}^{\prime}$.

Then we have proven $t_{1}\leavevmode\nobreak\
t_{2}^{\prime}=t_{1}\leavevmode\nobreak\ t_{2}$. Using confluence property, we
can reduce the $t_{1}$ to $\lambda x:A.t$ or a nb. If it is the former case,
then we using induction we have $t[t_{2}^{\prime}/x]=t[t_{2}/x]$ .Thus we have
$t_{1}\leavevmode\nobreak\ t_{2}^{\prime}=t_{1}\leavevmode\nobreak\ t_{2}$. If
it is the latter case, then $t_{2}$’s normal form can be is interpretable, and
on base type interpretation we have if $x=x^{\prime}$, then
$f(x)=f(x^{\prime})$. Thus we prove the case.

  * •

Case $t$ is $\frac{\partial t_{1}}{\partial x}|_{t_{2}}$

If $t_{2}$ is base type, then we can use the techniques for how we proved the
case $t_{1}*t_{2}$,

If $t_{2}$ is of type $(T_{1},T_{2},...,T_{n})$, we can reduce the $t_{2}$ and
$t_{2}^{\prime}$ to the normal forms $(t_{1},t_{2},...,t_{n})$ and
$(t_{1}^{\prime},t_{2}^{\prime},...,t_{n}^{\prime})$, and then we have

$\forall
i,(t_{1},t_{2}...,t_{i-1},x_{i},t_{i+1}...,t_{n})is\leavevmode\nobreak\
written\leavevmode\nobreak\ as\leavevmode\nobreak\ t_{i*}$ $\frac{\partial
t}{\partial x}|_{(t_{1},t_{2},...,t_{n})}\rightarrow(\frac{\partial
t[t_{1*}/x]}{\partial x_{1}}|_{t_{1}},\frac{\partial t[t_{2*}/x]}{\partial
x_{2}}|_{t_{2}},...,\frac{\partial t[t_{n*}/x]}{\partial x_{n}}|_{t_{n}})$

, using induction we have $t[t_{j*}/x]=t[t_{j*}^{\prime}/x]$, then based on
induction we have $\frac{\partial t[t_{j*}/x]}{\partial
x_{j}}|_{t_{j}}=\frac{\partial t[t_{j*}^{\prime}/x]}{\partial
x_{j}^{\prime}}|_{t_{j}^{\prime}}$, Thus we have proven the case.

Using the same technique, we can prove the case $\int_{t_{1}}^{t_{2}}t_{3}dx$
adn $case\leavevmode\nobreak\ t\leavevmode\nobreak\ of\leavevmode\nobreak\
inl\leavevmode\nobreak\ x_{1}\Rightarrow t_{1}\leavevmode\nobreak\
|\leavevmode\nobreak\ inr\leavevmode\nobreak\ {x_{2}}\Rightarrow t_{2}$.

Thus we have proven the lemma.

######  Lemma B.7.

If $t_{1}*(t_{2}\oplus t_{3})$ and $(t_{1}*t_{2})\oplus(t_{1}*t_{3})$ are
weak-normalizable, then $t_{1}*(t_{2}\oplus
t_{3})=(t_{1}*t_{2})\oplus(t_{1}*t_{3})$

######  Proof B.8.

if $t_{1}$, $t_{2}$ and $t_{3}$ are not closed, then we use the substitution
$[u_{1}/x_{1},...,u_{n}/x_{n}]$ to make it closed. For simplicity of notation,
we just use $t_{1}$, $t_{2}$ and $t_{3}$ to be the closed-term of themselves.

Because of the confluence and normalization property of the system, we can
assume that $t_{1}$, $t_{2}$, $t_{3}$ are all normal formss and we prove this
by induction on type.

  * •

Case:$t_{1}$, $t_{2}$ and $t_{3}$ are of base type. then based on base type
interpretation, we have $t_{1}*(t_{2}\oplus
t_{3})=(t_{1}*t_{2})\oplus(t_{1}*t_{3})$.

  * •

Case:$t_{1}$ is of type $A\rightarrow B$, $t_{2}$ and $t_{3}$ are of base
type. Suppose $t_{1}$ is $\lambda x:A.t$.

If $t_{1}$ ’s normal form is not $\lambda x:A.t$, then we notice that
$t_{1}=\lambda x:A.t_{1}\leavevmode\nobreak\ x$, use the Lemma 2.15, we know
we can use $\lambda x:A.t_{1}\leavevmode\nobreak\ x$ to substitute for
$t_{1}$, Thus we can suppose $\lambda x:A.t$.

Then we have for all u of type A,

$\begin{array}[]{llll}t_{1}*(t_{2}\oplus t_{3})\leavevmode\nobreak\ u\\\
\qquad=(\lambda x:A.t)*(t_{2}\oplus t_{3})\leavevmode\nobreak\ u\\\
\qquad=\lambda x:A.(t*(t_{2}\oplus t_{3}))\leavevmode\nobreak\ u\\\
\qquad=t[u/x]*(t_{2}\oplus t_{3})\end{array}$

And

$\begin{array}[]{llll}(t_{1}*t_{2})\oplus(t_{1}*t_{3})\leavevmode\nobreak\
u\\\ \qquad=((\lambda x:A.t)*t_{2}\oplus(\lambda
x:A.t)*t_{3})\leavevmode\nobreak\ u\\\ \qquad=(\lambda
x:A.(t*t_{2})\oplus\lambda x:A.(t*t_{3}))\leavevmode\nobreak\ u\\\
\qquad=(\lambda x:A.(t*t_{2})\oplus(t*t_{3}))\leavevmode\nobreak\ u\\\
\qquad=(t[u/x]*t_{2})\oplus(t[u/x]*t_{3})\par\end{array}$

Based on induction on type B, we have $t[u/x]*(t_{2}\oplus
t_{3})=(t[u/x]*t_{2})\oplus(t[u/x]*t_{3})$, Therefore we prove the case.

  * •

Case:$t_{1}$ is of type $(T_{1},T_{2},..,T_{n})$, $t_{2}$ and $t_{3}$ are of
base type. Suppose $t_{1}$ is
$(t_{1}^{\prime},t_{2}^{\prime},..,t_{n}^{\prime})$.

Then

$\begin{array}[]{llll}t_{1}*(t_{2}\oplus t_{3})\\\
\qquad=(t_{1}^{\prime},t_{2}^{\prime},..,t_{n}^{\prime})*(t_{2}\oplus
t_{3})\\\ \qquad=(t_{1}^{\prime}*(t_{2}\oplus
t_{3}),t_{2}^{\prime}*(t_{2}\oplus t_{3}),..,t_{n}^{\prime}*(t_{2}\oplus
t_{3}))\end{array}$

$\begin{array}[]{llll}(t_{1}*t_{2})\oplus(t_{1}*t_{3})\\\
\qquad=(t_{1}^{\prime},t_{2}^{\prime},..,t_{n}^{\prime})*t_{2}\oplus(t_{1}^{\prime},t_{2}^{\prime},..,t_{n}^{\prime})*t_{3}\\\
\qquad=(t_{1}^{\prime}*t_{2},t_{2}^{\prime}*t_{2},..,t_{n}^{\prime}*t_{2})\oplus(t_{1}^{\prime}*t_{3},t_{2}^{\prime}*t_{3},..,t_{n}^{\prime}*t_{3})\\\
\qquad=(t_{1}^{\prime}*t_{2}\oplus
t_{1}^{\prime}*t_{3},t_{2}^{\prime}*t_{2}\oplus
t_{2}^{\prime}*t_{3},..,t_{n}^{\prime}*t_{2}\oplus
t_{n}^{\prime}*t_{3})\end{array}$

And based on induction we have $t_{j}^{\prime}*(t_{2}\oplus
t_{3})=(t_{j}^{\prime}*t_{2})\oplus(t_{j}^{\prime}*t_{3})$, so we have
$t_{1}*(t_{2}\oplus t_{3})=(t_{1}*t_{2})\oplus(t_{1}*t_{3})$.

  * •

Case:$t_{1}$ is of type $T_{1}+T_{2}$, $t_{2}$ and $t_{3}$ are of base type:
this case is not possible because the righthand term is not well-typed.

  * •

Case:$t_{1}$ is of type $(T_{1},T_{2},..,T_{n})$, $t_{2}$ and $t_{3}$ are of
type $(T_{1}^{\prime},T_{2}^{\prime},..,T_{n}^{\prime})$. Suppose
$t_{1}:(t_{11}^{\prime},t_{12}^{\prime},..,t_{1n}^{\prime})$,$t_{2}:(t_{21}^{\prime},t_{22}^{\prime},..,t_{2n}^{\prime})$
and $t_{3}=(t_{31}^{\prime},t_{32}^{\prime},..,t_{3n}^{\prime})$.

Then

$\begin{array}[]{llll}t_{1}*(t_{2}\oplus t_{3})\\\
\qquad=(t_{11}^{\prime},t_{12}^{\prime},..,t_{1n}^{\prime})*((t_{21}^{\prime},t_{22}^{\prime},..,t_{2n}^{\prime})\oplus(t_{31}^{\prime},t_{32}^{\prime},..,t_{3n}^{\prime}))\\\
\qquad=t_{11}^{\prime}*(t_{21}^{\prime}\oplus t_{31}^{\prime})\oplus
t_{12}^{\prime}*(t_{22}^{\prime}\oplus t_{32}^{\prime})\oplus...\oplus
t_{1n}^{\prime}*(t_{2n}^{\prime}\oplus t_{3n}^{\prime})\end{array}$

And we have

$\begin{array}[]{llll}(t_{1}*t_{2})\oplus(t_{1}*t_{3})\\\
\qquad=(t_{11}^{\prime},t_{12}^{\prime},..,t_{1n}^{\prime})*(t_{21}^{\prime},t_{22}^{\prime},..,t_{2n}^{\prime})\oplus(t_{11}^{\prime},t_{12}^{\prime},..,t_{1n}^{\prime})*(t_{31}^{\prime},t_{32}^{\prime},..,t_{3n}^{\prime})\\\
\qquad=((t_{11}^{\prime}*t_{21}^{\prime})\oplus(t_{11}^{\prime}*t_{31}^{\prime}))\oplus((t_{12}^{\prime}*t_{22}^{\prime})\oplus(t_{12}^{\prime}*t_{32}^{\prime}))\oplus...\oplus((t_{1n}^{\prime}*t_{2n}^{\prime})\oplus(t_{1n}^{\prime}*t_{3n}^{\prime}))\end{array}$

Based on induction we have $\forall j,t_{1j}^{\prime}*(t_{2j}^{\prime}\oplus
t_{3j}^{\prime})=((t_{1j}^{\prime}*t_{2j}^{\prime})\oplus(t_{1j}^{\prime}*t_{3j}^{\prime}))$,
and using Lemma 2.14 $t_{1}=t_{1}^{\prime},t_{2}=t_{2}^{\prime}$, then
$t_{1}\oplus t_{2}=t_{1}^{\prime}\oplus t_{2}^{\prime}$ we prove the case.

######  Lemma B.9.

If $(t_{1}\ominus t_{2})\oplus(t_{2}\ominus t_{3})$ and $t_{1}\ominus t_{3}$
are weak-normalizable, then $(t_{1}\ominus t_{2})\oplus(t_{2}\ominus
t_{3})=t_{1}\ominus t_{3}$

######  Proof B.10.

If $t_{1}$, $t_{2}$ or $t_{3}$ is not closed, then we just substitute them to
be closed. Because of the confluence and normalization property, we can assume
that $t_{1}$, $t_{2}$ and $t_{3}$ are all normal forms.

Then we make induction on type of $t_{1}$.

  * •

Case base type

Then because on base type, we require that $(t_{1}\ominus
t_{2})\oplus(t_{2}\ominus t_{3})=t_{1}\ominus t_{3}$, Thus we have proven the
case.

  * •

Case A$\rightarrow$B

Then we need to prove that $\forall u,((t_{1}\ominus t_{2})\oplus(t_{2}\ominus
t_{3}))u=(t_{1}\ominus t_{3})u$.

Then we can suppose that $t_{1}$, $t_{2}$ and $t_{3}$ are of the form $\lambda
a:A.t$, if they are not, then we use $\lambda a:A.t_{i}\leavevmode\nobreak\ a$
to substitute for $t_{i}$.

Then we have

$\begin{array}[]{llll}((t_{1}\ominus t_{2})\oplus(t_{2}\ominus t_{3}))u\\\
\qquad=((\lambda a:A.t_{1}^{\prime}\ominus\lambda
a:A.t_{2}^{\prime})\oplus(\lambda a:A.t_{2}^{\prime}\ominus\lambda
a:A.t_{3}^{\prime}))u\\\ \qquad=\lambda a:A.((t_{1}^{\prime}\ominus
t_{2}^{\prime})\oplus(t_{2}^{\prime}\ominus t_{3}^{\prime}))u\\\
\qquad=((t_{1}^{\prime}[u/a]\ominus
t_{2}^{\prime}[u/a])\oplus(t_{2}^{\prime}[u/a]\ominus t_{3}^{\prime}[u/a]))\\\
\qquad=((\lambda a:A.t_{1}^{\prime}\leavevmode\nobreak\ u\ominus\lambda
a:A.t_{2}^{\prime}\leavevmode\nobreak\ u)\oplus(\lambda
a:A.t_{2}^{\prime}\leavevmode\nobreak\ u\ominus\lambda
a:A.t_{3}^{\prime}\leavevmode\nobreak\ u))\\\
\qquad=((t_{1}\leavevmode\nobreak\ u\ominus t_{2}\leavevmode\nobreak\
u)\oplus(t_{2}\leavevmode\nobreak\ u\ominus t_{3}\leavevmode\nobreak\
u))\end{array}$

And similarly we have $(t_{1}\ominus t_{3})u$ = $(t_{1}\leavevmode\nobreak\
u\ominus t_{3}\leavevmode\nobreak\ u)$.

Based on induction on type B, we have $(t_{1}\leavevmode\nobreak\ u\ominus
t_{3}\leavevmode\nobreak\ u)=((t_{1}\leavevmode\nobreak\ u\ominus
t_{2}\leavevmode\nobreak\ u)\oplus(t_{2}\leavevmode\nobreak\ u\ominus
t_{3}\leavevmode\nobreak\ u))$.

Thus we have proven the case.

  * •

Case $(T_{1},T_{2},...,T_{n})$

Let’s suppose $t_{1}$ to be $(t_{11},t_{12},...,t_{1n})$, $t_{2}$ to be
$(t_{21},t_{22},...,t_{2n})$ and $t_{3}$ to be $(t_{31},t_{32},...,t_{3n})$.

Then we have

$\begin{array}[]{llll}((t_{1}\ominus t_{2})\oplus(t_{2}\ominus t_{3}))\\\
\qquad=(((t_{11}\ominus t_{21})\oplus(t_{21}\ominus
t_{31})),...,((t_{1n}\ominus t_{2n})\oplus(t_{2n}\ominus t_{3n})))\end{array}$

And

$\begin{array}[]{llll}(t_{1}\ominus t_{3})\\\ \qquad=((t_{11}\ominus
t_{31}),...,(t_{1n}\ominus t_{3n}))\end{array}$

Base on induction on type $T_{i}$, we have $(t_{1i}\ominus
t_{2i})\oplus(t_{2i}\ominus t_{3i})=(t_{1i}\ominus t_{3i})$ Thus we prove the
case.

  * •

Case $T_{1}+T_{2}$: This case is not possible because it is not well-typed.

Thus we have proven the theorem.