(I have already asked this at MathOverflow, but got no answers there.)
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 normalizing if there exists a reduction strategy which brings $t$ to normal form. A term $t$ is said to be strongly normalizing 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 normalizing (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 normalizing.
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 normalize, 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 normalizing} \\ 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 normalities 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.
