### Background

In the untyped lambda calculus, a term may contain many redexes, and
different choices about which one to reduce may produce wildly
different results (e.g. $(\lambda x.y)((\lambda x.xx)\lambda x.xx)$
which in one step ($\beta$-)reduces either to $y$ or to itself).
Different (sequences of) choices of where to reduce are called
*reduction strategies*. A term $t$ is said to be *normalising* if
there *exists* a reduction strategy which brings $t$ to normal form.
A term $t$ is said to be *strongly normalising* if *every* reduction
strategy brings $t$ to normal form. (I'm not worried about which, but
confluence guarantees there can't be more than one possibility.)

A reduction strategy is said to be *normalising* (and is in some sense
best possible) if whenever $t$ has a normal form, then that's where
we'll end up. The leftmost-outermost strategy is normalising.

At the other end of the spectrum, a reduction strategy is said to be
*perpetual* (and is in some sense worst possible) if whenever there
is an infinite reduction sequence from a term $t$, then the strategy
finds such a sequence - in other words, we could possibly fail to
normalise, then we will.

I know of the perpetual reduction strategies $F_\infty$ and $F_{bk}$
given respectively by:
\begin{array}{ll}
F_{bk}(C[(\lambda x.s)t]) = C[s[t/x]] & \text{if $t$ is strongly normalising}\\\\
F_{bk}(C[(\lambda x.s)t]) = C[(\lambda x.s)F_{bk}(t)] &\text{otherwise}
\end{array}
and
\begin{array}{ll}
F_\infty(C[(\lambda x.s)t]) = C[s[t/x]] &\text{if $x$ occurs in $s$, or if $t$ is on normal form}\\\\
F_\infty(C[(\lambda x.s)t]) = C[(\lambda x.s)F_\infty(t)] &\text{otherwise}
\end{array}
(In both cases, the indicated $\beta$-redex is the *leftmost* one in
the term $C[(\lambda x.s)t]$ - and on normal forms, reduction
strategies are necessarily identity.) The strategy $F_\infty$ is even
*maximal* - if it normalises a term, then it has used a longest
possible reduction sequence to do so. (See e.g. 13.4 in Barendregt's
book.)

Consider now the *leftmost-innermost* reduction strategy. Informally,
it will only reduce a $\beta$-redex which contains no other redexes.
More formally, it is defined by
\begin{array}{ll}
L(t) = t
&\text{if $t$ on normal form}\\\\
L(\lambda x.s) = \lambda x. L(s)
&\text{for $s$ not on normal form}\\\\
L(st) = L(s)t
&\text{for $s$ not on normal form}\\\\
L(st) = s L(t)
&\text{if $s$, but not $t$ is on normal form}\\\\
L((\lambda x. s)t) = s[t/x]
&\text{if $s$, $t$ both on normal form}
\end{array}

The natural intuition for leftmost-innermost reduction is that it will
do *all* the work - no redex can be lost, and so it ought to be
perpetual. Since the corresponding strategy is perpetual for
(untyped) combinatory logic (innermost reductions are perpetual for
all orthogonal TRWs), this doesn't feel like completely unfettered
blue-eyed optimism...

Is leftmost-innermost reduction a perpetual strategy for the untyped $\lambda$-calculus?

If the answer turns out to be 'no', a pointer to a counterexample would be very interesting too.