ON GROUPS WITH EDT0L WORD PROBLEM
ALEX BISHOP, MURRAY ELDER, ALEX EVETTS, PAUL GALLOT, AND ALEX LEVINE
Abstract. We prove that the word problem for the infinite cyclic group is not EDT0L, and obtain as a corollary that a finitely generated group with EDT0L word problem must be torsion. In addition, we show that the property of having an EDT0L word problem is invariant under change of generating set, and passing to finitely generated subgroups. This represents significant progress towards the conjecture that all groups with EDT0L word problem are finite (i.e. precisely the groups with regular word problem).
1.		Introduction
An interesting problem is to classify finitely generated groups in terms of the language complexity of their word problem, the set of all words over generators and their inverses which spell the identity of the group. The formal study of this problem began when Anisimov [1] first observed that the word problem of a group is regular if and only if the group is finite. An influential result of Muller and Schupp [28] later showed that the word problem of a group is context-free if and only if the group is virtually free. Moreover, the following equivalences have been shown: the word problem is one-counter if and only if the group is virtually cyclic [21]; the intersection of finitely many one-counter languages if and only if the group is virtually abelian [22]; blind multicounter if and only if the group is virtually abelian [15, 34]; a language accepted by a Petri net if and only if the group is virtually abelian [29]; an NTS language if and only if the group is virtually free [2].
The family of EDT0L (Extended alphabet, Deterministic, Table, 0-interaction, Lindenmayer) languages have recently received a great amount of interest within geometric group theory and related areas [3–10, 23, 26, 27]. In this paper, we also consider the family of finite-index EDT0L languages. Figure 1 shows the relative expressive power of these families of languages, where each forwards arrow represents a strict inclusion. In particular, the family of EDT0L languages contains the family of finite- index EDT0L languages as a strict subfamily; and the family of context-free languages is incomparable (in terms of set inclusion) with the families of EDT0L and finite-index EDT0L languages.

context-free

finite-index regular
EDT0L

EDT0L ET0L indexed

context-sensitive

Figure 1. Inclusion diagram of formal languages (see Theorem 15 in [31] and Figure 8 in [17]).
We begin by showing that having an EDT0L word problem is invariant under change of generating set, which is not immediate since EDT0L languages are not closed under inverse monoid homomorphism [13]. From the following proposition, it makes sense to speak of a word problem being EDT0L without the need to specify a generating set. Let WP(G, X) and coWP(G, X) denote the word and coword problem, respectively, for a group G with respect to the generating set X .
Proposition A. Let G be a group with finite monoid generating sets X and Y . If WP(G, X) (resp. coWP(G, X)) is EDT0L, then WP(G, Y ) (resp. coWP(G, Y )) is EDT0L of finite index. These results also hold if Y instead generates a submonoid of G. In particular, this implies that, if a word problem is EDT0L, then it is EDT0L of finite index; and that having a word problem that is EDT0L of finite index is independent of choice of generating set.
The following conjecture was posed by Ciobanu, Ferov and the second author.
2020 Mathematics Subject Classification. 20F10, 68Q42, 20F65.
Key words and phrases. word problem, EDT0L language, finite-index EDT0L grammar.
Conjecture B (Conjecture 8.2 in [8]). If G has an EDT0L word problem, then G is finite.
Towards this conjecture, we have the following results.
Theorem C. The word problem for the infinite cyclic group Z is not EDT0L.
From the above theorem and Proposition A, we then obtain the following theorem.
Theorem D. If G has an EDT0L word problem, then G is a torsion group.
Our proof of Theorem C is an expanded version of the proof given by the fourth author [18, Chapter 8] in their PhD thesis. It remains to be shown whether there can exist an infinite torsion group with EDT0L word problem.
A language related to the word problem of Z with respect to a standard generating set is the Dyck language D1 , where
Dn = w ∈ {a1 , b1 , ..., an , bn }∗ |w|ai = |w|bi and, for each prefix u of w and each i, |u|ai ⩾ |u|bi where | · |x counts the instances of the letter x in w. By definition, we see that D1 is a proper subset of the word problem of Z (taking a1 as the generator 1 and b1 as -1). It was shown in [14, Theorem 9] that the language Dn is not EDT0L for n ⩾ 8. This was later strengthened in [33, Theorem 6.3.2] where it was shown that D1 is not EDT0L. However, this result and the techniques used therein were not helpful in proving Theorem C.
This paper is organised as follows. In Section 2 we fix some terminology about geodesic words. In Section 3 we define the families of EDT0L and finite-index EDT0L languages, and provide some tools for proving that an EDT0L language has finite index. In Section 4 we prove that the class of EDT0L languages is closed under string transduction. In Section 5 we prove that if the word problem of a group is EDT0L, then it is EDT0L of finite index, and obtain Proposition A. In Section 6 we define a non-permuting, non-erasing, non-branching multiple context-free grammar to be a multiple context- free grammar that does not permit permutation of variables, does not allow erasure of variables, and restricts productions to maintain a single nonterminal. For ease of reference, we refer to such a grammar as a restricted multiple context-free grammar (abbreviated R-MCFG) throughout the paper. We prove that every finite-index EDT0L language is the language of an R-MCFG. Finally, in Section 7, we prove Theorems C and D.
1.1.		High-level overview of the proof of Theorem C. This subsection furnishes a very brief outline of the main ideas of the proof, to motivate the technology required in the sections leading up to and including Section 7. We start the proof of Theorem C by assuming for contradiction that the word problem of Z with respect to the generators 1, -1 is generated by a given R-MCFG, and moreover we assume the grammar is in a particular normal form (see Definition 6.7). From this grammar, we obtain a bound C related to the difference in the number of 1 versus -1 letters in a tuple words that appear in a step of any derivation (see Lemma 7.3 for details). Using this bound, we construct a word W, which we call the counterexample word, having a very specific and controlled form (which uses two parameters m, k coming from the grammar and bound C). An example of W for k = 2, m = 4 is shown in Figure 2, where the generator 1 is represented by an up-step (1, 1), and -1 by a down-step (1, -1). The basic

Figure 2. The word W defined in Section 7 for values k = 2 and m = 4.

idea of the construction of this word is to ensure that it contains “long” up-step factors, having lengths exceeding some bound (depending on C and the grammar) and occurring sufficiently frequently, and all down-step factors of constant size, such that the total difference between the number of up and down steps is zero (so that W is in the word problem of Z). We show that any derivation of the R-MCFG in normal form generating W will have the form
S(W) ← Hℓ(W, ε, ..., ε) ← · · · ← H1(ε, ..., ε) ←
(for some nonterminals H1 , ..., Hℓ and starting nonterminal S; see Definition 6.1) where the words in the tuple (ε, ..., ε) do not have any long up-step factors, whereas W does (in particular, its prefix and suffix are such factors). Definition 7.20 defines a property of tuples that is enjoyed by (W, ε, ..., ε) and not by (ε, ..., ε). Specifically, a tuple is said to have a decomposition (as in Definition 7.20) if a particular inequality which compares the lengths and occurrences of long up-step factors at the prefix and suffix of coordinates, as well as several other quantities, is satisfied. We then prove (Proposition 7.31) that for each step of a derivation of the R-MCFG, if the target tuple has a decomposition then so must the source tuple. Since (W, ε, ..., ε) has a decomposition and (ε, ..., ε) does not, we have our contradiction.
1.2.		Notation. We write N = {0, 1, 2, 3, ...} for the set of nonnegative integers including zero, and N+ = N \ {0}. Unless otherwise stated, monoid actions are applied on the right: we make this choice to simplify the constructions within the proofs below. An alphabet is a finite set. If X is an alphabet, we let X∗ denote the set of words (finite length strings) of letters from X, and X+ = X∗ \ {ε}. We will sometimes speak of the word problem of a monoid. Suppose that M is a monoid with finite generating set X , and that 1M is the monoid identity. The word problem of (M, X ) is given by
WP(M, X) := {w ∈ X∗ | w = 1M}
where · : X ∗ → M is the natural homomorphism from the words over X to the monoid.
2.		Geodesics in finitely-generated groups
The results in this paper combine topics in formal language theory and geometric group theory. This section is provided for readers who are not familiar with some of the terms and basic notations of geometric group theory which are used in this paper. In particular, this section explains what it means for a word to be geodesic in a finitely generated group. Readers who are familiar with this terminology can safely skip this section.
Suppose that G is a group which is generated as a monoid by a finite subset X . That is, we have a surjective homomorphism, which we denote as · : X ∗ → G, from the free monoid over X to the group G. Thus, for each element g ∈ G, there exists at least one word w ∈ X ∗ such that w = g . If the word w ∈ X ∗ is a minimal-length word for which w = g , then we say that w is a geodesic for g. Notice that each element g ∈ G must have at least one corresponding geodesic.
For example, suppose that G is the group given by vectors in Z2 with group operator being vector addition. Such a group is generated by X = {x, x-1, y, y-1} where x = (1, 0) and y = (0, 1). The element (2, 3) can be written as any of the following words over X :
xxyyy	yxyxy	y xxyyyy	x xx yxyxyx.
Notice here that the word xxyyy and yxyxy are both geodesics.
We have the following properties of geodesics which are used in this paper:
(1)		any prefix or suffix of a geodesic is also a geodesic;
(2)		the only geodesic for the group identity is the empty word; and
(3)		if G is an infinite group, then it has arbitrarily long geodesics.
The above properties are straightforward to prove, and left as an exercise to the reader.
3.		EDT0L and EDT0L of finite index
In this section we provide background on the family of EDT0L languages and the subfamily of EDT0L languages of finite index. Our aim here is to prove Lemma 3.6 due to Latteux [25], which provides a method to show that a given language is EDT0L of finite index. We begin this section by defining the class of EDT0L grammars as follows. We note that our definition of EDT0L grammar differs from their original definition given in [32, Definition 1 and 2], in particular, we make additional assumptions of our tables in (4) of Definition 3.1. However, it can be seen from [11, Lemma 2.2] that our definition produces the same class of languages to that of [32, Definition 1 and 2].
Definition 3.1. An EDT0L grammar is a 4-tuple E = (Σ, V, I, H) where

(1)		Σ is an alphabet of terminal letters;
(2)		V is an alphabet of nonterminal letters which is disjoint from Σ;
(3)		I ∈ V is an initial symbol; and
(4)		H ⊂ End((V ∪ Σ)∗) is a finite set of monoid endomorphisms such that σ · h = σ for each h ∈ H and each σ ∈ Σ. The endomorphisms h ∈ H are called tables.
The language generated by such a grammar E is given by
L(E) := {I·α | α∈ H∗}∩Σ∗
where I · α denotes the (right) action of α ∈ End((V ∪ Σ)∗) on the word I. That is, L(E) is the set of words in Σ∗ that can be obtained by applying any sequence of maps from H to I .
For example, the language
L = {an1 ban2 ban3 b · · · ankb | ni, k ∈ N with 0 ⩽ n1 ⩽ n2 ⩽ · · · ⩽ nk}
is EDT0L [8, Proposition 7] as it can be generated using the grammar E = (Σ, V, I, H) where
(1)		Σ={a,b};
(2)		V = {I, A}; and
(3)		H = {h1, h2, h3} with

IAb if v = I, v·h1=	,
v

otherwise,

v · h2 =

(Aa if v = A,
v	otherwise,

v · h3 = ε

for each v ∈ V .
In particular, the word abaaab ∈ L can be generated as I · (h1h2h2h1h2h3).
Suppose that E = (Σ, V, I, H) is an EDT0L grammar. Then, we call w ∈ (Σ ∪ V )∗ a sentential form if there exists some sequence of tables α ∈ H ∗ such that w = I · α. For example, in the grammar given above, the word AabAaab is a sentential form which can be generated as I · (h1h2h1). Notice that the initial word I and every word generated by the grammar are examples of sentential forms.
Given a word w ∈ X ∗ over a finite alphabet X , we write |w| for its length. For each letter x ∈ X , we write |w|x to denote the number of instances of the letter x in w. Moreover, for any subset V ⊂ X , we write |w |V to denote v∈V |w|v . We now define the EDT0L languages of finite index as follows.
Definition 3.2 (See [31]). An EDT0L grammar E = (Σ, V, I, H) is of index n if |I · α|V ⩽ n for each monoid endomorphism α ∈ H∗ . That is, if there are at most n nonterminals in any sentential form. An EDT0L grammar is said to be of finite index if it is an EDT0L grammar of index n for some n ∈ N. A language is EDT0L of finite index if it can be generated by an EDT0L grammar of finite index.
From the formal grammar description of regular languages, we have the following result.
Lemma 3.3. Regular languages are EDT0L of index 1.
In order to prove the results in this section, we define the family of LULT grammars as follows.
Definition 3.4. An EDT0L grammar E = (Σ, V, I, H) is LULT (which stands for EDT0L-syst`eme ultralin´eaire, cf. [25, p. 361]) if for each word w ∈ L(E), there exists some α ∈ H∗ with w = I · α such that for each factorisation α = α1α2 with α1, α2 ∈ H∗, and each v ∈ V , either |I · α1 |v ⩽ 1 or |v · α2 | ⩽ 1.
In the next result we show that if a language is generated by a LULT grammar, then the language is EDT0L of finite index. Throughout the proof, we write f : A ⇀ B to denote a partial function from A to B, and we write dom(f) ⊆ A for its domain. That is, f : A ⇀ B is a function from some subset of A to a subset of B. Moreover, we write f = ∅ if dom(f) = ∅.
Lemma 3.5 (Latteux [24]). If E = (Σ, V, I, H) is an EDT0L grammar which is LULT, then the language L(E) is EDT0L of finite index.
Proof. Let E = (Σ, V, I, H) be a LULT grammar as in the lemma statement. In this proof, we construct an EDT0L grammar E′ = (Σ, V ′, I′, H′) with index |V | + 1 such that L(E) = L(E′). In particular, we first construct the grammar E′, then prove that it generates precisely the language L(E).
The construction given in this proof is quite involved. In order to assist the reader’s comprehension, we provide an informal overview as follows. From the definition of LULT grammars, we see that if w ∈ Σ∗ is generated by the grammar E, then there must exist some sequence of tables α ∈ H∗ with w = I · α such that for each factorisation α = α1α2, and each nonterminal v ∈ V , we have either |v · α1 |v ⩽ 1 or |v · α2 | ⩽ 1. Notice that we do not assume that α is uniquely defined. The idea of our construction
is to produce a grammar E′ which only considers such sequences of tables. In particular, we construct our grammar E′ such that each sentential form u ∈ (V ′ ∪ Σ)∗ of E′ is either some dead-end word (see case 2 in part 1.1 of this proof) which cannot lead to an accepted word, or corresponds to some word u′ = I · α1 of E (as before) where the nonterminals v with |u′|v ⩾ 2 have been replaced with the words v · α2 ∈ Σ∗. Notice then that the remaining nonterminals in u each appear at most once, thus resulting in our grammar having finite index as desired. In order to correctly emulate such productions of the grammar E, for technical reasons, each of the nonterminals of E′ must store information about which nonterminals are present in the sentential form: to do so, we introduce the following nonterminals. Their properties are explained in more detail at the end of part 1.1 of this proof.
1.		Nonterminals:
We begin our construction by defining our set of nonterminals V ′ as
V′ = {d, I′} ∪ {Xa,A,f | a ∈ A ⊆ V and f : V ⇀ (Σ ∪ {ε}) with dom(f) ∩ A = ∅}
∪ {YA,f | A ⊆ V and f : V ⇀ (Σ ∪ {ε}) with dom(f) ∩ A = ∅}.
We immediately notice that this set of nonterminals is finite, in particular, we have
|V′| ⩽2+ |V| ·2|V| ·(|Σ|+2)|V| + 2|V | ·(|Σ|+2)|V|.
We note here that the symbol I′ is the starting symbol of the new grammar, and that d is an additional nonterminal which we call the dead-end symbol. In our construction, we ensure that each table maps d to itself. Thus, once d enters a sentential form, there is no way to continue to generate a word in the language associated to the grammar. We describe the remaining symbols of V ′ in detail in part 1.1.
Informally, the nonterminals Xa,A,f correspond to instances of the nonterminal a ∈ A within sentential forms w of E, where each nonterminal v that appear in w either has the property that (1) it occurs at most once in w and v ∈ A, or (2) it goes on to produce the word f(v) ∈ Σ∗ . Similarly, the nonterminals YA,f are included to describe such a sentential form: these nonterminals are required for the case where we are representing a sentential form w of E where each nonterminal in w occurs more than once.
1.1.		Properties of sentential forms of E′ :
In our construction we ensure that, for each sequence of tables of the form α ∈ (H′)∗ , the resulting sentential form w = I′ · α ∈ (Σ ∪ V ′)∗ is in one of the following four forms:
(1)		initial: w = I′ , that is, w contains only the starting symbol;
(2)		dead-end: d is the only nonterminal in w and |w|d = 1;
(3)		production: there exists some A ⊆ V and f : V ⇀ (Σ ∪ {ε}) with dom(f) ∩ A = ∅ such that
{Xa,A,f | a ∈ A} ∪ {YA,f }
are the only nonterminals which appear in w, each such nonterminal appears exactly once in w, and the nonterminal YA,f appears as the last letter of w; or
(4)		final: w ∈ Σ∗ , that is, the word contains no nonterminals.
Notice that, with such a property, the grammar would be EDT0L of index |V | + 1.
Notice that if a word w is a production as in case 3, as described above, then w = w′Y∅,∅ would imply that w′ ∈ Σ∗. This is clear as, from the definition of the normal form, Y∅,∅ would be the only nonterminal which may appear in such a normal form, i.e., there are no nonterminals of the form Xa,∅,f .
Suppose that β1, β2 ∈ (H′)∗ with I′ · (β1β2) ∈ Σ∗, and that w = I′ · β1 ∈ (Σ ∪ V )∗ is a word as in case 3, as above, with A ⊆ V and f : V ⇀ (Σ ∪ {ε}). In our construction, these sequences β1, β2 ∈ (H′)∗ correspond to some sequences α1 , α2 ∈ H ∗ in the grammar E for which
•		I · α1 ∈ (Σ ∪ dom(f) ∪ A)∗;
•		for each a ∈ A, we have |I · α1 |a ⩽ 1; and
•		for each b ∈ dom(f), we have |b · α2 | ⩽ 1, in particular, we have b · α2 = f (b).
Compare the above with the definition of LULT grammars as in Definition 3.4. In the remainder of this proof, we construct the tables H′ of E′ such that the ab ove properties hold and L(E) = L(E ′).
2.		Table tinit :
We begin the productions of our grammar E′ with a table tinit ∈ H′ defined as

v · tinit =

X Y if v = I′,
,{ },	{ },
otherwise.

Notice that applying this table preserves the property of a word belonging to one of the four forms described in part 1.1 of this proof. In the remainder of this proof, we notice that in each production of E′ , we may assume that tinit is the first table we apply, and that it is applied exactly once.
3.		Table tend :
We end the production of our grammar with the table tend ∈ H′ defined as
	v if v ∈ Σ,	
v · tend =	d if v = YA,f where either A ̸= ∅ or f ̸= ∅, d if v ∈ {I′, d}, ε otherwise.	

Notice that applying this table preserves the property of a word being in one of the four forms described in part 1.1 of this proof. Moreover, we notice that given a word w ∈ (Σ ∪ V ′)∗ in one of the forms described in part 1.1 of this proof, that w · tend ∈ Σ∗ if and only if either w ∈ Σ∗ or w = w′Y∅,∅ in which case we would have w′ ∈ Σ∗ (see part 1.1 of this proof).
4.		Tables th,B,g:
Let h ∈ H be a table from the grammar E , let B ⊆ V be a subset of nonterminals of E , and let g : V ⇀ (Σ ∪ {ε}) be a partial function with dom(g) ∩ B = ∅. We then introduce a new table th,B,g ∈ H′. Such a table corresponds to an application of the table h of E , and is intended to produce words as in case 3 of part 1.1 which end in the nonterminal YB,g (with some edge cases for invalid productions).
We begin our construction of this table by specifying that
•		σ · th,B,g = σ for each σ ∈ Σ;
•		d · th,B,g = d; and
•		I′ · th,B,g = d.
Thus, we see that if w ∈ (Σ ∪ V ′)∗ is a word as in case 1, 2 or 4 as in part 1.1 of this proof, then w · th,B,g is also a word of such a form. Thus, it only remains to specify the table such that we understand how it acts on word in the form described in case 3 of part 1.1.
Let A ⊆ V and f : V ⇀ (Σ ∪ {ε}) with dom(f) ∩ A = ∅; and let w be a word as in case 3 of part 1.1 which ends in the nonterminal YA,f . In the remainder of this part, we describe the word w · th,B,g , in particular, we specify the action of the table on the nonterminals of the form Xa,A,f and YA,f .
4.1.		Notation. For each C ⊆ V and each partial function k : V ⇀ (Σ ∪ {ε}) with dom(k) ∩ C = ∅, we define a monoid homomorphism LabelC,k : (Σ ∪ C ∪ dom(k))∗ → (Σ ∪ V ′)∗ such that

if v ∈ Σ
if v ∈ A
if v ∈ dom(k)

v
LabelC,k (v) := Xv,C,k
k(v)
for each v ∈ Σ ∪ C ∪ dom(k). From our choice of C and k, we see that LabelC,k is well-defined.
Let k : V ⇀ (Σ ∪ {ε}) be a partial function as above, then we write k ∈ End(Σ ∪ V )∗ for the table defined such that

k(v) v · k :=
v

if v ∈ dom(k) otherwise

for each v ∈ (Σ ∪ V ).
4.2.		Intention. Our intention is for our construction to have the following property. If there exists some β1 , β2 ∈ (H′)∗ such that w = I′ · β1 and I′ · (β1 th,B,g β2) ∈ Σ∗, then there exists some α1, α2 ∈ H∗ where
(I1)		I′ · (β1 th,B,g · β2) =I·(α1hα2);
(I2)		I′ · β1 = LabelA,f (I · α1) YA,f is a word as in case 3 of part 1.1; and
(I3)		I′· (β1 th,B,g) = LabelB,g (I · α1h) YB,g is a word as in case 3 of part 1.1.
Thus, the table tt,B,g of E′ behaves similarly to the table h of E except it performs additional replacements, i.e. the replacements given by f and g which are completely specified by the nonterminals used in the sentential form. Thus, our reason for including the nonterminals YA,f and YB,g in these words is so that this information is always present in our sentential form.
4.3.		Technical details. We label the elements of A as A = {x1, x2, ..., xk} ⊆ V . We then define two sets B(1), B(⩾2) ⊆ V as
B(1) := v ∈ V	|(x1x2	· · ·xk) ·	h|v	= 1	and	B(⩾2)	:= v ∈ V	|(x1x2 · ·	·xk)	·	h|v	⩾ 2	
where h ∈ H is the table as in th,B,g. We are then interested in the case where the sets B(1) and B(⩾2) satisfy the following 4 additional properties:
(T1) B(⩾2) ⊆ dom(g);
(T2) B = B(1) \ dom(g);
(T3) for each a ∈ A, we have a · h ∈ (Σ ∪ dom(g) ∪ B)∗ ; and
(T4) for each v ∈ dom(f), we have v · h ∈ (Σ ∪ dom(g))∗ with f(v) = g˜(v · h).
If any of these above properties (T1 – 4) are violated, then we define
Xa,A,f · th,B,g = ε	and	YA,f · th,B,g = d
for each a ∈ A, which produces a dead-end word as in case 2 of part 1.1. Otherwise, if properties (T1 – 4)
are satisfied, then we define
Xa,A,f · th,B,g = LabelB,g (a · h)	and	YA,f · th,B,g = YB,g	(1) for each a ∈ A. From the definition of B(1) , B(⩾2) and properties (T1 –4), we see that the applications of LabelB,g, as above in (1), are well-defined.
Notice that we may then completely describe the action of the tables th,B,g by repeating the ab ove construction for any valid values of A and f .
4.4.		Property. Suppose that w ∈ (Σ ∪ V ′)∗ is a word in the form described in case 3 of part 1.1. Then, from the construction of B(1) and properties T1 and T2, as above, we see that w · th,B,g is either a deadend word as in case 2 of part 1.1, or a production as in case 3 of part 1.1. Further, suppose additionally that there exists some word u ∈ (Σ ∪ V )∗ such that w = LabelA,f (u) YA,f . Then either w · th,B,g is a dead-end word; otherwise it follows from property T4 that w · th,B,g = LabelB,g (u · h) YB,g .
5.		Soundness and Completeness:
Suppose that w ∈ L(E), then from the definition of LULT grammars, we see that there must exist some sequence of tables α = h1h2 · · · hk ∈ H∗ such that for each factorisation α = α1α2 with α1 , α2 ∈ H∗ , and each nonterminal v ∈ V , either |I · α1 |v ⩽ 1 or |v · α2 | ⩽ 1. For each i ∈ {1, 2, ..., k - 1}, let
Ci = v ∈ V |I · (h1h2 · · · hk)|v ⩾ 1 .
We then see that
I·(h1h2···hi) ∈ (Σ ∪ Ci)∗
for each i ∈ {1, 2, ..., k - 1}. From our choice of sequence α = h1h2 · · · hk, we see that we can partition each set Ci into two disjoint subsets
Bi=	v∈V |I · (h1h2 · · · hi)|v =1 and	|v·(hi+1hi+1···hk)| ⩾2	⊆Ci and
Ci(∗) =	v ∈	V |I· (h1h2···hi)|v ⩾ 1 and	|v·	(hi+1hi+2···hk)| ⩽ 1	⊆	Ci.
In particular, the two sets correspond to the two cases in the definition of LULT grammars. Notice then that,	for	each i ∈ {1, 2, ..., k - 1}, we	can	define a partial function	gi :	V	⇀ (Σ ∪ {ε}) with dom(gi) = Ci(∗)	such that gi(v) = v · (hi+1hi+2 · · ·	hk)	for each v ∈ Ci(∗) .
We then see that the word w is generated by the grammar E′ as
w = I · tinit th1,B1,g1 th2,B2,g2 · · · thk-1,Bk-1,gk-1 thk,∅,∅ tend .
Thus, we see that L(E) ⊆ L(E′).
Suppose then that w ∈ L(E′) where w = I′ · (τ1τ2 · · · τk) with each τi ∈ H′. Then, from the definitions of the tables in H′, we may assume without loss of generality that
•		k ⩾ 3 with τ1 = tinit and τk = tend; and
•		for each i ∈ {2, 3, ..., k - 1}, the table ti is of the form τi = thi,Bi,gi where each hi ∈ H.
From our construction, we then see that w = I · (h2h3 · · · hk-1). Thus, we have L(E′) ⊆ L(E).
We thus conclude that L(E) = L(E′) where E′ is an EDT0L grammar of index |V | + 1.	□
Using Lemma 3.5, we have the following result.

w = w1w2 · · · wk ∈ L and n0,n1,n2,...,nk ∈ N

Lemma 3.6 (Proposition 25 in [25]). Let L ⊆ Σ∗ and c ∈/ Σ. If the language
L↑c∗ := cn0w1cn1w2cn2 ···wkcnk ∈ (Σ∪ {c})∗
is EDT0L, then L is EDT0L of finite index.
Proof. Suppose that E = (Σ ∪ {c}, V, I, H) is an EDT0L grammar for the language L ↑ c∗ . We then introduce a monoid homomorphism h : (Σ ∪ {c} ∪ V )∗ → (Σ ∪ V )∗ such that
h(c) = ε and h(v) = v for each v ̸= c.
From this, we define an EDT0L grammar E′ = (Σ, V, I, H′) where H′ = {th | t ∈ H} . Notice that since c is a terminal letter of the grammar E , deleting the letter c after every application of a table is equivalent to removing all instances of c at the end of a production. Thus, we have L(E′) = L(E) · h = L. It only remains to be shown that E′ is a EDT0L language of finite index. We demonstrate this by proving that E′ is a LULT grammar, after which we apply Lemma 3.5 to obtain our result.
To simplify this proof, we define a (length-preserving) monoid homomorphism φ : H∗ → (H′)∗ which we define such that φ(t) = th ∈ H′ for each t ∈ H. Notice also that H′ = φ(H). Moreover, since c is a terminal letter, we see that w · φ(α) = w · (αh) for each α ∈ H∗ and each w ∈ (Σ ∪ {c} ∪ V )∗ , that is, removing the letter c after every application of a table is equivalent to removing every c only at the end.
Suppose we are given a word w′ = w1w2 · · · wk ∈ L(E ′), then it follows that
w = w1cw2c2w3c3 · · · wkck ∈ L ↑ c∗.
We then see that there exists some α = h1h2 · · · hk ∈ H∗ with w = I · α and thus w′ = I · (αh) = I · φ(α). We now show that the sequence α′ = h′1h′2 · · · h′k ∈ H′, where each h′i = φ(hi), is a choice of a sequence of tables which generates w′ in E′ and satisfies the constraints of a LULT grammar (see Definition 3.4).
Suppose for contradiction that there is a factorisation α′ = α′1 α′2 and a nonterminal v ∈ V such that both |I · α′1 |v ⩾ 2 and |v · α′2 | ⩾ 2. Let α = α1α2 be the unique factorisation of α ∈ H∗ with α′1 = φ(α1) and α′2 = φ(α2). We then have the follow two observations:
•		Since |I · α′1 |v ⩾ 2, from the definition of φ, we see that |I · α|v ⩾ 2, that is, I · α1 contains at least 2 distinct instances of the variable v.
•		Since |v · α′2 | ⩾ 2, from the definition of the word w and the map φ, we see that v · α2 must contain a factor of the form σ1 cm σ2 where σ1, σ2 ∈ Σ and m ∈ N+.
From these observations, we see that the word w = I · (α1α2) must contain two distinct factors of the form σ1cmσ2. This contradicts our choice of word w. Hence, we conclude that either |I · α1′ |v ⩽ 1 or |v · α′2 | ⩽ 1 holds. From this, we then see that E′ is a LULT grammar.
From Lemma 3.5, we conclude that the language L is EDT0L of finite index.	□
4.		EDT0L is closed under application of string transducers
In this section, we furnish a proof that the family of EDT0L languages is closed under mapping by a string transducer, also known as a deterministic finite-state transducer, or a deterministic generalised sequential machine (deterministic gsm). We begin with the following definition.
Definition 4.1. A (deterministic) string transducer is a tuple M = (Γ, Σ, Q, A, q0, δ) where
•		Γ and Σ are the input and output alphabets, respectively;
•		Q is a finite set of states;
•		A ⊆ Q is a finite set of accepting states;
•		q0 ∈ Q is the initial state ; and
•		δ : Γ × Q → Σ∗ × Q is a transition function.
Given a language L ⊆ Γ∗ , we may then define the language M (L) ⊆ Σ∗ as

M(L) = u1u2···uk ∈ Σ∗

there exists some word w = w1w2 · · · wk ∈ L ⊆ Γ∗  such that δ(wi, qi-1) = (ui, qi) for each i ∈ {1, 2, ..., k} . where q0 is the initial state, and q1 , q2, ..., qk ∈ Q with qk ∈ A
We then say that M (L) is the image of L under mapping by the string transducer M.

Example 4.2. Here is a simple example of a string transducer, which computes the successor of a non-negative integer. A non-negative integer is represented as a word of the form w$ where w ∈ {0, 1}∗ is the minimum-length binary encoding of the integer (with the least significant digit appearing first), and $ is an end-of-input symbol. For example, we encode the numbers 0, 4, 10 and 11 as $, 001$, 0101$ and 1101$, respectively. Notice that 100$ would not be a valid string as it does not represent the number 1 with minimal length. The string transducer M = (Γ, Σ, Q, A, q0, δ) where Γ = Σ = {0, 1, $}, Q = {q0, q1, q2, q3, q4}, A = {q4}, and δ: Γ × Q → Σ∗ × Q is described by

δ(0, q0) = (1, q1),
δ(1, q0) = (0, q0),
δ($, q0) = (1$, q4),

δ(0,q1)=(0,q1),
δ(1,q1)=(1,q2),
δ($,q1)=($,q3),

δ(0, q2) = (0, q1),
δ(1, q2) = (1, q2),
δ($, q2) = ($,q4),

δ(0,q3)=(0,q3),
δ(1,q3)=(1,q3),
δ($,q3)=($,q3),

δ(0,q4)=(0,q3),
δ(1,q4)=(1,q3), δ($,q4)=($,q3)

computes the successor of a given number. For example, if $, 001$, 0101$ and 1101$ are given to the transducer, then it will output the words 1$, 101$, 1101$ and 00101$, respectively. We can represent the string transducer by the graph in Figure 3 where the vertices are given by the state set Q, and for each transition δ(u, q) = (v, q′) there is a labelled edge of the form q →u/v q′.

Figure 3. Add one to a number encoded in binary with an end marker.

Note that the state
•		q0 corresponds to prefixes of the form 1n for some n ∈ N;
•		q1 corresponds to prefixes of the form w0 where w ∈ {0, 1}∗ ;
•		q2 corresponds to prefixes which can be written as w0v1 where w, v ∈ {0, 1}∗;
•		q3 corresponds to invalid input sequences; and
•		q4 corresponds to valid sequences of the form w$ where w ∈ {0, 1}∗ .
For the interested reader, further examples of string transducers abound in the literature on self-similar groups, see for example [20].
The following definition provides some useful notation when working with string transducers.
Definition 4.3. Let M = (Γ, Σ, Q, A, q0, δ) be a string transducer. Then, for each pair of states q, q′ ∈ Q, and words w = w1w2 · · · wk ∈ Γ∗ and w′ ∈ Σ∗ , we write q →(w,w′) q′ if there is a path from state q to q′ which rewrites the word w to w′; that is, if there is a sequence of states q1 , q2, ..., qk+1 ∈ Q such that
•		q = q1 and q′ = qk+1; and
•		δ(wi, qi) = (ui, qi+1) for each i ∈ {1, 2, ..., k} where w′ = u1u2 · · · uk.
Notice then that
M(L) = {w′ ∈ Σ∗ | q0 →(w,w ) q where w ∈ L and q ∈ A}
for each L ⊆ Γ∗ .
We then have the following.
Lemma 4.4 (Corollary 4.7 in [16]). The family of EDT0L languages is closed under applying a string transducer. That is, if L is an EDT0L language, and M is a string transducer, then M (L) is also an EDT0L language.
Proof. Let L be an EDT0L language with EDT0L grammar E = (Γ,V,I,H), and M = (Γ, Σ, Q, A, q0, δ) be a string transducer. In this proof, we construct an EDT0L grammar E′ = (Σ, V ′, I′ , H′) for the language M (L), thus showing that M(L) is EDT0L.
In this paragraph we give an informal description of our construction. We construct our grammar E′ such that it contains a nonterminal for every choice of nonterminal v ∈ V of E , and every choice of states q, q′ ∈ Q of M . That is, E′ will have nonterminals of the form Xv,q,q′ where v ∈ V and q, q′ ∈ Q. We construct E′ such that it has the property that, if
w = w0Xv1 ,q1 ,q1′ w1Xv2 ,q2,q2′ w2 · · · Xvk ,qk,qk′ wk	(2) is a sentential form that appears in some production of E′ where each wi′ ∈ Σ∗ , then there exists some sentential form
w = w0v1w1v2w2 · · · vkwk
which appears in a production of E where each wi ∈ Γ∗ such that
•		q0 →(w0,w′0) q1,
•		qi →(wi,wi′) qi+1 for each i ∈ {1, 2, ..., k - 1} and
•		qk →(wk ,wk′ ) q′ for some q′ ∈ A.
That is, the words wi′ in (2) correspond to words in Γ∗ which have been rewritten by M , and the nonterminals Xvi ,qi ,q′ are placeholders for words which are yet to be rewritten by M . Moreover, the states qi , qi′ are included to ensure that the sentential form w′ in (2) corresponds to a path in the automaton M . We achieve this by constructing the tables of E′ such that, for every replacement
v · h = w0u1w1u2w2 · · ·ukwk,	(3)
where v ∈ V , h ∈ H , each wi ∈ Γ∗ and each ui ∈ V , we have a table h′ ∈ H′ with the property that
Xv,q,q′ · h′ = w0′ Xu1,q1,q1′ w1′ Xu2,q2,q2′ w2′ · · · Xuk,qk,qk′ wk′	(4)
where
•		q →(w0,w0′) q1,
•		qi →(wi,wi′) qi+1 for each i ∈ {1, 2, ..., k - 1} and
•		qk →(wk,wk′) q′.
Thus, the application of the table h′ as in (4) corresponds to the application of h in (3) where each word in Γ∗ has been rewritten by M , and we are representing a path in M from q to q′ . It then follows that the language of all words in M (L) corresponds to the union of the languages obtained from EDT0L grammars with initial nonterminals of the form XI,q0,a where a ∈ A: we construct our grammar to correspond to this union by introducing a new start nonterminal I′ along with some additional tables tinit,a ∈ H′ . We finish this informal description of our construction by noting that there may be cases where there are no choices of states qi , qi′ ∈ Q for which we can define an expansion as in (4), thus we introduce an additional nonterminal d which we call a dead-end symbol which stops the production in such situations.
1.		Nonterminals:
The set of nonterminals of E′ is given as
V′ = {Xv,q,q′ | v ∈ V and q,q′ ∈ Q} ∪ {I′, d}.
Here, the nonterminals Xv,q,q′ of E′ correspond to nonterminals v ∈ V of E which generate words which are read by the string transducer M during a path from state q to q′ ; the nonterminals I′ and d are disjoint symbols which are used as the starting symbol and a dead-end symbol respectively. In our grammar, we ensure that every table maps d to itself. Thus, if a d appear in a sentential form, then there is no way of removing it to continue to generate a word in the language.
2.		Initial tables tinit,a ∈ H′:
For each accepting state a ∈ A of the string transducer M , we introduce a table tinit,a ∈ H′ such that v	if v ∈ Σ,
v · tinit,a = XI,q0,a ifv=I′,
d	otherwise.
(Note that we write v · tinit,a = v for v ∈ Σ only to comply with Definition 3.1, in our grammar to produce a word in the language such tables will only be applied to the sentential form I′.)
The remaining tables in H′ are modified versions of tables in H , described as follows.

3.		Tables th,r ∈ H′:
For each h ∈ H and each v ∈ V , we have
v · h = w0x1w1x2w2 · · · xkv wkv
for some kv ∈ N where each wi ∈ Σ∗ and each xi ∈ V . Then for each pair of states q, q′ ∈ Q, we define a finite set Ch,v,q,q′ ⊂ (Σ ∪ V ′)∗ as

u0 Xx1,q1,q1′ u1 Xx2,q2,q2′ u2 Ch,v,q,q′ =
	xkv ,qkv,qk′ v ukv

q →(w0,u0) q1,	
qi′ →(wi ,ui) qi+1 for each 1 ⩽ i < kv ,

and qk′ →(wkv ,ukv) q′

Notice that each set Ch,v,q,q′ is finite as there are only finitely many choices for each state qi′ ∈ Q; the state q1 is completely determined from q and w0; for each i ⩾ 1, that state qi+1 is completely determined from qi′ and wi ; and the words ui ∈ Σ∗ are completely determined from the state q and states qi .
From the sets Ch,v,q,q′ , we define a set of functions Rh ⊂ ((Σ ∪ V ′)∗ ∪ {d})V ×Q×Q as

Rh = r: V × Q × Q→ ((Σ∪V′)∗ ∪ {d})

where r(v, q, q′) ∈ Ch,v,q,q′ ∪ {d}
for each v ∈ V and q, q′ ∈ Q
Notice that Rh is finite, in particular,
|Rh| ⩽ Y Y Y(|Ch,v,q,q′|+1).
v∈V q∈Q q′∈Q
Notice that we added d as an option in Rh so that there is always a choice for the value of r(v, q, q′), in particular, so that there is a choice when Ch,v,q,q′ is empty.
For each r ∈ Rh , we then define a table th,r ∈ H′ such that
Xv,q,q′ · th,r = r (v, q , q )
for each v ∈ V , and each q, q′ ∈ Q.
4.		Soundness and completeness:
Suppose that w ∈ L(E ′), then there must exist some τ1, τ2, ..., τk ∈ H′ such that
w = I′ · (τ1τ2 · · · τk).
From the definition of the initial tables tinit,a , we see that
•		τ1 = tinit,a for some a ∈ A; and
•		τi = thi ,ri for each i ̸= 1.
From the construction of the tables of the form th,r , the word
u=I·(h2h3···hk)∈L(E)
has the property that q0 →(u,w) a, and thus w ∈ M (L(E)). Hence, M(L(E)) ⊆ L(E′).
Suppose that w ∈ M (L(E)), then there exists some word u ∈ L(E) and an accepting state a ∈ A such that q0 →(u,w) a. Thus, there exists a sequence h1h2 · · · hk ∈ H∗ such that
u = I · (h1h2 · · ·hk) ∈ L(E).
From the construction of our tables, we then see that
w = I · (tinit,a th1,r1 th2,r2 · · · thk,rk )
for some choice of functions r1 , r2 , ..., rk. Hence, we see that L(E′) ⊆ M (L(E)).
We now conclude that L(E′) = M (L(E)), and thus the family of EDT0L languages is closed under mapping by string transducer.
The following lemma, which makes use of string transducers, will be used in the next section. Recall that a subset W ⊂ Γ+ is an antichain with respect to prefix order if for each choice of words u, v ∈ W , the word u is not a proper prefix of v.
Lemma 4.5. Let W ⊂ Γ+ be a finite antichain with respect to prefix order. For each word w ∈ W , we fix a word xw ∈ Σ∗ . Define a map f : P(Γ∗) → P(Σ∗) as
f(L) = {xw1 xw2 · · · xwk ∈ Σ∗ | w1w2 · · · wk ∈ L where each wi ∈ W}.
Then, there is a string transducer M = (Γ, Σ, Q, A, q0, δ) such that f(L) = f(L ∩ W∗) = M (L).

Proof. Firstly we notice that if W = ∅, then f(L) = ∅ for each language L ⊆ Γ∗ . In this case, any such string transducer with A = ∅ satisfies the lemma statement. Thus, in the remainder of this proof, we assume that W ̸= ∅.
Let w ∈ Γ∗ be a word for which w ∈ W∗ . Then, since W is a finite antichain with respect to the prefix order, there is a unique factorisation of w as w = w1w2 · · · wk where each wi ∈ W.
We construct a string transducer M = (Γ, Σ, Q, A, q0 , δ) as follows. For each proper prefix u ∈ Γ∗ of a word w ∈ W , we introduce a state qu ∈ Q. The initial state is q0 = qε , and the set of accepting states is A = {qε}. Further, our automaton has one additional state qfail which is a fail state; that is,
δ(g, qfail) = (ε, qfail)
for each g ∈ Γ. We then specify the remaining transitions as follows.
For each state qu with u ∈ Γ∗ , and each g ∈ Γ, we define the transition
(xw , qε ) if w = ug ∈ W,
δ(g, qu) =	(ε, qug )	if ug is a proper prefix of some w ∈ W,
(ε, qfail ) otherwise.
We then see that the string transducer M is now completely specified. It is clear from our construction that f(L) = M(L) for each L ⊆ Γ∗.
5.		EDT0L word problem
A standard approach to showing that having word problem in a given formal class C is invariant under change of finite generating set is to rely on the fact that C is closed under inverse monoid homomorphism. For example, this holds when C is any class in the Chomsky hierarchy, indexed, ET0L, and finite-index EDT0L (for the class of finite-index EDT0L languages, see [31, Theorem 5]).
As noted in the introduction, EDT0L languages are not closed under taking inverse monoid homomorphism. In particular, the language L1 = {a2n | n ∈ N} can easily be shown to be EDT0L, however, the language L2 = {w ∈ {a, b}∗ | |w| = 2n for some n ∈ N}, which can be written as an inverse monoid homomorphism of L1 , is known to not be EDT0L (see either the proof of Theorem 1 on p. 22 of [30], or Corollary 2 on p. 22 of [12]). Instead, we prove Proposition A via the following steps.
Recall from Section 2 that if G is infinite then it has geodesics of arbitrary length.
Lemma 5.1. Suppose that G is an infinite group with finite monoid generating set X. Fix a finite number of words u1 , u2, ..., uk ∈ X∗ . Then there exists a choice of non-empty words w1 , w2, ..., wk ∈ X∗ \ {ε}, such that each wi = 1 and
W = {w1u1, w2u2,..., wkuk}
is an antichain in the sense of Lemma 4.5; that is, for each choice of words x, y ∈ W , the word x is not a proper prefix of y.
Proof. We begin by constructing the words w1 , w2, ..., wk as follows.
Let α1 ∈ X be a nontrivial generator, that is, α1 ̸= 1; then let β1 ∈ X∗ be a geodesic with α1β1 = 1 (Notice that if X is a symmetric generating set, then we may choose β1 = α1-1). From this selection, we then define w1 = α1β1 . We now choose the words w2 , w3, ..., wk sequentially as follows.
For each i ⩾ 2, we choose a geodesic αi ∈ X∗ with length |αi | = |αi-1βi-1 | + 1. We then choose a geodesic βi ∈ X∗ such that αiβi = 1 (Notice that if X is a symmetric generating set, then we may choose βi = αi-1). Then, define wi = αiβi.
We have now selected a sequence of words w1 , w2, ..., wk . For each word wi, let γi denote the longest prefix which is a geodesic. We then notice that
|γi-1| < |wi-1| < |αi| ⩽ |γi|
for each i ∈ {2, 3, ..., k}. Thus, |γ1 | < |γ2 | < · · · < |γk| and |γi| < |wiui | for each i.
We now see that, if wiui is a proper prefix of some word v ∈ X∗ , then γi is also the longest prefix of v which is a geodesic. Hence, we conclude that the set

is an antichain as required.

W = {w1u1, w2u2,..., wkuk}
□
Recall from the introduction that the word and coword problem for a group G with respect to a generating set X are denoted as

WP(G, X) := {w ∈ X∗ | w = 1}

and

coWP(G,X) :=X∗ \ WP(G, X).

We have the following result for groups with EDT0L (co-)word problem.
Proposition 5.2. Let G be a group with finite monoid generating set X. If the word problem WP(G, X) is EDT0L, then it is EDT0L of finite index. Moreover, if the coword problem coWP(G, X) is EDT0L, then it is EDT0L of finite index.
Proof. Notice that if G is finite, then this result follows from the fact that the word problem of a finite group is a regular language (see [1, Theorem 1]) and Lemma 3.3. Thus, in the remainder of this proof we may assume that G is an infinite group.
Let c be a letter which is disjoint from the alphabet X = {x1, x2, ..., xn}. From Lemma 5.1, there exists a choice of words w1, w2, ..., wn, wn+1 ∈ X∗ such that
W = {w1x1,w2x2,...,wnxn,wn+1}
is an antichain with respect to the prefix order where each wi = 1.
We define a map f : P(X∗) → P((X ∪ {c})∗) as

f(L) = yi1yi2···yik ∈ (X ∪ {c})∗
where ui = yi = xi for each i ∈ {1, 2, ..., n}, un+1 =

(wi1 ui1)(wi2 ui2) · · · (wik uik) ∈ L
where each ij ∈ {1, 2, ..., n + 1}
ε, and yn+1 = c. From Lemma 4.5, f is a mapping
by string transducer.
Notice that f (WP(G, X)) = WP(G, X) ↑ c∗ and f (coWP(G, X)) = coWP(G, X) ↑ c∗. In particular, given some word v = v1v2 · · · vk ∈ X∗ , if v ∈ WP(G, X) then
v′ := (wn+1)i1v1(wn+1)i2v2(wn+1)i3v3 · · · (wn+1)ik vk(wn+1)ik+1 ∈ WP(G,X)
for each ij ∈ N where wn+1 ∈ X∗ is the word as in the set W given above. Then f (v′) is the word ci1 v1 ci2 v2 · · · cik vk cik+1 ∈ WP(G, X) ↑ c∗ . Hence, we can construct any word in WP(G, X) ↑ c∗ in this way. A similar statement also holds for coWP(G, X) and coWP(G, X) ↑ c∗ .

Thus, □

(resp.

From Lemma 4.4, we see that WP(G, X) ↑ c∗ and coWP(G, X) ↑ c∗ are EDT0L languages. from Lemma 3.6, we conclude that WP(G, X) and coWP(G, X) are both EDT0L of finite index.
We then obtain the following result as a corollary to the above Proposition.
Proposition A. Let G be a group with finite monoid generating sets X and Y . If WP(G, X) coWP(G, X)) is EDT0L, then WP(G, Y) (resp. coWP(G, Y)) is EDT0L of finite index. These results also hold if Y instead generates a submonoid of G. In particular, this implies that, if a word problem is EDT0L, then it is EDT0L of finite index; and that having a word problem that is EDT0L of finite index is independent of choice of generating set.
Proof. Let X be a finite monoid generating set for G, let Y be a finite monoid generating set for a submonoid of G, and suppose that WP(G, X) (resp. coWP(G, X)) is EDT0L. Then by Proposition 5.2, WP(G, X) (resp. coWP(G, X)) is EDT0L of finite index. Let ψ : Y ∗ → X∗ be a monoid homomorphism such that ψ(y) =G y for each y ∈ Y . Then WP(G, Y ) = ψ-1 (WP(G, X)) (resp. coWP(G, Y ) = ψ-1 (coWP(G, X))). From [31, Theorem 5], it is known that the class of EDT0L languages of finite index is closed under inverse monoid homomorphisms, thus we conclude that the language WP(G, Y ) (resp. coWP(G, Y )) is EDT0L of finite index, so in particular the language is EDT0L.
6.		Non-branching multiple context-free languages
In this section, we introduce non-branching multiple context-free grammars, and define what it means for such a grammar to be non-permuting and non-erasing. We then show that every finite-index EDT0L language can be generated by a non-branching multiple context-free grammar which is both non-permuting and non-erasing. We conclude this section by providing a normal form for grammars of this type which is then used throughout the proof of our main result in Section 7.
Definition 6.1 (Non-branching multiple context-free grammar). Let Σ be an alphabet, and Q be a finite set of symbols called nonterminals where each H ∈ Q has a rank some positive integer. We define an initiating rule to be an expression of the form
H(u1,u2,...,uk) ←
where H ∈ Q has rank k, and each ui ∈ Σ∗ . A propagating rule is an expression of the form
K(u1,u2,...,um) ← H(x1,x2,...,xn)
where
•		K ∈ Q has rank m,
•		H ∈ Q has rank n,
•		x1 , x2, ..., xn are abstract variables,
•		each ui ∈ (Σ ∪ {x1, x2, ..., xn})∗, and
•		for each i ∈ {1, 2, ..., n}, the word u1u2 · · · um contains at most one instance of xi.
A non-branching multiple context-free grammar is a tuple M = (Σ, Q, S, P ) where Σ is an alphabet, Q is a finite set of nonterminals, S ∈ Q is the starting nonterminal which has rank 1, and P is a finite set of rewrite rules each of which is either initiating or propagating.
A word w ∈ Σ∗ is generated by the grammar if there is a sequence of rules from M starting with an initiating rule, then followed by propagating rules, and finishing at S (w), that is, if there exists a sequence
S(w) ← H1 (v1,1 , v1,2, ..., v1,m1 ) ← H2(v2,1, v2,2, ..., v2,m2 ) ← · · · ← Hk (vk,1 , vk,2, ..., vk,mk) ← where each Hi ∈ Q with Hk(vk,1, vk,2, ..., vk,mk) ← initiating, each vi,j ∈ Σ∗ , and each replacement follows from P . We refer to the symbols xi used to define a propagating rule as the variables of the rule. We refer to a sequence, as above, as a derivation of the word w. The language generated by M is the set of all words generated by M , that is, the set of all words which have a derivation as above.
A non-branching multiple context-free grammar is non-permuting if in each propagating replacement rule, the variables xi which appear in u1u2 · · · um , appear in the same order as on the right-hand side of the rule. Moreover, a grammar is non-erasing if for each propagating replacement rule, each variable xi which appears in the right-hand side also appears in the word u1u2 · · · um . Notice then that if a non-branching multiple context-free grammar is both non-permuting and non-erasing, then we have
u1u2···um ∈ Σ∗x1Σ∗x2Σ∗···xnΣ∗
for each propagating rule.
As noted in the introduction, we call a non-permuting non-erasing non-branching multiple context-free grammar a restricted multiple context-free grammar, abbreviated as R-MCFG.
Proposition 6.2. Let L be EDT0L of finite index. Then L is generated by an R-MCFG.
Proof. Let E = (Σ, V, I, H) be an EDT0L grammar of index n. In this proof, we construct an R-MCFG M = (Σ,Q,S,P).
For each sequence v1v2 · · · vk ∈ V ∗ with length k ⩽ n, we introduce a nonterminal Hv1v2···vk ∈ Q with rank k + 1 to our non-branching multiple context-free grammar. Notice then that there are finitely many such nonterminals, in particular, |Q| ⩽ (|V | + 1)n.
In our construction, a configuration of the form
Hv1v2···vk (u0, u1, u2,..., uk),
where each ui ∈ Σ∗, corresponds to a sentential form u0v1u1v2u2 ...vkuk generated by the EDT0L grammar E . Thus, the starting nonterminal of our non-branching multiple context-free grammar is S=Hε.
We begin our production by introducing an initiating rule of the form
HI (ε, ε) ←
which corresponds to a word containing only the starting symbol I of E. For each table h ∈ H of our EDT0L grammar, we introduce a monoid endomorphism
h: (Σ ∪ V ∪ {x0, x1, x2,..., xn})∗ → (Σ ∪ V ∪ {x0, x1, x2,..., xn})∗
such that h(u) = h(u) for each u ∈ Σ ∪ V , and h(xi) = xi for each i ∈ {0, 1, 2, ..., n}. We note here that these additional disjoint symbols x0, x1, ..., xn will correspond to words in Σ∗.
For each nonterminal Hv1v2···vk ∈ Q, we consider the word
Wh,H,v1v2···vk := h(x0v1x1v2x2v3x3 · · ·vkxk) ∈ (Σ ∪ V ∪ {x0, x1, x2,..., xk})∗.
Notice that Wh,H,v1v2···vk contains exactly one instance of each symbol x0, x2, ..., xk, and that these symbols appear in the same order in which they were given to the map h.
If the word Wh,H,v1v2···vk contains at most n instances of letters in V , then we may decompose it as
Wh,H,v1v2···vk = w0v1′w1v2′w2 · · · vm′ wm
where m ⩽ n, each wi ∈ (Σ ∪ {x0, x1 , x2, ..., xk})∗ , and each vi′ ∈ V . We introduce a propagating rule
Hv1′ v2′ ···vm′ (w0 , w1 , ..., wm ) ← Hv1 v2 ···vk (x1 , x2 , ..., xk ).
Notice that this new rule is non-erasing and non-permuting from our earlier observations on Wh,H,v1v2 ···vk .
From our construction, we see that the non-branching multiple context-free language described in this proof is both non-permuting and non-erasing, so is an R-MCFG, and generates the finite-index EDT0L language L(E).	□
Remark 6.3. The converse of Proposition 6.2 also holds, that is, every R-MCFG produces an EDT0L language of finite index. In particular, given an R-MCFG one may construct an equivalent EDT0L language with nonterminals of the form XH,k where H is a predicate of the R-MCFG and k ∈ {0, 1, ..., rH} where rH is the rank of H. One would then construct the EDT0L grammar such that productions of the R-MCFG of the form H(u1, u2, ..., uk) correspond to sentential forms XH,0 u1 XH,1 u2 XH,2 · · · uk XH,k of the EDT0L grammar. We do not prove this result as it is not required by the results in this paper.
We now describe three types of replacement rules for non-branching multiple context-free grammars as follows. These types of rules will be used to describe a normal form for R-MCFGs. We begin with insertions rules as follows.
Definition 6.4. A replacement rule is a left or right insertion if it is of the form
K(x1, x2,..., xi-1, σxi, xi+1,..., xk) ← H(x1, x2,..., xk)
or
K(x1,x2,...,xi-1,xiσ,xi+1,...,xk) ← H(x1, x2,..., xk), respectively, for some σ ∈ Σ and i ∈ {1, 2, ..., k}.
We then require a type of replacement rule which allows us to move the variables xi around. We do so using merge rules defined as follows.
Definition 6.5. A replacement rule is a left or right merge if it is of the form
K(x1,x2,...,xi-1,xixi+1,ε,xi+2,...,xk) ← H(x1, x2,..., xk)
or
K(x1,x2,...,xi-1,ε,xixi+1,xi+2,...,xk) ← H(x1, x2,..., xk), respectively, for some i ∈ {1, 2, ..., k - 1}.
Further, we require a type of replacement rule which generate words as follows.
Definition 6.6. An accepting replacement rule is one of the form
S(x1x2 · · · xk) ← H(x1, x2, ..., xk)
where S is the starting nonterminal of the non-branching multiple context-free grammar.
From these types of replacement rules as described in the previous definitions, we may now define normal forms for R-MCFGs as follows.
Definition 6.7. An R-MCFG M = (Σ, Q, S, P) is in normal form if there exists some k ⩾ 2 such that every nonterminal H ∈ Q, except for the starting nonterminal S , has rank k, and each replacement rule in P is either initiating of the form
H(ε,ε,ε,ε,...,ε) ←,
| {z }
k components
a left or right insertion (as in Definition 6.4), a left or right merge (as in Definition 6.5), or an accepting rule (as in Definition 6.6). Moreover, every production of the grammar has the form
S(w) ← H(w, ε, ε, ..., ε) ← · · · ← K(ε, ε, ..., ε) ←
where w ∈ Σ∗ and H, K ∈ Q.
The use of the term ‘normal form’ in the above definition is justified by the following lemma.
Lemma 6.8. Suppose that L ⊆ Σ∗ is the language of an R-MCFG. Then, L can be generated by an R-MCFG in normal form.
Proof. Let M = (Σ, Q, S, P) be an R-MCFG. Let k ∈ N be the smallest value for which both k ⩾ 2 and for each replacement rule
H(w1,w2,...,wℓ) ←	and	H(w1,w2,...,wn) ← K(x1, x2,..., xm)
in P , we have k ⩾ max{ℓ, m, n}. Such a constant k exists as there are finitely many replacement rules.
In this proof, we construct three R-MCFGs M′, M′′ and M′′′ . At the end of this proof, we have a grammar M′′′ in normal form which generates the same language as M.
The techniques used in this proof are quite straightforward. In step 1, we ensure that all nonterminals have the same rank by simply padding each predicate with empty components, as required; in step 2, we unfold each production of the grammar into a sequence of rules each of the form Definitions 6.4, 6.5 and 6.6 or a trivial rule of the form
H(x1,x2, · · · ,xk) ← K(x1, x2,..., xk);
then finally, in step 3, we remove these additional trivial rules to produce a grammar in normal form.
Step 1: We construct an R-MCFG, denoted as M′ = (Σ, Q′, S′, P′), from M as follows.
For each nonterminal A ∈ Q of the grammar M , we introduce the nonterminals
A0, A1, A2, ..., Ak ∈ Q′.
In our construction of M′, we ensure that if
Ai(w1,w2,...,wk)
appears in a derivation, then wj = ε for each j > i. Thus, the subscript of these nonterminals count the number of non-empty components. Moreover, we introduce the nonterminals
S′, F′ ∈ Q′
to our grammar M′. These additional nonterminals are used in the grammar M′ as follows.
The grammar M′ has the replacement rules
S′(x1x2 ...xk) ← S1(x1, x2, ..., xk)	and F′(ε, ε, ε, ε, ..., ε) ←
| {z }
k components.
For each replacement rule
H(w1, w2, ..., wℓ) ←
in P , we introduce a replacement rule
Hℓ(w1x1, w2x2,..., wℓxℓ, xℓ+1, ..., xk) ← F′(x1, x2,..., xk)
to P ′. Moreover, for each replacement rule of the form
H(w1,w2,...,wn) ← K(x1,x2,...,xm)
in P , we introduce a replacement rule
Hn(w1,w2,..., (wnxm+1xm+2 · · · xk), ε,ε,...,ε) ← Km(x1,x2, ..., xk)
to P′. This completes our construction of M′.
Properties of M′ : We see that M′ generates exactly the same language as M and that all derivations in the grammar M′ have the form
S (w) ← S1 (w, ε, ε, ..., ε) ← · · · ← F (ε, ε, ..., ε) ← .
The nonterminal S′ only appears as the leftmost nonterminal of a derivation, and each nonterminal A ∈ Q′ \ {S′} has rank k.
Step 2: We construct an R-MCFG, which we denote as M′′ = (Σ, Q′′, S′, P′′), from M′ by unfolding each replacement of M ′ into a sequence of more basic replacements as follows.
The nonterminals of the grammar M′′ contain the nonterminals of M′, that is, Q′ ⊆ Q′′. In this stage of the proof, we show how to decompose the replacement rules of M′ into sequences of finitely many replacement rules, each of which of the form as described in Definition 6.7, or of the form
H(x1,x2,...,xk) ← K(x1, x2,..., xk).	(5)
In Step 3 of this proof, we complete our construction by removing the replacement rules of the form (5). Firstly, our grammar M′′ contains the replacement rules
S′(x1x2 · · ·xk) ← S1(x1,x2,...,xk)	and	F′(x1,x2,..., xk) ← which are both a part of the grammar M′.
Suppose that the grammar M′ has a replacement rule p ∈ P′ of the form
p: A(w1, w2,..., wk) ← B(x1, x2,..., xk)
where each
wi = ti zi,1 u[zi,1] zi,2 u[zi,2] · · · zi,ℓi u[zi,ℓi]
for some ℓi ∈ N, each zi,j ∈ {x1 , x2 , ..., xk}, ti ∈ Σ∗ and each u[xi] ∈ Σ∗ .
We then introduce a nonterminal of the form
Cp,n,m ∈ Q
for each n ∈ {1, 2, ..., k} and each m ∈ {0, 1, 2, ..., |u(xn)|}. Let each
u[xn] = un,1un,2 · · · un,|u[xn]| ∈ Σ .
We then introduce replacement rules to M′′ as follows.
•		Cp,1,0(x1,x2,...,xk) ← B(x1, x2,..., xk);
•		for each n ∈ {1, 2, ..., k} and each m ∈ 0, 1, 2, ..., u[xn] - 1 , we have
Cp,n,m+1 (x1 , x2 , ..., xn-1 , (xn un,m+1 ), xn+1 , ..., xk ) ← Cp,n,m (x1 , x2 , ..., xk );
•		for each n ∈ {1, 2, ..., k - 1}, we have
Cp,n+1,0 (x1 , x2 , ..., xk) ← Cp,n,|u[xn]| (x1 , x2 , ..., xk ).
Notice then that we have the following production
Cp,k,|u[xk]|(x1u[x1], x2u[x2],..., xku[xk]) ← · · · ← B(x1, x2,..., xk) in the grammar M′′.
We now introduce a finite number of nonterminals of the form
Dp,⃗v ∈ Q′′
where ⃗v = (v1, v2, ..., vk) ∈ (Σ∗)k is a vector with each
vi ∈ {x1, x2,..., xk}∗	and	v1v2 · · · vk = x1x2 · · · xk.
For the grammar M′ , we then introduce all replacements of the form
Dp,(x1 ,x2 ,...,xk) (x1 , x2 , ..., xk) ← Cp,k,|u[xk]| (x1 , x2 , ..., xk );
Dp,(v1 ,v2 ,...,vi-1 ,vi vi+1 ,ε,vi+2 ,...,vk) (x1 , x2, ..., xi-1 , xixi+1 , ε, xi+2, ..., xk)
← Dp,(v1,v2,...,vk) (x1 , x2 , ..., xk) for each ⃗v = (v1, v2, ..., vk) as before, and each i ∈ {1, 2, ..., k - 1}; and
Dp,(v1 ,v2 ,...,vi-1 ,ε,vi vi+1 ,vi+2 ,...,vk ) (x1 , x2 , ..., xi-1 , ε, xi xi+1 , xi+2 , ..., xk)
← Dp,(v1,v2,...,vk) (x1 , x2 , ..., xk) for each ⃗v = (v1, v2, ..., vk) as before, and each i ∈ {1, 2, ..., k - 1}.
Notice then that
Dp,⃗v (v1 , v2 , ..., vk ) ← Cp,k,|u[xk]| (x1 , x2 , ..., xk )
for each Dp,⃗v as above.
Let
Z = ((z1,1z1,2 · · · z2,ℓ1), (z2,1z2,2 · · · z2,ℓ2), ..., (zk,1 zk,2 · · · zk,ℓk)).
We then see that in the grammar M′′, we have
Dp,Z⃗ (w1′ ,w2′ ,...,wk′ ) ← · · · ← B(x1, x2,..., xk)
where each
wi′ = zi,1 u(zi,1) zi,2 u(zi,2) · · · zi,ℓi u(zi,ℓi), that is, wi = tiwi′ where ti ∈ Σ∗ . We then introduce a nonterminal of the form
Gp,n,m ∈ Q
for each n ∈ {1, 2, ..., k} and each m ∈ {0, 1, 2, ..., |ti |}. Let each
ti = ti,1ti,2 · · · ti,|ti| ∈ Σ∗.
We then introduce replacement rules to M′′ as follows.
•		Gp,1,|t1|(x1,x2,..., xk) ← Dp,Z⃗ (x1, x2,..., xk);
• for each n ∈ {1, 2, ..., k} and each m ∈ {1, 2, ..., |tn |}, we have
Gp,n,m-1 (x1 , x2 , ..., xn-1 , (tn,m xn), xn+1 , ..., xk) ← Gp,n,m (x1 , x2 , ..., xk);
•		for each n ∈ {1, 2, ..., k - 1}, we have
Gp,n+1,|tn+1 | (x1, x2,..., xk) ← Gp,n,0(x1, x2,..., xk); and
•		A(x1, x2,..., xk) ← Gp,k,0(x1, x2,..., xk).
We then see that in the grammar M′′ we now have the derivation
A(w1, w2,..., wk) ← · · · ← B(x1, x2,..., xk)
where each rule in the sequence is either of the form as described in Definition 6.7, or the form as in (5).
Properties of M′′ : Observe that the grammar M′′ generates exactly the same language as M′ , and thus as M . Moreover, the only thing preventing M′′ from being in normal form is that it contains rules of the form given in (5) which we remove in the following step.
Step 3:
Suppose that M′′ contains a replacement rule as in (5), that is, a replacement rule of the form
p: H(x1, x2,..., xk) ← K(x1, x2,..., xk).
Then, we modify M′′ by
•		removing the nonterminal K from Q′′ ;
•		removing the replacement rule p from P ′′ ; and
•		replacing each instance of the nonterminal K with H in each rule contained in P′′.
Notice that after this modification, the number of rules of the form (5) is reduced by one, and that the grammar generates the same language. Moreover, we notice by induction that we can remove all such rules. We refer to the resulting grammar as M′′′ = (Σ, Q′′′ , S′ , P′′′).
Conclusion:
From the properties of the grammar M′′ in step 2, and the procedure described in step 3, we see that we may generate a grammar M ′′′ in normal form for the language L.	□
7.		Proof of the main theorem
Our aim in this section is to prove Theorem C. From Proposition A, it suffices to prove this theorem for a specific generating set. Thus, we introduce the following language.
Definition 7.1. Let Σ = {a, b}, and let ∆ : Σ∗ → Z to be the monoid homomorphism defined such that ∆(a) = 1 and ∆(b) = -1. Let L ⊆ Σ∗ as
L= {w ∈ Σ∗ | ∆(w) =0}
represent the word problem for Z with respect to the generating set X = {1, -1}.
The remainder of this section is organised as follows. We begin by introducing the constant C (in Corollary 7.4) and the counterexample word W (see Definition 7.5 in Section 7.1). We note here that the word W belongs to the language L, as in Definition 7.1, as is used to show that L is not EDT0L by contradiction. Sections 7.2 and 7.3 introduce several constants and functions on words which are used throughout the proofs of technical lemmas in this section. These constants correspond to the lengths of certain factors of W . Our motivation for introducing these constants and functions is so that we can define and study the properties of n-decompositions. In Section 7.4, we introduce the important concept of an n-decomposition (in Definition 7.20), we then spend the rest of this subsection proving technical lemmas which are used later in this section. In Section 7.5, we prove three propositions (Propositions 7.28, 7.29 and 7.30) which are used to show that, in some way, having a decomposition would be maintained during the production of W of an R-MCFG for L (from this we obtain a contradiction). These three propositions are summarised and generalised in Proposition 7.31 in Section 7.6. In Section 7.7, we use Proposition 7.31 to prove Theorem C, then obtain Theorem D as a corollary to Theorem C.
In the remainder of this paper L, Σ, ∆, a and b shall refer to the values as in Definition 7.1. To simplify the proofs in this section, we extend ∆ : Σ∗ → Z to the domain of all k-tuples as follows.
Definition 7.2. Let w⃗ = (w1 , w2, ..., wk) ∈ (Σ∗)k be a tuple of words, then ∆(w⃗) := ∆(w1w2 · · · wk).
From Propositions 5.2 and 6.2 and Lemma 6.8, we see that in order to prove Theorem C, it is sufficient to show that L cannot be generated by an R-MCFG in normal form. We have the following lemma and corollary which place restrictions on the structure of such a grammar.
Lemma 7.3. If L is generated by some R-MCFG M = (Σ, Q, S, P ), then for each nonterminal H ∈ Q, there exists a constant CH ∈ Z such that if
S(w) ← · · · ← H(u1, u2, ..., uk) ← · · · ←
is a derivation in the grammar M, then ∆(u1u2 · · · uk) = CH.
For example, we have CS = 0 where S is the start non-terminal of the grammar.
Proof. Let some nonterminal H ∈ Q be chosen and suppose that there exists at least one derivation of the form
S(g) ← · · · ← H(v1, v2, ..., vk) ← · · · ←	(6)
where g, v1 , v2, ..., vk ∈ Σ∗. To simplify the explanations in this proof, we write β ∈ P∗ for the sequence of replacement rules which generate the configuration H(v1, v2, ..., vk), and α ∈ P∗ for the sequence of replacement rules which generates S(g) from H(v1, v2, ..., vk). We then write
S(g) ←α H(v1, v2,..., vk) ←β
to denote the sequence in (6).
From the definition of an R-MCFG, we then see that there exist words m0, m1, m2, ..., mk ∈ Σ∗ such that
S(m0p1m1p2m2 · · ·pkmk) ←α H(p1,p2,...,pk)
for each p1, p2, ..., pk ∈ Σ∗. In particular, if g and vi are as in (6), then g = m0v1m1v2m2 · · · vkmk.
Suppose that u1 , u2, ..., uk ∈ Σ∗ are words such that there exists some derivation
S(w) ← · · · ← H(u1, u2, ..., uk) ← · · · ←
in the grammar M, and write γ ∈ P∗ for the sequence of replacements which generates H(u1, u2, ..., uk). That is,
H(u1,u2,...,uk) ←γ .
We then see that
S(m0u1m1u2m2 · · ·ukmk) ←α H(u1,u2,...,uk) ←γ
is a derivation in the grammar L and thus
m0u1m1u2m2 · · · ukmk ∈ L.
Thus, from the definition of the language L, we see that
∆(m0 u1 m1 u2 m2 · · · ukmk) = 0.
Since ∆ is a monoid homomorphism onto an abelian group, we then see that
∆(u1u2 · · · uk) + ∆(m0m1 · · · mk) = 0.
We thus conclude by setting CH = -∆(m0m1 · · · mk).	□
From this lemma, we have the following immediate corollary.
Corollary 7.4. Let L be generated by some R-MCFG M = (Σ, Q, S, P). Then there exists a constant C = CM ⩾ 1 such that, if
S(w) ← · · · ← H(u1, u2, ..., uk) ← · · · ←
is a derivation in the grammar M, then |∆(u1u2 · · · uk)| ⩽ C.
Proof. For each nonterminal H ∈ Q, let CH ∈ Z be the constant as in Lemma 7.3. We then see that our result follows with the constant CM = max{|CH | | H ∈ Q} which is well-defined since Q is finite. □ 7.1.	Counterexample word. In the remainder of this section, suppose for contradiction that there exists an R-MCFG M = (Σ, Q, S, P ) in normal form recognising L. Moreover, write C for the constant in Corollary 7.4, and write k for the rank of the nonterminals in M that are not the starting nonterminal.
We show that such a grammar M cannot exist by constructing a word W ∈ L which cannot be generated by any derivation in M .
Definition 7.5. Let m = 24k + 2C + 5. We define the word W ∈ Σ∗ as
W = am2k T2k am2k
where T2k is defined recursively such that
T0 = b2 and Tn = amn (Tn-1)2mamn
for each n ∈ {1, 2, 3, ..., 2k}.
Remark 7.6. Figure 2 illustrates the word W for the values m = 4, k = 2 with the letter a represented by an up-step (1, 1) and b by a down-step (1, -1). Note that Definition 7.5 requires m = 24k + 2C + 5 so m = 4 is not a realistic value, but larger values of m would make the figure difficult to draw, and one can already start to see the general behaviour with these values. Here is a calculation of the word in this case. We have
2	4 16 4	16^ 4 16 48 16	64^ 16^ 4 16 48 168 64
T0 = b , T1 = a b a , T2 = a a b a a , T3 = a a a b a a a ,
256^ 64^ 16^ 4 16 48 168 648 256
T4 = a	a a a b a a a a ,
so
W=a512^a64^a16^a4b16a48a168a648a512.
Notice that in the word W , every factor of b is of length exactly 16.
In the remainder of this section, m denotes the constant in Definition 7.5. We then have the following observation of the words W and Tn from Definition 7.5.
Lemma 7.7. For each n ∈ {0, 1, 2, 3, ..., 2k}, we have ∆(Tn) = -2mn with
|Tn|a = 2(2m)n - 2mn and |Tn|b = 2(2m)n.
Moreover, we have ∆(W) = 0 and thus W ∈ L.
Proof. From the recursive definition of Tn in Definition 7.5, we have
∆(T0) = -2 and ∆(Tn) = 2m∆(Tn-1) +2mn
for each n ⩾ 1. From this recurrence, we find that
∆(Tn) = -2mn
for each n ⩾ 0. Thus, ∆(T2k) = -2m2k. Again from Definition 7.5, we then have
∆(W) = ∆(T2k) + 2 m2k =0.
From the recursive definition of Tn , we also see that
|T0|b =2 and |Tn|b =2m|Tn-1|b.
Thus, we see that |Tn |b = 2(2m)n for each n ∈ {1, 2, 3, ..., 2k}; and we find that
|Tn|a = |Tn|b+∆(Tn) = 2(2m)n - 2mn
as desired.	□
7.2.		Constants. We now introduce some constants which are used in the proofs below.
Definition 7.8. For n ∈ {1, 2, 3, ..., 2k}, we define
m2k+2-n - m
Λn = m2k+1-n	and	Bn =	.
m-1
Moreover, for each n ∈ {1, 2, 3, ..., 2k}, we define σn = 2Λn + 2Bn.
The constants are chosen so that they satisfy the following relations.
Lemma 7.9. For each n ∈ {1, 2, 3, ..., 2k}, we have 12Λn > 6Bn ⩾ 6Λn > σn > 0.

Proof. We observe that Λn, Bn > 0 for each n ∈ {1, 2, 3, ..., 2k}, and that
m2k+2-n - m
Bn =	= m + m2 + · · · + m2k+1-n	and	Λn = m2k+1-n.
m-1
We thus see that Bn ⩾ Λn . Moreover, since m ⩾ 2, we see that 2Λn > Bn .
Then, since σn = 2Λn + 2Bn, we see that
σn < 2Λn + 4Λn = 6Λn.
Thus, we have our desired inequalities.	□
7.3.		Functions on words and word weights. In this section, we require a function to extract the a∗ factors which appear as part of the prefix and suffix of a given word in Σ∗ . To accomplish this, we introduce the following function.
Definition 7.10. We define Affix : Σ∗ ×{◁, ▷} → Σ∗ such that for each word w ∈ Σ∗ , the word Affix(w, ◁) is the longest prefix of w of the form a∗ ; and Affix(w, ▷) is the longest suffix of w of the form a∗ .
For example, if w = aaababbabbba then Affix(w, ◁) = aaa and Affix(w, ▷) = a. In the next lemma we compute Affix for some words of particular interest.

mn+1 - m
m-1

= B2k+1-n

Lemma 7.11. For each n ∈ {1, 2, 3, ..., 2k} and each s ∈ {◁, ▷}, we have
Affi
x(Tn, s)| = m + m2 + · · · + mn = where Tn is as in Definition 7.5. Proof. Let s ∈ {◁, ▷}, then from Definition 7.5, we see that
|Affix(T0, s)| = 0 and |Affix(Tn, s)| = mn + Affix(Tn-1, s) for each n ⩾ 1. From this recurrence, it follows immediately that mn+1 - m
|Affix(Tn, s)| = m + m2 + · · · + mn =
m-1
for each n ∈ {1, 2, 3, ..., 2k}.
From this, we then have the following result on the affixes of W . Corollary 7.12. We have |Affix(W, s)| = B1 + m2k for each s ∈ {◁, ▷}.
Proof. From the definition of W in Definition 7.5, we see that
|Affix(W, s)| = |Affix(T2k, s)| + m2k
for each s ∈ {◁, ▷}. Thus, from Lemma 7.11, we see that
|Affix(W, s)| = B1 + m2k
for each s ∈ {◁, ▷} as desired.
We now define what it means for a word to be heavy or light as follows.
Definition 7.13. Let n ∈ {1, 2, 3, ..., 2k}, we say that a word u ∈ Σ∗ is n-heavy if it contains a factor of the form a2Λn , otherwise we say that u is n-light. Given a tuple w⃗ = (w1 , w2, ..., wk), we define the set of indices Ln (w⃗) ⊆ {1, 2, ..., k} such that i ∈ Ln (w⃗) if and only if wi is an n-light word.
We then define the following function on n-heavy words.
Definition 7.14. Let u ∈ Σ∗ be an n-heavy word, we then define
•		segn (u, ◁) = x to be the shortest prefix of u such that u = xa2Λn u′; and
•		segn (u, ▷) = x to be the shortest suffix of u such that u = u′a2Λnx.
In the above, it should be understood that u′ ∈ Σ∗.
We now define the functions Remn : Σ∗ → Σ∗ as follows.
Definition 7.15. For n ∈ {1, 2, 3, ..., 2k}, we define Remn : Σ∗ → Σ∗ such that
•		if u ∈ Σ∗ is n-light, then Remn(u) = u; otherwise
•		if u ∈ Σ∗ is n-heavy, then Remn(u) = segn(u, ◁) seg(u, ▷).
Notice that in the second case, the word u is n-heavy, and thus it is well-defined.

We now define an additional function as follows.
Definition 7.16. We define the function Strip : Σ∗ → Σ∗ such that

Strip(u) :=

ε if u = Affix(u, ◁) = Affix(u, ▷), u′ where u = Affix(u, ◁) u′ Affix(u, ▷) otherwise. That is, Strip(u) is the word obtained by removing all leading and trailing instances of a from u. For example, Strip(aaababbabbba) = babbabbb. We observe the following. Lemma 7.17. For each n ∈ {1, 2, 3, ..., 2k}, we have
n+1
∆(Strip(T )) =-2mn-2m m
n	m-1
Moreover, for n ∈ {1, 2, 3, ..., 2k}, let wn be the word
wn = Affix(Tn,▷)TnAffix(Tn,◁), then, for each factor u of wn, we have |∆(u)| ⩽ |∆(Strip(Tn))|. Proof. From the recursive formula given in Definition 7.5, we see that
∆(Strip(Tn)) = 2m∆(Tn-1) -∆(Affix(Tn-1,◁)) - ∆(Affix(Tn-1, ▷))
for each n ⩾ 1. Thus, from Lemmas 7.7 and 7.11, we see that
mn - m
∆(Strip(T )) = 2m(-2mn-1) - 2
n	m-1
mn - m
= -4mn - 2
m-1
mn+1 - m
= -2mn-2m m,
m-1
as desired.
Considering the factors u of w1 = a2mb4ma2m = Affix(T1 , ▷) T1 Affix(T1, ◁), we see that -4m = ∆(b4m) ⩽ ∆(u) ⩽ ∆(a2m) = 2m.
Thus, |∆(u)| ⩽ 4m = |∆(Strip(T1))|.
Suppose, for induction, that |∆(v)| ⩽ |∆(Strip(Tn-1))| for every factor v of the word wn-1 = Affix(Tn-1, ▷) Tn-1 Affix(Tn-1, ◁)
for some value n ∈ {2, 3, ..., 2k}. Let u be a factor of
wn = Affix(Tn,▷)TnAffix(Tn,◁).
Notice from Lemmas 7.7 and 7.11 that
∆(wn) = ∆(Tn) + ∆(Affix(Tn, ◁)) + ∆(Affix(Tn, ▷))
-2mn + 2 mn+1 -m m-1

=2

mn - m
m-1

From Definition 7.5 and Lemma 7.11, we see

(7)

wn = aB2k+1-n Tn aB2k+1-n = amn+B2k+1-n (Tn-1)2m amn+B2k+1-n
and thus, the factor u falls into one of the following 4 cases:
Case 1:		The factor u has the form
u = ai(Tn-1)2maj
where i,j ∈ {0, 1, 2, ..., mn + B2k+1-n}. In this case, we see that
n
-4mn = 2m∆(Tn-1) = ∆((Tn-1)2m) ⩽ ∆(u) ⩽ ∆(wn) = 2m m ⩽ 2mn. m-1
From this, we then see that |∆(u)| ⩽ 4mn ⩽ |∆(Strip(Tn))| as desired.
Case 2:		The factor u has the form
u = ai(Tn-1)jv
where i ∈ {0, 1, 2, ..., mn + B2k+1-n}, j ∈ {0, 1, 2, ..., 2m - 1} and v is a factor of Tn-1.
From our inductive hypothesis we see that
(2m - 1)∆(Tn-1) - |∆(Strip(Tn-1))| ⩽ ∆(u) ⩽ (mn + B2k+1-n) + |∆(Strip(Tn-1))|.
From Lemmas 7.7 and 7.11, we see that
∆(u) ⩾ (2m - 1)∆(Tn-1) - |Strip(Tn-1)| n
= -(2m - 1)2mn-1 - 2mn-1 -2m -m m-1
mn - m
= -4mn - 2m	m
m-1
n+1
=-2mn-2m	m = -|∆(Strip(T ))|
m-1	n
and
∆(u) ⩽ (mn + B2k+1-n) + |∆(Strip(Tn-1))|
mn+1 - m	mn - m = mn + m m + 2mn-1 + 2m	m m-1	m-1
mn - m	mn - m = 2mn + m m + 2mn-1 + 2m m m-1	m-1 mn - m ⩽ ^2mn + 2mn-1 + 2mn-1 + 2 m-1 mn - m ⩽ 2mn + 4mn-1 + 2 m-1
n	n+1 ⩽ 2mn +2mn +2m m = 2mn +2m	m = |∆(Strip(Tn))| m-1	m-1 where some of the above inequalities hold since m ⩾ 2.
From this, we then see that |∆(u)| ⩽ |∆(Strip(Tn))| as desired.
Case 3:		The factor u has the form
u = v(Tn-1)jai
where i ∈ {0, 1, 2, ..., mn + B2k+1-n}, j ∈ {0, 1, 2, ..., 2m - 1} and v is a factor of Tn-1.
This case is symmetric to the previous case. In particular, we see that |∆(u)| ⩽ |∆(Strip(Tn))| as desired.
Case 4:		The factor u has the form
u = α(Tn-1)iβ
where i ∈ {0, 1, 2, ..., 2m - 2}, and α and β are factors of Tn-1 .
From our inductive hypothesis, we then see that
-2|∆(Strip(Tn-1))| + (2m - 2)∆(Tn) ⩽ ∆(u) ⩽ 2|∆(Strip(Tn-1))|.
Thus, from Lemma 7.7 and the fact that m ⩾ 2, we then see that
|∆(u)| ⩽ 2 2mn-1 +2mn-m + (2m - 2)mn-1
m-1
mn - m
= 2mn + 2mn-1 + 4
m-1
n+1
⩽ 2mn+2m	m = |∆(Strip(Tn))|
m-1
where the last inequality holds since m > 3, in particular,
mn - m	mn+1 - m	mn - m	mn+1 - m 2mn + 2mn-1 +4m m ⩽ 2mn +2m	m ⇐= mn-1 +2m	m ⩽ m m m-1	m-1	m-1 m-1 ⇐= mn-1 (m - 1) + 2(mn - m) ⩽ mn+1 - m ⇐= mn+1 - 3mn + mn-1 + m ⩾ 0
⇐= mn+1 - 3mn ⩾ 0
⇐= mn (m - 3) ⩾ 0 ⇐= m ⩾ 3.
Thus, |∆(u)| ⩽ |∆(Strip(Tn))| as desired.
Conclusion:
In all cases, we have our desired bound on |∆(u)|.
We then have the following lemma which we use to characterise the n-light factors of W .
Lemma 7.18. If u is a factor of W that does not contain a2Bn as a factor, with n ∈ {1, 2, 3, ..., 2k}, then |∆(u)| ⩽ σn.
Proof. For each n ∈ {1, 2, 3, ..., 2k}, notice from the definition of W that
W ∈ a∗T2k+1-na∗T2k+1-na∗T2k+1-na∗ · · · a∗T2k+1-na∗.
From Lemma 7.11, we see that
Affix(T2k+1-n, ◁) =Affix(T2k+1-n,▷) =aBn.
From this we see that if u does not contain a2Bn as a factor, then it must also be a factor of
w = Affix(T2k+1-n, ▷) T2k+1-n Affix(T2k+1-n, ◁).
Thus, from Lemma 7.17, we see that
2k+2-n
∆(u)| ⩽ 2m2k+1-n + 2 m	-m=σn,
m-1
as desired.
Corollary 7.19. If u is a factor of W, then
|∆(Remn(u))| ⩽ 2σn
for all n ∈ {1, 2, 3, ..., 2k}. If additionally u is n-light, then |∆(Remn(u))| ⩽ σn.
Proof. From the definition of Remn : Σ∗ → Σ∗ , we have two cases as follows.
(1)		The word u is n-light and thus Remn(u) = u does not contain a2Λn as a factor. From Lemmas 7.9 and 7.18, we see that |∆(Remn(u))| ⩽ σn.
(2)		The word u is n-heavy and thus Remn(u) = segn (u, ◁) segn (u, ▷) where both segn (u, ◁) and segn(u, ▷) are n-light and thus do not contain a2Λn as a factor. From Lemmas 7.9 and 7.18, we then see that |∆(Remn(u))| ⩽ 2σn.
We thus have our desired bounds.	□
7.4		. Decompositions. In the following we define what it means for a k-tuple of words in Σ∗ to have a decomposition. Later in this proof, we show that the property of having a decomposition is preserved, in some way, by the grammar M for L.
Definition 7.20. Let n ∈ {2, 3, ..., 2k}, then an n-decomposition of w⃗ = (w1, w2, ..., wk) ∈ (Σ∗)k is a nonempty subset
E ⊆ {1, 2,..., k} × {◁, ▷}
with |E| = n such that, for each (i, s) ∈ E, the word wi is n-heavy and
k
|Affix(wi, s)| ⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln(w⃗)|)σn - X ∆(Remn(wj)).	(8)
j=1
Notice that |Ln (w⃗)| is the number of n-light components in w⃗. We say that w⃗ has a decomposition if it has an n-decomposition for some n ∈ {2, 3, ..., 2k}.
Remark 7.21. Notice that if w⃗ = (W, ε, ε, ..., ε), then E = {(1, ◁), (1, ▷)} is a 2-decomposition of w⃗. In particular, we see that w1 = W is 2-heavy as it contains aB1 +m2k as a prefix (see Corollary 7.12) where B1 + m2k ⩾ 2Λ1 follows since we have 2Λ1 = 2m2k and B1 ⩾ m2k from Definition 7.8; and moreover, for each (i, s) ∈ E, we see that the left-hand side of (8) evaluates to B1 + m2k (from Corollary 7.12) while the right-hand side of (8) evaluates to
Λ1 -C - (2k-2 - (k - 1))σ2 -0 = Λ1 - C- (k- 1)σ2 = Λ1 - C- (k- 1)(2Λ2 +2B2)
where the last equality follows from the definition of σn in Definition 7.8, thus (8) is equivalent to B1 +m2k ⩾ Λ1 -C- (k- 1)(2Λ2 +2B2)
which follows immediately as we have B1 > Λ1 from Lemma 7.9.
To simplify the proofs of later lemmas in this section, we often assume without loss of generality that a given n-decomposition is maximal as follows.
Definition 7.22. We say that an n-decomposition E of w⃗ = (w1, w2, ..., wk) is maximal if there is no n′ -decomposition E′ of w⃗ with |E′ | = n′ > n = |E |.
To simplify notation, we define a set of tuples which we call W -sentential tuples as follows.
Definition 7.23. A W -sentential tuple is a k-tuple of the form w⃗ = (w1, w2, ..., wk) ∈ (Σ∗)k where
W = u0w1u1w2u2 · · ·wkuk
for some words u0, u1 , u2, ..., uk ∈ Σ∗, and |∆(w⃗)| ⩽ C. Thus, each word vector which appears in the derivation of W, in the grammar M , is an example of a W -sentential tuple.
We have the following property of n-decompositions.
Lemma 7.24. Let w⃗ = (w1 , w2, ..., wk) be a W -sentential tuple, and let E be an n-decomposition of w⃗. Then, |Affix(wi, s)| ⩾ 5Λn for every (i, s) ∈ E.
Proof. Since w⃗ = (w1 , w2, ..., wk) is a W -sentential tuple, we see that
k

|Affix(wi, s)| ⩾ Λn-1 - C - 2kσn

-	∆(Remn(wj)).
j=1
From Corollary 7.19, we then see that

C - 4kσn.

|Affix(wi, s)| ⩾ Λn-1 -
From the definition of the constant Λn , we see that |Affix(wi, s)| ⩾ Λn-1 - C - 4kσn = mΛn - C - 4kσn
= 5Λn + (m - 5)Λn - C - 4kσn.
From Lemma 7.9, we then see that
|Affix(wi , s)| ⩾ 5Λn + (m - 5)Λn - C - 24kΛn.
Thus,
|Affix(wi, s)| ⩾ 5Λn + (m - 5 - C - 24k)Λn.
From the value of m given in Definition 7.5, we see that |Affix(wi , s)| ⩾ 5Λn .
We now have the following lemma which we use to construct decompositions.
Lemma 7.25. Let w⃗ = (w1 , w2 , ..., wk) be a W -sentential tuple, and suppose that
E ⊆ {1, 2,..., k} × {◁, ▷}
is a set of size |E| = n + 1 ⩾ 2 such that |Affix(wi, s)| ⩾ Λn for each (i, s) ∈ E. Then, the set E is an (n + 1)-decomposition of w⃗.
Proof. From the definition of m and Λn in Definitions 7.5 and 7.8, we see that Λn ⩾ 2Λn+1 and thus, for each (i, s) ∈ E, the word wi is (n + 1)-heavy. From Corollary 7.19, we see that
|∆(Remn+1(wi))| ⩽ σn+1
for each (n + 1)-light word wi. From the definition of Remn : Σ∗ → Σ∗, if wi is (n + 1)-heavy, then |∆(Remn+1(wi))| ⩽ |∆(segn+1(wi,◁))| + |∆(segn+1(wi, ▷))|.
Notice also that each segn+1(wi, ▷)), as above, is (n + 1)-light and thus
|∆(segn+1(wi, ◁))| ⩽ σn+1
from Corollary 7.19. Moreover, if (i, s) ∈ E, then segn+1 (wi, s) = ε and thus |∆(segn+1 (wi, s))| = 0. Let H = {1, 2, ..., k} \ Ln+1 (w⃗) be the indices of all the (n + 1)-heavy words in w⃗. From the previous paragraph and the triangle inequality, we then see that
∆(Remn+1(wi)) ⩽ (2|H| - |E|)σn+1.
i∈H
Notice that 2|H| - |E| counts the sides of the (n + 1)-heavy words which are not in E.
From the above, we see that

k
∆(Remn+1(wi))
i=1

⩽ (|Ln+1 (w⃗)| + 2|H| - |E|)σn+1

= (|Ln+1 (w⃗)| + 2(k - |Ln+1 (w⃗)|) - (n + 1))σn+1.

= (2k - (n + 1) - |Ln+1 (w⃗)|)σn+1.
From this bound, we then see that
k
(2k - (n + 1) - |Ln+1 (w⃗)|)σn+1 + X ∆(Remn+1 (wj)) ⩾ 0.
j=1
Thus, we see that
k
Λn - (C - ∆(w⃗)) - (2k - (n + 1) - |Ln+1 (w⃗)|)σn+1 - X ∆(Remn+1 (wj)) ⩽ Λn - (C - ∆(w⃗)). j=1
Since w⃗ is a W -sentential tuple, by definition, we have |∆(w⃗)| ⩽ C, and thus
k
Λn - (C - ∆(w⃗)) - (2k - (n + 1) - |Ln+1 (w⃗)|)σn+1 - X ∆(Remn+1 (wj)) ⩽ Λn.
j=1
From the assumptions in our lemma statement, we then see that
k
|Affixn+1(wi,s)| ⩾Λn ⩾Λn- (C - ∆(w⃗)) - (2k- (n+1) - |Ln+1(w⃗)|)σn+1 -X∆(Remn+1(wj))
j=1
for each (i, s) ∈ E. Hence, E is an (n + 1)-decomposition as required.	□
We have the following property of maximal decompositions.
Lemma 7.26. Let E be a maximal n-decomposition of a W -sentential tuple w⃗. Then, for each n-heavy component i ∈/ Ln (w⃗) and each s ∈ {◁, ▷} we have segn (wi, s) = ε if and only if (i, s) ∈ E.
Proof. Let E be a maximal n-decomposition as in the lemma statement.
If (i, s) ∈ E, then from Lemma 7.24 we see that |Affix(wi , s)| ⩾ 5Λn and thus segn (wi , s) = ε. Thus, if (i, s) ∈ E, then segn(wi, s) = ε. All that remains is to show the converse of this statement as follows.
Suppose for contradiction that wi is an n-heavy word with segn (wi , s) = ε and (i, s) ∈/ E. Then, from the definition of segn : Σ∗ × {◁, ▷} → Σ∗ in Definition 7.14, we see that |Affix(wi, s)| ⩾ 2Λn. Thus, from Lemmas 7.24 and 7.25, we see that E′ = E ∪ {(i, s)} is an (n + 1)-decomposition of w⃗ which contradicts the maximality of E. Thus, if segn (wi, s) = ε, then (i, s) ∈ E.	□
We have the following lemma which is used in the proof of Proposition 7.30.
Lemma 7.27. Let w ∈ Σ∗ be an n-heavy factor of W, and suppose that w = uv with u, v ∈ Σ∗ . Then, at least one of the following five conditions holds.
(1)		|Affix(u, ▷)| ⩾Λn;
(2)		|Affix(v, ◁)| ⩾ Λn;
(3)		u and v are both n-heavy, and ∆(Remn(u)) + ∆(Remn(v)) ⩾ ∆(Remn(w)) - σn;
(4)		u is n-light, v is n-heavy, and ∆(Remn(u)) + ∆(Remn(v)) = ∆(Remn (w));
(5)		u is n-heavy, v is n-light, and ∆(Remn(u)) + ∆(Remn(v)) = ∆(Remn (w)).
Proof. Suppose that w is an n-heavy factor of W with w = uv as in the lemma statement. We separate our proof into two parts as follows.
Case 1:		both u and v are n-light.
Here we see that u and v must be of the form
u = segn (w, ◁)ap	and v = aq seg(w, ▷),
respectively, where p + q ⩾ 2Λn . Thus, we find that either p ⩾ Λn or q ⩾ Λn , and thus we are either in case (1) or (2), respectively.
Case 2:		at least one of u or v is n-heavy.
Notice that if
|Affix(u, ▷)| ⩾ Λn	or	|Affix(v, ◁)| ⩾ Λn,
then we are in case (1) or (2), respectively. Thus, in the remainder of this proof, we assume that both
|Affix(u, ▷)| < Λn and	|Affix(v, ◁)| < Λn,
and thus the factor
w′ = segn(u, ▷)segn(v, ◁)
of w does not contain a2Λn as a factor, that is, w′ is n-light.
Case 2.1:		both u and v are n-heavy.
From Lemmas 7.9 and 7.18, we then see that
(segn(u, ▷)) +∆(segn(u,◁)) = ∆(w′) ⩾ -σn.
From the definition of Remn : Σ∗ → Σ∗ , we see that
∆(Remn(u)) + ∆(Remn(v)) = ∆(segn(u,◁)) + ∆(segn(v, ▷)) +∆(segn(u,▷)) + ∆(segn(v,◁)) = ∆(segn(w, ◁)) + ∆(segn(w, ▷)) + ∆(segn(u, ▷)) + ∆(segn(v, ◁)) = ∆(Remn(w)) + ∆(w′) ⩾ ∆(Remn (w)) - σn.
Thus, we are in case (3) of the lemma.
Case 2.2:		u is n-light, and v is n-heavy.
The only way for u to be n-light is if it is either a factor of segn (w, ◁) or a word of the form segn (w, ◁)ap where p < 2Λn . We consider these cases as follows.
•		If u is a factor of segn (w, ◁), then we see that
Remn(w) = segn (w, ◁) segn(w, ▷)
= u segn (v, ◁) segn(v, ▷) = Remn(u) Remn(v).
Thus,
∆(Remn(u)) + ∆(Remn(v)) = ∆(Remn (w))
and we are in case (4) of the lemma.
•		If u = segn (w, ◁)ap where p < 2Λn, then v = aq v′ with p+q ⩾ 2Λn. So either p ⩾ Λn or q ⩾ Λn, which correspond to cases (1) and (2) of the lemma.
Case 2.3:		u is n-heavy, and v is n-light.
The proof of this case is symmetric to Case 2.2.
Conclusion: We see that in all cases, our words fall into one of the five cases listed in the lemma. Moreover, we see that these cases cover all possible situations.	□
7.5. Maintaining a decomposition. In this subsection we show that, for W -sentential tuples, the property of having a decomposition is maintained by the operations known as left letter deletion and left split (both of which are the reverse of some of the operations presented in Definition 6.7).
Proposition 7.28. Let w⃗ = (w1, w2, ..., wk) and ⃗v = (v1 , v2, ..., vk) be W -sentential tuples as in Definition 7.23, and suppose that x ∈ {1, 2, ..., k} with
(w1,w2,...,wk) = (v1,v2,...,vx-1,avx,vx+1,...,vk).
If w⃗ has an n-decomposition, then ⃗v has an n′ -decomposition where n′ ⩾ n. That is, given a W -sentential tuple with an n-decomposition, if we still have a W -sentential tuple after deleting an instance of the letter a from the left-hand side of some component, then there exists an n′-decomposition, with n′ ⩾ n, for the new tuple. (Recall that if w⃗ is a W -sentential tuple, then |∆(w⃗)| ⩽ C. Thus, we cannot directly use this process to remove sequences of a’s of arbitrarily large length and still obtain a decomposition.)
Proof. Without loss of generality, we assume that E is a maximal n-decomposition for the sentential tuple w⃗ . We note here that ∆( ⃗v) = ∆(w⃗) - 1, that Remn(vi) = Remn(wi) for each i ̸= x; and that Affix(vi, s) = Affix(wi, s) for each i ̸= x and s ∈ {◁, ▷}. The remainder of this proof is separated into three cases as follows.
Case 1: (x, ◁) ∈ E.
From Lemma 7.24, we see that
|Affix(vx, ◁)| = |Affix(wx, ◁)| - 1 ⩾ 5Λn - 1 ⩾ 2Λn.
Further, we see that
|Affix(vx, ▷)| ∈ {|Affix(wx, ▷)|, |Affix(wx, ▷)| - 1}, where the |Affix(wx, ▷)| - 1 corresponds to the case where wx = a|wx|.
Thus,
|Affix(vi, s)| ⩾ |Affix(wi, s)| - 1
for each i ∈ {1, 2, ..., k} and s ∈ {◁, ▷}.
We see that the words vx and wx are both n-heavy, and we see that
Ln ( ⃗v) = Ln (w⃗)	and	Remn (vx ) = Remn (wx).
We are now ready to prove this case as follows.
From the above observations, we see that
|Affix(vi , s)| ⩾ |Affix(wi, s)| - 1
k
⩾ Λn-1 - (C - (∆(w⃗) - 1)) - (2k - n - |Ln (w⃗)|)σn - X ∆(Remn(wj))
j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k-n- |Ln(⃗v)|)σn-X∆(Remn(vj))
j=1
for each (i, s) ∈ E. Hence, we find that E is an n-decomposition for ⃗v.
Case 2: (x, ◁) ∈/ E and wx is n-heavy.
From Lemma 7.26, we see that segn (wx , ◁) ̸= ε and thus removing an a from the left-hand side of wx does not affect its status as being n-heavy, and furthermore does not affect Affix(wx , ▷). That is, we have
Affix(vx, ▷) = Affix(wx, ▷).
Moreover, from the definition of Remn : Σ∗ → Σ∗ on n-heavy words, we see that
∆(Remn(vx)) = ∆(Remn(wx)) - 1.
From the above observations, we see that
|Affix(vi, s)| ⩾ |Affix(wi , s)|
x-1
⩾ Λn-1 - (C - (∆(w⃗) - 1)) - (2k - n - |Ln (w⃗)|)σn - X ∆(Remn(wj))
j=1
k
- (∆(Remn(wx)) - 1) - X ∆(Remn(wj))
j=x+1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X ∆(Remn(vj))
j=1
for each (i, s) ∈ E. Hence, we find that E is an n-decomposition for ⃗v.
Case 3:		wx is n-light.
Notice here that (x, ▷) ∈/ E since wx and thus vx are n-light.
We then see that a Remn (vx) = Remn (wx), and hence,
∆(Remn(vx)) = ∆(Remn(wx)) - 1.
From the above observations, we see that
|Affix(vi, s)| ⩾ |Affix(wi , s)|
x-1 ⩾ Λn-1 - (C - (∆(w⃗) - 1)) - (2k - n - |Ln (w⃗)|)σn - X ∆(Remn(wj)) j=1
k
-		(∆(Remn(wx)) - 1) - X ∆(Remn(wj))
j=x+1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X ∆(Remn(vj))
j=1
for each (i, s) ∈ E. Hence, we find that E is an n-decomposition for ⃗v.
Conclusion:
We see that in all cases E is an n-decomposition for ⃗v .	□
Proposition 7.29. Let w⃗ = (w1, w2, ..., wk) and ⃗v = (v1 , v2, ..., vk) be W -sentential tuples as in Definition 7.23, and suppose that x ∈ {1, 2, ..., k} with
(w1,w2,...,wk) = (v1,v2,...,vx-1,bvx,vx+1,...,vk).
If w⃗ has an n-decomposition, then ⃗v has an n-decomposition. That is, given a W -sentential tuple with an n-decomposition, if we still have a W -sentential tuple after deleting an instance of the letter b from the left-hand side of some component, then there exists an n-decomposition for the new tuple.
Proof. Let E be an n-decomposition for w⃗. In this proof, we show that E is also an n-decomposition for ⃗v. Notice that since the leftmost letter of wx is b, we have (x, ◁) ∈/ E. In addition, removing an occurrence of b from the left of wx does not change its n-heavy/n-light status, and does not affect Affix(wx , ▷). Thus,
Ln(⃗v) = Ln (w⃗)	and	Affix(vx, ▷) = Affix(wx, ▷).
Notice that ∆(⃗v) = ∆(w⃗) + 1, that Remn(vi) = Remn(wi) for each i ̸= x, and Affix(vi, s) = Affix(wi, s) for each i ̸= x and s ∈ {◁, ▷}. We also see that bRemn(vx) = Remn(wx) and thus
∆(Remn(vx)) = ∆(Remn(wx)) + 1.
From our observations as above, we see that
|Affix(vi, s)| ⩾ |Affix(wi, s)|
x-1
⩾ Λn-1 - (C- (∆(w⃗) + 1)) - (2k-n- |Ln(w⃗)|)σn-X∆(Remn(wj))
j=1
k
-		(∆(Remn(wx)) + 1) - X ∆(Remn(wj)) j=x+1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X∆(Remn(vj))
j=1
for each (i, s) ∈ E. Hence, we see that E is an n-decomposition for ⃗v.	□
Proposition 7.30. Let w⃗ = (w1, w2, ..., wk) and ⃗v = (v1 , v2, ..., vk) be W -sentential tuples as in Definition 7.23, and suppose that x ∈ {1, 2, ..., k - 1} with wx = ε, wx+1 = vx vx+1, and
w⃗ = (w1,w2,...,wk) = (v1,v2,...,vx-1,ε,vxvx+1, vx+2,..., vk).
If w⃗ has an n-decomposition, then ⃗v has an n′ -decomposition where n′ ⩾ n. That is, given a W -sentential tuple w⃗ with an n-decomposition, if we split one of its components into two adjacent components to obtain another W -sentential tuple, then the resulting tuple will also have an n′ -decomposition with n′ ⩾ n.
(Notice that if w⃗ and ⃗v are different vectors, then ⃗v will have one fewer component equal to ε then w⃗ . Thus, this proposition cannot be directly repeated arbitrarily many times.)

Proof. Without loss of generality, we assume that E is a maximal n-decomposition for the sentential tuple w⃗. We note here that ∆(⃗v) = ∆(w⃗), and vi = wi for each i ∈/ {x, x + 1}.
The remainder of this proof is separated into cases based on whether the word wx+1 is n-heavy, and the memberships of its sides to the set E.
Case 1: The word wx+1 is n-light.
Since wx+1 = vxvx+1, we then see that both vx and vx+1 are also n-light. Hence,
Ln(⃗v) =Ln(w⃗),	∆(wx+1) = ∆(vx) + ∆(vx+1)
and thus
∆(Remn(wx)) + ∆(Remn(wx+1)) = ∆(Remn(wx+1))
= ∆(Remn(vx)) + ∆(Remn(vx+1)).
Since wx+1 is n-light and wx = ε, it then follows that
(x, ◁), (x, ▷), (x + 1, ◁), (x + 1, ▷) ∈/ E.
Thus, we have vi = wi if (i, s) ∈ E for some s ∈ {◁, ▷}. Hence, we find that
|Affix(vi, s)| = |Affix(wi,s)|
k
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn - X∆(Remn(wj))
j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X∆(Remn(vj))
j=1
for each (i, s) ∈ E. Thus, E is an n-decomposition for ⃗v.
Case 2: The word wx+1 is n-heavy with (x + 1, ◁), (x + 1, ▷) ∈/ E.
Notice that since wx = ε, we have that
(x, ◁), (x, ▷), (x + 1, ◁), (x + 1, ▷) ∈/ E.
Thus, we have vi = wi if (i, s) ∈ E for some s ∈ {◁, ▷}.
From Lemma 7.27, we are in one of the following five cases.
(1)		We have |Affix(vx, ▷)| ⩾ Λn.
From Lemmas 7.24 and 7.25, we see that E′ = E ∪ {(x, ▷)} is an (n + 1)-decomposition for ⃗v.
(2)		We have |Affix(vx+1 , ◁)| ⩾ Λn.
From Lemmas 7.24 and 7.25, we see that E′ = E ∪ {(x + 1, ◁)} is an (n + 1)-decomposition for ⃗v. (3)	We have that vx and vx+1 are both n-heavy, and

(9)

∆(Remn(vx)) + ∆(Remn(vx+1)) ⩾ ∆(Remn(wx+1)) - σn.
It then follows that Ln(⃗v) = Ln (w⃗) \ {x}, in particular, |Ln(⃗v)| = |Ln (w⃗)| - 1.
Recall that wi = ui if (i, s) ∈ E for some s ∈ {◁, ▷}. Hence, for each (i, s) ∈ E, we have

k
- X ∆(Remn(wj)) j=1

|Affix(vi,s)| = |Affix(wi,s)|
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn k
= Λn-1 - (C - ∆(w⃗)) - (2k - n - (|Ln (w⃗)| - 1))σn + σn - X∆(Remn(wj))

k
- X ∆(Remn(vj)). j=1

j=1
⩾ Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln( ⃗v)|)σn
Notice that the last inequality, as above, follows from our case assumption in (9). We then see that E is an n-decomposition for ⃗v.
(4)		We have that vx is n-light, vx+1 is n-heavy, and
∆(Remn(vx)) + ∆(Remn(vx+1)) = ∆(Remn(wx+1)).
Notice that we have Ln( ⃗v) = Ln (w⃗), in particular, |Ln(⃗v)| = |Ln (w⃗)|.
Recall that wi = ui if (i, s) ∈ E for some s ∈ {◁, ▷}. Hence, for each (i, s) ∈ E, we have
|Affix(vi, s)| = |Affix(wi,s)|
k
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn - X∆(Remn(wj))
j=1
k = Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X∆(Remn(vj)).
j=1
Notice that this follows from our case assumption since ∆(Remn(wx)) = ∆(Remn (ε)) = 0.
Thus, we see that E is an n-decomposition for ⃗v.
(5)		We have that vx is n-heavy, vx+1 is n-light, and
∆(Remn(vx)) + ∆(Remn(vx+1)) = ∆(Remn(wx+1)).
We have Ln( ⃗v) = (Ln (w⃗) \ {x}) ∪ {x + 1}, in particular, |Ln(⃗v)| = |Ln (w⃗)|.
Recall that wi = ui if (i, s) ∈ E for some s ∈ {◁, ▷}. Hence, for each (i, s) ∈ E, we have
|Affix(vi, s)| = |Affix(wi,s)|
k
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn - X∆(Remn(wj))
j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X∆(Remn(vj)).
j=1
Notice that this follows from our case assumption since ∆(Remn(wx)) = ∆(Remn (ε)) = 0.
Thus, we see that E is an n-decomposition for ⃗v.
Case 3: The word wx+1 is n-heavy with (x + 1, ◁) ∈ E and (x + 1, ▷) ∈/ E.
Notice that either vx is a prefix of Affix(wx+1 , ◁), or Affix(wx+1, ◁) is a prefix of vx. We consider these two cases separately as follows.
Case 3.1: The word vx is a prefix of Affix(wx+1, ◁).
From Lemma 7.24, we see that vx and vx+1 are words of the form
vx = ap	and	vx+1 = aqu
with
p + q = |Affix(wx+1, ◁)| ⩾ 5Λn	and u ∈ Σ∗.
Notice that if p ⩾ Λn, then from Lemmas 7.24 and 7.25, we see that
E′=(E\{(x+1,◁)})∪{(x,◁),(x,▷)}
is an (n + 1)-decomposition for ⃗v. We consider the case where p < Λn as follows.
Since p < Λn, we see that vx is n-light, and that vx+1 is n-heavy. From this, we see that Ln ( ⃗v) = Ln (w⃗). Further, we then see that
|Affixn(vx+1, ◁)| = |Affixn(wx+1, ◁)| - p.
Moreover, since q ⩾ 2Λn, we have segn (vx+1 , ◁) = ε, and
∆(Remn(vx)) + ∆(Remn(vx+1)) = p+ ∆(Remn(wx+1)).
We then see that
|Affix(vi, s)| ⩾ |Affix(wi, s)| - p
⩾ Λn-1 - (C - ∆(w⃗))
x
-		(2k - n - |Ln (w⃗)|)σn -	∆(Remn(wj)) j=1
k
-		(p+ ∆(Remn(wx+1))) -	∆(Remn(wj)) j=x+2
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X ∆(Remn (vj))
j=1
for each (i, s) ∈ E. Thus, we see that E is an n-decomposition for ⃗v.
Case 3.2: The word Affix(wx+1, ◁) is a prefix of vx.
In this case, the words vx and vx+1 are of the form
vx = Affix(wx, ◁) u	and	vx+1 ∈ Σ∗
where u ∈ Σ∗. From Lemma 7.24, |Affix(wx, ◁)| ⩾ 5Λn and thus vx is n-heavy.
We may apply Lemma 7.27 to the factorisation wx+1 = vxvx+1 to obtain the following five cases.
(1)		We have |Affix(vx, ▷)| ⩾ Λn.
Then, from Lemmas 7.24 and 7.25, we see that
E′=(E\{(x+1,◁)})∪{(x,◁),(x,▷)}
is an (n + 1)-decomposition for ⃗v.
(2)		We have |Affix(vx+1 , ◁)| ⩾ Λn.
Then, from Lemmas 7.24 and 7.25, we see that
E′ = E ∪ {(x, ◁)}
is an (n + 1)-decomposition for ⃗v.
(3)		We have that vx and vx+1 are both n-heavy, and
∆(Remn(vx)) + ∆(Remn(vx+1)) ⩾ ∆(Remn(wx+1)) - σn.
We then see that Ln( ⃗v) = Ln (w⃗) \ {x}, in particular, |Ln( ⃗v)| = |Ln (w⃗)| - 1. Let E′= (E \ {(x + 1, ◁)}) ∪ {(x, ◁)}
and notice that
k
|Affix(vi, s)| ⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn - X ∆(Remn (wj)) j=1
k
= Λn-1 - (C - ∆(w⃗)) - (2k - n - (|Ln (w⃗)| - 1))σn + σn - X ∆(Remn(wj)) j=1
k
⩾ Λn-1 - (C - ∆(⃗v)) - (2k-n- |Ln(⃗v)|)σn-X∆(Remn(vj))
j=1
for each (i, s) ∈ E′ . Thus, we see that E′ is an n-decomposition for ⃗v.
(4)		We have that vx is n-light, vx+1 is n-heavy, and
∆(Remn(vx)) + ∆(Remn(vx+1)) = ∆(Remn(wx+1)).
This case does not need to be considered as it contradicts our earlier case assumption that vx is n-heavy.
(5)		We have that vx is n-heavy, vx+1 is n-light, and
∆(Remn(vx)) + ∆(Remn(vx+1)) = ∆(Remn(wx+1)).
We have Ln( ⃗v) = (Ln (w⃗) \ {x}) ∪ {x + 1}, in particular, |Ln(⃗v)| = |Ln (w⃗)|. Let
E′= (E \ {(x + 1, ◁)}) ∪ {(x, ◁)}
and notice that
k
|Affix(vi, s)| ⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn - X ∆(Remn(wj))
j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X∆(Remn(vj))
j=1
for each (i, s) ∈ E′ . Thus, we see that E′ is an n-decomposition for ⃗v.
Case 4: The word wx+1 is n-heavy with (x + 1, ◁) ∈/ E and (x + 1, ▷) ∈ E.
The proof of this case is symmetric to the proof of Case 3 as above.
Case 5: The word wx+1 is n-heavy with (x + 1, ◁), (x + 1, ▷) ∈ E.
This case is separated into two subcases:
(5.1)		wx+1 does not contain the letter b, in particular,
wx+1 = Affix(wx+1, ◁) = Affix(wx+1, ▷); and
(5.2)		wx+1 contains at least one b, in particular,
wx+1 = Affix(wx+1, ◁) u Affix(wx+1, ▷)
where u ∈ Σ∗ with |u| ⩾ 1.
We consider these cases as follows.
Case 5.1: wx+1 = Affix(wx+1, ◁) = Affix(wx+1, ▷).
Here we see that
vx = ap	and	vx+1 = aq
where p + q = |wx+1 |. We then separate this into three subcases based on the value of p as follows.
Case 5.1.1: Λn ⩽ p ⩽ |wx+1| - Λn and thus Λn ⩽ q ⩽ |wx+1| - Λn.
From Lemmas 7.24 and 7.25, we see that
E′ = E ∪ {(x, ◁)}	and	E′′ = E ∪ {(x, ▷)}
are both (n + 1)-decompositions of ⃗v.
Case 5.1.2: p < Λn and thus q > |wx+1 | - Λn.
We then see that vx is n-light. Moreover, from Lemma 7.24, we see that |wx+1 | ⩾ 5Λn and thus vx+1 is n-heavy. We then notice that Ln(⃗v) = Ln (w⃗),
∆(Remn(vx)) = p and	∆(Remn(vx+1)) = ∆(Remn(wx+1)) = 0
For each (i, s) ∈ E, we then see that
|Affix(vi, s)| ⩾ |Affix(wi , s)| - p
k
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln(w⃗)|)σn -p - X∆(Remn(wj))
j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X ∆(Remn(vj)).
j=1
Thus, E is an n-decomposition for ⃗v.
Case 5.1.3: p > |wx+1 | - Λn and thus q < Λn.
We see that vx+1 is n-light. Moreover, from Lemma 7.24 we see that |wx+1 | ⩾ 5Λn and thus vx is n-heavy. We notice that Ln( ⃗v) = (Ln (w⃗) \ {x}) ∪ {x + 1}, and thus
|Ln(⃗v)| = |Ln (w⃗)|.
Moreover,
∆(Remn(vx)) = ∆(Remn(wx+1)) = 0 and	∆(Remn(vx+1)) = q
For each (i, s) ∈ E \ {(x + 1, ◁), (x + 1, ▷)}, we then see that
|Affix(vi, s)| ⩾ |Affix(wi, s)|
⩾ |Affix(wi, s)| - q
k
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn - q - X∆(Remn(wj)) j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X ∆(Remn(vj)).
j=1
Moreover, we see that for each s ∈ {◁, ▷},
|Affix(vx, s)| = |Affix(wx+1, s)| - q
k
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln(w⃗)|)σn - q - X∆(Remn(wj)) j=1
k
rΛn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X∆(Remn(vj)).
j=1
Thus,
E′= (E\{(x+1,◁),(x+1,▷)})∪{(x,◁),(x,▷)}
is an n-decomposition for ⃗v.
Case 5.2: wx+1 = Affix(wx+1, ◁) u Affix(wx+1 , ▷) where u ∈ Σ∗ with |u| ⩾ 1.
We separate this case into five subcases based on the length of vx as follows.
Case 5.2.1: |vx| < 2Λn.
We then see that vx is n-light, vx+1 is n-heavy and thus Ln ( ⃗v) = Ln (w⃗).
From Lemma 7.24, we see that vx and vx+1 are of the form
vx = ap	and	vx+1 = aq u Affix(wx+1, ▷)
where p + q = |Affix(wx+1 , ◁)| ⩾ 5Λn, p < 2Λn and q ⩾ 3Λn. We then see that
∆(Remn(vx))) = p and	∆(Remn(vx+1)) = ∆(Remn(wx+1)) = 0.
For each (i, s) ∈ E, we then have
|Affix(vi, s)| ⩾ |Affix(wi , s)| - p
k
⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln(w⃗)|)σn -p - X∆(Remn(wj)) j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X ∆(Remn(vj)).
j=1
Notice that this follows since ∆(Remn(wx))) = ∆(Remn(wx+1)) = 0.
Thus, we see that E is an n-decomposition for ⃗v.
Case 5.2.2: 2Λn ⩽ |vx| ⩽ |Affix(wx+1, ◁)|.
In this case we see that
vx = ap	and	vx+1 = aq u Affix(wx+1, ▷)
for some u ∈ Σ∗ where p + q = |Affix(wx+1, ◁)| and p ⩾ 2Λn.
From Lemmas 7.24 and 7.25, we see that
E′=(E\{(x+1,◁)})∪{(x,◁),(x,▷)}
is an (n + 1)-decomposition of ⃗v.
Case 5.2.3: |Affix(wx+1, ◁)| ⩽ |vx| ⩽ |wx+1| - |Affix(wx+1, ▷)|.
We notice then that
vx = Affix(wx+1, ◁) u	and vx+1 = u′ Affix(wx+1, ▷)
for some u, u′ ∈ Σ∗ . Thus, both vx and vx+1 are n-heavy.
From Lemma 7.27, we are in one of the following five cases.
(1)		We have |Affix(vx, ▷)| ⩾ Λn.
Then, from Lemmas 7.24 and 7.25, we see that
E′=(E\{(x+1,◁)})∪{(x,◁),(x,▷)}
is an (n + 1)-decomposition for ⃗v.
(2)		We have |Affix(vx+1 , ◁)| ⩾ Λn.
Then, from Lemmas 7.24 and 7.25, we see that
E′ = E ∪ {(x, ◁)}
is an (n + 1)-decomposition for ⃗v.
(3)		We have that vx and vx+1 are both n-heavy, and
∆(Remn(vx)) + ∆(Remn(vx+1)) ⩾ ∆(Remn(wx+1)) - σn.
We then see that Ln( ⃗v) = Ln (w⃗) \ {x}, in particular, |Ln( ⃗v)| = |Ln (w⃗)| - 1. Let
E′= (E \ {(x + 1, ◁)}) ∪ {(x, ◁)}
and notice that
k
|Affix(vi, s)| ⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - (|Ln (w⃗)| - 1))σn + σn - X ∆(Remn(wj)) j=1
k
⩾ Λn-1 - (C - ∆(⃗v)) - (2k-n- |Ln(⃗v)|)σn-X∆(Remn(vj))
j=1
for each (i, s) ∈ E′ . Thus, we see that E′ is an n-decomposition for ⃗v.
(4)		We have that vx is n-light, vx+1 is n-heavy, and
∆(Remn(vx)) + ∆(Remn(vx+1)) = ∆(Remn(wx+1)).
This case does not need to be considered as it contradicts our case assumption vx is n-heavy. (5)	We have that vx is n-heavy, vx+1 is n-light, and
∆(Remn(vx)) + ∆(Remn(vx+1)) = ∆(Remn(wx+1)).
This case does not need to be considered as it contradicts our case assumption vx+1 is n-heavy.
Case 5.2.4: |wx+1| - |Affix(wx+1,▷)| ⩽ |vx| ⩽ |wx+1| - 2Λn.
In this case we see that
vx = Affix(wx+1, ◁) uap and	vx+1 = aq
for some u ∈ Σ∗ where p + q = |Affix(wx+1, ◁)| and q ⩾ 2Λn.
From Lemmas 7.24 and 7.25, we see that
E′ = E ∪ {(x, ◁)}
is an (n + 1)-decomposition of ⃗v.
Case 5.2.5: |vx| > |wx+1 | - 2Λn.
We then see that vx is n-heavy, vx+1 is n-light and thus
Ln(⃗v) = (Ln(w⃗) \ {x}) ∪ {x + 1},
in particular, this means that |Ln ( ⃗v)| = |Ln (w⃗)|.
From Lemma 7.24, we see that vx and vx+1 are of the form
vx = Affix(wx+1, ◁) uap and	vx+1 = aq
where p + q = |Affix(wx+1 , ◁)| ⩾ 5Λn, p > 3Λn and q < 2Λn. We then see that
∆(Remn(vx))) = ∆(Remn(wx+1)) = 0 and	∆(Remn(vx+1)) = q
For each (i, s) ∈ E \ {(x + 1, ◁), (x + 1, ▷)}, we then have
|Affix(vi,s)| = |Affix(wi,s)|
⩾ |Affix(wi, s)| - q
k ⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln (w⃗)|)σn - q - X∆(Remn(wj)) j=1
k = Λn-1 - (C - ∆(⃗v)) - (2k - n - |Ln(⃗v)|)σn - X ∆(Remn(vj)).
j=1
Moreover, for each s ∈ {◁, ▷}, we see that
|Affix(vx, s)| ⩾ |Affix(wx+1, s)| - q
k ⩾ Λn-1 - (C - ∆(w⃗)) - (2k - n - |Ln(w⃗)|)σn - q - X ∆(Remn(wj)) j=1
k
= Λn-1 - (C - ∆(⃗v)) - (2k-n- |Ln(⃗v)|)σn - X ∆(Remn(vj)).
j=1
Thus,
E′= (E\{(x+1,◁),(x+1,▷)})∪{(x,◁),(x,▷)}
is an n-decomposition for ⃗v.
Conclusion:
In all cases, if w⃗ has a maximal n-decomposition, then we can either construct an n-decomposition or construct an (n + 1)-decomposition for ⃗v.	□
7.6.		Mirroring decompositions. We introduce Mirror : Σ∗ → Σ∗ such that Mirror(w) = wn · · · w2w1 for each w = w1w2 · · · wn ∈ Σ∗ . We then extend this function to operate on tuples of words as follows. We define Mirror : (Σ∗)k → (Σ∗)k such that for each w⃗ = (w1, w2, ..., wk) ∈ (Σ∗)k,
Mirror(w⃗) = (Mirror(wk), ..., Mirror(w2), Mirror(w1))
We define Mirror : P ({1, 2, ..., k} × {◁, ▷}) → P({1,2,...,k} × {◁, ▷}) on decompositions as follows. Suppose that E ⊆ {1, 2, ..., k} × {◁, ▷} is an n-decomposition of w⃗ . We then define Mirror(E) such that
•		(i, ◁) ∈ Mirror(E) if and only if (k + 1 - i, ▷) ∈ E; and
•		(i, ▷) ∈ Mirror(E) if and only if (k + 1 - i, ◁) ∈ E.
We then see that Mirror(E) is an n-decomposition for the word vector Mirror(w⃗).
Notice from the definition of the word W in Definition 7.5 that Mirror(W) = W. Thus, from the definition of W -sentential tuple in Definition 7.23, we see that if w⃗ is a W -sentential tuple, then Mirror(w⃗) is also a W -sentential tuple. Finally, notice that in each of the above usages of Mirror, the function Mirror is an involution. Using these maps, we may now derive the following proposition which is a generalisation of Propositions 7.28, 7.29 and 7.30.
Proposition 7.31. Let w⃗ = (w1, w2, ..., wk) and ⃗v = (v1 , v2, ..., vk) be W -sentential tuples as in Definition 7.23, and suppose that w⃗ has one of the four forms
w⃗ =	(w1,w2,...,wk) =	(v1,v2,...,vx-1, avx,vx+1, ...,vk),	(10)
w⃗ =	(w1,w2,...,wk) =	(v1,v2,...,vx-1, vxa,vx+1, ...,vk),	(11)
w⃗ =	(w1,w2,...,wk) =	(v1,v2,...,vx-1, bvx,vx+1,...,vk),	(12)
w⃗ =	(w1,w2,...,wk) =	(v1,v2,...,vx-1, vxb,vx+1,...,vk)	(13) for some x ∈ {1, 2, ..., k}, that is, ⃗v is obtained from w⃗ by deleting an a or b from the left or right-hand side of some component of w⃗; or w⃗ has one of the following two forms
w⃗ = (w1,w2,...,wk) = (v1,..., vx-1, ε, vxvx+1, vx+2,..., vk),	(14)
w = (w1,w2,...,wk) = (v1,..., vx-1, vxvx+1, ε, vx+2,..., vk)	(15) for some x ∈ {1, 2, ..., k - 1}, that is, ⃗v is a vector for which (wx, wx+1) ∈ {(vxvx+1, ε), (ε, vxvx+1)} and wi = vi for each i ∈/ {x, x + 1}. If the tuple w⃗ has an n-decomposition, then ⃗v has an n′ -decomposition for some n′ ⩾ n. (Compare the above cases with the grammar rules in Definitions 6.4, 6.5 and 6.6.)
Proof. We see that cases (10), (12) and (14) follow from Propositions 7.28, 7.29 and 7.30, respectively. We consider the remaining cases as follows.
•		Suppose our vectors w⃗ and ⃗v are in (11). Thus, the pair of vectors Mirror(w⃗) and Mirror( ⃗v) are related as in (10), and Mirror(w⃗) has an n-decomposition. From Proposition 7.28, we obtain an n′-decomposition E, with n′ ⩾ n, for Mirror(⃗v). Thus, Mirror(E) is an n′-decomposition for ⃗v.
•		Suppose our vectors w⃗ and ⃗v are in (13). Thus, the pair of vectors Mirror(w⃗) and Mirror( ⃗v) are related as in (12), and Mirror(w⃗) has an n-decomposition. From Proposition 7.29, we obtain an n′-decomposition E, with n′ ⩾ n, for Mirror(⃗v). Thus, Mirror(E) is an n′-decomposition for ⃗v.
•		Suppose our vectors w⃗ and ⃗v are in (15). Thus, the pair of vectors Mirror(w⃗) and Mirror( ⃗v) are related as in (14), and Mirror(w⃗) has an n-decomposition. From Proposition 7.30, we obtain an n′-decomposition E, with n′ ⩾ n, for Mirror(⃗v). Thus, Mirror(E) is an n′-decomposition for ⃗v.
Hence, we have proven each of the cases of the proposition.	□
7.7.		Main result. We are now ready to prove our main result as follows.
Theorem C. The word problem for the infinite cyclic group Z is not EDT0L.
Proof. Earlier in this section, we assumed for contradiction that there exists some R-MCFG M = (Σ, Q, S, P) which is in normal form (as in Lemma 6.8) that generates the language L as introduced in the beginning of Section 7. Moreover, we let C be the constant for the grammar M as in Corollary 7.4.
From Lemma 7.7, we see that W ∈ L and so there must be a derivation for W in the grammar M of the form
S(W) ← H1 (W, ε, ε, ..., ε) ← H2(w1,1 , w1,2, ..., w1,k)
← H3(w2,1, w2,2,..., w2,k) ← · · · ← Ht+1(wt,1,wt,2,...,wt,k)
← Ht+2(ε, ε, ..., ε) ←
for some t ∈ N where each wi,j ∈ Σ∗ , and each Hi ∈ Q.
We may then define a sequence of tuples w⃗1, w⃗2, ..., w⃗ t+2 such that
w⃗1 = (W,ε,ε,...,ε), w⃗ t+2 = (ε,ε,...,ε) and w⃗i = (wi-1,1,wi-1,2,..., wi-1,k)
for each i ∈ {2, 3, ..., t + 1}. From the definition of the constant C in Corollary 7.4, and the definition of an R-MCFG multiple context-free grammar, we see that each vector w⃗j , as above, is a W -sentential tuple as defined in Definition 7.23.
Notice here that the six cases of Proposition 7.31 correspond to the reverse of the insertion and merge replacement rules as in Definitions 6.4 and 6.5. In particular, given an application of such a rule as
H(w1,w2,...,wk) ← K(v1,v2,...,vk),
the vectors w⃗ = (w1 , w2, ..., wk) and ⃗v = (v1 , v2, ..., vk) satisfy one of the relations in Proposition 7.31. In particular, (10–13) correspond to left and right insertion rules (as in Definition 6.4); and (14) and (15) corresponds to left and right merge rules (as in Definition 6.5).
Hence, from Proposition 7.31, for each i ∈ {1, 2, ..., t + 1}, we see that if w⃗i has an n-decomposition, then w⃗ i+1 has an n′ -decomposition for some n′ ⩾ n. Thus, by an induction on i, we find that if w⃗1 has a decomposition, then so must w⃗ t+2 .
From Corollary 7.12 and Lemmas 7.9 and 7.25, we see that E = {(1, ◁), (1, ▷)} is a 2-decomposition of the W -sentential tuple w⃗1 = (W, ε, ε, ..., ε) (as demonstrated in Remark 7.21). Thus, the sentential tuple w⃗ t+2 = (ε, ε, ..., ε) must have a decomposition. However, it is not possible for w⃗ t+2 to have a decomposition since none of its components are n-heavy for any n ∈ {2, 3, ..., 2k}. In particular, for a component to be n-heavy, it must contain a factor a2Λn where each Λn > 0 from Lemma 7.9. We thus conclude that no such grammar M for the language L can exist, and thus L cannot be an EDT0L language.	□
7.8.		Corollary. We can immediately generalise Theorem C to obtain Theorem D.
Theorem D. If G has an EDT0L word problem, then G is a torsion group.
Proof. Suppose for contradiction that the group G has an EDT0L word problem and an element g ∈ G of infinite order, so ⟨g⟩ ∼= Z. From Proposition A, it follows that the subgroup ⟨g⟩ ∼= Z has an EDT0L word problem with respect to the generating set {g, g-1}. Thus, Z has an EDT0L word problem which contradicts Theorem C.	□
Acknowledgements
The first author acknowledges support from Swiss NSF grant 200020-200400. The second author was supported by Australian Research Council grant DP210100271, and the London Mathematical Society Visiting Speakers to the UK–Scheme 2, 2024. The third author was supported by the Heilbronn Institute for Mathematical Research. The fifth author was supported by the Heilbronn Institute for Mathematical Research and the EPSRC Fellowship grant EP/V032003/1 ‘Algorithmic, topological and geometric aspects of infinite groups, monoids and inverse semigroups’.
References
[1]		A. V. Anisimov. The group languages. Kibernetika (Kiev), 7(4):18–24, 1971.
[2]		Jean-Michel Autebert, Luc Boasson, and G´eraud S´enizergues. Groups and NTS languages. J. Comput. System Sci., 35(2):243–267, 1987.
[3]		Laurent Bartholdi, Leon Pernak, and Emmanuel Rauzy. Groups with presentations in EDT0L, 2024. arXiv:2402.01601.
[4]		Alex Bishop and Murray Elder. Bounded automata groups are co-ET0L. In Language and automata theory and applications, volume 11417 of Lecture Notes in Comput. Sci., pages 82–94. Springer, Cham, 2019.
[5]		Tara Brough, Laura Ciobanu, Murray Elder, and Georg Zetzsche. Permutations of context-free, ET0L and indexed languages. Discrete Math. Theor. Comput. Sci., 17(3):167–178, 2016.
[6]		Laura Ciobanu, Volker Diekert, and Murray Elder. Solution sets for equations over free groups are EDT0L languages. Internat. J. Algebra Comput., 26(5):843–886, 2016.
[7]		Laura Ciobanu and Murray Elder. The complexity of solution sets to equations in hyperbolic groups. Israel J. Math., 245(2):869–920, 2021.
[8]		Laura Ciobanu, Murray Elder, and Michal Ferov. Applications of L systems to group theory. Internat. J. Algebra Comput., 28(2):309–329, 2018.
[9]		Volker Diekert, Artur Jez˙ , Manfred Kufleitner, and Alexander Thumm. Solutions of word equations over partially commutative structures, 2025. arXiv:1603.02966.
[10]		Andrew Duncan, Alex Evetts, Derek F. Holt, and Sarah Rees. Using EDT0L systems to solve some equations in the solvable B aumslag-Solitar groups. J. Algebra, 630:434–456, 2023.
[11]		A. Ehrenfeucht and G. Rozenberg. Three useful results concerning L languages without interactions. In L systems (Third Open House, Comput. Sci. Dept., Aarhus Univ., Aarhus, 1974), volume Vol. 15 of Lecture Notes in Comput. Sci., pages 72–77, 327–338. Springer, Berlin-New York, 1974.
[12]		A. Ehrenfeucht and G. Rozenberg. A pumping theorem for deterministic ET0L languages. Revue fran¸caise d’automatique informatique recherche op´erationnelle. Informatique th´eorique, 9(R2):13–23, 1975.
[13]		A. Ehrenfeucht and G. Rozenberg. On inverse homomorphic images of deterministic ET0L languages. In Automata, languages, development, pages 179–189. North-Holland, Amsterdam-New York-Oxford, 1976.
[14]		A. Ehrenfeucht and G. Rozenberg. On some context free languages that are not deterministic ETOL languages. RAIRO Informat. Th´eor., 11(4):273–291, i, 1977.
[15]		Murray Elder, Mark Kambites, and Gretchen Ostheimer. On groups and counter automata. Internat. J. Algebra Comput., 18(8):1345–1364, 2008.
[16]		Joost Engelfriet. Top-down tree transducers with regular look-ahead. Mathematical Systems Theory, 10(1):289–303, December 1976.
[17]		Joost Engelfriet, Erik Meineche Schmidt, and Jan Van Leeuwen. Stack machines and classes of nonnested macro languages. Journal of the ACM (JACM), 27(1):96–117, 1980.
[18]		Paul Gallot. Safety of data transformations. PhD thesis, Universit´e Lille Nord de France, 2021.
[19]		Robert Gilman. 4 Groups with multiple context-free word problems, pages 161–182. De Gruyter, Berlin, Boston, 2024.
[20]		Rostislav Grigorchuk and Igor Pak. Groups of intermediate growth: an introduction for beginners, July 2006. arXiv:math/0607384.
[21]		Thomas Herbst. On a subclass of context-free groups. RAIRO Inform. The´or. Appl., 25(3):255–272, 1991.
[22]		Derek F. Holt, Matthew D. Owens, and Richard M. Thomas. Groups and semigroups with a one-counter word problem. J. Aust. Math. Soc., 85(2):197–209, 2008.
[23]		Sanjay Jain, Alexei Miasnikov, and Frank Stephan. The complexity of verbal languages over groups. Journal of Computer and System Sciences, 101:68–85, 2019.
[24]		M Latteux. EDT0L-systemes ultralineaires et operateurs associes. Publication du laboratoire de Calcul de l’Universit´e de Lille I, 100, 1977.
[25]		Michel Latteux. Sur les g´en´erateurs alg´ebriques et lin´eaires. Acta Inform., 13(4):347–363, 1980.
[26]		Quang Loc Le and Mengda He. A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In Sukyoung Ryu, editor, Programming Languages and Systems, pages 350–372, Cham, 2018. Springer International Publishing.
[27]		Alex Levine. EDT0L solutions to equations in group extensions. J. Algebra, 619:860–899, 2023.
[28]		David E. Muller and Paul E. Schupp. Groups, the theory of ends, and context-free languages. J. Comput. System Sci., 26(3):295–310, 1983.
[29]		Gabriela AslıRino Nesin and Richard M. Thomas. Groups whose word problem is a Petri net language. In Descriptional complexity of formal systems, volume 9118 of Lecture Notes in Comput. Sci., pages 243–255. Springer, Cham, 2015.
[30]		G. Rozenberg and A. Ehrenfeucht. Some ET0L languages which are not deterministic. Technical Report CU-CS-018-73, University of Colorado Boulder, December 1973.
[31]		G. Rozenberg and D. Vermeir. On ET0L systems of finite index. Information and Control, 38(1):103–133, 1978.
[32]		Grzegorz Rozenberg. Extension of tabled 0L-systems and languages. International Journal of Computer & Information Sciences, 2(4):311–336, December 1973.
[33]		Brigitte Rozoy. The Dyck language D1′∗ is not generated by any matrix grammar of finite index. Inform. and Comput., 74(1):64–89, 1987.
[34]		Takao Yuyama. Groups whose word problems are accepted by abelian G-automata. In Developments in language theory, volume 13911 of Lecture Notes in Comput. Sci., pages 246–257. Springer, Cham, 2023.
Section de math´ematiques, Universit´e de Gene`ve, rue du Conseil-G´ene´ral 7-9, 1205 Gene`ve, Switzerland Email address: alexbishop1234@gmail.com
School of Mathematical and Physical Sciences, University of Technology Sydney, Broadway NSW 2007, Australia
Email address: murray.elder@uts.edu.au
Department of Mathematics, The University of Manchester, Manchester M13 9PL, UK
Email address: alex.evetts@manchester.ac.uk
Database Group, Universita¨t Bremen - FB 03 Postfach 33 04 40, 28334 Bremen, Germany
Email address: pgallot@uni-bremen.de
School of Engineering, Mathematics and Physics, University of East Anglia, Norwich NR4 7TJ, UK
Email address: a.levine@uea.ac.uk
Appendix A. An alternative proof of Proposition A
We note here that this paper is almost completely self-contained. In particular, the only result which we do not prove is in Section 5 where we cite that the family of finite-index EDT0L languages is closed under inverse monoid homomorphism. This result is used in Proposition A to show that having an EDT0L word or co-word problem is invariant under change of generating set. Our reason for structuring the paper in this way is to further motivate the study of finite-index EDT0L languages.
Here we give a short alternative proof of Proposition A which only uses results proven in this paper. This alternative proof is a corollary to the following lemma which is itself a specialisation of a result of Gilman (see Theorem 4.26 and 4.29 in [19]).
Lemma A.1. Let F be a family of formal languages which contains the regular languages and is closed under mapping by string transducer; let G be a group with finite monoid generating set X , and let Y be a finite set that generates a submonoid of G. If WP(G, X) (resp. coWP(G, X)) lies in the family of languages F, then WP(G, Y ) (resp. coWP(G, Y )) also lies in F.
Proof. Notice that if G is finite, then this result follows from the fact that the word problem of a finite group, and any submonoid thereof, is a regular language (see [1, Theorem 1]). Thus, in the remainder of this proof, we may assume without loss of generality that G is an infinite group.
In the remainder of this proof, suppose that Y = {y1, y2, ..., yn}. Notice that, for each yi ∈ Y , we can choose a word ui ∈ X∗ for which yi =G ui. From Lemma 5.1, there exists a choice of words w1, w2, ..., wn, wn+1 ∈ X∗ such that W = {w1u1, w2u2, ..., wnun} is an antichain with respect to the prefix order where each wi = 1.
We define a map f : P(X∗) → P(Y ∗) as

f(L) = yi1yi2 ···yik ∈ Y∗

(wi1 ui1)(wi2 ui2) · · · (wik uik) ∈ L where each ij ∈ {1, 2, ..., n}
From Lemma 4.5, we see that f is a string transducer.
We that f (WP(G, X)) = WP(G, Y ) and f (coWP(G, X)) = coWP(G, Y ). Since the family F is closed under string transduction, we conclude that WP(G, Y ) and coWP(G, Y ) both belong to F.	□
We then obtain an alternative proof of Proposition A as follows.
Proposition A. Let G be a group with finite monoid generating sets X and Y . If WP(G, X) (resp. coWP(G, X)) is EDT0L, then WP(G, Y ) (resp. coWP(G, Y )) is EDT0L of finite index. These results also hold if Y instead generates a submonoid of G. In particular, this implies that, if a word problem is EDT0L, then it is EDT0L of finite index; and that having a word problem that is EDT0L of finite index is independent of choice of generating set.
Proof. This follows by combining Lemma A.1 with Lemmas 3.3 and 4.4, and Proposition 5.2.	□