.

\smallskip

A \emph{variable} $A\not\in R$ is \emph{$R$-decomposable}
if $A\sim_R \alpha$ where $\alpha$ is $R$-redundancy-free 
and $|\alpha|>1$; 
if $A\not\in R$ is not $R$-decomposable, then $A$ is
\emph{non-$R$-decomposable}.

\begin{proposition}\label{prop:redfree}
\hfill\\
	(1) If $\alpha$ is $R$-redundancy-free, then 
$\bnorm{\alpha}_R\geq |\alpha|$.
\\
(2)
If $A$ is $R$-decomposable, then 
$A\sim_R \beta B$ where $B$ is non-$R$-decomposable and
$\bnorm{A}_R>\bnorm{B}_R\geq 1$.
\end{proposition}	
\begin{proof}
(1) follows from the already observed fact that
$X\gamma\not\sim\gamma$ implies that the cc-length of any path
$X\gamma\trans{u}\gamma$ is positive. 

(2): If $A$ is $R$-decomposable, then by definition we have $A\sim_R \beta B$
where $\beta B$ is $R$-redundancy-free, $\beta\neq\eps$, and 
$\bnorm{A}_R=\bnorm{\beta}_{R'}+\bnorm{B}_R$ where $R'=\red(B,R)$
(which follows from the definitions and Prop.~\ref{prop:Rsummary}).
Since $B\not\in R$ and 
$\beta$ is $R'$-redundancy free, we have $\bnorm{A}_R>\bnorm{B}_R\geq
1$.
Similarly, if $B$ is $R$-decomposable, then 
$B\sim_R \delta C$ where $\bnorm{B}_R>\bnorm{C}_R\geq 1$, which
entails $A\sim_R \beta B\sim_R \beta\delta C$.
We could thus immediately take $\beta$ and $B$
so that $\bnorm{B}_R$ is minimal, in which case $B$ is
non-$R$-decomposable.
\qed
\end{proof}


\textbf{$R$-prime form.}
For any (suffix-generated) $R\subseteq\var$, the equivalence $\sim_R$ induces a partition
on the set of all non-$R$-decomposable variables
(from $\var\smallsetminus R$). In each class of
this partition (containing non-$R$-decomposable variables 
that are pairwise equivalent w.r.t. $\sim_R$) we choose
a variable and call it an \emph{$R$-prime}.

\smallskip

\textbf{Convention.}
We further assume that the $R$-primes for all (suffix-generated)
sets $R\subseteq \var$ have been fixed, in our assumed nBPA system
$\calG=(\var,\act,\calR)$, unless stated otherwise.

\smallskip

We say that $\alpha\in\var^*$
is in the \emph{$R$-prime form} if 
\begin{itemize}
	\item
		either $\alpha=\eps$, 
	\item
		or 
$\alpha = \beta X$ where $X$ is an $R$-prime and $\beta$ is in the
$R'$-prime form for
$R'=\red(X, R)$.
\end{itemize}
The next lemma shows that for any $\alpha$ and
$R$ there is
the unique $\alpha'$ in the $R$-prime form such that
$\alpha\sim_R\alpha'$.


\begin{lemma}\label{lem:rel-udp}
\hfill\\
(1) For any  $\alpha\in\var^*$ and
$R\subseteq\var$ there is $\alpha'$ in the $R$-prime form where
$\alpha\sim_R\alpha'$.
\\
(2)
If $\alpha \sim_R \beta$ and both $\alpha$ and $\beta$ are in the
$R$-prime form, then $\alpha = \beta$.
\end{lemma}

\begin{proof}
(1): We show the claim for 
$\alpha,R$ by induction on $\bnorm{\alpha}_R$.
If  $\bnorm{\alpha}_R=0$, i.e. $\alpha\in R^*$, then $\alpha\sim_R\eps$
(where $\eps$ is in the $R$-prime form).
We thus assume $\alpha=\beta X \gamma$ where $\gamma\in R^*$ and
$X\not\in R$; note that $\alpha\sim_R\beta X\gamma\sim_R\beta X$.
Recalling Prop.~\ref{prop:redfree}(2), we deduce that 
$X\sim_R \delta Y$ where 
$Y$ is non-$R$-decomposable (maybe $\delta=\eps$ and $X=Y$);
hence $\alpha\sim_R\beta X\sim_R \beta \delta Y\sim_R 
\beta \delta Z$ where $Z$ is the
(unique) $R$-prime such that $Y\sim_R Z$.
We  put $R'=\red(Z,R)$, and note that 
 $\bnorm{\alpha}_R=\bnorm{\beta\delta}_{R'}+\bnorm{Z}_R$;
 hence $\bnorm{\beta\delta}_{R'}<\bnorm{\alpha}_R$.
By the induction
hypothesis there is $\beta'$ in the $R'$-prime form 
such that $\beta'\sim_{R'}\beta\delta$; hence $\alpha\sim_R\beta'Z$
and $\beta' Z$ is in the $R$-prime form.

(2):
Suppose 
the claim is not true.
Then there are $\alpha \sim_R \beta$, both $\alpha$ and $\beta$ being in the
$R$-prime form, such that $\alpha=\alpha'X\gamma$ and
$\beta=\beta'Y\gamma$ where $X,Y$ are different $R'$-primes for
$R'=\red(\gamma,R)$; hence $\alpha'X\sim_{R'}\beta' Y$, and 
by symmetry we can assume $\bnorm{X}_{R'}\geq\bnorm{Y}_{R'}$.

More generally, if the claim is not true, then we deduce that
there are some $R,\alpha,\beta$, and two \emph{different} $R$-primes $X,Y$ where
\begin{center}
$\alpha X\sim_R\beta Y$
and
$\bnorm{X}_{R}\geq\bnorm{Y}_{R}$.
\end{center}
We take such a counterexample with a shortest possible $R$-witness
path for $\alpha X$.
(Note that we do not require that $\alpha X$ and $\beta Y$ are in the $R$-prime form.)

We note that $\alpha X\not\sim_R X$ (since otherwise
$X\sim_R \beta Y$, and thus
either
$\bnorm{X}_{R}>\bnorm{Y}_{R}$ and $X$ is $R$-decomposable,
or
$X\sim_R\beta Y\sim_{R}Y$, which  
is impossible by our definition of $R$-primes).
We thus also have $\alpha X\not\sim_R Y$
(since $\bnorm{\alpha X}_R>\bnorm{Y}_R$).

Hence the first step in the $R$-witness path for $\alpha X$ is 
$\alpha X\trans{a}\alpha'X$ (where $\alpha' X$ has a shorter
$R$-witness path than $\alpha X$).
Since $\alpha X\sim_R \beta Y$, and  $\alpha X\not\sim_R Y$,
this first step 
 must have a response
$\beta Y=\beta_0 Y\trans{\tau}\beta_1
Y\trans{\tau}\cdots\trans{\tau}\beta_k Y\trans{a}\beta'Y$ where
$\alpha'X\sim_{R}\beta'Y$
(and all $\beta_i$ are nonempty since $\alpha X\not\sim_R Y$);
this contradicts the choice of our
counterexample.
\qed
\end{proof}
Lemma~\ref{lem:rel-udp} allows us to soundly define 
 \begin{center}
 $\PD_R(\alpha)$, the \emph{prime decomposition of} $\alpha$ w.r.t.
(i.e., in the context of) $R$,
\end{center}
as