Manfred Kufleitner
email: kufleitner@fmi.uni-stuttgart.de

Pascal Weil
email: pascal.weil@labri.fr

ON LOGICAL HIERARCHIES WITHIN FO 2 -DEFINABLE LANGUAGES

We consider the class of languages defined in the 2-variable fragment of the first-order logic of the linear order. Many interesting characterizations of this class are known, as well as the fact that restricting the number of quantifier alternations yields an infinite hierarchy whose levels are varieties of languages (and hence admit an algebraic characterization). Using this algebraic approach, we show that the quantifier alternation hierarchy inside FO 2 [<] is decidable within one unit. For this purpose, we relate each level of the hierarchy with decidable varieties of languages, which can be defined in terms of iterated deterministic and co-deterministic products. A crucial notion in this process is that of condensed rankers, a refinement of the rankers of Weis and Immerman and the turtle languages of Schwentick, Thérien and Vollmer.

Many important properties of systems are modeled by finite automata. Frequently, the formal languages induced by these systems are definable in first-order logic. Our understanding of its expressive power is of direct relevance for a number of application fields, such as verification.

The first-order logic we are interested in, in this paper, is the first-order logic of the linear order, written FO[<], interpreted on finite words. It is well-known that the languages that are definable in this logic are exactly the star-free languages, or equivalently the regular languages whose syntactic monoid is aperiodic (that is: satisfies an identity of the form x n+1 = x n for some integer n) [START_REF] Paul | On finite monoids having only trivial subgroups[END_REF][START_REF] Mcnaughton | Counter-Free Automata[END_REF] (see also [START_REF] Diekert | First-order definable languages[END_REF][START_REF] Pin | Varieties of Formal Languages[END_REF][START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF][START_REF] Straubing | An introduction to automata theory[END_REF]); and that deciding whether a finite automaton accepts such a language is PSPACE-complete [START_REF] Cho | Finite automaton aperiodicity is PSPACE-complete[END_REF].

Fragments of first-order logic defined by the limitation of certain resources have been studied in detail. For instance, the quantifier alternation hierarchy, with its close relation with the dot-depth hierarchy of star-free languages, offers one of the oldest open problems in formal language theory: we know that the hierarchy is infinite and that its levels are characterized algebraically (by a property of the syntactic monoids), but we do not know whether these levels (besides levels 0 and 1) are decidable. In contrast, it is known that the quantifier alternation hierarchy for the first-order logic of the successor, FO[S], collapses at level 2 [START_REF] Thomas | Classifying regular events in symbolic logic[END_REF][START_REF] Pin | Expressive power of existential first-order sentences of Büchi's sequential calculus[END_REF].

Another natural limitation considers the number of variables in a formula. This limitation has attracted a good deal of attention, as the trade-off between formula size and number of variables is known to be related with the trade-off between parallel time and number of processes, see [START_REF] Immerman | Descriptive Complexity[END_REF][START_REF] Adler | An n! lower bound on formula size[END_REF][START_REF] Grohe | The succinctness of first-order logic on linear orders[END_REF].

It is well-known that every first-order formula is equivalent to one using at most three variables. On the other hand, the first-order formulas using at most two variables, written FO 2 [<], are strictly less expressive. The class of languages defined by such formulas admits many remarkable characterizations [START_REF] Tesson | Diamonds are forever: The variety DA[END_REF]. To begin with, a language is FO 2 [<]-definable if and only if it is recognized by a monoid in the pseudovariety DA [START_REF] Thérien | Over words, two variables are as powerful as one quantifier alternation[END_REF] (a precise definition will be given in Section 2). As with the characterization of FO[<]-definability by aperiodic monoids, this characterization implies decidability. The FO 2 [<]-definable languages are also characterized in terms of unambiguous products of languages (see Section 6.3) and in terms of the unary fragment of propositional temporal logic [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF] (see Section 1.3). For a survey of these properties, the reader is referred to [START_REF] Tesson | Diamonds are forever: The variety DA[END_REF][START_REF] Volker Diekert | A survey on small fragments of first-order logic over finite words[END_REF].

In this paper, we consider the quantifier alternation hierarchy within the two-variable fragment of first-order logic. We denote by FO 2 m [<] the fragment of FO 2 [<] consisting of formulas using at most 2 variables and at most m alternating blocks of quantifiers. In the sequel, we omit specifying the predicate < and we write simply FO, FO 2 or FO 2 m . Schwentick, Thérien and Vollmer introduced the so-called turtle programs to characterize the expressive power of FO 2 [START_REF] Schwentick | Partially-ordered two-way automata: A new characterization of DA[END_REF]. These programs are sequences of directional instructions of the form go to the next a to the right, go to the next b to the left. More details can be found in Section 1.2 below. Turtle programs were then used, under the name of rankers, by Weis and Immerman [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF] (first published in [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF]) to characterize FO 2 m in terms of rankers with m alternations of directions (right vs. left). Their subtle characterization, Theorem 1.8 below, does not yield a decidability result. It forms however the basis of our results.

Rankers are actually better suited to the study of a natural alternation hierarchy within the unary fragment of propositional temporal logic (Sections 1. 3 and 4), than to the study of the quantifier alternation within FO 2 [<]. For the latter, we define the notion of condensed rankers, which introduce a notion of efficiency in the path they describe in a word, see Section 3.

Recent results of Kufleitner and Lauser [START_REF] Kufleitner | Lattices of logical fragments over words[END_REF] and Straubing [START_REF] Straubing | Algebraic characterization of the alternation hierarchy in FO 2 [<] on finite words[END_REF] show that FO 2 m (the set of FO 2 m -definable languages) forms a variety of languages. We show that the classes of languages defined by condensed rankers with at most m changes of directions also form varieties of languages, written R m and L m depending on whether the initial move is towards the right or towards the left (Section 3.3). The meaning of these results is that membership of a language L in these classes depends only on the syntactic monoid of L. This justifies using algebraic methods to approach the decidability problem for FO 2 m -a technique that has proved very useful in a number of situations (see for instance [START_REF] Pin | Varieties of Formal Languages[END_REF][START_REF] Tesson | Diamonds are forever: The variety DA[END_REF][START_REF] Straubing | Varieties[END_REF][START_REF] Volker Diekert | A survey on small fragments of first-order logic over finite words[END_REF]).

In fact, we use this algebraic approach to show that the classes R m and L m are decidable (Section 3.5), and that they admit a neat characterization in terms of closure under alternated deterministic and co-deterministic products (Section 3.4). Moreover, we show (Theorem 5.1) that

R m ∪ L m ⊆ FO 2 m ⊆ R m+1 ∩ L m+1
. This shows that one can effectively compute, given a language L in FO 2 , an integer m such that L is in FO 2 m+1 , possibly in FO 2 m , but not in FO 2 m-1 . That is, we can compute the quantifier alternation depth of L within one unit. As indicated above, this is much more precise than the current level of knowledge on the general quantifier alternation hierarchy in FO [<].

We conjecture that FO 2 m is actually equal to the intersection of R m+1 and L m+1 . This would prove that each FO 2 m is decidable. Many of these results were announced in [START_REF] Kufleitner | On FO 2 quantifier alternation over words[END_REF], with a few differences. In particular, the definition of the sets R X m,n (Section 1.2) in [START_REF] Kufleitner | On FO 2 quantifier alternation over words[END_REF] introduced a mistake which is corrected here. The proof of [START_REF] Kufleitner | On FO 2 quantifier alternation over words[END_REF]Theorem 2] contained a gap: we do not have a proof that the classes defined by the alternation hierarchy within unary temporal logic are varieties. And the proof of [14, Proposition 2.9] also contained a gap: the correct statement is Theorem 4.3 below.

Rankers and logical hierarchies

Let A be a finite alphabet. We denote by A * the set of all words over A (that is, of sequences of elements of A), and by A + the set of non-empty words. If u is a length n (n > 0) word over A, we say that an integer 1 ≤ i ≤ n is an a-position of u if the i-th letter of u, written u [i], is an a. If 1 ≤ i ≤ j ≤ n, we let u[i; j] be the factor u

[i] • • • u[j] of u.
FO denotes the set of first-order formulas using the unary predicates a (a ∈ A) and the binary predicate <, and FO 2 denotes the fragment of FO consisting of formulas which use at most two variable symbols.

If u is a length n (n > 0) word over A, we identify the word u with the logical structure ({1, . . . , n}, (a) a∈A ), where a denotes the set of a-positions in u. Formulas from FO are naturally interpreted over this structure, and we denote by L(ϕ) the language defined by the formula ϕ ∈ FO, that is, the set of all words which satisfy ϕ.

1.1. Quantifier-alternation within FO 2 . We now concentrate on FO 2formulas and we define two important parameters concerning such formulas. To simplify matters, we consider only formulas where negation is used only on atomic formulas so that, in particular, no quantifier is negated. This is naturally possible up to logical equivalence. Now, with each formula ϕ ∈ FO 2 , we associate in the natural way a parsing tree: each occurence of a quantification, ∃x or ∀x, yields a unary node, each occurrence of ∨ or ∧ yields a binary node, and the leaves are labeled with atomic or negated atomic formulas. The quantifier depth of ϕ is the maximum number of quantifiers along a path in its parsing tree.

With each path from root to leaf in this parsing tree, we also associate its quantifier label, which is the sequence of quantifier node labels (∃ or ∀) encountered along this path. A block in this quantifier label is a maximal factor consisting only of ∃ or only of ∀, and we define the number of blocks of ϕ to be the maximum number of blocks in the quantifier label of a path in its parsing tree. Naturally, the quantifier depth of ϕ is at least equal to its number of blocks.

We let FO 2 m,n (n ≥ m) denote the set of first-order formulas with quantifier depth at most n and with at most m blocks and let FO 2 m denote the union of the FO 2 m,n for all n. We also denote by

FO 2 (FO 2 m , FO 2 m,n ) the class of FO 2 (FO 2 m , FO 2 m,n )-definable languages. Remark 1.1. Recall that a language is piecewise testable if it is a Boolean combination of languages of the form A * a 1 A * • • • a k A * (a i ∈ A).
It is an elementary observation that the piecewise testable languages coincide with FO 2 1 . It is well-known that this class of languages is decidable (see Section 2 below).

Rankers.

A ranker is a non-empty word on the alphabet {X a , Y a | a ∈ A}. Rankers define positions in words: given a word u ∈ A + and a letter a ∈ A, we denote by X a (u) (resp. Y a (u)) the least (resp. greatest) integer 1 ≤ i ≤ |u| such that u[i] = a. If a does not occur in u, we say that Y a (u) and X a (u) are not defined. If in addition q is an integer such that 0 ≤ q ≤ |u|, we let

X a (u, q) = q + X a (u[q + 1; |u|]) Y a (u, q) = Y a (u[1; q -1]).
These definitions are extended to all rankers: if r is a ranker, Z ∈ {X a , Y a | a ∈ A} and r = r Z, we let r(u, q) = Z(u, r (u, q)) if r (u, q) and Z(u, r (u, q)) are defined, and we say that r(u, q) is undefined otherwise. In particular: rankers are processed from left to right.

Finally, if r starts with an X-(resp. Y-) letter, we say that r defines the position r(u) = r(u, 0) (resp. r(u) = r(u, |u| + 1)), or that it is undefined on u if this position does not exist. Remark 1.2. Rankers were first introduced, under the name of turtle programs, by Schwentick, Thérien and Vollmer [START_REF] Schwentick | Partially-ordered two-way automata: A new characterization of DA[END_REF], as sequences of instructions: go to the next a to the right, go to the next b to the left, etc. These authors write (→, a) and (←, a) instead of X a and Y a . Weis and Immerman [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF] write a and a instead, and they introduced the term ranker. We rather follow the notation in [START_REF] Volker Diekert | A survey on small fragments of first-order logic over finite words[END_REF][START_REF] Kufleitner | Polynomials, fragments of temporal logic and the variety DA over traces[END_REF][START_REF] Diekert | Pure future local temporal logics are expressively complete for Mazurkiewicz traces[END_REF], where X and Y refer to the future and past operators of PTL.

Example 1.3. The ranker X a Y b X c (go to the first a starting from the left, thence to the first b towards the left, thence to the first c towards the right) is defined on bac and bca, but not on abc or cba.

By L(r) we denote the language of all words on which the ranker r is defined. We say that the words u and v agree on a class R of rankers if exactly the same rankers from R are defined on u and v. And we say that two rankers r and s coincide on a word u if they are both defined on u and

r(u) = s(u). Example 1.4. If r = X a 1 • • • X a k (resp. r = Y a k • • • Y a 1 ), then L(r) is the set of words that contain a 1 • • • a k as a subword, L(r) = A * a 1 A * • • • a k A * .
The depth of a ranker r is defined to be its length as a word. A block in r is a maximal factor in

{X a | a ∈ A} + (an X-block) or in {Y a | a ∈ A} + (a Y-block). If n ≥ m, we denote by R X m,n (resp. R Y m,n
) the set of mblock, depth n rankers, starting with an X-(resp. Y-) block, and we let

R m,n = R X m,n ∪ R Y m,n and R X m,n = m ≤m,n ≤n R X m ,n ∪ m <m,n <n R Y m ,n . We define R Y m,n dually and we let R X m = n≥m R X m,n , R Y m = n≥m R Y m,n and R m = R X m ∪ R Y m . Remark 1.5.
Readers familiar with [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF] will notice differences between our R X m,n and their analogous R m ,n ; introduced for technical reasons, it creates no difference between our R m,n and their R m,n , the classes which intervene in crucial Theorem 1.8 below.

Rankers and unary temporal logic.

Let us depart for a moment from the consideration of FO 2 -formulas, to observe that rankers are naturally suited to describe the different levels of a natural class of temporal logic. The symbols X a and Y a (a ∈ A) can be seen as modal (temporal) operators, with the future and past semantics respectively. We denote the resulting temporal logic (known as unary temporal logic) by TL: its only atomic formula is , the other formulas are built using Boolean connectives and modal operators. Let u ∈ A + and let 0 ≤ i ≤ |u| + 1. We say that holds at every position i, (u, i) |= ; Boolean connectives are interpreted as usual; and (u

, i) |= X a ϕ (resp. Y a ϕ) if and only if (u, X a (u, i)) |= ϕ (resp. (u, Y a (u, i)) |= ϕ). We also say that u |= X a ϕ (resp. Y a ϕ) if (u, 0) |= X a ϕ (resp. (u, 1 + |u|) |= Y a ϕ).
TL is a fragment of propositional temporal logic PTL; the latter is expressively equivalent to FO and TL is expressively equivalent to FO 2 [START_REF] Kufleitner | Polynomials, fragments of temporal logic and the variety DA over traces[END_REF].

As in the case of FO 2 -formulas, one may consider the parsing tree of a TL-formula and define inductively its depth and number of alternations (between past and future operators

of R m,n , R X m,n , R Y m,n , R X m , R Y m and R m .
We also denote by TL X m,n (TL X m , TL m , etc.) the class of TL X m,n (TL X m , TL m , etc.) -definable languages. Proof. Since every ranker can be viewed as a TL-formula, it is easily verified that if u and v satisfy the same TL X m,n -formulas, then they agree on rankers from R X m,n . To prove the converse, it suffices to show that a TL X m,n -formula is equivalent to a Boolean combination of formulas that are expressed by a single ranker. That is: we only need to show that modalities can be brought outside the formula. This follows from the following elementary logical equivalences: [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF]Theorem 4.5] between rankers and formulas in FO 2 m,n , Theorem 1.8 below, is much deeper. If x, y are integers, we let ord(x, y), the order type of x and y, be one of the symbols <, > or =, depending on whether x < y, x > y or x = y. Theorem 1.8 (Weis and Immerman [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF]). Let u, v ∈ A * and let 1 ≤ m ≤ n. Then u and v satisfy the same formulas in FO 2 m,n if and only if (WI 1) u and v agree on rankers from R m,n , (WI 2) if the rankers r ∈ R m,n and r ∈ R m-1,n-1 are defined on u and v, then ord(r(u), r (u)) = ord(r(v), r (v)).

X a (ϕ ∧ ψ) ≡ X a ϕ ∧ X a ψ, X a (ϕ ∨ ψ) ≡ X a ϕ ∨ X a ψ, X a (¬ϕ) ≡ X a ∧ ¬X a ϕ
(WI 3) if r ∈ R m,n and r ∈ R m,n-1 are defined on u and v and end with different direction letters, then ord(r(u), r (u)) = ord(r(v), r (v)).

Corollary 1.9. For each n ≥ m ≥ 1, TL m,n ⊆ FO 2 m,n and TL m ⊆ FO 2 m . Proof. Let L be a TL m,n -definable language. For each u ∈ L, let ϕ u be the conjunction of the FO 2 m,n -sentences satisfied by u and let ϕ be the disjunction of the formulas ϕ u (u ∈ L). Since FO 2 m,n is finite (up to logical equivalence), the conjunctions and disjunctions in the definition of ϕ are all finite. We show that L = L(ϕ).

A word v satisfies ϕ if and only if it satisfies ϕ u for some word u ∈ L. Then v satisfies the same FO 2 m,n -sentences as u and, by comparing the statements in Proposition 1.6 and Theorem 1.8, we see that u and v satisfy the same TL m,n -formulas. Since L is defined by such a formula, it follows that v ∈ L. Conversely, every word v ∈ L satisfies ϕ since it satisfies ϕ v , which is logically equivalent to a term in the disjunction defining ϕ. This concludes the proof.

On varieties and pseudovarieties

Recent results show that the FO 2 m -definability of a language L can be characterized algebraically, that is, in terms depending only on the syntactic monoid of L. This justifies exploring the algebraic path to tackle the decidability of this definability problem. Eilenberg's theory of varieties provides the mathematical framework. In this section, we summarize the information on monoid and variety theory that will be relevant for our purpose. For more detailed information and proofs, we refer the reader to [START_REF] Pin | Varieties of Formal Languages[END_REF][START_REF] Almeida | Finite Semigroups and Universal Algebra[END_REF][START_REF] Tesson | Diamonds are forever: The variety DA[END_REF][START_REF] Tesson | Logic meets algebra: The case of regular languages[END_REF][START_REF] Straubing | Varieties[END_REF], among other sources.

A semigroup is a set equipped with a binary associative operation. A monoid is a semigroup which contains a unit element. The set A * of all words on alphabet A, equipped with the concatenation product, is the free monoid on A: it has the specific property that, if ϕ : A → M is a map into a monoid, then there exists a unique monoid morphism ψ : A * → M which extends ϕ. Apart from free monoids, the semigroups and monoids which we will consider in this paper are finite.

If A is a finite alphabet and M is a finite monoid, we say that a language L ⊆ A * is recognized by M if there exists a morphism ϕ :

A * → M such that L = ϕ -1 (ϕ(L)). Example 2.1. If u ∈ A * and B ⊆ A, let alph(u) = {a ∈ A | u = vaw for some v, w ∈ A * }, [B] = {u ∈ A * | alph(u) = B}
Let ϕ be the following morphism from A * into the direct product of |A| copies of the 2-element monoid {1, 0} (multiplicative): for each letter a ∈ A, ϕ(a) is the A-tuple in which every component is 1, except for the a-component.

It is elementary to show that

[B] = ϕ -1 (ϕ([B]
)) and hence, [B] is accepted by a monoid that is idempotent (every element is equal to its own square) and commutative. Conversely, one can show that every language recognized by an idempotent and commutative monoid is a Boolean combination of languages of the form [B] (B ⊆ A).

A pseudovariety of monoids is a class of finite monoids which is closed under taking direct products, homomorphic images and submonoids. A class of languages V is a collection V = (V(A)) A , indexed by all finite alphabets A, such that V(A) is a set of languages in A * . If V is a pseudovariety of monoids, we let V(A) be the set of all languages of A * which are recognized by a monoid in V. The class V has important closure properties: each V(A) is closed under Boolean operations and under taking residuals (if L ∈ V(A) and u ∈ A * , then Lu -1 and u -1 L are in V(A)); and if ϕ : A * → B * is a morphism and L ∈ V(B), then ϕ -1 (L) ∈ V(A). Classes of recognizable languages with these properties are called varieties of languages, and Eilenberg's theorem (see [START_REF] Pin | Varieties of Formal Languages[END_REF]) states that the correspondence V → V, from pseudovarieties of monoids to varieties of languages, is one-to-one and onto. Moreover, the decidability of membership in the pseudovariety V, implies the decidability of the variety V: indeed, a language is in V if and only if its (effectively computable) syntactic monoid is in V.

For every finite semigroup S, there exists an integer, usually denoted ω, such that every element of the form s ω in S is idempotent. The Green relations are another important concept to describe semigroups and monoids: if S is a semigroup and s, t ∈ S, we say that s ≤ J t (resp. s ≤ R t, s ≤ L t) if s = utv (resp. s = tv, s = ut) for some u, v ∈ S ∪ {1}. We also say that s J t is s ≤ J t and t ≤ J s. The relations R and L are defined similarly.

Pseudovarieties that will be important in this paper are the following.

-J 1 , the pseudovariety of idempotent and commutative monoids; as discussed in Example 2.1, the corresponding variety of languages consists of the Boolean combinations of languages of the form [B].

-R, L and J, the pseudovarieties of R-, Land J -trivial monoids; a monoid is, say, R-trivial if each of its R-classes is a singleton. The variety of languages corresponding to J was described by Simon (see [START_REF] Pin | Varieties of Formal Languages[END_REF]): it is exactly the class of piecewise testable languages, i.e., the class of FO 2 1 -definable languages, see Remarks 1.1 and 1.7.

-A, the variety of aperiodic monoids, i.e., monoids in which x ω = x ω+1 holds for each x. Celebrated theorems of Schützenberger, McNaughton and Papert and Kamp show that the corresponding variety of languages consists of the star-free languages, the languages that are definable in FO, and the languages definable in propositional temporal logic, see for instance [START_REF] Pin | Varieties of Formal Languages[END_REF][START_REF] Tesson | Logic meets algebra: The case of regular languages[END_REF][START_REF] Diekert | First-order definable languages[END_REF][START_REF] Straubing | An introduction to automata theory[END_REF][START_REF] Straubing | Varieties[END_REF].

-DA is the pseudovariety of all monoids in which (xy) ω x(xy) ω = (xy) ω for all x, y. This pseudovariety has many characterizations in combinatorial, algebraic and logical terms. Of particular interest to us is the fact that a 1 a 2 a 3 a 4 a 5 a 6 a 7

Figure 1. The positions defined by r in u, when r = X a 1 X a 2 X a 3 X a 4 Y a 5 Y a 6 X a 7 is condensed on u the corresponding variety of languages consists of the languages that are definable in FO 2 , and equivalently, of the languages that are defined in unary temporal logic, see [START_REF] Tesson | Diamonds are forever: The variety DA[END_REF][START_REF] Tesson | Logic meets algebra: The case of regular languages[END_REF][START_REF] Volker Diekert | A survey on small fragments of first-order logic over finite words[END_REF][START_REF] Kufleitner | Polynomials, fragments of temporal logic and the variety DA over traces[END_REF][START_REF] Trotter | The lattice of pseudovarieties of idempotent semigroups and a non-regular analogue[END_REF] among others.

-Straubing showed that, for each m ≥ 1, FO 2 m is a variety of languages, and he described the corresponding pseudovariety of monoids, which we write FO 2 m , in terms of iterated block products [START_REF] Straubing | Algebraic characterization of the alternation hierarchy in FO 2 [<] on finite words[END_REF]. We will not need to discuss the definition of the block product here, retaining only that this characterization does not imply decidability, and that Straubing gave identities (using products and ω-powers like the identities given above for A and DA) which he conjectures define each FO 2 m . Establishing this conjecture would prove the decidability of FO 2 m -definability. -Kufleitner and Lauser also showed that, for each n ≥ m ≥ 1, FO 2 m,n and FO 2 m form varieties of languages, using a general result on logical fragments [START_REF] Kufleitner | Lattices of logical fragments over words[END_REF]Cor. 3.4]. Their result also does not imply a decidability statement.

-On a given monoid M , we define the congruences ∼ K and ∼ D as follows.

• u ∼ K v if and only if, for each idempotent e in M , we have either eu, ev < J e or eu = ev, • u ∼ D v if and only if, for each idempotent e in M , we have either have ue, ve < J e or ue = ve. If V is a pseudovariety of monoids, we say that the monoid

M ∈ K m V if M/∼ K ∈ V, and that M ∈ D m V if M/∼ D ∈ V. The classes K m V
and D m V are pseudovarieties as well, which are usually defined in terms of Mal'cev products with the pseudovarieties K and D, see [START_REF] Rhodes | The q-theory of finite semigroups[END_REF]Thm 4.6.50] or [START_REF] Krohn | Homomorphisms and semilocal theory[END_REF][START_REF] Hall | On radical congruence systems[END_REF].

The following equalities are well-known [START_REF] Pin | Varieties of Formal Languages[END_REF]:

K m J 1 = K m J = R, D m J 1 = D m J = L.

Condensed rankers

Our main tool to approach the decidability of FO 2 m -definability lies in the notion of condensed rankers, a variant of rankers which was introduced implicitly by Weis and Immerman to prove Theorem 6.4 below (see [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF]Theorem 4.7]). Recall that a ranker can be seen as a sequence of directional instructions (see Example 1.3). We say that a ranker r is condensed on u if it is defined on u, and if the sequence of positions visited zooms in on r(u), never crossing over a position already visited, see Figure 1. Formally,

r = Z 1 • • • Z n is condensed on u if there exists a chain of open intervals (0; |u| + 1) = (i 0 ; j 0 ) ⊃ (i 1 ; j 1 ) ⊃ • • • ⊃ (i n-1 ; j n-1 ) r(u)
such that for all 1 ≤ ≤ n -1 the following properties are satisfied:

• If Z Z +1 = X a X b then (i , j ) = (X a (u, i -1 ), j -1 ). • If Z Z +1 = Y a Y b then (i , j ) = (i -1 , Y a (u, j -1 ). • If Z Z +1 = X a Y b then (i , j ) = (i -1 , X a (u, i -1 )). • If Z Z +1 = Y a X b then (i , j ) = (Y a (u, j -1 ), j -1 ).
Remark 3.1. The i and j are either 0 or 1 + |u|, or positions of the form r (u) for some prefix of r of r. More precisely, if r is the depth prefix of r

( < n), then r (u) = i if Z +1 is of the form X a , and r (u) = j if Z +1 is of the form Y a . Remark 3.2. If r = r 1 r 2 is condensed on u, then r(u) > r 1 (u) if r 2 starts
with an X-letter, and r(u) < r 1 (u) if r 2 starts with a Y-letter.

Example 3.3. The ranker X a Y b X c is defined on the words bac and bca, but it is condensed only on bca.

Rankers in R 1,n and rankers of the form X a Y b 1 • • • Y b k or Y a X b 1 • • • X b k are condensed
on all words on which they are defined.

Condensed rankers form a natural notion, which is equally well-suited to the task of describing FO 2 m -definability (see Theorem 3.11 below). With respect to TL, for which Proposition 1.6 shows a perfect match with the notion of rankers, they can be interpreted as adding a strong notion of unambiguity, see Section 6.3 below and the work of Lodaya, Pandya and Shah [START_REF] Kamal Lodaya | Marking the chops: an unambiguous temporal logic[END_REF].

Let us say that two words u and v agree on condensed rankers from a set R of rankers, if the same rankers in R are condensed on u and v. We write

u m,n v (resp. u m,n v) if u and v agree on condensed rankers in R X m,n (resp. R Y m,n
). If r is a ranker, let L c (r) be the language of all words on which r is condensed. We define R m (resp. L m ) to be the Boolean algebra generated by the languages of the form

L c (r), r ∈ R X m,n (resp. R Y m,n ), n ≥ m. 3.1. Technical properties of condensed rankers. A factorization u = u -au + of a word u ∈ A * is called the a-left factorization of u if a ∈ alph(u -). Symmetrically, u = u -au + is the a-right factorization of u if a ∈ alph(u + ).
Thus, the a-left (resp. a-right) factorization of a identifies the first occurrence of a when reading u from the left (resp. the right).

Lemmas 3.4 and 3.5 admit an elementary verification.

Lemma 3.4. Let s be a ranker, a ∈ A and r = X a s. Let also u ∈ A + and let u = u -au + be its a-left factorization. Then r is condensed on u if and only if

• s is condensed on u + if s starts with an X-block;

• s is condensed on u -if s starts with a Y-block. A dual statement holds if r is of the form r = Y a s, with respect to the a-right factorization of u. Lemma 3.5. Let r be a ranker and a ∈ A. Let also u ∈ A + and let u = u -au + be its a-left factorization.

If r starts with an X-letter, then • r is defined on u -if and only if r is defined on u, r does not contain X a or Y a and, for every prefix p of r ending with an X-letter, pY a is not defined on u. • r is condensed on u - -if and only if r is defined on u -and condensed on u, -if and only if r is condensed on u, r does not contain X a or Y a and, if p is the maximal prefix of r consisting only of X-letters, then pY a is not defined on u,

-if and only if r is condensed on u, r does not contain X a or Y a and, if p = X b 1 • • • X b k (k ≥ 1) is the initial X-block of r, then X a Y b k • • • Y b 1 is defined on u. • r is defined on u + if and only if X a r is defined on u and, for every prefix p of r ending with a Y-letter, X a pY a is defined on u. • r is condensed on u + if and only if X a r is condensed on u. If r starts with a Y-letter, then
• r is defined on u -if and only if X a r is defined on u, r does not contain X a or Y a and, for every prefix p of r ending with an X-letter, X a pY a is not defined on u. • r is condensed on u -if and only if X a r is condensed on u.

• r is defined on u + if and only if r is defined on u and, for every prefix p of r ending with a Y-letter, pY a is defined on u. • r is condensed on u + -if and only if r is defined on u + and condensed on u, -if and only if r is condensed on u and

, if p = Y b 1 • • • Y b k (k ≥ 1)
is the initial Y-block of r, then pY a is defined on u.

We also note the following, very useful characterization of the relations

(2) If m ≥ 2, then u m,n v if and only if alph(u) = alph(v), u m-1,n-1 v and for each letter a ∈ alph(u), the a-left factorizations u = u -au + and v = v -av + satisfy u -m-1,n-1 v -and u + m,n-1 v + (u + m-1,n-1 v + if n = m). (3) If m ≥ 2, then u m,n v if and only if alph(u) = alph(v), u m-1,n-1
v and for each letter a ∈ alph(u), the a-right factorizations u =

u -au + and v = v -av + satisfy u + m-1,n-1 v + and u -m,n-1 v - (u -m-1,n-1 v -if n = m).
Proof. Statement (1) follows directly from Examples 1.4 and 3.3. Let us now assume that m ≥ 2. Suppose that alph(u) = alph(v), u m-1,n-1 v and for each a ∈ alph(u), the a-left factorizations u = u -au

+ and v = v -av + satisfy u -m-1,n-1 v - and u + m,n-1 v + if n > m (u + m-1,n-1 v + if n = m). Let r ∈ R X m,n be condensed on u. If r starts with a Y-letter, then r ∈ R Y m-1,n-1
, and hence r is condensed on v since u m-1,n-1 v. If instead r starts with an X-letter, say r = X a s, we consider the a-left factorizations of u and v. If s starts with a Y-letter,

then s ∈ R Y m-1,n-1 , s is condensed on u -(Lemma 3.4) and hence s is condensed on v -since u -m-1,n-1 v -, from which it follows again that r is condensed on v. Finally, if s starts with an X-letter, then s is condensed on u + by Lemma 3.4. Moreover, s ∈ R X m,n-1 if n > m. If n = m, we have in fact r ∈ R X m-1,n (since r starts with two X-letters) and hence s ∈ R X m-1,n-1 . Since u + m,n-1 v + if n > m and u + m-1,n-1 v + if n = m,
it follows that s is condensed on v + , and hence r is condensed on v.

Conversely, let us assume that u m,n v, that is, u and v agree on con-

densed rankers in R X m,n . Considering rankers in R X 1,1 ⊆ R X m,n shows that alph(u) = alph(v). Similarly, considering rankers in R Y m-1,n-1 ⊆ R X m,n shows that u m-1,n-1 v. Finally, let a ∈ alph(u) and let u = u -au + and v = v -av + be a-left factorizations. Let s ∈ R Y m-1
,n-1 be condensed on u -. Note that s contains neither X a nor Y a , since a ∈ alph(u -). If s starts with a Y-letter, then r = X a s is condensed on u (Lemma 3.4) and since r ∈ R X m,n , r is condensed on v as well, which implies that s is condensed on v -. If instead s starts with an X-letter, then s is condensed on u and hence on v.

Moreover, if p = X b 1 • • • X b k is the maximal prefix of s consisting only of X-letters, then X a Y b k • • • Y b 1 ∈ R X 2,n is condensed on u (Lemma 3.5). Since R X 2,n ⊆ R X m,n , it is condensed on v as well and hence, s is condensed on v -. Finally, assume that s ∈ R X m,n-1 (R X m-1,n-1 if n = m) is condensed on u + . The reasoning is similar: if s starts with an X-letter, then X a s ∈ R X m,n is condensed on u. Therefore X a s is condensed on v and s is condensed on v + . If instead s starts with a Y-letter, then s is condensed on u and s ∈ R Y m-1,n-2 (R X m-2,n-2 if n = m). In particular s ∈ R X m,n and hence, s is condensed on v as well. Moreover, if p is the initial Y-block of s, then pY a is condensed on u. Note that pY a ∈ R Y 1,n-1 ⊆ R X m,n , so pY a is condensed on v and s is condensed on v + . Lemma 3.7. Let n ≥ m ≥ 2, u, v ∈ A * , a ∈ A and let u = u -au + and v = v -av + be a-left factorizations. If u m,n v, then u -m,n-1 v -(u -m-1,n-1 v -if n = m). And if u m,n v, then u + m,n-1 v + (u + m-1,n-1 v + if n = m). Dual statements hold for the factors of the a-right factorizations of u and v if u m,n v or u m,n v.
Proof. We give the proof if n > m; it is easily adapted to the case where n = m.

Assume that u m,n v and r ∈ R X m,n-1 is condensed on u -. By Lemma 3.5, we have:

-If r starts with an X-letter, then r is condensed on u, r does not contain occurrences of X a or Y a , and

if p = X b 1 • • • X b k is the initial X-block of r, then q = X a Y b k • • • Y b 1 is condensed on u. Since q ∈ R X
2,k+1 and k < n, we have q ∈ R X m,n and hence r and q are condensed on v. Therefore r is condensed on v -.

-If r starts with a Y-letter, then

X a r is condensed on u. But r ∈ R Y m-1,n-2 , so X a r ∈ R X m,n and hence X a r is condensed on v. It follows that r is con- densed on v -. Assume now that u m,n v and r ∈ R Y m,n-1 is condensed on u + . Then -If r starts with an X-letter (which is possible only if m ≥ 2), then r ∈ R X m-1,n-2 and X a r is condensed on u. But X a r ∈ R X m-1,n-1 ⊆ R Y m,n , so X a r is condensed on v and r is condensed on v + .
-If instead r starts with a Y-letter, then r is condensed on u and if p is the initial Y-block of r, then pY a is condensed on u. But r, pY a ∈ R Y m,n , so r and pY a are condensed on v, and r is condensed on v + .

3.2.

Condensed rankers, rankers and FO 2 . We now show that, in the characterization of FO 2 m,n in Theorem 1.8, condensed rankers can be used just as well. This is done in Theorem 3.11. The first step is to relate agreement on rankers and agreement on condensed rankers. We start with a technical lemma.

Lemma 3.8. If a ranker r ∈ R Z m,n (Z ∈ {X, Y}
) is defined but not condensed on u, and if s is the maximal prefix of r which is condensed on u, then one of the following holds, for some ≥ 1:

• r = sX b t, s = s 0 Y a X b 1 • • • X b -1 and s 0 Y a (u) ≤ s(u) < s 0 (u) ≤ sX b (u); • r = sY b t, s = s 0 X a Y b 1 • • • Y b -1 and s 0 X a (u) ≥ s(u) > s 0 (u) > sY b (u) = s 0 Y b (u). Moreover s 0 is not empty, s 0 ∈ R Z m-1,n-; sX b (u) = s 0 (u) (resp. sY b (u) = s 0 (u)) if the last letter of s 0 is in {X b , Y b }; and sX b (u) = s 0 X b (u) (resp. sY b (u) = s 0 Y b (u)) otherwise.
Proof. Rankers in R 1,n are condensed on each word on which they are defined (Example 3.3). Therefore we have m ≥ 2. By hypothesis, s = r. We consider the case where the first letter after s is an X-letter, the other case is dual. Then r is of the form r = sX b t, where t may be empty. In view of Example 3.3,

s = s 0 Y a X b 1 • • • X b -1
for some non-empty s 0 and ≥ 1. Since s is condensed on u but sX b is not, we have the following (see Remark 3.2): Proof. The result is trivial if m = 1, since rankers in R 1,n are condensed on each word on which they are defined (Example 3.3). We now assume that m ≥ 2.

s 0 Y a (u) < s 0 Y a X b 1 (u) • • • < s 0 Y a X b 1 • • • X b -1 (u) = s(u) < s 0 (u),
Let p and q be positions in u and v and let r ∈ R Z m,n such that r(u) = p and r(v) = q. If r is not condensed on u, then r is not condensed on v (since the two words agree on condensed rankers). With the notation of Lemma 3.8, r coincides on both u and v with r = s 0 t, s 0 X b t or s 0 Y b t (depending on the last letter of s 0 and on the letter following s in r), which starts with the same letter as r. If r is not condensed on u and v, we repeat the reasoning. This process must terminate since each iteration reduces the depth of r . Proof. If u and v do not agree on rankers from R Z m,n , let r ∈ R Z m,n be a minimum depth ranker on which u and v disagree. Without loss of generality, we may assume that u ∈ L(r) and v ∈ L(r). In particular, r is not condensed on u.

Let s, s 0 and t be as in Lemma 3.8. Without loss of generality again, we may assume that the letter following s in r is X b . Since s is condensed on u and sX b is not, the ranker s is condensed on v and sX b is not. Moreover, sX b coincides on u with s = s 0 , or s 0 X b , depending on the last letter of s 0 . Observe that s is shorter than r, so s is defined on v. In particular, there exists a b-position in v to the right of s, which is not to the left of s 0 (since sX b is not condensed on v). It follows that sX b (v) = s (v). Let now r = s t: then r is shorter than r, it coincides with r on u, and it is not defined on v since s coincides with s on that word. This contradicts the minimality of r.

We can now prove the following variant of Theorem 1.8. Proof. We need to prove that together, Properties (WI 1), (WI 2) and (WI 3) are equivalent to Properties (WI 1c), (WI 2c) and (WI 3c).

Let us first assume that (WI 1), (WI 2) and (WI 3) hold. It is immediate that (WI 2c) and (WI 3c) hold. If (WI 1c) does not hold, let r be a ranker in R m,n which is condensed on v and not on u. Since (WI 1) holds, r is defined on u. Let s 0 , s and t be as in Lemma 3.8 and let us assume, without loss of generality, that the letter following s in r is X b . Then s 0 and sX b are defined on both u and v, with s 0 ∈ R m-1,n-1 and sX b ∈ R m,n . Since r is condensed on v, we have sX b (v) < s 0 (v), and since sX b is not condensed on u, we have s 0 (v) ≤ sX b (v), contradicting Property (WI 2). Thus (WI 1c) holds.

Conversely, let us assume that (WI 1c), (WI 2c) and (WI 3c) hold. Then (WI 1) holds by Proposition 3.10. Let us verify Property (WI 2): suppose that r ∈ R m,n and r ∈ R m-1,n-1 are defined on u and v. In view of (WI 1c), Proposition 3.9 shows that there exist rankers s ∈ R m,n and s ∈ R m-1,n-1 which are condensed on u and v, and which coincide with r and r , respectively, on both words. By (WI 2c), we have ord(s(u), s (u)) = ord(s(v), s (v)), and hence ord(r(u), r (u)) = ord(r(v), r (v)). Thus Property (WI 2) holds. The verification of (WI 3) is identical.

These results imply the following statement, which refines Corollary 1.9 and can be proved like that Corollary, using Propositions 1.6 and 3.10, and Theorem 3.11. Proof. The relations m,n and m,n are clearly equivalence relations, of finite index since R m,n is finite. We now verify that if b ∈ A and if u and v are m,n -equivalent, then so are ub and vb (resp. bu and bv).

The proof is by induction on m + n. The property of having the same subwords of length n is easily seen to be a congruence (and the proof of this fact can be found in [START_REF] Pin | Varieties of Formal Languages[END_REF] as it is related to Simon's theorem on piecewise testable languages). In view of Proposition 3.6 [START_REF] Adler | An n! lower bound on formula size[END_REF], this shows that 1,n and

-m-1,n-1 v -and u + m,n-1 v + (u + m-1,n-1 v + if n = m). By induction, we have u m,n-1 v, bu -m-1,n-1 bv -and u + b m,n-1 v + b (u + b m-1,n-1 v + b if n = m).
If a ∈ alph(u), and hence a = b, the a-left factorizations of ub and vb (resp. bu and bv) are u b ε and v b ε (resp. ε b u and ε b v), and we do have

u m-1,n-1 v and u m,n-1 v (u m-1,n-1 v if m = n).
Thus all the conditions in Proposition 3.6 (2) are satisfied, whether a occurs in u and v or not, and we have established that ub m,n vb and bu m,n bv. The proof regarding m,n is symmetric. Proof. We carry out the proof for the congruence m,n by induction on m + n. The proof for m,n is symmetrical.

For m = 1, we show that if a ranker r ∈ R X 1,n is condensed on ϕ(u), then it is condensed on ϕ(v). If u = a 1 • • • a , the word ϕ(u) has a natural factorization in blocks, namely the ϕ(a i ) and the sequence of positions in ϕ(u) defined by the prefixes of r visits (some of) the ϕ(a i )-blocks. This yields a factorization of r, r = r 1 r 2 • • • r k , where all the positions in ϕ(u) visited while running r 1 are in the same block, say, ϕ(a j [START_REF] Adler | An n! lower bound on formula size[END_REF] ); then all the positions visited by the prefixes of r between r 1 (excluded) and r 1 r 2 (included) are in the block ϕ(a j(2) ) with j(2) > j [START_REF] Adler | An n! lower bound on formula size[END_REF]; and so on. In particular, the ranker X a j(1) • • • X a j(k) is defined on u, and hence on v. Therefore

v = v 0 a j(1) v 1 • • • a j(k) v k+1
. By construction, each r i is defined on ϕ(a j(i) ), so r is defined on ϕ(v), and condensed on that word (Example 3.3).

We now let n ≥ m ≥ 2 and u m,n v. It is immediate that alph(ϕ(u)) = alph(ϕ(v)) since u and v have the same alphabet. By Proposition 3.6 (2), we have u m-1,n-1 v, and by induction it follows that ϕ(u) m-1,n-1 ϕ(v). Let now b ∈ alph(ϕ(u)) and let ϕ(u) = x -bx + and ϕ(v) = y -by + be b-left factorizations. The occurrence of b thus singled out in ϕ(u) sits in some ϕ(a), a ∈ A, and the corresponding occurrence of a in u is the leftmost one: we have an a-left factorization u = u -au + and a b-left factorization ϕ(a) = x bx such that x -= ϕ(u -)x and x + = x ϕ(u + ). Similarly, the leftmost occurrence of b in ϕ(v) sits in some ϕ(a ), a ∈ A: a is the leftmost letter in v such that b occurs in ϕ(a ). If a = a, the consideration of the rankers X a Y a and X a Y a , which are simultaneously defined or not defined on u and v, yields a contradiction. Therefore a = a and if v = v -av + is the a-left factorization, then y -= ϕ(v -)x and y + = x ϕ(v + ). By Proposition 3.6 (2) again, we

B * B * / m,n A * 1 / m,n × • • • × A * k / m,n A * / m,n N A * M π B π ϕ ψ ı π A β δ γ Figure 2. A commutative diagram have u -m-1,n-1 v -and u + m,n-1 v + (u + m-1,n-1 v + if n = m)
. By induction, it follows that the same relations hold between the ϕ-images of u -, v -, u + and v + , and we have x -m-1,n-1 y -and x + m,n-1 y + (x + m-1,n-1 y + if n = m) by Lemma 3.13. Therefore ϕ(u) m,n ϕ(v) by Proposition 3.6 (2).

For each n ≥ m ≥ 1, let R m,n (resp. L m,n ) be the pseudovariety of monoids generated respectively by the monoids of the form A * / m,n (resp. A * / m,n ). Since m,n refines m,n when n ≥ n, the sequence (R m,n ) n is increasing and we let R m be its union (a pseudovariety as well). The pseudovariety L m is defined similarly, as the union of the L m,n . Proof. By definition, there exists an onto morphism δ : N → M , and an injective morphism ı :

N → A * 1 / m,n × • • • × A * k / m,n .
Let B be the disjoint union of the A i , and for each i, let π i be the morphism from B * to A * i which erases all the letters not in A i . By Lemma 3.14, m,n -equivalent elements have m,n -equivalent images, so we have a morphism π : B * / m,n → i A * i / m,n as in Figure 2. For each letter a ∈ A, we then pick a word ϕ(a

) in π -1 B π -1 δ -1 γ(a) ⊆ B * : this defines a morphism ϕ : A * → B * such that δ • π • π B • ϕ = γ. By Lemma 3.14 again, there exists a morphism ψ : A * / m,n → B * / m,n such that ψ • π A = π B • ϕ. It follows that if u m,n v, then π B ϕ(u) = π B ϕ(v),
and hence γ(u) = γ(v). This concludes the proof.

Proof. Every

L c (r) (r ∈ R X m,n
) is a union of m,n -classes, and hence it is recognized by A * / m,n . Therefore every language in R m is recognized by a monoid in R m (and indeed, by π A : A * → A * / m,n for n large enough).

Conversely, suppose that L ⊆ A * is recognized by a morphism γ : A * → M , into a monoid M ∈ R m . Then M ∈ R m,n for some n ≥ m and by Corollary 3.15, there exists a morphism β : A * / m,n → M such that γ = β • π A . It follows that L is also accepted by π A , L is a union of m,n -classes, and hence L ∈ R m .

Example 3.17. It follows from Proposition 3.6 (i) that R 1 = L 1 is the variety of piecewise testable languages, and R 1 = L 1 = J, the pseudovariety of J -trivial monoids.

Remark 3.18. The proof of Corollary 3.16 also establishes that for each n ≥ m ≥ 1, the Boolean algebra R m,n generated by the languages of the form L c (r), r ∈ R X m,n , defines a variety of languages, for which the corresponding pseudovariety of monoids is R m,n . In variety-theoretic terms, Corollary 3.15 states that A * / m,n is the free object of R m,n over the alphabet A. The symmetrical statement also holds for L m,n and the monoids A * / m,n .

We note the following containments. Proof. Since FO 2 is the variety of languages corresponding to DA, Corollary 3.12 yields the containment of R m and L m in DA. Similarly, R m and L m are contained in both R m+1 and L m+1 by definition of these classes of languages -and this in turn implies the containment of the corresponding pseudovarieties.

Condensed rankers and deterministic products. Recall that a product of languages

L = L 0 a 1 L 1 • • • a k L k (k ≥ 1, a i ∈ A, L i ⊆ A * ) is deterministic if, for 1 ≤ i ≤ k, each word u ∈ L has a unique prefix in L 0 a 1 L 1 • • • L i-1 a i . If for each i, the letter a i does not occur in L i-1 , the product L 0 a 1 L 1 • • • a k L k is called
visibly deterministic: this is obviously a particular case of a deterministic product.

The definition of a co-deterministic or visibly co-deterministic product is dual, in terms of suffixes instead of prefixes. If V is a class of languages and A is a finite alphabet, let V det (A) (resp. V vdet (A), V codet (A), V vcodet (A)) be the set of all Boolean combinations of languages of V(A) and of deterministic (resp. visibly deterministic, co-deterministic, visibly co-deterministic) products of languages of V(A).

Pin gave algebraic characterizations of the operations V -→ V det and V -→ V codet , see [START_REF] Pin | Propriétés syntactiques du produit non ambigu[END_REF][START_REF] Pin | Locally trivial categories and unambiguous concatenation[END_REF]. Proposition 3.20. If V is a variety of languages and if V is the corresponding pseudovariety of monoids, then V det and V codet are varieties of languages and the corresponding pseudovarieties are, respectively, K m V and D m V. This leads to the following statement.

A * A * / m,n M M/∼ K α β γ π Figure 3. M ∈ K m L m Theorem 3.21. For each m ≥ 1, we have R m+1 = L vdet m = L det m , L m+1 = R vcodet m = R codet m , R m+1 = K m L m and L m+1 = D m R m . In particular, R 2 = R and L 2 = L.
The proof uses the following technical property of monoids in DA, whose proof can be found for instance in [6, Lemma 4.2]. + be the a-left factorization of u. Let [B] be the language of all strings with alphabet B,

[B] = {u ∈ A * | alph(u) = B}. Observe that [B] = a∈B L c (X a ) \ a ∈B L c (X a ) = a∈B L c (Y a ) \ a ∈B L c (Y a ).
+ if n > m + 1, the m,n-1 -class of u (a) + if n = m + 1.
By definition of an a-left factorization, each of these products is visibly deterministic and, since every m,n-1 -class is a language in L m , we have shown that the m+1,n -class of u is in L vdet m . Thus R m+1 ⊆ L vdet m . To establish the last inclusion, namely L det m ⊆ R m+1 , we rather show

K m L m ⊆ R m+1 .
Let γ : A * → M be a surjective morphism, onto a monoid M ∈ K m L m : we want to show that there exists a morphism from A * / m+1,n onto M for some n > m. Since M ∈ K m L m , the monoid M/∼ K ∈ L m and by Corollary 3.15, there exists an integer n and a morphism β :

A * / m,n → M/∼ K such that β • α = π • γ,
where α is the projection from A * onto A * / m,n and π is the projection from M onto M/∼ K , see Figure 3.

Let be the maximal length of a strict R-chain in M , that is: if

x k < R . . . < R x 1 in M , then k ≤ . We show that, for any u, v ∈ A * , u m+1, |A|+n+1 v =⇒ γ(u) = γ(v). ( 1
)
If n = |A| + n + 1, this implies the existence of a morphism from A * / m+1,n onto M , as announced.

To prove implication (1), it suffices to show that we have

u m+1, |alph(u)|+n+1 v =⇒ γ(u) = γ(v), (2)
which we prove by induction on |alph(u)|. If |alph(u)| = 0, then u = ε, alph(v) = ∅ and v = ε as well, so that γ(u) = γ(v). Now suppose that u = ε and assume that u m+1,

|alph(u)|+n+1 v. Let u = u 1 a 1 • • • a k u k+1 be the factorization of u such that each u i is a word, each a i is a letter and 1 R γ(u 1 ) > R γ(u 1 a 1 ) • • • > R γ(u 1 a 1 • • • u k a k ) R γ(u 1 a 1 • • • a k u k+1 ).
Then k + 1 ≤ , so k < . Moreover, by Fact 3.22 (and Corollary 3.19), for each 1

≤ i ≤ k, a i ∈ u i , so that each product u i a i (u i+1 • • • a k u k+1 ) is an a i -left factorization (1 ≤ i ≤ k).
An easy induction on k, using Lemma 3.7, shows that v can then be factored as

v = v 1 a 1 v 2 • • • a k v k+1 , where u i m+1, |alph(u)|+n-i+1 v i for each 1 ≤ i ≤ k + 1. Moreover, for 1 ≤ i ≤ k, |alph(u i )| < |alph(u)|. Since i ≤ k < , we have |alph(u)|+n-i ≥ |alph(u i )| + n + 1,
and by induction, we have γ(u i ) = γ(v i ). However, it is possible that alph(u k+1 ) = alph(u), so we cannot conclude that γ(u k+1 ) = γ(v k+1 ).

But we do have the following:

u k+1 m+1, |alph(u)|+n-k v k+1 and γ(u ) = γ(v ), where u = u 1 a 1 • • • u k a k and v = v 1 a 1 • • • v k a k . The first relation implies that u k+1 m, |alph(u)|+n-k-1 v k+1 . Since k < , we have |alph(u)| + n - k -1 ≥ n, so u k+1 m,n v k+1 and hence, πγ(u k+1 ) = πγ(v k+1 ), that is, γ(u k+1 ) ∼ K γ(v k+1 ).
Moreover, there exists a string x ∈ A * such that γ(u ) = γ(u u k+1 x). Let ω be an integer such that every ω-power is idempotent in M : then

γ(u ) = γ(u )γ(u k+1 x) ω . Now observe that γ(u k+1 x) ω J γ(u k+1 x) ω γ(u k+1 ), since γ(u k+1 x) ω is equal to γ(u k+1 x) 2ω . It follows from the equivalence γ(u k+1 ) ∼ K γ(v k+1 ) that γ(u k+1 x) ω γ(u k+1 ) = γ(u k+1 x) ω γ(v k+1 ). Therefore we have γ(u )γ(u k+1 ) = γ(u )γ(v k+1 ) and hence γ(u) = γ(u )γ(u k+1 ) = γ(u )γ(v k+1 ) = γ(v )γ(v k+1 ) = γ(v).
This concludes the proof of Formula (2), and therefore of Theorem 3.21.

3.5.

Structure of the R m and L m hierarchies. It turns out that the hierarchies of pseudovarieties given by the R m and the L m were studied in the semigroup-theoretic literature (Trotter and Weil [35], Kufleitner and Weil [START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF]). In [START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF], they are defined as the hierarchies of pseudovarieties obtained from J by alternated applications of the operations X → K m X and X → D m X. Theorem 3.21 shows that these are the same hierarchies as those considered in this paper 1 The results in [START_REF] Trotter | The lattice of pseudovarieties of idempotent semigroups and a non-regular analogue[END_REF][START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF] go actually further, and give defining pseudoidentities for the pseudovarieties R m and L m . Remark 3.24. The way up in the R m -L m hierarchy, by means of Mal'cev products with K and D, is strongly reminiscent of the structure of the lattice of band varieties [START_REF] Gerhard | The lattice of equational classes of idempotent semigroups[END_REF]. This observation is no coincidence, and forms the basis of the results in [START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF] which are used here.

The R m hierarchy and unary temporal logic

We have seen in Corollary 3.12 that TL X m ⊆ R m and TL Y m ⊆ L m . In Theorem 4.3 below, we prove a weak converse. Let us however make the following observation. Proposition 4.1. We have

TL X 1 = TL Y 1 = R 1 = L 1 , TL X 2 = R 2 , TL Y 2 = L 2 .
Proof. The statement concerning TL 1 was already proved in Remark 1.7. Let us now establish that R 2 ⊆ TL X 2 . We show, by induction on n ≥ 2, that if u and v agree on rankers in R X 2,2n , then they agree on condensed rankers in R X 2,n : u 2,n v. We use the characterization of 2,n in Proposition 3.6. The consideration of 1-letter rankers shows that alph(u

) = alph(v). More- over, since R Y 1,n-1 is contained in R X 2,2n
, and since these rankers are condensed where they are defined, we find that u 1,n-1 v. Similarly, let u = u -au + and v = v -av + be a-left factorizations, and let s ∈ R Y 1,n-1 . Then s is condensed on u -if and only if s is defined on u -, if and only if X a s is defined on u (Lemma 3.5). Since X a s ∈ R X 2,2n and u and v agree on such rankers, it follows that X a s is defined on v, and s is condensed on v -. Thus u -1,n-1 v -.

1 More precisely, the pseudovarieties Rm and Lm in [START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF] are pseudovarieties of semigroups, and the Rm and Lm considered in this paper are the classes of monoids in these pseudovarieties.

Now we need to show that u

+ 2,n-1 v + if n ≥ 3, u + 1,1 v + if n = 2.
Suppose first that n = 2 and consider s ∈ R X 1,1 , condensed on u + . Then s = X b for some b ∈ A and the consideration of r = X a X b (in R X 2,2 ) shows that s is condensed on v + as well. This settles the case n = 2.

Let us now assume that n ≥ 3 and let us show that u + 2,n-1 v + . By induction, it suffices to show that u + and v + agree on rankers in R X 2,2n-2 . So let s ∈ R X 2,2n-2 be defined on u + . Then for every prefix p of s ending with a Y-letter, X a pY a is defined on u (Lemma 3.5). Since X a pY a ∈ R X 2,2n , it follows that X a pY a is defined on v, and hence s is defined on v + . This concludes the proof. Example 4.2 below shows that the statement of Proposition 4.1 cannot be extended to the higher of the hierarchy.

Example 4.2. We show in this example that

TL X 3 is properly contained in R 3 . More precisely, let r 0 = X a Y b X c ∈ R X 3,3 . We show that L c (r 0 ), a language in R 3 , is not TL X 3 -definable. Let u n = (bc) n (a(bc) n ) n and v n = (bc) n b(a(bc) n ) n (n ≥ 1)
. It is easily verified that r 0 is condensed on u n , and that it is defined and not condensed on v n : that is, for each n, u n ∈ L c (r 0 ) and v n ∈ L c (r 0 ).

We now show that u n and v n agree on all rankers in R X 3,n , so that any TL X 3 -definable language contains either both u n and v n , or neither -and hence L c (r 0 ) is not TL X 3 -definable. Let r ∈ R X 3,n . If r starts with a Y-letter, then any two words ending with (a(bc) n ) n agree on r. In particular, u n and v n agree on r. Similarly, if r starts with an X-letter and does not contain the letters X a or Y a , then any two words starting with (bc) n agree on r, so u n and v n agree on r.

Finally, assume that r starts with an X-letter and that r = s 0 Z

(1)

a s 1 • • • Z (k)
a s k with k > 0, each Z (i) ∈ {X, Y} and each s i a (possibly empty) ranker avoiding the letters X a and Y a . We denote by p i the prefix

p i = s 0 Z (1) a s 1 • • • Z (i) a .
Suppose first that r ∈ R X 1,n . Then p i coincides with X i a on u n as well as on v n . Therefore r is defined and coincides with X k a s k on both words. Suppose now that r ∈ R X 2,n , say r = r r with r a non-empty string of X-letters and r a non-empty string of Y-letters. If r is shorter than p 1 , then Z (1) = Y and r is not defined on either u n or v n . If Z (1) = X, let i be maximal such that p i is a prefix of r , say r = p i s i . Then i > 0 and p i coincides with X i a on u n , as well as on v n . If i = k, then r is defined on u n and v n , and it coincides with X k a s k on both words.

If 1 ≤ i < k, s i is non-empty and s i is defined on (bc) n , then p i+1 coincides with X i a on u n and v n . Thus r is defined on u n (resp. v n ) if and only i ≥ k-i, and in that case, it coincides with X k-2i a s k .

If 1 < i < k, s i is non-empty and s i is not defined on (bc) n , or if s i is empty, then p i+1 coincides with X i-1 a on u n and v n . Thus r is defined on u n (resp. v n ) if and only i > ki, and in that case, it coincides with X k-2i-1 a s k . Finally, if 1 = i < k, s i is non-empty and s i is not defined on (bc) n , or if s i is empty, then r (and even p i+1 ) is not defined on either u n or v n .

Finally, let us assume that r ∈ R X 3,n , say r = r r r with r and r nonempty strings of X-letters and r a non-empty string of Y-letters. Again, let i be maximal such that p i is a prefix of r (i = 0 if p 1 is not a prefix of r ) and let j be maximal such that p j is a prefix of r r . Then r r = p j s j for some prefix s j of s j . By the previous analysis, if i ≤ 1 < j, then r r is not defined on u n nor on v n , and hence neither is r. In all other cases, r r is defined on both words and coincides with X 2i-j a s j or X 2i-j-1 a s j . Since (kj) + (2ij) ≤ k, r is defined on u n and v n , and coincides on these words with X k-j+2i-j a s k or X k-j+2i-j-1 a s k . To conclude this example, note that u n and v n disagree on rankers in R X 4 . More precisely, the ranker X a Y c X b Y a is defined on u n but not on v n . Further getting ahead of ourselves, we note that this example also shows (in view of Theorem 5.1) that TL 3 is properly contained in FO 2 3 .

Finally we prove a result on the containment of the R m and L m hierarchies in the TL m hierarchy.

Theorem 4.3. Let m ≥ 1. Then R m ⊆ TL X 2m-1 and L m ⊆ TL Y 2m-1 .
More precisely, for all n ≥ m, Z ∈ {X, Y} and u, v ∈ A * , if u and v agree on rankers in R Z 2m-1,2n-1 , then they agree on condensed rankers in R Z m,n .

Proof. Without loss of generality, we may assume Z = X. The proof is by induction on m. The result is trivial if m = 1, since 2m -1 = 1 and 2n -1 ≥ n. We now assume that m ≥ 2 and u, v agree on rankers in

R X 2m-1,2n-1 .
We use the characterization of m,n in Proposition 3.6: the consideration of length 1 rankers shows that alph(u

) = alph(v). Since R Y 2m-3,2n-3 is con- tained in R X 2m-1,2n-1 , we have u m-1,n-1 v by induction. Now, for each letter a ∈ alph(u), let u = u -au + and v = v -av + be the a-left factorizations. We want to show that u -m-1,n-1 v -and u + m,n-1 v + (u + m-1,n-1 v + if m = n).
By induction, it suffices to show that u -and v -agree on rankers in R Y 2m-3,2n-3 , and u + and v + agree on rankers in

R X 2m-1,2n-3 (R X 2m-3,2n-3 if m = n).
In the rest of the proof we silently rely on the results of Lemma 3.5.

Let s ∈ R Y 2m-3,2n-3 be defined on u -. If s starts with a Y-block, then X a s ∈ R X 2m-2,2n-2 and X a s is defined on u. Moreover, if p is any prefix of s, then X a pY a ∈ R X 2m-1,2n-1 is not defined on u. It follows that s is defined on v -.

If instead s starts with an X-block, then s ∈ R X 2m-4,2n-4 and s is defined on u. If p is any prefix of s, then pY a ∈ R X 2m-3,2n-3 and pY a is not defined on u. As all these rankers are in R X 2m-1,2n-1 , the same holds on v and s is defined on

v -. Let now s ∈ R X 2m-1,2n-3 (s ∈ R X 2m-3,2n-3 if n = m) be defined on u + . If s starts with an X-block, then X a s ∈ R X 2m-1,2n-2 (X a s ∈ R X 2m-3,2n-2 if n = m) and X a s is defined on u. Moreover, for each prefix p of s ending with a Y-letter, X a pY a ∈ R X 2m-1,2n-1 (X a pY a ∈ R X 2m-3,2n-1 if n = m
) and X a pY a is defined on u. As all these rankers are in R X 2m-1,2n-1 , the same holds on v and s is defined on v + .

If instead s starts with a Y-block,

then s ∈ R Y 2m-2,2n-4 (s ∈ R Y 2m-4,2n-4 if n = m) and s is defined on u. Moreover, if p is any prefix of s ending with a Y-letter, pY a ∈ R Y 2m-2,2n-3 (pY a ∈ R Y 2m-4,2n-3 if n = m)
and pY a is defined on u. As all these rankers are in R X 2m-1,2n-1 , the same holds on v and s is defined on v + .

The containment of R m and L m into TL X 2m-1 and TL Y 2m-1 , respectively, is not very precise, unfortunately, especially in view of Theorem 6.4 below.

The R m hierarchy and FO 2 m

The objective of this section is to prove the following theorem.

Theorem 5.1. Let m ≥ 1. Every language in R m or L m is FO 2 m -definable, and every FO 2 m -definable language is in R m+1 ∩L m+1 . Equivalently, we have R m ∨ L m ⊆ FO 2 m ⊆ R m+1 ∩ L m+1
, where V ∨ W denotes the least pseudovariety containing V and W.

5.1.

Are the containments in Theorem 5.1 strict? In the particular case where m = 1, we know that R 2 ∩L 2 = R∩L = J = R 1 ∨L 1 : this reflects the fact that FO 2 1 is the class the piecewise testable languages. However, we conjecture that this equality does not hold for larger values of m.

Conjecture 5.2. For m ≥ 2, R m ∨ L m is properly contained in R m+1 ∩ L m+1 .
The following example proves the conjecture for m = 2.

Example 5.3. L = {b, c} * ca{a, b} * is FO 2
2 -definable, by the following formula:

∃i (c(i) ∧ (∀j (j < i → ¬a(j))) ∧ (∀j (j > i → ¬c(j)))) ∧ ∃i (a(i) ∧ (∀j (j < i → ¬a(j))) ∧ (∀j (j > i → ¬c(j)))) ∧ ∀i (b(i) → (∃j (j < i ∧ a(j)) ∨ (∃j (j > i ∧ c(j)))).
The words u n = (bc) n (ab) n are in L, while the words v n = (bc) n b(ca) n are not. Almeida and Azevedo showed that R 2 ∨ L 2 is defined by the pseudoidentity (bc) ω (ab) ω = (bc) ω b(ab) ω [2, Theorem 9.2.13 and Exercise 9.2.15]).

In particular, for each language K recognized by a monoid in R 2 ∨ L 2 , the words u n and v n (for n large enough) are all in K, or all in the complement of K. Therefore L is not recognized by such a monoid, which proves that R 2 ∨ L 2 is strictly contained in FO 2 2 , and hence also in R 3 ∩ L 3 . It also shows that TL 2 is properly contained in FO 22 .

Finally, we formulate the following conjecture.

Conjecture 5.4. For each m ≥ 1, FO 2 m = R m+1 ∩ L m+1 . 5.2. Proof of Theorem 5.1. Corollary 3.12 already established that every language in R m or L m is FO 2 m -definable 2 . In view of Theorem 3.11, to establish that FO 2 m is contained in R m+1 ∩ L m+1 , it suffices to prove the following result.

For each n ≥ m ≥ 1, if u m+1,2n v or u m+1,2n v, then Properties (WI 1c), (WI 2c) and (WI 3c) hold for m, n. The result is trivial if m = 1, since in that case, only Property (WI 1c) is non-vacuous.

So we now assume that m ≥ 2, and u m+1,2n v or u m+1,2n v. Property (WI 1c) holds trivially, by definition of the m+1,2n and m+1,2n relations. We now concentrate on proving that Properties (WI 2c) and (WI 3c) also hold for m, n, a task that will be completed in Section 5.2.3.

5.2.1.

The case where r and r start with opposite directions.

Proposition 5.5. Let n ≥ m ≥ 1, r = Y a 1 s ∈ R Y m,n and r = X c . If u, v ∈ A * ,
r is condensed on u and v and u m,n+1 v or u m+1,n+1 v, then ord(r(u), r (u)) = ord(r(v), r (v)). The dual statement (involving r = X a 1 s ∈ R X m,n and r = Y c ) holds as well. Proof. First suppose that u m+1,n+1 v, that is, u and v agree on condensed rankers in R Y m+1,n+1 . We are in exactly one of the following three situations: -rY c is defined on u, in which case r (u) < r(u); -rY c is undefined on u and c is the last letter to occur in r, in which case r (u) = r(u);

-rY c is undefined on u and c is not the last letter to occur in r, in which case r(u) < r (u).

The same trichotomy holds for v. Since rY c ∈ R Y m+1,n+1 , u and v agree on rY c (Proposition 3.10), and hence ord(r(u), r (u)) = ord(r(v), r (v)).

Let us now assume that u m,n+1 v, so that u and v agree on condensed rankers in

R X m,n+1 . If m = 1 then r is of the form r = Y a 1 • • • Y a k and we observe again that -either X c X a k • • • X a 1 ∈ R X 1,n+1
is defined on u, and we have r (u) < r(u); -or X c X a k • • • X a 1 is undefined on u and c = a k , and we have r (u) = r(u); -or X c X a k • • • X a 1 is undefined on u and c = a k , and we have r (u) > r(u).

The same holds for

v since X c X a k • • • X a 1 ∈ R X
1,n+1 and such rankers are condensed where they are defined. Therefore we have ord(r(u), r (u)) = ord(r(v), r (v)).

We now assume that m ≥ 2. Let u = u -cu + and v = v -cv + be c-left factorizations. We distinguish two cases depending on the direction of the second letter of r.

First suppose that r = Y a 1 Y a 2 s . If a 1 ∈ alph(u + ), then r(u) < r (u) (because r is condensed on u). Since u + m,n v + , we have alph(u

+ ) = alph(v + ), so r(v) < r (v) as well. If instead a 1 ∈ alph(u + ) = alph(v + ), let u + = u 0 a 1 u 1 and v + = v 0 a 1 v 1 be the a 1 -right factorizations. Then ord(r(u), r (u)) = ord(Y a 2 s (u -cu 0 ), r (u -cu 0 )) and ord(r(v), r (v)) = ord(Y a 2 s (v -cv 0 ), r (v -cv 0 )).
Since (u -cu 0 )a 1 u 1 and (v -cv 0 )a 1 u 1 are a 1 -right factorizations as well, we deduce from Lemma 3.7 that u -cu 0 m,n v -cv 0 and it follows by induction on the length of r that ord(Y a 2 s (u

-cu 0 ), r (u -cu 0 )) = ord(Y a 2 s (v -cv 0 ), r (v -cv 0 )). The other case is r = Y a 1 X b 1 s . If a 1 ∈ alph(cu + ) = alph(cv + ) then r (u) < r(u) and r (v) < r(v). If instead a 1 ∈ alph(cu + ) = alph(cv + )
, we first consider the case where r has a single alternation, i.e., r

= Y a 1 X b 1 • • • X b k .
We have r(u) < r (u) if and only if r is defined on u -, and hence condensed (Example 3.3). Since u -m,n v -(Lemma 3.7), this is the case if and only if r is defined on v -. Hence, if r is defined on u -, we have r(u) < r (u) and r(v) < r (v). If r is not defined on u -, but Y a 1 X b 1 • • • X b k-1 is defined on u -and b k = c, then the same holds for v and we have r(u) = r (u) and r(v) = r (v). Otherwise, we have r(u) > r (u) and r(v) > r (v).

The last situation arises if r is of the form r

= Y a 1 X b 1 • • • X b k Y d s . In particular, m ≥ 3. If Y a 1 X b 1 • • • X b k is defined on u -c,
then it is defined on v -c as well (by the same reasoning as in the previous paragraph) and we have r(u) < r (u) and r(v) < r (v).

Similarly, if

Y a 1 X b 1 • • • X b k-1
is not defined on u -and v -, then we have r (u) < r(u) and r (v) < r(v).

Finally, let us assume that

Y a 1 X b 1 • • • X b k is not defined on u -c or v -c, but Y a 1 X b 1 • • • X b k-1 is defined on u -and v -. Let u + = u 0 b k u 1 and v + = v 0 b k v 1 be b k -left factorizations. Then ord(r(u), r (u)) = ord(Y d s (u -cu 0 ), r (u -cu 0 )) and ord(r(v), r (v)) = ord(Y d s (v -cv 0 ), r (v -cv 0 )).
Since u m,n+1 v, we have u + m,n v + , and by Lemma 3.7 , u -m,n v - and u 0 m,n-

1 v 0 . Therefore u -cu 0 m,n-1 v -cv 0 . Since Y d s ∈ R Y m-2,n-2
is condensed on both u -cu 0 and v -cv 0 , we conclude by induction on the length of r that ord(Y d s (u -cu 0 ), r (u -cu 0 )) = ord(Y d s (v -cv 0 ), r (v -cv 0 )) and hence ord(r(u), r (u)) = ord(r(v), r (v)).

This concludes the proof. Proof. Without loss of generality, we assume that u m+1,n v. We proceed by induction, first on m.

If m = 1, then r = X a 1 • • • X a k and r = Y b 1 • • • Y b with k + l ≤ n. We observe that if p = rX b • • • X b 1 is defined on u, then r(u) < r (u); if p is not defined on u, but a k = b and rX b -1 • • • X b 1 is defined on u, then r(u) = r (u)
; and in all other cases, r(u) > r (u). The same holds for v, and this completes the proof in case m = 1. We now assume that m ≥ 2 and proceed by induction on n. We first note that if one of r, r has length 1, then the result was established in Proposition 5.5. We now assume that |r| , |r | ≥ 2 (so |r| , |r | ≤ n -2).

Suppose that n = m + 1 and let β(r) the number of alternating blocks in r: then β(r) ≤ |r| ≤ n -|r | ≤ n -2 = m -1. The same inequality holds for r and we conclude by induction on m.

We must now consider the case where n > m + 1 > 2. In particular, we have r ∈ R X m,n-2 and r ∈ R X m+1,n-1 . First case: s starts with an X-block. Let u = u -au + and v = v -av + be aleft-factorizations. Then s is condensed on u + and v + and u + m+1,n-1 v + , so u + and v + agree on rankers in R X m+1,n-1 (Proposition 3.10). In particular, u + and v + agree on r . If r is defined on u + , then ord(r(u), r (u)) = ord(s(u + ), r (u + )). Moreover, r is defined on v + as well and ord(r(v), r (v)) = ord(s(v + ), r (v + )), so we conclude by induction. If instead r is not defined on u + or v + , then r (u) ≤ X a (u) < r(u) and r (v) ≤ X a (v) < r(v).

Second case: s starts with a Y-block. Let u = u -bu + and v = v -bv + be b-right factorizations. Then u -m+1,n-1 v -by Lemma 3.7 and this case can be handled exactly like the previous one.

Third case: s starts with a Y-block and s starts with an X-block. If X a (u) ≤ Y b (u), then X a (v) ≤ Y b (v) (by Proposition 5.5), we have r(u) < X a (u) ≤ Y b (u) < r (u), and the same inequalities hold for v.

We now assume that X a (u) > Y b (u) and X a (v) > Y b (v). In particular, a = b. Identifying the first a and the last b in u and v, we get factorizations u = u -bu 0 au + and v = v -bv 0 av + such that a ∈ alph(u -bu 0 ) ∪ alph(v -bv 0 ) and b ∈ alph(u 0 au + ) ∪ alph(v 0 av + ). In particular, r(u) = s(u -bu 0 ), r (u) is the position s (u 0 au + ) in the suffix u 0 au + of u, and the same holds in v. Moreover, u = (u -bu 0 )au + is an a-left factorization, u = u -b(u 0 au + ) is a b-right factorization, and the same holds in v. Therefore, and since u m+1,n v, we have u -bu 0 m,n-1 v -bv 0 by definition and u 0 m,n-2 v 0 by Lemma 3.7.

Since

s ∈ R Y m-1,n-3 and s ∈ R X m-1,n-3 ⊆ R Y m,n-2
, Proposition 3.10 shows that, if s is not defined on u 0 , then it is not defined on v 0 either, and r(u) ≤ Y b (u) < r (u) and similarly, r(v) < r (v). Symmetrically, if s is not defined on u 0 , then r(u) < X a (u) ≤ r (u) and r(v) < r (v). Let us observe that under this assumption, if n = m, then the number of alternating blocks in r is less than or equal to m -2: indeed it is at most equal to |r| ≤ n -2 = m -2. The same inequality holds for r , so this situation is handled by induction on m. We can now assume that n > m.

Let u = u -au + = u -bu + and v = v -av + = v -bv + be a-left and b-left factorizations.

First case: a = b. If s starts with an X-block and s starts with a Y-block, then r (u) < r(u) and r (v) < r(v). Dually, if s starts with a Y-block and s starts with an X-block, then r (u) > r(u) and r (v) > r(v).

If s and s both start with a Y-block (which can happen only Second case: a = b, s and s start with X-blocks. Then s ∈ R X m and s ∈ R X m-1 are condensed on u + and v + . Without loss of generality, X b (u) < X a (u), so we have r

if m-1 ≥ 2), then s ∈ R Y m-1 and s ∈ R Y m-2 are condensed on u -and v -and ord(r(u), r (u)) = ord(s(u -), s (u -)) and ord(r(v), r (v)) = ord(s(v -), s (v -)). Since u -m-1,n-1 v -and |s| + |s | ≤ n -2,
(u) = X a s(u) = X b X a s(u) = X b r(u).
In particular, ord(r(u), r (u)) = ord(r(u + ), s (u + )). By Proposition 5.7, we also have

X b (v) < X a (v), and hence ord(r(v), r (v)) = ord(r(v + ), s (v + )). Since u m,n v, we have u + m,n-1 v + and we conclude by induction on n since |r| + |s | ≤ n -1.
Third case: a = b, s and s start with Y-blocks. This can occur only if m -1 ≥ 2. Then s ∈ R Y m-1 and s ∈ R Y m-2 are condensed on u -and v -, r(u) = s(u -) and r (u) = s (u -), and the same equalities hold for v. Without loss of generality, we may assume that X b (u) < X a (u), and hence X b (v) < X a (v) (Proposition 5.7). Let u 0 and v 0 be such that u = u -bu 0 au + and v = v -bv 0 av + : then u 0 is the left factor in the a-left decomposition of u + and the right factor in the b-left decomposition of u -. An analogous statement is true for v 0 . There are two cases, depending on whether s is defined on bu 0 . If this is the case, then r (u) < r(u). Moreover, we have u + m,n-1 v + and u 0 m-1,n-2 v 0 , so s is defined on bv 0 as well, by Proposition 3.10.

If instead, s is not defined on bu 0 or bv 0 , let p be the longest prefix of s which is defined on bu 0 (and hence on bv 0 ): then p is either empty or a Y-block and s = pY c t, where c has no occurrence in u

[X b (u); X a p(u) -1] (so Y c is defined on u -). If Y c t is defined on u -, then r(u) = s(u -) = Y c t(u -), so that ord(r(u), r (u)) = ord(Y c t(u -), s (u -)). Now u m,n v implies u -m,n-1 v -by Proposition 3.7, so Y c t is defined on v -and hence we have ord(r(v), r (v)) = ord(Y c t(v -), s (v -)) as well. Since |Y c t| ≤ |s| < |r|, we conclude by induction that ord(r(u), r (u)) = ord(r(v), r (v)).
If Y c t is not defined on u -, then let Y c q be the longest prefix of Y c t which is defined on u -(and hence on v -). Then q is either empty or an X-block and

Y c t = Y c qX d t . If d = b, then qX d (u -b) = X b (u), so r(u) = X b t (u) and similarly, r(v) = X b t (v)
. We conclude by induction on m that ord(r(u), r (u)) = ord(r(v), r (v)) since X b t has 2 blocks less than r.

If d = b, then we have X b (u) < X a pY c qX d (u). If X d t is defined on bu 0 , then r(u) lies in u 0 and r (u) lies in u -, so r(u) > r (u). Similarly r(v) > r (v), and we are done. If instead X d t is not defined on bu 0 , then X a pY c q(u) < X b (u) and X a pY c qX d (u) = X b X d (u), so the condensedness of r = X a pY c qX d t on u implies that X b X d t is condensed on u as well. The same holds for v, and we have ord(r(u), r (u)) = ord(X b X d t (u), r (u)) and similarly, ord(r(v), r (

v)) = ord(X b X d t (v), r (v)).
We conclude by induction on m since X b X d t has 2 blocks less than r.

Fourth case: a = b, s and s start with different directions. Without loss of generality, we may assume that s starts with an X-block and s starts with a Y-block. Since r starts with 2 X-letters, the number of alternating blocks of r is less than |r| -

1 ≤ n -3. Therefore if n = m + 1, r ∈ R X m-2
and r ∈ R X m-1 , a case that can be decided by induction on m. So we now assume that n ≥ m -2.

If X b (u) < X a (u), then the same inequality holds in v (by Proposition 5.7) and we have r (u) < r(u) and r (v) < r(v). If instead X a (u) < X b (u) and X a (v) < X b (v), then the b-left factorizations of u + and v + are of the form u + = u 0 bu + and v + = v 0 bv + .

Several cases arise, according to whether s and s are defined (and condensed) on u 0 or not. We have u + m,n-1 v + and u 0 m,n-2 v 0 by Lemma 3.7. It follows as usual that s and s are defined on v 0 if and only if they are defined on u 0 . If s is not defined on u 0 then the order types ord(r(u), r (u)) and ord(r(v), r (v)) are both >. Therefore, from now on we can assume that s is defined on u 0 and v 0 .

If s is defined on u 0 then we can chop off u -a from u, v -a from v, and X a from r: ord(r(u), r (u)) = ord(s(u + ), r (u + )) and ord(r(v), r (v)) = ord(s(v + ), r (v + )). Since u + m,n-1 v + , ord(s(u + ), r (u + )) and ord(s(v + ), r (v + )) are equal by induction on n, and hence ord(r(u), r (u)) = ord(r(v), r (v)).

If s is not defined on u 0 , then, as in the third case, we have to split the ranker s at those points at which it crosses the position X a (u). Let

X b s = p 1 q 1 • • • p k q k such
that all p i are defined on u 0 and all p i are starting with an X-letter followed by a (possibly empty) Y-block. The sole exception is p k which might contain further blocks. Moreover, each p i is the maximal prefix of p i q i • • • p k q k which is defined on u 0 . All q i are defined on u -a and all q i are starting with a Y-letter followed by a (possibly empty) X-block. The sole exception is q k which might be empty or which might contain further blocks. Each q i is the maximal prefix of q i p i+1 • • • p k q k which is defined on u -a. Since u -a m,n-1 v -a (Lemma 3.7) and u 0 m-1,n-2 v 0 , the same definedness and maximality properties hold on v -a and v 0 .

If q k is empty, then k ≥ 2 and p 1 and q 1 are non-empty. We see that ord(r(u), r (u)) = ord(s(u 0 ), p k (u 0 )) and ord(r(v), r (v)) = ord(s(v 0 ), p k (v 0 )). By induction on n, we have ord(s(u 0 ), p k (u 0 )) = ord(s(v 0 ), p k (v 0 )), and hence ord(r(u), r (u)) = ord(r(v), r (v)).

Finally, if q k is non-empty, then we have r(u) > r (u) and r(v) > r (v).

5.2.3.

Completing the proof of Theorem 5.1. Let us (at last!) verify that, if u m+1,2n v or u m+1,2n v, then Properties (WI 2c) and (WI 3c) hold for m, n. By symmetry, we simply handle the case where u m+1,2n v.

To verify Property (WI 2c), we consider rankers r ∈ R m,n and r ∈ R m-1,n-1 that are condensed on u and v. If both start with X-blocks, Proposition 5.8 shows that ord(r(u), r (u)) = ord(r(v), r (v)). If both start with Y-blocks, the same proposition allows us to conclude, after observing that we have u m,2n-1 v. And if r and r start with different direction blocks, we conclude by Proposition 5.6.

To verify Property (WI 3c), we consider rankers r ∈ R m,n and r ∈ R m,n-1 that end with different directions, and that are condensed on u and v. If r and r start with different direction blocks, we again conclude by Proposition 5.6. If both start with X-blocks, then they must have different number of alternations, so we have r ∈ R X m 1 ,n 1 and r ∈ R X m 2 ,n 2 for some n 1 ≤ n, n 2 ≤ n -1 and for distinct values m 1 , m 2 ≤ m. In particular, one of m 1 and m 2 is less than or equal to m -1, and we can apply Proposition 5.8.

We proceed similarly if r and r both start with Y-blocks, after observing that u m,2n-1 v. This completes the proof of Theorem 5.1. m hierarchy is infinite. Weis and Immerman had already proved this result by combinatorial means [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF]Theorem 4.11], whereas our proof is algebraic. From that result on the FO 2 m hierarchy, it is also possible to recover the strict hierarchy result on the R m and L m and the fact that their union is equal to DA.

By the same token, Corollary 3.12 and Theorem 4.3 show that the TL m (resp. TL m ) hierarchy is infinite and that its union is all of FO 2 (resp. DA). Theorem 6.3. The hierarchies FO 2 m and TL m are infinite, and their union is all of FO 2 .

Similarly, the fact (stated in Proposition 3.23) that an m-generated element of DA lies in R m+1 ∩ L m+1 , shows that an FO and TL Y 2|A|+1 -definable. Even though we arrived at Theorem 6.4 by algebraic means, it is interesting to note that its statement reflects the following combinatorial property (an idea that was already used by Weis and Immerman [START_REF] Weis | Structure theorem and strict alternation hierarchy for FO 2 on words[END_REF]Theorem 4.7]). Lemma 6.5. A ranker that is condensed on a word on alphabet A, has at most |A| alternating blocks.

Proof. Let u be a word and let r be a ranker that is condensed on u. Without loss of generality, we may assume that r ∈ R X m,n , say

r = X a 1 • • • X a k 1 Y a k 1 +1 • • • Y a k 2 • • • Z a k m-1 +1 • • • Z a km with 0 < k 1 < k 2 < • • • < k m = n
and Z = X (resp. Y) if m is odd (resp. even). By definition of condensed rankers (and with the notation in that definition, see Section 3), the interval I k h is of the form (i k h -1 ; X a k h (u, i k h -1 )) if h is odd, of the form (Y a k h (u, j k h -1 ); j k h -1 ) if h is even. In either case, a k h+1 occurs in u within the interval I k h but a k h does not. Since the intervals I k h are nested, it follows that the letters a k 1 , a k 2 , . . . , a km are pairwise distinct, and hence m ≤ |A|. 6.3. Infinite hierarchies and unambiguous polynomials. Finally we note the following refinement of [START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF]Proposition 4.6]. One of the classical (and one of the earliest) results concerning the languages recognized by monoids in DA is the following: they are exactly the disjoint unions of unambiguous products of the form

B * 0 a 1 B * 1 • • • a k B * k ,
where each B i is a subset of A (Schützenberger [START_REF] Paul | Sur le produit de concaténation non ambigu[END_REF], see also [START_REF] Tesson | Diamonds are forever: The variety DA[END_REF][START_REF] Tesson | Logic meets algebra: The case of regular languages[END_REF][START_REF] Volker Diekert | A survey on small fragments of first-order logic over finite words[END_REF]). Recall that such a product is unambiguous if each word w ∈ B * More precisely, every unambiguous product of the form B * 0 a 1 B * 1 • • • a k B * k , where each B i is a subset of A, can be expressed in terms of Boolean operations and at most |A| + 1 alternated applications of visibly deterministic and visibly co-deterministic products -starting with a visibly deterministic (resp. co-deterministic) product.

The analogous, but weaker statement with the word visibly deleted was proved in [START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF] by algebraic means, and independently by Lodaya, Pandya and Shah using logical and combinatorial arguments [START_REF] Kamal Lodaya | Marking the chops: an unambiguous temporal logic[END_REF].

Conclusion. We have related the FO 2

m hierarchy with the R m -L m hierarchy, a hierarchy of varieties of languages which is connected with the alternation of closures under deterministic and co-deterministic products.

The varieties R m and L m are decidable, but the link we establish with FO 2 m (Theorem 5.1) is not tight enough to prove decidability of the quantifier alternation hierarchy. We recall the readers of our conjecture (Conjecture 5.4 above), according to which FO 2 m is equal to the intersection R m+1 ∩ L m+1 . Establishing this conjecture would prove that each level of the quantifier alternation hierarchy FO 2 m is decidable. Finally, we refer the reader to Straubing's result: he showed [START_REF] Straubing | Algebraic characterization of the alternation hierarchy in FO 2 [<] on finite words[END_REF] that the pseudovariety FO 2 m is the m-th weakly iterated power of the pseudovariety J of J -trivial monoids (more precisely, FO 2 1 = J and FO 2 m+1 = FO 2 m J). This result offers a different avenue to solve the decidability problem for FO 2 m -definability, and our conjecture would show the equality between two algebraic hierarchies which seem completely unrelated.

Proposition 3 . 9 .

 39 and sX b (u) ≥ s 0 (u). More precisely, sX b (u) is the first b-position to the right of s(u), so sX b (u) = s 0 (u) if s 0 (u) is a b-position (i.e., if s 0 ends with X b or Y b ), and sX b(u) = s 0 X b (u) otherwise. Let n ≥ m ≥ 1, u, v ∈ A + and Z ∈ {X, Y}. If u and v agree on condensed rankers in R Z m,n and if r ∈ R Z m,nis defined on both u and v, then there exists r ∈ R Z m,n which is condensed on u and v and coincides with r on both words.

Proposition 3 . 10 .

 310 Let n ≥ m ≥ 1, u, v ∈ A + and Z ∈ {X, Y}. If u and v agree on condensed rankers in R Z m,n , then they agree on rankers from the same class.

Theorem 3 . 11 .

 311 Let u, v ∈ A * and let 1 ≤ m ≤ n. Then u and v satisfy the same formulas in FO 2 m,n if and only if (WI 1c) u and v agree on condensed rankers from R m,n , (WI 2c) if the rankers r ∈ R m,n and r ∈ R m-1,n-1 are condensed on u and v, then ord(r(u), r (u)) = ord(r(v), r (v)). (WI 3c) if r ∈ R m,n and r ∈ R m,n-1 are condensed on u and v and end with different direction letters, then ord(r(u), r (u)) = ord(r(v), r (v)).

Corollary 3 . 12 . 3 . 3 .Lemma 3 . 13 .

 31233313 For each m ≥ 1, we have TL X m ⊆ R m ⊆ FO 2 m and TL Y m ⊆ L m ⊆ FO 2 m .Condensed rankers determine a hierarchy of varieties. We now examine the algebraic properties of the relations m,n and m,n . The relations m,n and m,n are finite-index congruences.

1

  ,n are congruences. Let us now assume that n ≥ m ≥ 2 and u m,n v. By Proposition 3.6 (2), we have alph(u) = alph(v) and u m-1,n-1 v. It follows that alph(ub) = alph(bu) = alph(vb) = alph(bv), and that ub m-1,n-1 vb and bu m-1,n-1 bv by induction. Let now a ∈ alph(u) ∪ {b}. If a ∈ alph(u) and if u = u -au + and v = v -av + are a-left factorizations, then the a-left factorizations of ub and vb are u -a (u + b) and v -a (v + b). And the a-left factorizations of bu and bv are (bu -) a u + and (bv -) a v + -unless a = b, in which case these factorizations are εbu and εbv. By Proposition 3.6 (2) we have u

Lemma 3 . 14 .

 314 If ϕ : A * → B * is a morphism and if u, v ∈ A * are m,nequivalent (resp. m,n -equivalent), then so are ϕ(u) and ϕ(v).

Corollary 3 . 15 .

 315 If γ : A * → M is a morphism into a monoid in R m,n , then there exists a morphism β : A * / m,n → M such that γ = β • π A , where π A : A * → A * / m,n is the projection morphism. The same result holds for L m,n and the quotient A * / m,n .

Corollary 3 . 16 .

 316 For each m ≥ 1, R m and L m are varieties of languages and the corresponding pseudovarieties of monoids are R m and L m .

Corollary 3 . 19 .

 319 For each m ≥ 1, R m and L m are contained in DA, and also in R m+1 ∩ L m+1 .

Fact 3 . 22 .

 322 Let σ : A * → S be a morphism into a monoid S ∈ DA. If u, v ∈ A * , a ∈ alph(v) and σ(u) R σ(uv), then σ(uva) R σ(u).Proof of Theorem 3.21. It is immediate from the definition that L vdet m ⊆ L det m . Let u ∈ A * and let B = alph(u). For each a ∈ B, let u = u

  This shows that [B] ∈ R 1 = L 1 . (It is also well-known that [B] is piecewise testable, and hence [B] ∈ R 1 = L 1 .) Now let n > m ≥ 1. It follows from Proposition 3.6 that the m+1,n -class of u is the intersection of [B], the m,n-1 -class of u and the products KaL (a ∈ B) where K is the m,n-1 -class of u (a) -and L is the m+1,n-1 -class of u (a)

Proposition 3 . 23 .

 323 . The following results are proved in[START_REF] Kufleitner | On the lattice of sub-pseudovarieties of DA[END_REF] Section 4]. The hierarchies (R m ) m and (L m ) m are infinite chains of decidable pseudovarieties, and their unions are equal to DA. Moreover, every m-generated monoid in DA lies in R m+1 ∩ L m+1 .

Proposition 5 . 6 .

 56 Let n > m ≥ 1, let r = X a s ∈ R X m and r = Y b s ∈ R Y m such that |r| + |r | ≤ n,and let u, v ∈ A * such that r and r are condensed on u and v. If u m+1,n v or u m+1,n v, then ord(r(u), r (u)) = ord(r(v), r (v)).

Proposition 5 . 8 .

 58 Let n ≥ m ≥ 2, let r = X a s ∈ R X m and r = X b s ∈ R X m-1such that |r| + |r | ≤ n, and let u, v ∈ A * such that r and r are condensed on u and v. If u m,n v, then ord(r(u), r (u)) = ord(r(v), r (v)). The dual statement (where r, r start with Y-blocks and u m,n v) holds as well.Proof. The proof is by induction on m, and then on n. If one of r and r has length 1, then the result was established in Proposition 5.7. This takes care of the cases where n ≤ 3, including the base case m = n = 2. We now assume that |r| , |r | ≥ 2.

  we have ord(r(u), r (u)) = ord(r(v), r (v)) by induction on m. If instead s and s both start with an X-block, then s ∈ R X m and s ∈ R X m-1 are condensed on u + and v + , and we have ord(r(u), r (u)) = ord(s(u + ), s (u + )) and ord(r(v), r (v)) = ord(s(v + ), s (v + )). Since u + m,n-1 v + and |s| + |s | ≤ n -2, we have ord(r(u), r (u)) = ord(r(v), r (v)) by induction on n.

6 . Consequences 6 . 1 .Theorem 6 . 1 .Proposition 6 . 2 . 6 . 2 .

 661616262 Decidability results. The main consequence we draw of Theorem 5.1 and of the decidability of the pseudovarieties R m and L m is summarized in the next statement. Given an FO 2 -definable language L, one can compute an integer m such that L is FO 2 m+1 -definable, possibly FO 2 m -definable, but not FO 2 m-1 -definable. That is: we can decide the quantifier alternation level of L within one unit. Proof. Let L ∈ FO 2 and let M be its syntactic monoid. Since each pseudovariety R m ∩ L m is decidable (Proposition 3.23), we can compute the largestm such that M ∈ R m ∩ L m . By Theorem 5.1, M ∈ R m+1 ∩ L m+1 ⊆ FO 2 m+1 and hence L is FO 2 m+1 -definable. On the other hand, M ∈ FO 2 m-1 ⊆ R m ∩ L m .Let us also record the following consequences of Proposition 3.23, Proposition 4.1 and the decidability ofR 2 ∨ L 2 (discussed in Example 5.3). The classes TL X 1 = TL Y 1 = TL 1 = FO 2 1 , TL X 2 , TL Y2 and TL 2 are decidable. Infinite and collapsing hierarchies. The fact that the R m and L m form strict hierarchies (Proposition 3.23), together with Theorem 5.1, proves that the FO 2

0 a 1 Proposition 6 . 6 .

 166 B * 1 • • • a k B * k factors in a unique way as w = u 0 a 1 u 1 • • • a k u k with u i ∈ B * i .Deterministic and codeterministic products (see Section 3.4) are easily seen to be particular cases of unambiguous products. Propositions 3.21 and 3.23 imply the following statement. The least variety of languages containing the languages of the form B * (B ⊆ A) and closed under visibly deterministic and visibly co-deterministic products, is FO 2 .

  ). If n ≥ m, the fragment TL X m,n (resp. TL Y m,n ) consists of the TL-formulas with depth n and with m alternated blocks, in which every branch (of the parsing tree) with exactly m alternations starts with future (resp. past) operators. Branches with less alternations may start with past (resp. future) operators. The fragments TL m,n , TL X m,n , TL Y m,n , TL X m , TL Y m and TL m are defined according to the same pattern as in the definition

  Proposition 1.6. Let 1 ≤ m ≤ n. Two words satisfy the same TL X

	m,n
	formulas if and only if they agree on rankers from R X m,n . A language is in
	TL X m,n if and only if it is a Boolean combination of languages of the form
	L(r), r ∈ R X m,n .
	Similar statements hold for TL Y m,n , TL X

m , TL Y m and TL m , relative to the corresponding classes of rankers.

. Remark 1.7. Together with Example 1.4, this proposition confirms the elementary observation that a language is TL 1 (resp. TL X 1 , TL Y 1 ) definable if and only if it is piecewise testable (see Remark 1.1). It follows that TL 1 - definability is decidable. 1.4. Rankers and FO 2 . The connection established by Weis and Immer- man

  2 -definable language in A * lies in R |A|+1 ∩ L |A|+1 , and hence in FO 2 |A|+1 -a fact that was already established by combinatorial means by Weis and Immerman [37, Theorem 4.7]. It also shows that such a language is in TL 2|A|+1 by Theorem 4.3. Theorem 6.4. A language L ⊆ A * is FO 2 -definable if and only if it is FO 2 |A|+1 -definable. And it is TL-definable if and only if it is both TL X

	2|A|+1

Of course, the same fact can be proved by the direct construction of an FO 2 m -formula for each m,n-class (by induction on m and using Proposition

3.6).

Acknowledgements. The authors gratefully acknowledge the contribution of the referees, which helped clarify certain points in the paper, suggested simpler proofs for certain technical lemmas and -especially! -pointed out a mistake in one of the proofs.

The first author was supported by the German Research Foundation (DFG) under grant DI 435/5-1. The second author was supported by the French ANR project 2010 blan 0202 01 frec. Both authors acknowledge support from the ESF program AutoMathA.

Finally, if s and s are defined on u 0 , then ord(r(u), r (u)) = ord(s(u 0 ), s (u 0 )) and ord(r(v), r (v)) = ord(s(v 0 ), s (v 0 )), and we conclude by induction. 5.2.2. The case where r and r start with the same direction.

starting with a Y-letter, and u m,n+1 v) holds as well.

Proof. We proceed by induction, first on m.

In the first case, the order type ord(r(u), r (u)) depends, as in the proof of Proposition 5.6, on whether

2,n+1 and are condensed where they are defined (Example 3.3), we have ord(r(u), r (u)) = ord(r(v), r (v)).

In the second case, where

2,n+1 , Proposition 3.10 shows that rY c is defined on u if and only if it is defined on v, and ord(r(u), r (u)) = ord(r(v), r (v)).

We now assume that m ≥ 3. If r has less than m alternating blocks, we conclude by induction on m. Let us suppose now that r has m alternating blocks and let us proceed by induction on |r| ≥ m.

Let r = X a s. If s starts with a Y-letter (which includes the base case where

, then r(u) < r (u) and r(v) < r (v). In all other cases, ord(r(u), r (u)) = ord(s(u -), r (u -)) and ord(r(v), r (v)) = ord(s(v -), r (v -)).

Since u -m,n v -by Lemma 3.7, these two order types are equal by Proposition 5.5.

If instead s starts with an X-letter, then |r| > m, s ∈ R X m,n-1 is condensed on u + and v + (Lemma 3.4) and we distinguish two cases. If c ∈ alph(u -a) = alph(v -a), then r (u) < r(u) and r (v) < r(v). Otherwise ord(r(u), r (u)) = ord(s(u + ), r (u + )) and ord(r(v), r (v)) = ord(s(v + ), r (v + )).

Since u + m,n v + , these two order types are equal by induction on n.