Bluebirds and mockingbirds cannot produce a fixed-point combinator

Let $B$ be the bluebird combinator with reduction rule $Bxyz{\to }_{w}x\left(yz\right)$, let $M$ be the mockingbird combinator with reduction rule $Mx{\to }_{w}xx$, and let $I$ be the identitybird combinator with reduction rule $Ix{\to }_{w}x$. For a fixed variable $x$, we construct an invariant ${\mathrm{T}\mathrm{r}}_x\left(u\right)$ of a $BMI$-term $u$ with respect to ${\to }_w$. This invariant traces the occurrences of $x$ in the leftmost-innermost reduction sequence of $u$. We then prove that ${\mathrm{T}\mathrm{r}}_x\left(Yx\right)\mathrm{\ne }{\mathrm{T}\mathrm{r}}_x\left(x^r\left(Yx\right)\right)$ for every $x$-free $BMI$-term $Y$ and every $r\ge 1$. Consequently, there exists no fixed-point combinator in $BMI$-combinatory logic under weak equivalence. This provides a negative answer to the problem posed by Smullyan in 1985.