We make use of a functional representation of the initial structures. Without
this functional representations we would not be able to eliminate all
quantifiers. Indeed, with this functional representation we can talk of a node
at distance 2 from \(x\)  using the quantifier-free term \(f(f(x))\) , avoiding the
existential quantification of the middle point. This idea was already taken
in [1]} for eliminating first-order quantifiers over structures of
bounded degree. Our approach differs from theirs in the fact that in the bounded
degree case the functions can be assumed to be permutations (in particular
they are invertible) while this is no longer true in our setting, complicating
significantly the combinatorics.
