On equations and inequalities in words and word lengths

By $\Pi_{m}$ we denote, as usual, a free semigroup with an empty word as the neutral element of rank $m$ with free generators $a_1,\ldots,a_m$. An open question in the theory of equations on free semigroup $\Pi_{m}$, which have been well known for more than 40 years, concerns the algorithmic undecidability of the problem of compatibility for systems of equations and inequalities in words and word lengths, i.e., for systems of the type
$$ \underset{i=1}{\overset{k}{\&}} \, w_i (x_1, \ldots , x_n, a_1, \ldots , a_m) \, = \, u_i(x_1, \ldots , x_n, a_1, \ldots , a_m)\; \& \; \underset{\{ i, j \}\, \in \, A}{\&} \; |x_i| \, = \, |x_j|, $$
where, as usual, by $|w|\, = \, |u|$, we denote the predicate "the lengths of the words $w$ and $u$ are equal". Such systems of equations and inequalities in words and word lengths were studied in the beginning of 1970s by Yu.V. Matiyasevich [15] (1968) and N. K. Kosovskiĭ [9], [10], [11].
We prove the algorithmic undecidability of a compatibility problem for systems of equations and inequalities in words and word lengths on free non-cyclic semigroup $\Pi_{m}$.
For an arbitrary system of equations and inequalities of the type
$$ \underset{i=1}{\overset{k}{\&}} \, w_i (x_1,\ldots,x_n,a_1,\ldots,a_m)\, \leq \, u_i (x_1,\ldots,x_n,a_1,\ldots,a_m)\; \& \; \underset{\{ i, j \}\, \in \, A}{\&} \; |x_i| \, = \, |x_j|, $$
where $w_i(x_1,\ldots,x_n,a_1,\ldots,a_m)$ and $u_i(x_1,\ldots,x_n,a_1,\ldots,a_m)$ are words in the alphabet
$$ \lbrace\,x_1,x_2,\ldots,x_n, a_1,a_2,\ldots,a_m\,\rbrace , $$
it is shown that no algorithm can decide whether this system has a solution in free semigroup $\Pi_{m}$ at $m \geq 2$. Here $w\, \leq \, u$ denotes the predicate "the sequence $w$ of letters is a subsequence of the sequence $u$".