The usual fixed point combinator is $$ Y = \lambda f . ( (\lambda x. f(xx)) \; (\lambda x. f(xx)) ) $$ However this combinator fails to generate a recursive function when call by value is imposed. Plotkin uses the following combinator that works well under call by value
$$ Z = \lambda f. (\lambda y. f(\lambda z.yyz)) \;(\lambda y. f(\lambda z.yyz))$$
I've been trying to prove that this is in fact a fixed point combinator by showing that $Z \; f = f \;(Z\;f)$, however I'm not really sure how to proceed without using $\eta$-reduction.
Call by value says that: $$\dfrac{M \rightarrow M'}{(MN) \rightarrow (M'N)}$$ $$\dfrac{N \rightarrow N'}{(\lambda x.M) N \rightarrow (\lambda x.M) N'}$$ $$ \dfrac{v \text{ is a value}}{(\lambda x.M) v \rightarrow M[x:=v]} $$
So when I evaluate $Z \; f $ I get the following. Lets say that $\theta = \lambda y.f(\lambda z.yyz)$
\begin{align*} Z \; f &\rightarrow (\lambda y.f(\lambda z.yyz)) \; \theta\\ &\rightarrow f \; (\lambda z.\theta\theta z) \end{align*}
If I could use $\eta$-reduction on $\lambda z.\theta\theta z$, then I would be done, but I can't.
How else could I prove that Z is in fact a fixed point combinator?