How to prove that Z is a fixed point combinator under call by value? 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?
 A: It's not clear what you mean by "$=$" in $Zf=f(Zf)$. Even if you allow $\eta$-reduction, this can't be the judgemental/definitional equality as it is the case for your expressions for $Y$, $Z$ and $\theta$. If you mean $\beta$-equivalence, which is the most commonly used in untyped lambda calculus, then it can be shown that $Zf$ and $f(Zf)$ are NOT $\beta$-equivalent.
Lambda calculus with $\beta$-reduction has Church-Rosser property, so if $Zf$ and $f(Zf)$ are $\beta$-equivalent then they should joinable. But $Zf$ can be reduced to terms of form -
$(\lambda f. \theta \theta)f$ or $(\lambda f. f(\lambda z.\theta \theta z))f$ or $(\lambda f. f(\lambda z. f(\lambda z.\theta \theta z) z))f$ or $(\lambda f. f(\lambda z. f(\lambda z.f(\lambda z.\theta \theta z) z) z))f$ so on, or
$\theta \theta$ or $f(\lambda z.\theta \theta z)$ or $f(\lambda z. f(\lambda z.\theta \theta z) z)$ or $f(\lambda z. f(\lambda z.f(\lambda z.\theta \theta z) z) z)$ so on
But $f(Zf)$ reduces to any of the above with an extra $f$ in front.
By above, $Zf$ and $f(Zf)$ can't be reduced to same term, so they are not joinable. So, they are not $\beta$-equivalent as well.
And finally, note that if you restrict to call by value only, then it will make it still harder for 2 term to be equivalent. That is, call-by-value-equivalence implies $\beta$-equivalence, so as the above two are not $\beta$-equivalent, they are not call-by-value-equivalent as well.
