. Proof, Immediate from Lemma 6.2 and Theorem 2.3 via the same type of manipulation that proves Theorem 1

A. Definability, Invariance We now use Lemma 6.3 to show that a regular language is definable in Arb-invariant FO(Succ) iff it is definable in FO(Succ, lm). The " only if " direction is straightforward as any predicate of the form lm can be expressed in Arb-invariant FO(Succ) (actually only addition is needed)

. Xe-i,-e-i-yf-i,-e-i-uf-i, e i vf i and f i z to their corresponding substring in the other string. Hence by Theorem 5.1 we have xe 2i uf 2i ye 2i vf 2i z ? L iff xe 2i vf 2i ye 2i uf 2i z ? L. But again, as e and f are idempotents, this implies xeuf yevf z ? L iff xeuf yevf z ? L. Therefore L is closed under swaps. The pumping argument for closure under transfers is identical. By Lemma 6.3 there are constants c and n 0 such that L is closed under (log n) c -transfers for strings of length bigger than n 0 . Consider x, u, y, v, z as in the hypothesis for closure under transfers. As u ? and v ? are idempotents we have for all i ? N, xu ?·i uyv ?·i z ? L iff xu ? uyv ? z ? L. Take i large enough so that i · ? ? (log |xu ?·i uyv ?·i z|) c ? (log n 0 ) c . Hence we can apply closure under (log n) c -transfers and by Lemma 6, xe 2i vf 2i ye 2i uf 2i z via the bijection sending respectively

S. Abiteboul, R. Hull, and V. Vianu, Foundations of Databases, 1995.

A. Ajtai, ???11-Formulae on finite structures, Annals of Pure and Applied Logic, vol.24, issue.1, pp.1-48, 1983.
DOI : 10.1016/0168-0072(83)90038-6

M. Ajtai, First-order definability on finite structures, Annals of Pure and Applied Logic, vol.45, issue.3, pp.211-225, 1989.
DOI : 10.1016/0168-0072(89)90036-5

A. E. Andreev, On a method for obtaining lower bounds for the complexity of individual monotone functions, Soviet Math. Dokl, vol.31, issue.3, pp.530-534, 1985.

M. Anderson, D. Van-melkebeek, N. Schweikardt, and L. Segoufin, Locality of Queries Definable in Invariant First-Order Logic with Arbitrary Built-in Predicates, Proc. Intl. Colloq. on Automata, Languages and Programming (ICALP), pp.368-379, 2011.
DOI : 10.1007/10703163_10

. Danì, J. Beauquier, and . Pin, Factors of words, Proc. Intl, pp.63-79, 1989.

M. Benedikt and L. Segoufin, Regular tree languages definable in FO and FO mod, ACM Transactions on Computational Logic, vol.11, issue.1, 2009.

M. Benedikt and L. Segoufin, Towards a Characterization of Order-Invariant Queries over Tame Structures, Journal of Symbolic Logic, vol.74, issue.1, pp.168-186, 2009.
DOI : 10.1007/11538363_20

E. M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking, 1999.

A. Durand, C. Lautemann, and M. More, Counting results in weak formalisms, Circuits, Logic, and Games, number 06451 in Dagstuhl Seminar Proc. Internationales Begegnungs-und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, 2007.

[. Ebbinghaus and J. Flum, Finite model theory, 1999.

M. Furst, J. Saxe, and M. Sipser, Parity, circuits, and the polynomial-time hierarchy, Mathematical Systems Theory, vol.3, issue.1, pp.13-27, 1984.
DOI : 10.1007/BF01744431

[. Fagin, L. J. Stockmeyer, and M. Y. Vardi, On monadic NP vs. monadic co-NP. Information and Computation, pp.78-92, 1995.

H. Gaifman, On Local and Non-Local Properties, Proc. Herbrand Symposium, Logic Colloquium, pp.105-135, 1981.
DOI : 10.1016/S0049-237X(08)71879-2

M. Grohe and S. Kreutzer, Methods for algorithmic meta theorems, Model Theoretic Methods in Finite Combinatorics, 2011.
DOI : 10.1090/conm/558/11051

M. Grohe, Fixed-Point Definability and Polynomial Time, Proc. Conf. for Computer Science Logic (CSL), pp.20-23, 2009.
DOI : 10.1016/S0304-3975(98)00314-4

M. Grohe and T. Schwentick, Locality of order-invariant first-order formulas, ACM Transactions on Computational Logic, vol.1, issue.1, pp.112-130, 2000.
DOI : 10.1145/343369.343386

DOI : 10.1016/B978-0-7204-2233-7.50020-4

L. Addison, A. Henkin, and . Tarski, The Theory of Models, pp.132-145, 1965.

J. Håstad, Computational limitations for small-depth circuits, 1986.

L. Hella, L. Libkin, and J. Nurmonen, Abstract, The Journal of Symbolic Logic, vol.1450, issue.04, pp.1751-1773, 1999.
DOI : 10.1016/0168-0072(94)00025-X

N. Immerman, Relational queries computable in polynomial time, Information and Control, vol.68, issue.1-3, pp.86-104, 1986.
DOI : 10.1016/S0019-9958(86)80029-8

N. Immerman, Languages that Capture Complexity Classes, SIAM Journal on Computing, vol.16, issue.4, pp.760-778, 1987.
DOI : 10.1137/0216051

[. Immerman, Descriptive Complexity, 1999.
DOI : 10.1007/978-1-4612-0539-5

L. Libkin, Expressive power of SQL, Theoretical Computer Science, vol.296, issue.3, pp.379-404, 2003.
DOI : 10.1016/S0304-3975(02)00736-3

L. Libkin, Elements of Finite Model Theory, 2004.
DOI : 10.1007/978-3-662-07003-1

N. Linial, Y. Mansour, and N. Nisan, Constant depth circuits, Fourier transform, and learnability, Journal of the ACM, vol.40, issue.3, pp.607-620, 1993.
DOI : 10.1145/174130.174138

L. Libkin and J. Nurmonen, Counting and Locality over Finite Structures A Survey, Generalized Quantifiers and Computation, 9th European Summer School in Logic, Language, and Information (ESSLLI'97, pp.18-50, 2000.
DOI : 10.1007/3-540-46583-9_2

J. A. Makowsky, Invariant definability, Proc. 5th Kurt Gödel Colloquium (KGC'97, pp.186-202, 1997.
DOI : 10.1007/3-540-63385-5_43

J. A. Makowsky, Invariant Definability and P/poly, Proc. Conf. for Computer Science Logic (CSL), pp.142-158, 1998.
DOI : 10.1007/10703163_10

M. Otto, Abstract, The Journal of Symbolic Logic, vol.2, issue.04, pp.1749-1757, 2000.
DOI : 10.1006/inco.1996.0070

A. A. Razborov, Lower bounds on the monotone complexity of some boolean functions, Soviet Math. Dokl, vol.31, pp.354-357, 1985.

B. Rossman, Abstract, The Journal of Symbolic Logic, vol.1, issue.02, pp.601-618, 2007.
DOI : 10.2178/jsl/1185803625

B. Rossman, On the constant-depth complexity of k-clique, Proceedings of the fourtieth annual ACM symposium on Theory of computing, STOC 08, pp.721-730, 2008.
DOI : 10.1145/1374376.1374480

B. Rossman, Average-Case Complexity of Detecting Cliques, 2010.

N. Schweikardt, Arithmetic, first-order logic, and counting quantifiers, ACM Transactions on Computational Logic, vol.6, issue.3, pp.634-671, 2005.
DOI : 10.1145/1071596.1071602

N. Schweikardt and L. Segoufin, Addition-Invariant FO and Regularity, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.273-282, 2010.
DOI : 10.1109/LICS.2010.16

[. Schweikardt, T. Schwentick, and L. Segoufin, Database Theory, Algorithms and Theory of Computation Handbook, 2009.
DOI : 10.1201/9781584888215-c19

D. Thérien and A. Weiss, Graph congruences and wreath products, Journal of Pure and Applied Algebra, vol.36, pp.205-215, 1985.
DOI : 10.1016/0022-4049(85)90071-4

M. Vardi, The complexity of relational query languages, Proc. Symp. on the Theory of Computing (STOC), pp.137-146, 1982.

A. Yao, Separating the polynomial-time hierarchy by oracles (Preliminary Version), Proc. Symp. on Foundations of Computer Science (FOCS), pp.1-10, 1985.