Infinite sets with bijection are strongly minimal I'm working through Tent and Ziegler "A Course in Model Theory" and I got stuck on the Exercise 5.7.2:

Show that the theory of an infinite set equipped with a
bijection without finite cycles is strongly minimal and that the associated
geometry is trivial.

I think I understand how to do the trivial geometry part. For the strong minimality, however, I do not know how to get quantifier elimination, which seems to be the key to the problem. Any hints would be appreciated!
 A: Let $\mathcal{L}=\{f\}$, the language of a unary function, and let $T$ be the theory of a bijection without finite cycles. We first show that $T$ eliminates quantifiers; by, eg, lemma 3.2.4. of Tent and Ziegler, it suffices to consider primitive existential formulas.  There are no constant symbols in our language, so the only terms are of the form $f^n(v)$ for some $n\in\omega$ and some variable $v$, where we use the notation indicated by Alex in his comments. Additionally, the only relation symbol in our language is equality, so the only atomic formulas are of the form $f^m(v)=f^n(w)$. Thus, any conjunction of atomic formulas and their negations will be of the form $$\phi(\overline{v})\wedge\left(\bigwedge_{l=1}^af^{m'_l}(w)=f^{m_l}(v_{i_l})\right)\wedge\left(\bigwedge_{l=1}^{b}f^{n'_l}(w)\neq f^{n_l}(v_{j_l})\right)\wedge\psi(w)$$ where $\psi$ and $\phi$ are themselves quantifier-free and of the same form as the two conjuncts in the middle. Now, denoting by $\theta(v_1,\dots,v_k,w)$ the formula above, we wish to show that $\exists w\theta$ is equivalent to a quantifier-free formula, modulo $T$.
First we claim that we can ignore $\psi(w)$; indeed, if $\psi(w)$ contains any conjunct of the shape $f^m(w)\neq f^m(w)$, then $\exists w\theta$ will of course be unsatisfiable and so equivalent to $\bot$. On the other hand, consider the case where $\psi(w)$ contains any conjunct of the shape $f^m(w)=f^n(w)$ for $m\neq n$. Any value of $w$ satisfying this formula would be part of a finite cycle, of cycle length dividing $m-n$. Since models of $T$ have no finite cycles, in this case $\exists w\theta$ is again equivalent to $\bot$. Conversely, if $\psi$ does not contain any conjuncts of the above two forms, then every element of a model of $T$ will satisfy it, and so we may safely omit it from considerations. Indeed, in this case every conjunct of $\psi$ will be of form $f^m(w)=f^m(w)$ (clearly satisfied by any element of a model of $T$) or $f^m(w)\neq f^n(w)$ for $m\neq n$ (again satisfied by any element of a model of $T$, since such models have no finite $f$-cycles).
Thus it suffices to consider the case where $\theta$ has an empty $\psi(w)$ term. Since $f$ is a bijection, we may replace each $m_l$ in $\theta$ with $m_l-m_l'$ and each $n_l$ in $\theta$ with $n_l-n_l'$ and hence assume that each $m'_l=0$ and $n'_l=0$. (Note, however, that this means $m_l$ and $n_l$ may be negative, so the corresponding expression may not be an $\mathcal{L}$-formula.)
Now, because any model of $T$ has infinitely many elements, if $a=0$ then $\exists w\theta$ will be equivalent to $\phi(\overline{v})$. Thus we may assume $a>0$, and then we have that $\exists w\theta$ is equivalent to $$\phi(\overline{v})\wedge\left(f^{m_1}(v_{i_1})=\dots=f^{m_a}(v_{i_a})\right)\wedge\left(\bigwedge_{l=1}^b f^{m_1}(v_{i_1})\neq f^{n_l}(v_{j_i})\right).$$ Now, since there may be negative values of $m_l$ and $n_l$, this will not necessarily be an $\mathcal{L}$-formula. However, if there are negative values of $m_l$ and $n_l$, then we may simply apply $f$ a total of $|\min\{m_1,\dots,m_a,n_1,\dots,n_b\}|$ times to every term and thence obtain an $\mathcal{L}$-formula. Since $f$ is a bijection, the resulting formula will be logically equivalent to the original.

It follows immediately that $T$ is strongly minimal. Indeed, if $M\models T$, then by quantifier elimination (and the fact that $\mathcal{L}$ has no relation symbols) every $\mathcal{L}_M$-formula in one free variable will cut out a boolean combination of finite sets, and thus be either finite or cofinite, as desired.
