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?
Trouble Replicating Proof of The Lambda Calculus Fixed Point Theorem
lambda calculus;combinatory logic
$\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&= (\lambda  u x . x (u u x)) (\lambda  u x . x (u u x)) V \\&= (\lambda x . x ((\lambda  u x . x (u u x)) (\lambda  u x . x (u u x)) x)) V \\&= V ((\lambda  u x . x (u u x)) (\lambda  u x . x (u u x)) V) \\&= V (\Y V)\end{align*}and hence\begin{align*}X y_1 \ldots y_n&= \Y V y_1 \ldots y_n \\&= V (\Y V) y_1 \ldots y_n \\&= (\lambda x y_1 \ldots y_n . Z) (\Y V) y_1 \ldots y_n \\&= (\lambda x y_1 \ldots y_n . Z) X y_1 \ldots y_n \\&= [X/x, y_1/y_1, \ldots, y_n/y_n] Z \\&= [X/x] Z.\end{align*}