, 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 + )
,
Towards a characterization of orderinvariant queries over tame graphs, J. Symb. Log, 2009. ,
Expressivity and succinctness of order-invariant logics on depth-bounded structures, Mathematical Foundations of Computer Science (MFCS) -39th International Symposium, 2014. ,
Order invariance on decomposable structures, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, 2016. ,
On monadic NP vs. monadic co-np, Inf. Comput, 1995. ,
A new perspective on FO model checking of dense graph classes, 2018. ,
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
Locality of order-invariant firstorder formulas, ACM Trans. Comput. Log, 2000. ,
Elements of Finite Model Theory. Texts in Theoretical Computer Science, An EATCS Series, 2004. ,
Successor-invariant first-order logic on finite structures, J. Symb. Log, 2007. ,
Impossibility of an algorithm for the decision problem in finite classes, Doklady Akademii Nauk SSSR, 1950. ,