Trouble Replicating Proof of The Lambda Calculus Fixed Point Theorem From pg. 35 of Lambda Calculus and Combinators An Introduction:


  Corollary 3.3.1 in $\lambda$ and $CL$: for every $Z$ and $n \ge 0$, the equation
  
  $$ xy_1 \ldots y_n = Z $$
  
  can be solved for $x$. That is, there is a term $X$ such that
  
  $$ Xy_1 \ldots y_n =_{\beta, w} [X/x]Z. $$
  
  Proof: Choose $X \equiv \mathsf{Y} (\lambda x y_1 \ldots y_n.Z)$.


Note: In the book, we assume that $\mathsf{Y} \equiv (\lambda ux. xuux)(\lambda ux. xuux)$. Further, for ease of notation, let $V \equiv (\lambda x y_1 \ldots y_n.Z)$.

The problem is that when I check this with my own examples, I'm not getting this result.

For example, suppose that neither $x$ nor any of $y_1, \ldots , y_n$ is in the free variables of $Z$ (to make it easy). Then this theorem asserts that if $X \equiv \mathsf{Y}(\lambda x y_1 \ldots y_n . Z)$, then

$$
Xy_1 \ldots y_n =_{\beta, w} Z
$$

When I check whether this true, I get

$$
(\mathsf{Y}(\lambda x y_1 \ldots y_n . Z))y_1 \ldots y_n = (\mathsf{Y}V)y_1 \ldots y_n = (V\mathsf{Y}V)y_1 \ldots y_n =_{\beta, w} Zy_n 
$$

Am I doing something wrong?
$\newcommand{\Y}{\mathsf{Y}}$

Did you leave out any parentheses by any chance? We should take $\Y = (\lambda  u x . x (u u x)) (\lambda  u x . x (u u x))$. Note that $x u u x$ is the same as $(x u u) x$, which is not the same as $x (u u x)$.

We use the abbreviations $V = (\lambda x y_1 \ldots y_n . Z)$ and $X = \Y V$, as in your question. Then we calculate:
\begin{align*}
\Y V
&amp;= (\lambda  u x . x (u u x)) (\lambda  u x . x (u u x)) V \\
&amp;= (\lambda x . x ((\lambda  u x . x (u u x)) (\lambda  u x . x (u u x)) x)) V \\
&amp;= V ((\lambda  u x . x (u u x)) (\lambda  u x . x (u u x)) V) \\
&amp;= V (\Y V)
\end{align*}
and hence
\begin{align*}
X y_1 \ldots y_n
&amp;= \Y V y_1 \ldots y_n \\
&amp;= V (\Y V) y_1 \ldots y_n \\
&amp;= (\lambda x y_1 \ldots y_n . Z) (\Y V) y_1 \ldots y_n \\
&amp;= (\lambda x y_1 \ldots y_n . Z) X y_1 \ldots y_n \\
&amp;= [X/x, y_1/y_1, \ldots, y_n/y_n] Z \\
&amp;= [X/x] Z.
\end{align*}