other words, $t \in \L CP$ if and only if the stack constants are in argument positions in $t$.\
Let $\s$ be a function defined on $V \bigcup P$ such that :

-   - If $x \in V$, then $\s (x) \in \L CP$ ;

-   - If $p \in P$, then $\s (p)=\sou{t}=t_1,...,t_n$, $n \geq 0$, $t_i \in \L CP \bigcup P$ $1 \leq i \leq n$.

We define $\s(t)$ for all $t \in \L CP$ by :

-   - $\s ((u)v)=(\s (u))\s (v)$ if $v \not \in P$ ;

-   - $\s (\l xu)=\l x \s (u)$ ;

-   - $\s ((t)p)=(t)\sou{t}$ if $\s (p)=\sou{t}$.

$\s$ is said to be a $P$-substitution.\
We consider, on the set $\L CP$, the following rules of reduction :

-   1\) $(\l xu)tt_1...t_n \f (u[t/x])t_1...t_n$ for all $u,t \in \L CP$ and $t_1,...,t_n \in \L
    CP \bigcup P$ ;

-   2\) $(C)tt_1...t_n \f (t)\l x(x)t_1...t_n$ for all $t \in \L CP$ and $t_1,...,t_n \in \L CP
    \bigcup P$, and $x$ being $\l$-variable not appearing in $t_1,...,t_n$.

For any $t,t' \in \L CP$, we shall write $t \rhd_C t'$, if $t'$ is obtained from $t$ by applying these rules finitely many times.

If 