The following problem is attributed to Klop mentioned in Barendregt's book (as per notes I'm going through).
Here's the problem:
Show that $\underline{Y_2}$ is a fixed-point operator, where
$$ LET \ @ = \lambda abcdefghijklmnopqstuvwxyzr. r(thisisafixedpointcombinator) $$
$$ LET \ \underline{Y_2} = @@@@@@@@@@@@@@@@@@@@@@@@@@ $$
Here's my try:
$\underline{Y_2} \ E = \underbrace{@..@}_\text{26 @'s}E = (\lambda a..qs..zr. r(\underbrace{...}_\text{26 letters not r}r))\underbrace{@..@}_\text{25 @'s}E = (\lambda r. r(\underbrace{@..@}_\text{26 @'s}r))E = E(\underbrace{@..@}_\text{26 @'s}E) = E(\underline{Y_2}E) $
$\square$
Are steps correct and reasonable? Thanks a bunch!