of the longest reduction of $M$.

-   If $M \tr_r^* N$, we denote by $lg(M \tr_r^* N)$ the number of steps in the reduction $M \tr_r^* N$. If $M \tr^* N$, we denote by $lg_r(M \tr^* N)$ the number of $\tr_r$ steps of the reduction in $M \tr^* N$.

Strong normalization of $\cal{S}$ {#3}
=================================

This section gives a simple proof (due to the first author) of the strong normalization of the simply typed $\l$-calculus.

\[a\] Let $M,N, \overrightarrow{O} \in {\cal M}$. If $M,N,\overrightarrow{O}
\in SN_{\b}$ and $(M\;N\;\overrightarrow{O} )\not\in SN_{\b}$, then $(M_{1}[x:=N]\;\overrightarrow{O})\not\in SN_{\b}$ for some $M_1$ such that $M \tr_{\b}^* \l x.M_{1}$.

Since $M,N,\overrightarrow{O}\in SN_{\b}$, the infinite reduction of $T=(M\;N\; \overrightarrow{O})$ looks like: $T\tr_{\b}^*(\l
x.M_{1}\;N_{1} \ \overrightarrow{O_{1}}\;)\tr_{\b}(M_{1}[x:=N_{1}]\;
\overrightarrow{O_{1}})\tr_{\b}^*\ldots $. The result immediately follows from the fact that $(M_{1}[x:=N]\;\overrightarrow{O}
)\tr_{\b}^*(M_{1}[x:=N_{1}]\;\overrightarrow{O_{1}})$.

\[b\] If $M,N \in SN_{\b}$ are typed $\l$-terms, then $M[x:=N] \in SN_{\b}$.

By induction on $(type(N),\eta_{\b}(M),size(M))$ where $type(N)$ is the complexity of the type of $N$. The cases $M=\l x.M_1$ and $M=(y\;
\overrightarrow{O})$ for $y \neq x$ are trivial.

-   $M=(\lambda y.P\;Q\;\overrightarrow{O})$. By the induction hypothesis, $P[x:=N],Q[x:=N]$ and $\overrightarrow{O}[x:=N]$ are in $SN_{\b}$. By lemma \[a\] it is enough to show that $(P[x:=N][y:=Q[x:=N]]\; \overrightarrow{O}[x:=N])=M^{\prime
    }[x:=N] \in SN_{\b}$ where $M^{\prime
    }=(P[y:=Q]\;\overrightarrow{O})$. But $\eta_{\b}(M^{\prime
    