, S 1 ) and (G 2 , S 2 ) have the same number of occurrences of every r-type

, S2) (h(x)) = tp k (G1,S1) (x) There is nothing to prove for k = 0. Moving from k to k + 1, let x ? A 1 and let y be such that dist G1 (x, y) = d, for some 1 ? d ? k + 1. Note that y ? B, hence it has an image by h, We prove by induction on 0 ? k ? r that ?x ? A 1 , tp k (G2

, Because of (Layer[r]), it only remains to show that the S -successors of x and h(x), as well as their S -predecessors

, Let's prove this for the successors, respectively named x + and h(x) + . If x + ? A 1 , then by construction h(x) + = h(x + ), and the induction hypothesis allows us to conclude

, Otherwise, neither x + nor h(x) + belongs to A 1 . Under this hypothesis, Lemma 4.7 ensures that tp r G2 (h(x) + ) = tp r G2 (h(x)) = tp r G1 (x) = tp r G1 (x + )

. Now,

M. Benedikt and L. Segoufin, Towards a characterization of orderinvariant queries over tame graphs, J. Symb. Log, 2009.

K. Eickmeyer, M. Elberfeld, and F. Harwath, Expressivity and succinctness of order-invariant logics on depth-bounded structures, Mathematical Foundations of Computer Science (MFCS) -39th International Symposium, 2014.

M. Elberfeld, M. Frickenschmidt, and M. Grohe, Order invariance on decomposable structures, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, 2016.

R. Fagin, L. J. Stockmeyer, and M. Y. Vardi, On monadic NP vs. monadic co-np, Inf. Comput, 1995.

J. Gajarský, P. Hlinený, D. Lokshtanov, J. Obdrzálek, and M. S. Ramanujan, A new perspective on FO model checking of dense graph classes, 2018.

J. Grange and L. Segoufin, Order-Invariant First-Order Logic over Hollow Trees, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Schloss Dagstuhl, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02310749

M. Grohe and T. Schwentick, Locality of order-invariant firstorder formulas, ACM Trans. Comput. Log, 2000.

L. Libkin, Elements of Finite Model Theory. Texts in Theoretical Computer Science, An EATCS Series, 2004.

. Benjamin-rossman, Successor-invariant first-order logic on finite structures, J. Symb. Log, 2007.

A. Boris and . Trakhtenbrot, Impossibility of an algorithm for the decision problem in finite classes, Doklady Akademii Nauk SSSR, 1950.