\john{an alternative inductive definition?}
\begin{deff}\em
\label{D.4.2.New}
Let  $Red$ be the set of all reductions in an OERS $R$, let $\reg$ be a
regular stable set of terms in $R$, and let $Red^{*}$ be the  set of
$\reg$-semi-needed reductions.  We will define a function $K:Red \ar Red^{*}$.
For any reduction $P$, with finite $\reg$-needed steps, we will denote
the $\reg$-needed part $K_{N}(P)$ and the $\reg$-unneeded part $K_{U}(P)$
so that $K(P)=K_{N}(P)+K_{U}(P)$.
$K$ is defined inductively as follows:

(a) If $\vert P\vert = 0$ then $K(P)=P$.

(b) If $P=Q+u$ and $u$ is $\reg$-unneeded or $K_{U}(Q)=\emptyset$
then $K(P)=K(Q)+u$. Since $Q\leeqv K(Q)$ and $K(Q)\in Red^{*}$,
it is clear that $K(P)\in Red^{*}$ and $P\leeqv K(P)$.
Note that if $\vert P\vert=\infty$ but $NE_\reg \vert P\vert$ is finite
then $P=Q+P_U$ where $Q$ is finite and $P_U$ is $\reg$-unneeded. Then
$K(P)=K(Q)+P_U$.

(c) Otherwise, $P=Q+s\red{v}o$ and $v$ is $\reg$-needed. Now
$K(Q)$ must take the form $Q'+t\red{u}s$ where $u$ is $\reg$-unneeded.
By \Pr{P.3.3.c.}.(2), $v$ is a residual of a redex
$v'\subt t$, which is $\reg$-needed by \Pr{P.3.3.c.}.(1). Since $\reg$ is
regular, $v$ is the only residual of $v'$, hence $u+v$
and $v'+u/v'$ are
both complete developments of the set $u,v'\subt t$.
Then $K(P)=K(Q'+v')+u/v'$. As $u/v'$ contains only $\reg$-unneeded steps, $K(P)\in Red^{*}$. $P=Q+v\leeqv$ $Q'+u+v\leeqv$ $Q'+v'+u/v'\leeqv$ $K(P)$.

\end{deff}