Our contribution

We consider a subclass of QWEs called regular equations (RWEs) introduced in [23]. A word equation is regular if each variable occurs at most once on each side of the equation. Thus, for example, \(x {\mathtt {a}}{\mathtt {b}} y \doteq y {\mathtt {b}} {\mathtt {a}} x\) is regular while \(x {\mathtt {a}} {\mathtt {b}} x \doteq y {\mathtt {b}} {\mathtt {a}} y\) is not. Understanding RWEs is a vital step towards understanding the quadratic case, not only because they constitute a significant and general subclass, but also because many non-regular quadratic equations can exhibit the same behaviour as regular ones (consider, e.g. HCode \(zz \doteq x{\mathtt {a}}{\mathtt {b}} y y{\mathtt {b}}{\mathtt {a}} x\) for which all solutions must satisfy z = xy = yx). The satisfiability problem was shown in [8] to be NP-hard for RWEs, and shown to be in NP in [9] for some restricted subclasses including the classes of regular-reversed and regular-ordered equations.

For RWEs E, we investigate the structure of the graphs \({\mathscr{G}}^{\Rightarrow _{NT}}_{[E]}\), and as a consequence, are able to describe some of their most important properties. We achieve this by first noting that \({\mathscr{G}}^{\Rightarrow _{NT}}_{[E]}\) can be divided into strongly connected components \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\) for which all the vertices are equations of the same length (⇒ shall be used to denote the restriction of ⇒_NT to length preserving transformations only). The ‘full’ graph \({\mathscr{G}}^{\Rightarrow _{NT}}_{[E]}\) is comprised of these individual components \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\) arranged in a DAG-like structure of linear depth (see Section 3) and therefore many properties and parameters of the ‘full’ graph \({\mathscr{G}}^{\Rightarrow _{NT}}_{[E]}\) are determined by the equivalent properties and parameters of the individual components \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\). We then focus on the structure of the subgraphs \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\), and as a result are able to give bounds on certain parameters such as diameter, size, and DAG-width.

Our structural results come in two stages, based on whether the equation belongs to a the class of ‘jumbled’ equations introduced in Section 6. In the first stage, we consider equations which are not jumbled, and we show that for all such equations E, there exists a jumbled equation \(\hat {E}\) such that \({\mathscr{G}}^{\Rightarrow }_{[E]}\) is comprised mainly of several well-connected near-copies of \({\mathscr{G}}^{\Rightarrow }_{[\hat {E}]}\). For jumbled equations \(\hat {E}\), we show in Section 7 that every vertex in \({\mathscr{G}}^{\Rightarrow }_{[\hat {E}]}\) is close to a vertex in a certain normal form. We show that the vertices in this normal form are determined to a large extent by a property invariant under ⇒ introduced in Section 5.

With regards to the diameter of \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\), we give upper bounds which are polynomial in the length of the equation. It follows that the diameter of the full graph \({\mathscr{G}}^{\Rightarrow _{NT}}_{[E]}\) is also polynomial, and consequently, that the satisfiability problem for RWEs is NP-complete. This can be generalised to systems of equations satisfying a natural extension of the regularity property (see Section 11). We also give exact upper and lower bounds on the number of vertices² in \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\) for a subclass of RWEs called basic RWEs (see Section 4), as well as describing exactly for which equations these bounds are achieved. For RWEs which are not basic, we can infer similar bounds, at the cost of a small (linear in the length of the equation) degree of imprecision. Since in the worst case (e.g. for equations without a solution), running the algorithm will perform a full ‘search’ of the graph, the number of vertices is integral to the running time of the algorithm, and is potentially a better indicator of difficult instances than the complexity class alone. An example of this, comes from comparing two subclasses of RWEs called regular-ordered and regular rotated equations. It follows from our results that while both classes have an NP-complete satisfiability problem, if \(E^{\prime }\) is regular-ordered, then \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\) will contain at most n vertices, where n is the length of the equation, while if \(E^{\prime }\) is regular rotated, but not regular-ordered, then \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\) will contain \(\frac {n!}{2}\) vertices, indicating a vast difference in the number of vertices the algorithm would have to visit.

Motivated by generalisations of the satisfiability problem permitting additional constraints, we also consider the connectivity of the graphs \({\mathscr{G}}^{\Rightarrow _{NT}}_{[E]}\). To do this, we use DAG-width, a measure for directed graphs which is in several ways analogous to treewidth for undirected graphs. Intuitively, equations for which \({\mathscr{G}}^{\Rightarrow _{NT}}_{[E]}\) has low DAG-width are likely to be more amenable when considering additional constraints such as length constraints (see Section 3.3). We give an example class of equations for which the DAG-width is unbounded, as well as a class for which the DAG-width is at most two. The latter includes the class of regular-ordered equations which is the most general subclass of QWEs for which it is known that the satisfiability problem with length constraints is decidable [20], and we expect that both cases will be interesting classes to consider in the context of this problem.

Definition 4.1 (Basic Equations)

Let E be a QWE given by \(\alpha \doteq \beta \). Then E is decomposable if there exist proper prefixes \(\alpha ^{\prime }, \beta ^{\prime }\) of α and β such that \({var}(\alpha ^{\prime }) \cap {qv}(E) = {var}(\beta ^{\prime }) \cap {qv}(E)\). Otherwise, E is indecomposable. E is basic if it is indecomposable and α, β ∈ qv(E)^∗.

Lemma 4.2

Let E be a RWE given by \(\alpha _{1}\alpha _{2} \doteq \beta _{1}\beta _{2}\) where α₁, α₂, β₁, β₂ ∈ (X ∪Σ)^∗ such that α₁, β₁≠ε and var(α₁) ∩ qv(E) = var(β₁) ∩ qv(E). Let \(E^{\prime }\) be a RWE. Then \(E \Rightarrow E^{\prime }\) if and only if there exist α₃, β₃ ∈ (X ∪Σ)^∗ such that \(E^{\prime }\) is given by \(\alpha _3 \alpha _{2} \doteq \beta _3\beta _{2}\) and \(\alpha _{1} \doteq \beta _{1} \Rightarrow \alpha _3 \doteq \beta _3\).

Proof

Suppose E is a RWE given by \(\alpha _{1}\alpha _{2} \doteq \beta _{1}\beta _{2}\) where α₁, α₂, β₁, β₂ ∈ (X ∪Σ)^∗ with α₁, β₁≠ε such that var(α₁) ∩ qv(E) = var(β₁) ∩ qv(E). Let \(E^{\prime }\) be a RWE. Suppose firstly that α₃, β₃ ∈ (X ∪Σ)^∗ such that \(\alpha _{1} \doteq \beta _{1} \Rightarrow _L \alpha _3 \doteq \beta _3\) (the case that \(\alpha _{1} \doteq \beta _{1} \Rightarrow _R \alpha _3 \doteq \beta _3\) is symmetric). Then it follows from the definition of ⇒_L that α₁ has a prefix y ∈ qv(E). Hence, there exist x ∈ X ∪Σ and γ, δ₁, δ₂ ∈ (X ∪Σ)^∗ such that α₁ = yγ, β₁ = xδ₁yδ₂, α₃ = α₁ and β₃ = δ₁xyδ₂. By the definition of ⇒_L, it follows that \(\alpha _{1} \alpha _{2} \doteq \beta _{1} \beta _{2} \Rightarrow _L \alpha _3 \alpha _{2} \doteq \beta _3\beta _{2}\) and thus \(E \Rightarrow E^{\prime }\).

Now suppose instead that \(E \Rightarrow _L E^{\prime }\) (again, the case that \(E \Rightarrow _R E^{\prime }\) is symmetric). Then by definition of ⇒_L, there exists a variable y ∈ qv(E) in the leftmost position of α₁ which also occurs in β₁β₂. Moreover, it follows from the definition of ⇒_L and the fact that \(E \Rightarrow _L E^{\prime }\) that y≠β₁[1]. Furthermore, since var(α₁) ∩ qv(E) = var(β₁) ∩ qv(E), y must in fact occur somewhere in β₁, so there exist x ∈ X ∪Σ and γ, δ₁, δ₂ ∈ (X ∪Σ)^∗ such that α₁ = yγ and β₁ = xδ₁yδ₂, and such that \(E^{\prime }\) is given by \(\alpha _3\alpha _{2} \doteq \beta _3 \beta _{2}\) where α₃ = α₁ and β₃ = δ₁xyδ₂. It follows from the definition of ⇒_L that \(\alpha _{1} \doteq \beta _{1} \Rightarrow _L \alpha _3 \doteq \beta _3\) and thus the statement holds. □

Corollary 4.3

Let E₁, E₂ be RWEs such that E₁ ⇒ E₂. Then E₁ is indecomposable if and only if E₂ is indecomposable. Consequently E₁ is basic if and only if E₂ is basic.

Corollary 4.4

Let E be a decomposable RWE given by \(\alpha _{1}\alpha _{2} \doteq \beta _{1}\beta _{2}\) where α₁, α₂, β₁, β₂ ∈ (X ∪Σ)^∗ such that α₁, β₁≠ε and var(α₁) ∩ qv(E) = var(β₁) ∩ qv(E). Then \({\mathscr{G}}_{[E]}^{\Rightarrow }\) is isomorphic to \({\mathscr{G}}_{[\alpha _{1} \doteq \beta _{1}]}^{\Rightarrow }\) and can be obtained from \({\mathscr{G}}_{[\alpha _{1} \doteq \beta _{1}]}^{\Rightarrow }\) by replacing each vertex \(\alpha _3 \doteq \beta _3 \in [\alpha _{1} \doteq \beta _{1}]_{\Rightarrow }\) with \(\alpha _3 \alpha _{2} \doteq \beta _3 \beta _{2}\).

Definition 4.5 (Isolated path compression)

Let G₁, G₂ be (directed) graphs. We say that G₁ is an isolated path compression of order n of G₂ if G₂ may be obtained from G₁ by replacing each edge \((e,e^{\prime })\) in G₁ by a path \((e,e_{1}), (e_{1}, e_{2}), {\ldots } (e_{k-1},e_k), (e_k, e^{\prime })\) such that k ≤ n and e₁, e₂, e₃,…,e_k are new vertices unique to the edge \((e,e^{\prime })\).

Remark 4.6

Consider graphs G₁, G₂ such that G₁ is an isolated path compression of order n of G₂. If dgw(G₁) = 1, then dgw(G₂) ∈{1,2}.⁴

If dgw(G₁) ≥ 2, then the dgw(G₁) = dgw(G₂). Moreover, diam(G₂) ≤ (n + 1)diam(G₁), and the number of vertices (resp. edges) in G₂ is at most the number of vertices in G₁ plus n times the number of edges of G₁.

Lemma 4.7

Let E be an indecomposable RWE given by \(\alpha \doteq \beta \). Then the graph \({\mathscr{G}}_{[\pi _{{qv}(E)}(\alpha ) \doteq \pi _{{qv}(E)}(\beta )]}^{\Rightarrow }\) is isomorphic to an isolated path compression of order |E| of \({\mathscr{G}}_{[E]}^{\Rightarrow }\).

Proof

Let E be an indecomposable RWE given by \(\alpha \doteq \beta \). Note that by Corollary 4.4, it follows that \(E^{\prime }\) is indecomposable for every \(E^{\prime } \in [E]_{\Rightarrow }\). We begin by considering the simple cases arising when Card(qv(E)) < 2. If Card(qv(E)) = 0, then \({\mathscr{G}}^{\Rightarrow }_{[E]}\) is a single vertex with no edges. Moreover, \(\pi _{{qv}(E)} (\alpha ) \doteq \pi _{{qv}(E)} (\beta )\) is the trivial equation \(\varepsilon \doteq \varepsilon \), so \({\mathscr{G}}_{[\pi _{{qv}(E)}(\alpha ) \doteq \pi _{{qv}(E)}(\beta )]}^{\Rightarrow }\) is also a single vertex with no edges. The two graphs are clearly isomorphic, so the lemma holds trivially.

Now suppose that Card(qv(E)) = 1. Then E has the form \(w_{1} x w_{2} \doteq w_3 x w_4\) where qv(E) = {x} and w₁, w₂, w₃, w₄ ∈ ((X ∪Σ)∖{x})^∗. It necessarily follows that the equation \(\pi _{{qv}(E)} (\alpha ) \doteq \pi _{{qv}(E)} (\beta )\) has the form \(x \doteq x\), meaning that \({\mathscr{G}}_{[\pi _{{qv}(E)}(\alpha ) \doteq \pi _{{qv}(E)}(\beta )]}^{\Rightarrow }\) is again a single vertex with no edges. If w₁, w₂≠ε, then E is decomposable, a contradiction. Otherwise, \({\mathscr{G}}^{\Rightarrow }_{[E]}\) is a cycle of length \(\max \limits \{|w_{1}|,|w_{2}|\} < |E|\), so again the statement of the lemma follows directly. Thus, for the remainder of the proof, we shall suppose that Card(qv(E)) ≥ 2.

Before proceeding, we remark that for any equation \(E^{\prime }\) given by \(\alpha ^{\prime } \doteq \beta ^{\prime }\), if \(\alpha ^{\prime }[1], \beta ^{\prime }[1] \notin {qv}(E^{\prime })\), then either \(E^{\prime }\) is decomposable, or \(|\alpha ^{\prime }|, |\beta ^{\prime }| \in \{0,1\}\). Both are contradictions to previous assumptions (the former to the fact that E is indecomposable, and hence \(E^{\prime }\) is indecomposable for all \(E^{\prime } \in [E]_{\Rightarrow }\), and the latter to the assumption that Card(qv(E)) ≥ 2 which is only possible if |α|,|β|≥ 2). Consequently, we may partition [E]_⇒ into two sets S₁ and S₂ where S₁ contains all equations \(E^{\prime }\) given by \(\alpha ^{\prime } \doteq \beta ^{\prime }\) such that \(\alpha ^{\prime }[1]\) and \(\beta ^{\prime }[1] \) are both in \( {qv}(E^{\prime })\), and S₂ contains all equations \(E^{\prime }\) given by \(\alpha ^{\prime } \doteq \beta ^{\prime }\) such that exactly one of \(\alpha ^{\prime }[1],\beta ^{\prime }[1]\) is in \({qv}(E^{\prime })\). Intuitively, S₁ will be the set of ‘surviving’ vertices in the isolated path compression while S₂ consists of those vertices which belong only to the ‘isolated paths’ which are contracted/compressed. Supporting this, we show the following two claims regarding elements of S₂.

Claim 4.7.1

Suppose that \(E^{\prime }\in S_{2}\). Then the in-degree and out-degree of \(E^{\prime }\) in \({\mathscr{G}}_{[E]}^{\Rightarrow }\) are both exactly one.

Proof

W.l.o.g. suppose that \(E^{\prime }\) is given by \(x \alpha ^{\prime }_{1} y \alpha _{2}^{\prime } \doteq y \beta ^{\prime }\) with \(y \in {qv}(E^{\prime })\) and \(x \notin {qv}(E^{\prime })\). It follows from the definitions of ⇒_L and ⇒_R that there is no \(E^{\prime \prime }\) such that \(E^{\prime } \Rightarrow _R E^{\prime \prime }\), and exactly one \(E^{\prime \prime }\) such that \(E^{\prime } \Rightarrow _L E^{\prime \prime }\). Thus the out-degree is one as claimed. Now consider the in-degree and let \(E^{\prime \prime } \in [E]_{\Rightarrow }\) such that \(E^{\prime \prime } \Rightarrow E^{\prime }\). Note that by the definition of ⇒_R, we cannot have that \(E^{\prime \prime } \Rightarrow _R E^{\prime }\), so we must have that \(E^{\prime \prime } \Rightarrow _L E^{\prime }\). It follows from the fact that the Nielsen transformation morphisms ψ_y<x are injective that there is exactly one such \(E^{\prime \prime }\), and thus we also have that the in-degree of \(E^{\prime }\) is one as claimed. □

Claim 4.7.2

Proof

Claim 4.7.3

The graph \({\mathscr{G}}_{S_{1}}^{\diamond }\) is an isolated path compression of order |E| of \({\mathscr{G}}_{[E]}^{\Rightarrow }\).

Proof

Directly from Claims 4.7.1 and 4.7.2. □

Claim 4.7.4

Let \(\hat {\alpha _{1}},\hat {\alpha _{2}},\hat {\beta _{1}},\hat {\beta _{2}} \in {qv}(E)^{*}\) such that \(\hat {\alpha _{1}} \doteq \hat {\beta _{1}} \in [\hat {E}]_{\Rightarrow }\), and \(\sigma _{LHS}(\hat {\alpha _{1}}) \doteq \sigma _{RHS}(\hat {\beta _{1}}) \in [E]_{\Rightarrow }\). Then \(\hat {\alpha _{1}} \doteq \hat {\beta _{1}} \Rightarrow \hat {\alpha _{2}} \doteq \hat {\beta _{2}}\) if and only if \(\sigma _{LHS}(\hat {\alpha _{1}}) \doteq \sigma _{RHS}(\hat {\beta _{1}}) \diamond \sigma _{LHS}(\hat {\alpha _{2}}) \doteq \sigma _{RHS}(\hat {\beta _{2}})\).

Proof

Suppose firstly that \(\hat {\alpha _{1}} \doteq \hat {\beta _{1}} \Rightarrow \hat {\alpha _{2}} \doteq \hat {\beta _{2}}\), and w.l.o.g. suppose that \(\hat {\alpha _{1}} \doteq \hat {\beta _{1}} \Rightarrow _L \hat {\alpha _{2}} \doteq \hat {\beta _{2}}\). Then there exist z₁, z₂,…,z_n ∈ qv(E), μ ∈ qv(E)^∗ such that \(\hat {\alpha _{1}} = z_i \mu \) for some i,1 ≤ i ≤ n, \(\hat {\beta _{1}} = z_{1}z_{2} {\ldots } z_n\), \(\hat {\alpha _{2}} = \hat {\alpha _{1}}\) and \(\hat {\beta _{2}} = z_{2}{\ldots } z_{i-1} z_{1} z_i {\ldots } z_n\). Let a₁, a₂,…a_k ∈ (X∖qv(E)) ∪Σ such that σ_RHS(z₁) = z₁a₁a₂…a_k. Let E₀ be given by \(\sigma _{LHS}(z_i \mu ) \doteq \sigma _{RHS}(z_{1}z_{2}{\ldots } z_n)\), and for 1 ≤ j ≤ k, let E_j be given by \(\sigma _{LHS}(z_i \mu ) \doteq a_j a_{j+1} {\ldots } a_k \sigma _{RHS}(z_{2} {\ldots } z_{i-1}) z_{1} a_{1} a_{2} {\ldots } a_{j-1} \sigma _{RHS}(z_i {\ldots } z_n)\), and let E_k+ 1 be given by \(\sigma _{LHS}(z_i \mu ) \doteq \sigma _{RHS}(z_{2} {\ldots } z_{i-1}) z_{1} a_{1} a_{2} {\ldots } a_k \sigma _{RHS}(z_i {\ldots } z_n)\). Then we have E₀ ⇒_LE₁ ⇒_L… ⇒_LE_k+ 1. Moreover, we have that E₀ ∈ S₁ is given by \(\sigma _{LHS}(\hat {\alpha _{1}}) \doteq \sigma _{RHS}(\hat {\beta _{1}})\), E_k+ 1 ∈ S₁ is given by \(\sigma _{LHS}(\hat {\alpha _{2}}) \doteq \sigma _{RHS}(\hat {\beta _{2}})\), and E_j ∈ S₂ for 1 ≤ j ≤ k so E₀ ◇ E_k+ 1 as required.

Now suppose that \(\sigma _{LHS}(\hat {\alpha _{1}}) \doteq \sigma _{RHS}(\hat {\beta _{1}}) \diamond \sigma _{LHS}(\hat {\alpha _{2}}) \doteq \sigma _{RHS}(\hat {\beta _{2}})\). Then by the definition of ◇, there exist E₀, E₁,…,E_k+ 1 ∈ [E]_⇒ such that E₀ ∈ S₁ is given by \(\sigma _{LHS}(\hat {\alpha _{1}}) \doteq \sigma _{RHS}(\hat {\beta _{1}})\), E_k+ 1 ∈ S₁ is given by \(\sigma _{LHS}(\hat {\alpha _{2}}) \doteq \sigma _{RHS}(\hat {\beta _{2}})\), E₀ ⇒_ZE₁ ⇒_Z… ⇒_ZE_k+ 1 for some Z ∈{L, R}, and E_j ∈ S₂ for 1 ≤ j ≤ k.

Theorem 4.8

Let E be a RWE given by \(\alpha \doteq \beta \). Let \(\alpha ^{\prime },\beta ^{\prime }\) be the shortest non-empty prefixes of α, β respectively such that \({var}(\alpha ^{\prime }) \cap {qv}(E) = {var}(\beta ^{\prime }) \cap {qv}(E)\). Let \(E^{\prime }\) be the equation given by \(\pi _{{qv}(E)}(\alpha ^{\prime }) \doteq \pi _{{qv}(E)}(\beta ^{\prime })\). Then \(E^{\prime }\) is basic, and \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\) is isomorphic to an isolated path compression of order |E| of \({\mathscr{G}}^{\Rightarrow }_{[E]}\).

Proof

Let \(S = {qv}(\alpha ^{\prime } \doteq \beta ^{\prime })\). Firstly, we shall show that \(\alpha ^{\prime } \doteq \beta ^{\prime }\) is indecomposable. Suppose for contradiction that \(\alpha ^{\prime } \doteq \beta ^{\prime }\) is decomposable. Then there exist proper prefixes \(\alpha ^{\prime \prime }, \beta ^{\prime \prime }\) of \(\alpha ^{\prime }\) and \(\beta ^{\prime }\) respectively such that \({var}(\alpha ^{\prime \prime }) \cap S = {var}(\beta ^{\prime \prime }) \cap S\). Then \(\alpha ^{\prime \prime }\) and \(\beta ^{\prime \prime }\) are proper prefixes of α and β, and since they are shorter than \(\alpha ^{\prime }\) and \(\beta ^{\prime }\), by our assumptions about \(\alpha ^{\prime }\) and \(\beta ^{\prime }\), we cannot have that \({var}(\alpha ^{\prime \prime }) \cap {qv}(E) = {var}(\beta ^{\prime \prime }) \cap {qv}(E)\). Consequently, either there exists \(x \in {var}(\alpha ^{\prime \prime }) \cap {qv}(E)\) such that \( x\notin {var}(\beta ^{\prime \prime }) \cap {qv}(E)\) or there exists \(x \in {var}(\beta ^{\prime \prime }) \cap {qv}(E)\) such that \(x \notin {var}(\alpha ^{\prime \prime }) \cap {qv}(E)\). W.l.o.g. suppose the former is true. Then \(x \notin {var}(\beta ^{\prime \prime })\), but since x ∈ qv(E), it follows from \({var}(\alpha ^{\prime }) \cap {qv}(E) = {var}(\beta ^{\prime }) \cap {qv}(E)\) that \(x \in {var}(\beta ^{\prime })\). However, this implies that x ∈ S, and since \(x \in {var}(\alpha ^{\prime \prime })\) but \(x\notin {var}(\beta ^{\prime \prime })\), we arrive at a contradiction to our assumption that \({var}(\alpha ^{\prime \prime }) \cap S = {var}(\beta ^{\prime \prime }) \cap S\).

Now, let \(E^{\prime \prime }\) be the equation given by \(\pi _{S}(\alpha ^{\prime }) \doteq \pi _S(\beta ^{\prime })\). By the assumption that \({var}(\alpha ^{\prime }) \cap {qv}(E) = {var}(\beta ^{\prime }) \cap {qv}(E)\), there is no variable x ∈ qv(E)∖S occurring in \(\alpha ^{\prime }\) or \(\beta ^{\prime }\). Consequently, \(E^{\prime \prime } = E^{\prime }\), and by Lemma 4.7, we have that \({\mathscr{G}}^{\Rightarrow }_{[E^{\prime }]}\) is isomorphic to an isolated path compression of order |E| of \({\mathscr{G}}^{\Rightarrow }_{[\alpha ^{\prime } \doteq \beta ^{\prime }]}\), which by Corollary 4.4 is isomorphic to \({\mathscr{G}}^{\Rightarrow }_{[E]}\). □

Definition 5.1 (The invariant Υ _E)

Let E be a basic RWE such that Card(var(E)) > 1. Let # be a new symbol not in X. Then we may write E as \(x \alpha _{1} y \alpha _{2} \doteq y \beta _{1} x \beta _{2}\) with x, y ∈ X and α₁, α₂, β₁, β₂ ∈ (X∖{x, y})^∗. Let \({\mathscr{Z}}_E = {var}(\alpha _{1}\alpha _{2}\beta _{1}\beta _{2}) \cup \{\#\}\). Let the function \(Q_E : \mathcal {Z}_E \to X^2\) be defined as follows: for each \(z \in \mathcal {Z}_E \backslash \{\#\}\), let Q_E(z) = (u, v) where uz is a factor of xα₁yα₂ and vz is a factor of yβ₁xβ₂. Let Q_E(#) = (u, v) where uy is a factor of xα₁yα₂ and vx is a factor of yβ₁xβ₂. Let \({\varUpsilon }_{\!E} = \{Q_E(z) \mid z \in \mathcal {Z}_E\}\). If Card(var(E)) ≤ 1, then Υ_E = ∅.

Remark 5.2

Let E be a basic regular word equation given by \(\alpha y \doteq \beta x\) with x, y ∈ X and α, β ∈ X^∗. Then for each z ∈ var(α), there is exactly one element (u, v) ∈Υ_E such that u = z. For each z∉var(α), there is no element (u, v) ∈Υ_E such that u = z. Similarly, for each w ∈ var(β), there is exactly one element (u, v) ∈Υ_E such that v = w and for each w∉var(β), there is no element (u, v) ∈Υ_E such that v = w.

Theorem 5.3

Let E₁, E₂ be basic RWEs such that E₁ ⇒^∗E₂. Then \({\varUpsilon }_{\!E_{1}} = {\varUpsilon }_{\!E_{2}}\).

Proof

Suppose that we have the first case, then \(\mathcal {Z}_{E_{1}} = {var}(\alpha _{1}\alpha _{2}\alpha _3) \cup \{\#, w\}\) and \(\mathcal {Z}_{E_{2}} = {var}(\alpha _{1}\alpha _{2}\alpha _3) \cup \{\#,y\}\). Moreover, for each z ∈ var(α₁α₂α₃), there exist u, v ∈ X such that uz (resp. vz) is a factor of the LHS (resp. RHS) of both E₁ and E₂, so \(Q_{E_{1}}(z) = Q_{E_{2}}(z)\). Now, let a, b, c be the rightmost variables in xα₁, wα₂ and wβ₁ respectively (i.e. their length-1 suffixes). Then we have that \(Q_{E_{1}}(w) = (a,y)\), \(Q_{E_{1}}(\#) = (b,c)\), \(Q_{E_{2}}(y) = (b,c)\), and \(Q_{E_{2}}(\#) = (a,y)\). Thus \({\varUpsilon }_{\!E_{1}} = {\varUpsilon }_{\!E_{2}}\).

Now suppose instead that we have the second case. Similarly to the first case, we have that \(\mathcal {Z}_{E_{1}} = {var}(\alpha _{1}\alpha _{2}\alpha _3) \cup \{\#, w\}\), \(\mathcal {Z}_{E_{2}} = {var}(\alpha _{1}\alpha _{2}\alpha _3) \cup \{\#,y\}\) and for each z ∈ var(α₁α₂α₃), \(Q_{E_{1}}(z) = Q_{E_{2}}(z)\). Now, let a, b, c be the rightmost variables in xα₁, wβ₁ and yα₂ respectively. Then we have that \(Q_{E_{1}}(w) = (c,y)\), \(Q_{E_{1}}(\#) = (a,b)\), \(Q_{E_{2}}(y) = (c,y)\), and \(Q_{E_{2}}(\#) = (a,b)\). Thus \({\varUpsilon }_{\!E_{1}} = {\varUpsilon }_{\!E_{2}}\) in both cases as required. □

Definition 6.1 (Jumbled Equations and Δ(E))

Let E be a basic RWE and let Δ(E) = {x ∈ var(E)∣(x, x) ∈Υ_E}. If Card(Δ(E)) = 0, then E is jumbled.

Remark 6.2

Let E be a basic RWE. It follows directly from Definition 5.1 that if Card(var(E)) < 2, then Card(Δ(E)) = 0. Otherwise, E can be written as \(\alpha x \doteq \beta y\) for some x, y ∈ X, α ∈ (X∖{x})^∗ and β ∈ (X∖{y})^∗. Since E is basic, it is indecomposable, so we may additionally conclude that x≠y. By Remark 5.2, neither (x, x) nor (y, y) can be contained in Υ_E, so we must have Card(Δ(E)) ≤Card(var(E)) − 2.

Lemma 6.3

Let E be a basic RWE given by \(\alpha \doteq \beta \) and let Y = var(E)∖Δ(E). Then the equation E_Y given by \(\pi _Y(\alpha ) \doteq \pi _Y(\beta )\) is a jumbled basic RWE.

Proof

If Δ(E) = ∅, then the lemma holds trivially. Assume that Δ(E)≠∅. We shall prove the following statement, from which the lemma follows by a simple induction.

Claim 6.3.1

Suppose that E is a basic RWE given by \(\alpha \doteq \beta \), and that x ∈Δ(E). Let \(E^{\prime }\) be the equation \(\pi _{{var}(E)\backslash \{x\}}(\alpha ) \doteq \pi _{{var}(E)\backslash \{x\}}(\beta )\). Then \(E^{\prime }\) is a basic RWE and \({\varUpsilon }_{E^{\prime }} = {\varUpsilon }_{E} \backslash \{ (x,x) \}\).

Proof

Let \(Q_E, \mathcal {Z}_E\) be defined as per Definition 5.1. We shall consider two cases depending on whether Q_E(#) = (x, x). Suppose firstly that Q_E(#)≠(x, x). Then there exist α₁, α₂, β₁, β₂ such that α = α₁xyα₂, β = β₁xyβ₂, π_var(E)∖{x}(α) = α₁yα₂ and π_var(E)∖{x}(β) = β₁yβ₂. Suppose for contradiction that \(E^{\prime }\) is not basic. Clearly both sides of \(E^{\prime }\) belong to \({qv}(E^{\prime })\), so we may infer that \(E^{\prime }\) is decomposable, and thus that there exist proper prefixes \(\alpha ^{\prime }\) and \(\beta ^{\prime }\) of α₁yα₂ and β₁yβ₂ respectively such that \({var}(\alpha ^{\prime }) \cap {qv}(E^{\prime }) = {var}(\beta ^{\prime }) \cap {qv}(E^{\prime })\). Clearly, either y occurs in both \(\alpha ^{\prime }\) and \(\beta ^{\prime }\), or in neither. Let \({\tau } : {var}(E^{\prime })^{*} \to {var}(E)^{*}\) be the morphism such that τ(y) = xy and τ(z) = z for \(z \in {var}(E^{\prime }) \backslash \{y\}\). Then \(\alpha ^{\prime \prime } = {\tau }(\alpha ^{\prime })\) and \(\beta ^{\prime \prime } = {\tau }(\beta ^{\prime })\) are proper prefixes of α and β respectively which satisfy \({var}(\alpha ^{\prime \prime }) \cap {qv}(E) = {var}(\beta ^{\prime \prime }) \cap {qv}(E)\). Thus E is decomposable and therefore not basic, a contradiction.

To see that \({\varUpsilon }_{\!E^{\prime }} = {\varUpsilon }_{\!E} \backslash \{(x,x)\}\), suppose firstly that x is not a prefix of α or β, and thus that α₁≠ε and β₁≠ε. Then \( \mathcal {Z}_{E} = ({var}(E) \backslash \{ \alpha _{1}[1], \beta _{1}[1]\}) \cup \{\#\} \), and \(\mathcal {Z}_{E^{\prime }} = ({var}(E) \backslash \{ \alpha _{1}[1], \beta _{1}[1], x\} ) \cup \{\#\}\). It follows from the definitions that \(Q_{E^{\prime }}(y) = Q_{E}(x) = (\alpha _{1}[|\alpha _{1}|], \beta _{1}[|\beta _{1}|])\). Since α₁, β₁≠ε, α₁[1]∉{x, y} and β₁[1]∉{x, y}. Consequently there exist u_#, v_# ∈ var(E)∖{x} such that u_#α₁[1] is a factor of both α and π_var(E)∖{x}(α) and such that v_#β₁[1] is a factor of both β and π_var(E)∖{x}(β). It follows that \(Q_E(\#) = Q_{E^{\prime }}(\#) = (u_\#,v_\#)\). Likewise, for any z∉{x, y, α₁[1],β₁[1]}, there exist u, v ∈ var(E)∖{x} such that uz is a factor of both α and π_var(E)∖{x}(α) and such that vz is a factor of both β and π_var(E)∖{x}(β). It follows that \(Q_E(z) = Q_{E^{\prime }}(z) = (u,v)\). Thus we may conclude that \({\varUpsilon }_{\!E^{\prime }} = {\varUpsilon }_{\!E} \backslash \{(x,x)\}\).

Next, suppose that α₁ = ε and β₁≠ε (the case that β₁ = ε and α₁≠ε is symmetric). Then \(\mathcal {Z}_{E} = ({var}(E) \backslash \{x,\beta _{1}[1] \}) \cup \{\#\}\) and \(\mathcal {Z}_{E^{\prime }} = ({var}(E) \backslash \{y,x,\beta _{1}[1] \}) \cup \{\#\}\). Then Q_E(#) = (u_#, β₁[|β₁|]) where u_#β₁[1] is a factor of xyα₂. Since E is regular, each variable occurs once per side, so we may infer that β₁[1]≠y, and hence that u_#≠x. It follows that u_#β₁[1] is also a factor of yα₂, so we may further conclude that \(Q_{E^{\prime }}(\#) = (u_\#,\beta _{1}[|\beta _{1}|]) = Q_E(\#)\). Note that Q_E(y) = (x, x). Let z ∈ var(E)∖{x, y, β₁[1]}. Then there exist u, v ∈ var(E)∖{x} such that uz is a factor of both xyα₂ and yα₂, and such that vz is a factor of both β₁xyβ₂ and β₁yβ₂. It follows that \(Q_E(z) = Q_{E^{\prime }}(z) = (u,v)\). Again we have \({\varUpsilon }_{E^{\prime }} = {\varUpsilon }_{E}\backslash \{(x,x)\}\). Finally, note that if α₁ = β₁ = ε, then E is decomposable, which is a contradiction to the assumption that E is basic.

It remains to consider the case that Q_E(#) = (x, x). This implies that there exist u, v ∈ var(E)∖{x} and α₁, α₂, β₁, β₂ ∈ var(E)^∗ such that α = uα₁xvα₂, β₂ = vβ₁xuβ₂, meaning \(E^{\prime }\) is given by \(u \alpha _{1} v \alpha _{2} \doteq v \beta _{1} u \beta _{2}\). Suppose for contradiction that \(E^{\prime }\) is not basic. Then as in the previous case, it must be decomposable, and there exist proper prefixes \(\alpha ^{\prime }, \beta ^{\prime }\) of uα₁vα₂ and vβ₁uβ₂ respectively which satisfy \({var}(\alpha ^{\prime }) \cap {qv}(E^{\prime }) = {var}(\beta ^{\prime }) \cap {qv}(E^{\prime })\). Then we must have that \(\alpha ^{\prime } = u \alpha _{1} v \alpha _3\) and \(\beta ^{\prime } = v \beta _{1} u \beta _3\) for some α₃, β₃ ∈ X^∗. However, it follows that \(\alpha ^{\prime \prime } = u \alpha _{1} x v \alpha _3\) and \(\beta ^{\prime \prime } = v \beta _{1} x u \beta _3\) are proper prefixes of α and β satisfying \({var}(\alpha ^{\prime \prime }) \cap {qv}(E) = {var}(\beta ^{\prime \prime }) \cap {qv}(E)\), so E is decomposable which is a contradiction to the assumption that E is basic.

To see that \({\varUpsilon }_{\!E^{\prime }} = {\varUpsilon }_{\!E} \backslash \{(x,x)\}\), note that in this case \(\mathcal {Z}_E = ({var}(E) \backslash \{u,v\}) \cup \{\#\}\) and \(\mathcal {Z}_{E^{\prime }} = ({var}(E) \backslash \{u,v,x\}) \cup \#\). It follows from the definitions that \(Q_{E^{\prime }}(\#) = Q_{E}(x) = (w_{1},w_{2})\), where w₁ is the leftmost variable in uα₁ and w₂ is the leftmost variable in vβ₁. Moreover, for any z ∈ var(E)∖{u, v, x}, there exist \(w_{1}^{\prime },w_{2}^{\prime } \in {var}(E)\backslash \{x\}\) such that \(w_{1}^{\prime }z\) is a factor of both uα₁xvα₂ and uα₁vα₂, and such that \(w_{2}^{\prime }z\) is a factor of both vβ₁xuβ₂ and vβ₁uβ₂, meaning that \(Q_{E^{\prime }}(z) = Q_{E}(z) = (w_{1}^{\prime },w_{2}^{\prime })\). It follows that \({\varUpsilon }_{E^{\prime }} = {\varUpsilon }_{E}\backslash \{(x,x)\}\) as required. □

Definition 6.4 (The set Φ _E)

Let E be a basic RWE. Let Y = var(E)∖Δ(E). Let Φ_E be the set of morphisms φ : Y^∗→ var(E)^∗ satisfying φ(y) ∈Δ(E)^∗y for all y ∈ Y, and \(\sum \limits _{y \in Y} |{\varphi }(y)|_x = 1\) for all x ∈Δ(E).

Definition 6.5 (\(V_{\varphi }^E, U_{\varphi }^E\) and \(H_{\varphi }^E\))

Definition 6.6 (Close morphisms φ ₁, φ ₂ ∈Φ _E)

Lemma 6.7

Let E be a basic RWE and suppose that \({\varphi }^{\prime }, {\varphi }^{\prime \prime } \in {{\varPhi }}_E\) with \({\varphi }^{\prime } \not = {\varphi }^{\prime \prime }\). Then there exist k ≤ 4Card(Δ(E)) + 1 and φ₁, φ₂, φ₃,…,φ_k ∈Φ_E such that \({\varphi }^{\prime } = {\varphi }_{1}\), \({\varphi }^{\prime \prime } = {\varphi }_k\), and φ_i, φ_i+ 1 are close for all i,1 ≤ i < k.

Proof

Let Y = var(E)∖Δ(E). If Δ(E) = ∅, then Φ_E contains only the identity morphism. Thus we may assume that Δ(E)≠∅ and consequently by Remark 6.2 that Card(Y ) ≥ 2. Note the following claim.

Claim 6.7.1

Proof

Let φ₃ be the morphism such that φ₃(y₁) = γ₂y₁, φ₃(y₂) = γ₁zφ₁(y₂), and φ₃(y) = φ₁(y) for all y ∈ Y ∖{y₁, y₂}. Then it follows directly from the definitions that φ₁, φ₃ are close. Moreover, since φ₂(y) = φ₁(y) for all y ∈ Y ∖{y₁, y₂}, it also follows from the definitions that φ₂, φ₃ are also close. □

Theorem 6.8

Proof of Theorem 6.8

The rest of the section focuses on the proof of Theorem 6.8. The main technical content is presented in the following series of lemmas. Statement 1 is given by Lemmas 6.15 and 6.16, while Statements 2 and 3 are given by Lemmas 6.17 and 6.18 respectively. Throughout the remainder of this section, for a basic RWE E given by \(\alpha \doteq \beta \) and a morphism φ, we shall use the notation φ(E) as shorthand for \({\varphi }(\alpha ) \doteq {\varphi }(\beta )\). We begin by noting some properties of equations belonging to the sets \(H_{\varphi }^E\). The first deals with equations belonging to \(V_{\varphi }^E\) and follows directly from the definitions.

Fact 6.9

Lemma 6.10

Proof

Now suppose instead that \(E^{\prime } \in U_{\varphi }^E\). Then there exists some \(E^{\prime \prime } \in V_{\varphi }^E\), \(k \in \mathbb {N}\) and Z ∈{L, R} such that \(E^{\prime \prime } \Rightarrow _Z^k E^{\prime }\). Suppose we choose \(E^{\prime \prime },Z\) and k such that k is minimal. Suppose additionally that Z = L. We shall show that Statement 1 of the lemma is satisfied. The case that Z = R is symmetric and results in Statement 2 being satisfied.

Lemma 6.11

Let E be a basic RWE. Let Y = var(E)∖Δ(E) and let E_Y = π_Y(E). Then there exists φ ∈Φ_E such that φ(E_Y) ∈ [E]_⇒.

Proof

Note that if Δ(E) = ∅, then E_Y = E and Φ_E contains only the identity morphism, so the lemma holds trivially. Suppose that Δ(E)≠∅. By Remark 6.2, we may therefore assume that E is a basic RWE with at least two variables, so may write it as \( x \alpha _{1} u_{1} u_{2} {\ldots } u_n y \alpha _{2} \doteq y \beta _{1} u_{1} u_{2} {\ldots } u_n x \beta _{2}\) where x, y, u₁, u₂,…,u_n ∈ X are pairwise distinct variables and α₁, α₂, β₁, β₂ ∈ (var(E)∖{x, y, u₁, u₂,…,u_n})^∗, and such that α₁ and β₁ do not share a common non-empty suffix. Then \(E\Rightarrow ^{*}_R E^{\prime }\) where \(E^{\prime }\) is given by \(u_{1}u_{2} {\ldots } u_n x \alpha _{1} y \alpha _{2} \doteq y \beta _{1} u_{1} u_{2} {\ldots } u_n x \beta _{2}\).

Now, consider the function \(Q_{E^{\prime }}\) as defined in Definition 5.1. Note in particular that \(Q_{E^{\prime }}(\#) = (v,w)\) where v, w ∈ X are the length-1 suffixes of xα₁ and yβ₁, and hence v≠w. By Theorem 5.3, \({\varUpsilon }_{\!E} = {\varUpsilon }_{\!E^{\prime }}\) (and hence \({{\varDelta }}(E) = {{\varDelta }}(E^{\prime })\)). Thus, for every z ∈Δ(E), there exists \(z^{\prime } \in {var}(E)\) such that \(Q_{E^{\prime }}(z^{\prime }) = (z,z)\), meaning that z occurs directly to the left of \(z^{\prime }\) on both the LHS and RHS of \(E^{\prime }\). It follows that each z ∈Δ(E) has a unique ‘successor’ variable \(z^{\prime }\) occurring to the right of z on both sides of the equation, and therefore that there exists some morphism φ ∈Φ_E such that \(E^{\prime } = {\varphi }(\pi _Y(E^{\prime }))\). Finally, notice that \(u_i \in {{\varDelta }}(E^{\prime }) = {{\varDelta }}(E)\) for 1 ≤ i ≤ n, and consequently, \(\pi _Y(E^{\prime })= \pi _Y(E) = E_Y\). □

Lemma 6.12

Proof

Note that if Card(Y ) < 2, then [E_Y]_⇒ is a singleton and the lemma holds trivially. We may therefore assume that Card(Y ) ≥ 2. Suppose that Z = R. The case that Z = L is symmetric. Then there exist x, y ∈ Y and α₁, α₂, β₁, β₂ ∈ Y^∗ such that \(E^{\prime }\) may be written as \(x \alpha _{1} y \alpha _{2} \doteq y \beta _{1} x \beta _{2}\) and \(E^{\prime \prime }\) may be written as \(\alpha _{1} xy \alpha _{2} \doteq y \beta _{1} x \beta _{2}\). Let \(E_0 = {\varphi }(E^{\prime })\) and \(E_{k+1} = {\varphi }(E^{\prime \prime })\). If φ(x) = x, then E₀ ⇒_RE_k+ 1 so the lemma holds for k = 0. Suppose that φ(x)≠x.

Lemma 6.13

Let E be a basic RWE. Then there exist n₁, n₂ < |E|² and \(\hat {E}\) such that \(E \Rightarrow ^{n_{1}} \hat {E}\) and \(\hat {E} \Rightarrow ^{n_{2}} E\) where \(\hat {E}\) can be written as \(x \alpha y \doteq y \beta x\) where x, y ∈ var(E) and α, β ∈ (var(E)∖{x, y})^∗

Proof

We shall prove the case that \(E \Rightarrow ^{n_{1}} \hat {E}\). The case that \(\hat {E} \Rightarrow ^{n_{2}} E\) is easily adapted. Recall that we may write any basic RWE as \(x \alpha _{1} y \alpha _{2} \doteq y \beta _{1} x \beta _{2}\) where x, y ∈ X and α₁, α₂, β₁, β₂ ∈ (X∖{x, y})^∗. We have the following claim:

Claim 6.13.1

For every basic, regular equation E given by \(x \alpha _{1} y \alpha _{2} \doteq y \beta _{1} x \beta _{2}\), either α₂ = β₂ = ε, or there exists n < |E| and \(E^{\prime }\) such that \(E\Rightarrow ^n E^{\prime }\) and \(E^{\prime }\) may be written as \(x^{\prime } \alpha _{1}^{\prime } y^{\prime } \alpha _{2}^{\prime } \doteq y^{\prime } \beta _{1}^{\prime } x^{\prime } \beta _{2}^{\prime }\) where \(x^{\prime },y^{\prime } \in X\), \(\alpha _{1}^{\prime },\alpha _{2}^{\prime },\beta _{1}^{\prime },\beta _{2}^{\prime } \in (X \backslash \{x^{\prime },y^{\prime }\})^{*}\), and such that \(|\alpha _{1}^{\prime }|+ |\beta _{1}^{\prime }| > |\alpha _{1}| + |\beta _{1}|\).

Proof

Let E be given by \(x \alpha _{1} y \alpha _{2} \!\doteq \! y \beta _{1} x \beta _{2}\) where x, y ∈ var(E) and α₁, α₂, β₁, β₂ ∈ (var(E)∖{x, y})^∗. We have two cases, either var(α₁) = var(β₁), in which case, due to the fact that E is basic and therefore indecomposable, we must have that α₂ = β₂ = ε, so the claim holds. Otherwise, there exists z ∈ (var(α₁)∖var(β₁)) ∪ (var(β₁)∖var(α₁)). W.l.o.g. suppose that z ∈ var(α₁)∖var(β₁). Then since E is regular, z ∈ var(β₂) and we can write E as \(x \gamma _{1} z \gamma _{2} y \alpha _{2} \doteq y \beta _{1} x \delta _{1} z \delta _{2}\) where γ₁, γ₂, δ₁, δ₂ ∈ (var(E)∖{x, y, z})^∗. Consequently, we have that \(E \Rightarrow _R^{*} E^{\prime }\) where \(E^{\prime }\) is given by \(z \gamma _{2} x \gamma _{1} y \alpha _{2} \doteq y \beta _{1} x \delta _{1} z \delta _{2}\). By Remark 3.2, we have that \(E\Rightarrow ^n E^{\prime }\) where n < |E|. Moreover, \(E^{\prime }\) clearly has the form described in the claim as witnessed by \(x^{\prime } = z\), \(y^{\prime } = y\), \(\alpha _{1}^{\prime } = \gamma _{2} x \gamma _{1}\), \(\alpha _{2}^{\prime } = \alpha _{2}\), \(\beta _{1}^{\prime } = \beta _{1} x \delta _{1}\) and \(\beta _{2}^{\prime } = \delta _{2}\). □

Lemma 6.14

Let E be a basic RWE. Let Y = var(E)∖Δ(E) and let E_Y = π_Y(E). Let φ₁, φ₂ ∈Φ_E. Then \(H^E_{{\varphi }_{1}} \cap H^E_{{\varphi }_{2}} \not = \emptyset \) if and only if φ₁, φ₂ are close.

Proof

If Card(Y ) < 2, then Φ_E consists of the identity morphism only so the statement holds trivially. Suppose that Card(Y ) ≥ 2. Suppose firstly that φ₁, φ₂ are close. Then there exist y₁, y₂ ∈ Y with y₁≠y₂ and γ₁, γ₂ ∈Δ(E)^∗ such that φ₁(y₁) = γ₁γ₂y₁, φ₂(y₁) = γ₂y₁, φ₂(y₂) = γ₁φ₁(y₂), and for y ∈ Y ∖{y₁, y₂}, φ₁(y) = φ₂(y). In order to show that \(H^E_{{\varphi }_{1}} \cap H^E_{{\varphi }_{2}} \not = \emptyset \), we need the following claim.

Claim 6.14.1

Proof

By Lemma 6.13, there exists \(\hat {E}^{\prime } \in [E_Y]_{\Rightarrow }\) such that \(\hat {E}^{\prime }\) may be written as \(x \hat {\alpha } z \doteq z \hat {\beta } x\) where x, z ∈ Y, x≠z and \(\hat {\alpha },\hat {\beta } \in (Y \backslash \{x,z\})^{*}\). By Lemma 6.3, E_Y is basic, meaning that each variable in Y = var(E_Y) occurs exactly once on each side of E_Y. It follows by properties of ⇒ that each variable in Y also occurs exactly once in each of \(x \hat {\alpha } z\) and \(z \hat {\beta } x\). Hence there exist \(\hat {\alpha }^{\prime }, \hat {\alpha }^{\prime \prime } \in (Y \backslash \{y_{2}\})^{*}\) such that \(x \hat {\alpha } z = \hat {\alpha }^{\prime } y_{2} \hat {\alpha }^{\prime \prime }\) (and such that y₁ occurs in either \(\hat {\alpha }^{\prime }\) or \(\hat {\alpha }^{\prime \prime })\).

so \(y_{2} \hat {\alpha }^{\prime \prime \prime } \hat {\alpha }^{\prime } z \doteq y_{1} \hat {\beta }^{\prime \prime } \hat {\beta }^{\prime } y_{2} \hat {\beta }^{\prime \prime \prime } \in [E_Y]_{\Rightarrow }\). Since y₁ occurs either in \(\hat {\alpha }^{\prime }\) or in \(\hat {\alpha }^{\prime \prime } = \hat {\alpha }^{\prime \prime \prime }z\), we may write \(\hat {\alpha }^{\prime \prime \prime } \hat {\alpha }^{\prime } z\) as \(\hat {\alpha }_{1} y_{1} \hat {\alpha }_{2}\) for some \(\hat {\alpha }_{1},\hat {\alpha }_{2} \in (Y\backslash \{y_{1},y_{2}\})^{*}\). Thus the first statement of the lemma holds with \(\hat {\beta }_{1} = \hat {\beta }^{\prime \prime } \hat {\beta }^{\prime }\) and \(\hat {\beta }_{2} = \hat {\beta }^{\prime \prime \prime }\). □

Claim 6.14.2

Let \({\varphi }^{\prime },{\varphi }^{\prime \prime } \in {{\varPhi }}_E\) and \(\mu ^{\prime }, \mu ^{\prime \prime } \in Y^{*}\) such that \(|\mu ^{\prime }|_y = |\mu ^{\prime \prime }|_y = 1\) for all y ∈ Y. If \({\varphi }^{\prime }(\mu ^{\prime }) = {\varphi }^{\prime \prime }(\mu ^{\prime \prime })\), then \({\varphi }^{\prime } = {\varphi }^{\prime \prime }\) and \(\mu ^{\prime } = \mu ^{\prime \prime }\).

Proof

Suppose that \({\varphi }^{\prime }(\mu ^{\prime }) = {\varphi }^{\prime \prime }(\mu ^{\prime \prime })\). It follows from the definition of Φ_E that for any φ ∈Φ, the morphism π_Y ∘ φ is the identity over Y. Thus \(\mu ^{\prime } = \pi _Y({\varphi }^{\prime }(\mu ^{\prime })) = \pi _Y({\varphi }^{\prime \prime }(\mu ^{\prime \prime })) = \mu ^{\prime \prime }\). Furthermore, for each y ∈ Y, we may uniquely reconstruct \({\varphi }^{\prime }(y)\) and \({\varphi }^{\prime \prime }(y)\) as the longest factors of the form Δ(E)^∗y in \({\varphi }^{\prime }(\mu ^{\prime })\) and \({\varphi }^{\prime \prime }(\mu ^{\prime \prime })\) respectively. It follows from the definition of Φ_E and the fact that \(|\mu ^{\prime }|_y, |\mu ^{\prime \prime }|_y = 1\) that these factors will exist and be unique. Thus, under the assumption that \({\varphi }^{\prime }(\mu ^{\prime }) = {\varphi }^{\prime \prime }(\mu ^{\prime \prime })\), it follows that \({\varphi }^{\prime }(y) = {\varphi }^{\prime \prime }(y)\) for all y ∈ Y and hence \({\varphi }^{\prime } = {\varphi }^{\prime \prime }\). □

Lemma 6.15

Let E be a basic RWE. Then \(H_{\varphi }^E \subseteq [E]_{\Rightarrow }\) for each φ ∈Φ_E.

Proof

Let Y = var(E)∖Δ(E) and let E_Y = π_Y(E). By Lemma 6.11, there exists φ ∈Φ_E such that φ(E_Y) ∈ [E]_⇒. Let \(\tilde {E} \in H^E_{{\varphi }^{\prime }}\) for some arbitrary \({\varphi }^{\prime } \in {{\varPhi }}_E\). By Lemma 6.7, there exist k ≤ 4Card(Δ(E)) + 1 and φ₁, φ₂,…,φ_k ∈Φ_E such that \({\varphi } = {\varphi }_{1}, {\varphi }^{\prime } = {\varphi }_k\), and for 1 ≤ i < k, φ_i and φ_i+ 1 are close. Thus, by Lemma 6.14, there exist E₁, E₂,…,E_k such that \(E_i \in H^E_{{\varphi }_i} \cap H^E_{{\varphi }_{i+1}} \) for 1 ≤ i < k.

It follows from Lemma 6.12 that if \(E^{\prime },E^{\prime \prime } \in H^E_{{\varphi }_i}\) for some i,1 ≤ i ≤ k, then \(E^{\prime } \Rightarrow ^{*} E^{\prime \prime }\). Thus, φ(E_Y) ⇒^∗φ(E₁), \(E_k \Rightarrow ^{*} \tilde {E}\), and for 1 ≤ i ≤ k, E_i ⇒^∗E_i+ 1. Consequently, \(\tilde {E} \in [E]_{\Rightarrow }\). Since this holds for all \(\tilde {E} \in {\mathscr{H}}^E_{{\varphi }^{\prime }}\) for all \({\varphi }^{\prime } \in {{\varPhi }}_E\), the lemma follows. □

Lemma 6.16

Let E be a basic RWE. Let Y = var(E)∖Δ(E), let E_Y = π_Y(E), and let φ ∈Φ_E. Then \({\mathscr{G}}^{\Rightarrow }_{[E_Y]}\) is isomorphic to an isolated path contraction of order Card(Δ(E)) of \({\mathscr{H}}_{\varphi }^E\).

Proof

For k ≥ 0, we shall say that a sequence of equations E₀, E₁,…,E_k+ 1 as a U-path if \(E_0, E_{k+1} \in V^E_{\varphi }\), \(E_i \in U^E_{\varphi }\) for 1 ≤ i ≤ k, and there exists Z ∈{L, R} such that E₀ ⇒_ZE₁ ⇒_ZE₂ ⇒_Z… ⇒_ZE_k ⇒_ZE_k+ 1. Let ◇ be the relation on \(V_{\varphi }^E\) such that \(E^{\prime } \diamond E^{\prime \prime }\) if and only if \(E^{\prime },E^{\prime \prime } \in V_{\varphi }^E\) and there exists a U-path starting with \(E^{\prime }\) and ending with \(E^{\prime \prime }\). We shall show firstly that the graph \({\mathscr{G}}^{\diamond }_{V_{\varphi }^E}\) is an isolated path compression of order Card(Δ(E)) of \({\mathscr{H}}_{\varphi }^E\), and secondly that \({\mathscr{G}}^{\Rightarrow }_{[E_Y]}\) is isomorphic to \({\mathscr{G}}^{\diamond }_{V_{\varphi }^E}\).

Clearly, every U-path is a path in \({\mathscr{H}}^E_{\varphi }\). Moreover, it follows from the definition of \(H^E_{\varphi }\), along with the fact that \(\Rightarrow _Z^{*}\) is an equivalence relation for Z ∈{L, R}, that for every vertex \(E^{\prime } \in U^E_{\varphi }\), there exist \(E^{\prime \prime },E^{\prime \prime \prime } \in V^E_{\varphi }\) and Z ∈{L, R} such that \(E^{\prime \prime } \Rightarrow _Z^{*} E^{\prime }\) and \(E^{\prime } \Rightarrow _Z^{*} E^{\prime \prime \prime }\). Consequently, every vertex in \({\mathscr{H}}^E_{\varphi }\) either belongs to \(V^E_{\varphi }\) or is the internal vertex of some U-path. It follows as a direct consequence of the following claim that U-path containing a given vertex in \(U_{\varphi }^E\) is unique, and therefore that no two distinct U-paths share an internal vertex. Thus \({\mathscr{G}}^{\diamond }_{V_{\varphi }^E}\) is an isolated path compression of order k of \({\mathscr{H}}_{\varphi }^E\) where k is the number of internal vertices in the longest U-path in \({\mathscr{H}}_{\varphi }^E\).

Claim 6.16.1

Let \(E^{\prime } \in U_{\varphi }^E\). Then the in- and out-degrees of \(E^{\prime }\) in \({\mathscr{H}}_{\varphi }^E\) are exactly one.

Proof

Claim 6.16.2

Proof

Claim 6.16.3

Let \(\hat {E}_{1},\hat {E}_{2} \in [E_Y]_{\Rightarrow }\). Then \(\hat {E}_{1} \Rightarrow \hat {E}_{2}\) if and only if \({\varphi }(\hat {E}_{1}) {\diamond } {\varphi }(\hat {E}_{2})\).

Proof

Lemma 6.17

Let E be a basic RWE. Then \({\mathscr{G}}^{\Rightarrow }_{[E]} = \bigcup \limits _{{\varphi } \in {{\varPhi }}_E} {\mathscr{H}}^E_{\varphi }\).

Proof

We have already shown in Lemma 6.15 that each vertex of \(\bigcup \limits _{{\varphi } \in {{\varPhi }}_E} {\mathscr{H}}^E_{\varphi }\) is a vertex of \({\mathscr{G}}^{\Rightarrow }_{[E]}\). Moreover, it follows directly from the definition of \({\mathscr{H}}^E_{\varphi }\) that each edge in \(\bigcup \limits _{{\varphi } \in {{\varPhi }}_E} {\mathscr{H}}^E_{\varphi }\) is also an edge of \({\mathscr{G}}^{\Rightarrow }_{[E]}\). It remains to show that each vertex/edge of \({\mathscr{G}}^{\Rightarrow }_{[E]}\) is a vertex/edge of \({\mathscr{H}}^E_{\varphi }\) for some φ ∈Φ_E. The main step is Claim 6.17.1 as follows.

Claim 6.17.1

For every \(E^{\prime } \in [E]_{\Rightarrow }\), and Z ∈{L, R}, there exists φ ∈Φ_E and \(E^{\prime \prime } \in V_{\varphi }^E\) such that \(E^{\prime \prime } \Rightarrow _Z^{*} E^{\prime }\).

Proof

Note that by Lemma 6.11, there exists E₀ ∈ [E]_⇒ and φ₀ ∈Φ_E such that \(E_0 \in V_{{\varphi }_0}^E\) and thus the claim holds for \(E_0 = E^{\prime }\). Note also that for every \(E^{\prime } \in [E]_{\Rightarrow }\), since ⇒^∗ is an equivalence relation, we have \(E_0 \Rightarrow ^{*} E^{\prime }\). Thus it is sufficient to show that if the claim holds for E_i and E_i ⇒ E_i+ 1, then it also holds for E_i+ 1.

Suppose that the claim holds for E_i ∈ [E]_⇒ and that \(E_i \Rightarrow _{Z_i} E_{i+1}\). Then there exist φ_i ∈Φ_E and \(E^{\prime \prime }_i \in V^E_{{\varphi }_i}\) such that \(E^{\prime \prime }_i \Rightarrow _{Z_i}^{*} E_i\) and thus \(E^{\prime \prime }_i \Rightarrow _{Z_i}^{*} E_{i+1}\). Thus \(E_{i+1} \in H^E_{{\varphi }_i}\). If \(E_{i+1} \in V^E_{{\varphi }_i}\), then the claim holds trivially. Suppose instead that \(E_{i+1} \in U_{{\varphi }_i}^E\).

Consequently \(E^{\prime \prime }_{i+1} \Rightarrow _R^{*} E_{i+1}\), so the claim holds for E_i+ 1 and by induction, it holds for all \(E^{\prime } \in [E]_{\Rightarrow }\). □

Lemma 6.18

Let E be a basic RWE. Let Y = var(E)∖Δ(E) and let E_Y = π_Y(E). Let \(d= \max \limits \{1,{diam}({\mathscr{G}}^{\Rightarrow }_{[E_Y]})\}\). Then \({diam}({\mathscr{G}}^{\Rightarrow }_{[E]}) \in O(d|E|^2)\).

Proof

Let \(E^{\prime }, E^{\prime \prime } \in [E]_{\Rightarrow }\). Then by Lemma 6.17, there exist \({\varphi }^{\prime },{\varphi }^{\prime \prime } \in {{\varPhi }}_E\) such that \(E^{\prime } \in H_{{\varphi }^{\prime }}\) and \(E^{\prime \prime } \in H_{{\varphi }^{\prime \prime }}\). For each φ ∈Φ_E, note that by Lemma 6.16 and Remark 4.6, there is path of length O(d Card(Δ(E))) between any two vertices in \(H^E_{\varphi }\). Thus if \({\varphi }^{\prime } = {\varphi }^{\prime \prime }\), then there is path of length O(d Card(Δ(E))) from \(E^{\prime }\) to \(E^{\prime \prime }\).

Suppose otherwise that \({\varphi }^{\prime } \not = {\varphi }^{\prime \prime }\). Then it follows from Lemma 6.7, there exist k ∈ O(Card(Δ(E))) and φ₁, φ₂,…,φ_k ∈Φ_E such that \({\varphi }^{\prime } = {\varphi }_{1}\), \({\varphi }^{\prime \prime } = {\varphi }_k\) and φ_i, φ_i+ 1 are close for 1 ≤ i < k. By Lemma 6.14, there exist E₁, E₂,…,E_k− 1 such that \(E_i \in H^E_{{\varphi }_i} \cap H^E_{{\varphi }_{i+1}}\) for 1 ≤ i < k.

It follows that there exist paths from \(E^{\prime }\) to E₀, from E_k to \(E^{\prime \prime }\) and from E_i to E_i+ 1 for 1 ≤ i < k of length O(d Card(Δ(E))). Thus there is a path from \(E^{\prime }\) to \(E^{\prime \prime }\) of length O(kd Card(Δ(E))) = O(d Card(Δ(E))²) = O(d|E|²). Since this is true for all \(E^{\prime },E^{\prime \prime }\), the statement of the lemma follows. □

Definition 7.1 (\(\xrightarrow {u,v}\) and ⊙)

For each u, v ∈ X, we define the relation \(\xrightarrow {u,v} \) over basic regular equations as \(E_{1}\xrightarrow {u,v} E_{2}\) if there exist x, y ∈ X and α₁, α₂, α₃, β₁, β₂, β₃ ∈ (X∖{u, v, x, y})^∗ such that E₁ may be written as \(x \alpha _{1} u \alpha _{2} v \alpha _3 y \doteq y \beta _{1} u \beta _{2} v \beta _3 x\) and E₂ may be written as \(x \alpha _{1} v \alpha _3 u \alpha _{2} y \doteq y \beta _{1} v \beta _3 u \beta _{2} x\). Additionally, we define \(\odot = \bigcup \limits _{u,v\in X} \xrightarrow {u,v} \).

Lemma 7.2

Let x, y, u, v ∈ X and α₁, α₂, α₃, β₁, β₂, β₃ ∈ (X∖{x, y, u, v})^∗. Let E₁ be the basic RWE given by \(x \alpha _{1} u \alpha _{2} v \alpha _3 y \doteq y \beta _{1} u \beta _{2} v \beta _3 x\) and let E₂ be the basic RWE given by \(x \alpha _{1} v \alpha _3 u \alpha _{2} y \doteq y \beta _{1} v \beta _3 u \beta _{2} x\). Then there exist n₁, n₂ < 4|E₁| such that \(E_{1} \Rightarrow ^{n_{1}} E_{2}\) and \(E_{2} \Rightarrow ^{n_{2}} E_{1}\).

Proof

Then it follows directly from the definitions that \(E_{1} \Rightarrow _R^{*} E_3 \Rightarrow _L^{*} E_5 \Rightarrow _R^{*} E_4 \Rightarrow _L^{*} E_{2}\). Thus, by Remark 3.2, there exists n₁ < 4|E₁| such that \(E_{1} \Rightarrow ^{n_{1}} E_{2}\). By the same remark, we know that \(\Rightarrow _L^{*},\Rightarrow _R^{*}\) are symmetric, and thus we may similarly conclude that \(E_{2} \Rightarrow _L^{*} E_4 \Rightarrow _R^{*} E_5 \Rightarrow _L^{*} E_3 \Rightarrow _R^{*} E_{1}\) so there exists n₂ < 4|E₁| such that \(E_{2} \Rightarrow ^{n_{2}} E_{1}\). □

Corollary 7.3

Let E₁, E₂ be basic RWEs. If E₁ ⊙^mE₂ for some \(m\in \mathbb {N}\), then E₁ ⇒ⁿE₂ for some n ∈ O(|E₁|m).

Definition 7.4 (Normal Form)

Let E be a basic RWE. Then E is in normal form if it can be written as \(x \alpha _{1} \alpha _{2}, {\ldots } \alpha _n y \doteq y \alpha _{1}^R \alpha _{2}^R {\ldots } \alpha _n^R x\) where x, y ∈ X, α_i ∈ X⁺ for 1 ≤ i ≤ n, and |α_i|≤ 3 for 1 ≤ i < n.

Theorem 7.5

Let E be a jumbled basic RWE. Then there exists \(\overline {E}\) which is in normal form and such that \(E \Rightarrow ^{n_{1}} \overline {E}\) and \(\overline {E} \Rightarrow ^{n_{2}} E\) for some n₁, n₂ ∈ O(|E|³).

Lemma 7.6

Proof

Proof Theorem 7.5.

By Lemma 6.13, we have that \(E \Rightarrow ^{n_{1}} E^{\prime }\) and \(E^{\prime } \Rightarrow ^{n_{1}^{\prime }} E\) where \(E^{\prime }\) is a basic regular equation of the form \(x \beta _{1} y \doteq y \beta _{2} x\) such that x, y ∈ X and β₁, β₂ ∈ (X∖{x, y})^∗ with \(n_{1},n_{1}^{\prime } \in O(|E|^2)\). By Theorem 5.3, since E is jumbled, \(E^{\prime }\) is also jumbled. By a simple induction using Lemma 7.6 (starting with the case that γ₁ = γ₂ = ε) we can therefore infer that \(E^{\prime } \odot ^{n_{2}} \overline {E}\) for some \(\overline {E}\) in normal form and n₂ ∈ O(|E|²). It follows directly from the definitions that ⊙, is symmetric, so we also have that \(\overline {E} \odot ^{n_{2}} E^{\prime }\). Thus, by Corollary 7.3 we have that \(E^{\prime } \Rightarrow ^{n_3} \overline {E}\) and \(\overline {E} \Rightarrow ^{n_{3}^{\prime }} E^{\prime }\) for some \(n_3,n_{3}^{\prime } \in O(|E|^3)\), and therefore also that \(E \Rightarrow ^n \overline {E}\) and \(\overline {E} \Rightarrow ^{n^{\prime }} E\) for some \(n,n^{\prime } \in O(|E|^3)\) as claimed. □

Definition 7.7 (Blocks)

Definition 7.8 (Block Decomposition)

Fact 7.9

For every basic RWE in normal form, there exists a unique block decomposition (B₀, B₁,…,B_k) where k ≤Card(var(E)), B_k is a final block, and if k > 0, then B₀ is an initial block.

Definition 7.10 (Lex Normal Form)

Let E be a basic RWE in normal form. Then there exist x, y ∈ X and α, β ∈ (X∖{x, y})^∗ such that E has the form \(x \alpha y \doteq y \beta x\). Let (B₀, B₁,…,B_k) be the block decomposition of E. For each i, 0 ≤ i ≤ k, let \(\gamma _i, \gamma _i^{\prime } \in X^{*}\) such that \(B_i = (\gamma _i,\gamma _i^{\prime })\), let S_i = {γ_i[2],y} whenever B_i is Type B and S_i = {y} otherwise, and let \({{\varGamma }}^E_i = \left (\bigcup \limits _{i \leq j \leq k} {var}(\gamma _j)\right )\backslash S_i \). A block B_i is lex-minimal if γ_i[1] is lexicographically minimal in \({{\varGamma }}^E_i\). The equation E is in Lex Normal Form (LNF) if, for each i, 0 < i < k, B_i is lex-minimal.