Proof. We show additionally that the required factorization must satisfy \(h=\Delta(u)+1\). We prove the statement by induction on \(|uv|\). In case \(|uv|\leq 1\), then either \(\mathop{\mathrm{ext}}_{u,v}=\mathop{\mathrm{ext}}_{\varepsilon,\varepsilon}\), or there is some \(c\in\Sigma_\text{int}\) such that \(\mathop{\mathrm{ext}}_{u,v}=\mathop{\mathrm{ext}}_{\varepsilon,c}\) or \(\mathop{\mathrm{ext}}_{u,v}=\mathop{\mathrm{ext}}_{c,\varepsilon}\). In any of these cases, we uniquely factorize \(\mathop{\mathrm{ext}}_{u, v}\) as \(\mathop{\mathrm{ext}}_{x_1, y_1}\) with \(x_1 = u\) and \(y_1 = v\).

Let us consider the case when \(|uv|\geq 2\) and let \(h=\Delta(u)+1\). Note that since \(uv\in\Sigma^\triangle\) we have \(u\in\Sigma^\triangle\) if, and only if, \(v\in\Sigma^\triangle\). In case \(u,v\in\Sigma^\triangle\) we have \(\Delta(u)=0\), hence the only factorization of the desired form is indeed \(\mathop{\mathrm{ext}}_{u,v}=\mathop{\mathrm{ext}}_{x_1,y_1}\), where \(x_1=u\) and \(y_1=v\). Let us finally treat the case when \(u,v\notin\Sigma^\triangle\), thus \(\Delta(u)\geq 1\) and hence \(h\geq 2\). Let \(x\) be the maximal prefix of \(u\) satisfying \(x\in\Sigma^\triangle\) and let \(y\) be the maximal suffix of \(v\) satisfying \(y\in\Sigma^\triangle\). Due to maximality of \(x\) and \(y\) there must exist \(a\in\Sigma_\text{call}\), \(b\in\Sigma_\text{ret}\), and \(u',v'\in\Sigma^*\) such that \(u=xau'\), \(v=v'by\) and \(u'v'\in\Sigma^\triangle\) with \(\Delta(u')=\Delta(u)-1=h-2\). Let \(\mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_{h-2},y_{h-2}} \circ \mathop{\mathrm{ext}}_{a_{h-2},b_{h-2}} \circ \mathop{\mathrm{ext}}_{x_{h-1},y_{h-1}}\) be the unique factorization of the desired form for \(\mathop{\mathrm{ext}}_{u',v'}\) by induction hypothesis. We claim that \[\mathop{\mathrm{ext}}_{x,y} \circ \mathop{\mathrm{ext}}_{a,b} \circ \mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_{h-2},y_{h-2}} \circ \mathop{\mathrm{ext}}_{a_{h-2},b_{h-2}} \circ \mathop{\mathrm{ext}}_{x_{h-1},y_{h-1}}\] is the unique factorization of the desired form for \(\mathop{\mathrm{ext}}_{u,v}\). Indeed, since \(\Delta(u) \geq 1\) any potential factorization of the desired form for \(\mathop{\mathrm{ext}}_{u,v}\) must be of the form \(\mathop{\mathrm{ext}}_{x',y'}\circ\mathop{\mathrm{ext}}_{a',b'}\circ\pi\), where \(x'\) is a prefix of \(u\) satisfying \(x'\in\Sigma^\triangle\), \(y'\) is a suffix of \(v\) satisfying \(y'\in\Sigma^\triangle\), \(a'\in\Sigma_\text{call}\), and \(b'\in\Sigma_\text{ret}\). In particular \(x'\) is a prefix of \(x\) and \(y'\) is suffix of \(y\). In case \(x'=x\) and \(y'=y\) it follows \(a'=a\) and \(b'=b\) and uniqueness follows from induction hypothesis. It remains to consider the case when \(x'\) is a strict prefix of \(x\) or \(y'\) is a strict suffix of \(y\). We only treat the former case. It must hold \(x=x'a's\) for some \(s\in\Sigma^+\) such that \(a's\in\Sigma^\triangle\). But then \(\pi\) is a factorization for \(\mathop{\mathrm{ext}}_{su',v'z}\) for some \(z\in\Sigma^*\) which is a contradiction since \(\Delta(s)=-1\) due to \(a's\in\Sigma^\triangle\). ◻

Proof. We define \(\overline{\varphi}\) based on a refinement of the structural definition of well-matched words. For each \(w\in\Sigma^\triangle\) we inductively define: \[\overline{\varphi}(w) = \begin{cases} 1_R & \text{if w=\varepsilon (type 1)}\\ \varphi(c) & \text{if w=c\in\Sigma_\text{int} (type 2)}\\ \psi(\mathop{\mathrm{ext}}_{a,b})(\overline{\varphi}(x)) & \text{if w=axb for a\in\Sigma_\text{call}, b\in\Sigma_\text{ret} and x\in\Sigma^\triangle (type 3)}\\ \overline{\varphi}(x)\overline{\varphi}(y) & \text{if w=xy for x,y\in\Sigma^\triangle\setminus\{\varepsilon\}, where |x| is minimal (type 4)} \end{cases}\] Observe that the four above types give unique decompositions. For proving that \(\overline{\varphi}\) is indeed a monoid morphism one proves that for all \(w,v\in\Sigma^\triangle\) we have \(\overline{\varphi}(wv)=\overline{\varphi}(w)\overline{\varphi}(v)\) by structural induction on \(w\) given by the four types. The case \(v=\varepsilon\) is direct, we only treat the case \(v\in\Sigma^\triangle\setminus\{\varepsilon\}\) in the following. If \(w\) is of type 1 we have \(\overline{\varphi}(wv)=\overline{\varphi}(v)=1_R\cdot \overline{\varphi}(v)=\overline{\varphi}(w)\overline{\varphi}(v)\). If \(w\) is of type 2 or 3, then \(wv\) is of type 4 and \(w\) is the shortest prefix of \(wv\) with \(w\in\Sigma^\triangle\setminus\{\varepsilon\}\), hence \(\overline{\varphi}(wv)=\overline{\varphi}(w)\overline{\varphi}(v)\). If \(w\) is of type 4, then \(w=xy\) for some \(x,y\in\Sigma^\triangle\setminus\{\varepsilon\}\), where \(x\) is of minimal length. Then \(wv\) is of type 4, where \(wv=x(yv)\) and \(x\) is the shortest prefix of \(wv\) with \(x\in\Sigma^\triangle\setminus\{\varepsilon\}\). Hence \(\overline{\varphi}(wv)=\overline{\varphi}(x)\overline{\varphi}(yv)= \overline{\varphi}(x)\overline{\varphi}(y)\overline{\varphi}(v)= \overline{\varphi}(xy)\overline{\varphi}(v)=\overline{\varphi}(w)\overline{\varphi}(v)\), where the first equality follows by definition of \(\overline{\varphi}\) and the second and third equality follow from the induction hypothesis. Given any \(\mathop{\mathrm{ext}}_{u,v}\in\mathcal{O}(\Sigma^\triangle)\) let \[\mathop{\mathrm{ext}}_{u,v} \quad=\quad \mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \quad\cdots\quad \circ \mathop{\mathrm{ext}}_{x_{h-1},y_{h-1}} \circ \mathop{\mathrm{ext}}_{a_{h-1},b_{h-1}} \circ \mathop{\mathrm{ext}}_{x_h,y_h}\] be the unique stair factorization given by Lemma [lemma32ext]. We define \[\overline{\psi}(\mathop{\mathrm{ext}}_{u,v})= \bigcirc_{i=1}^{h-1} \bigl( \mathrm{left}_{\overline{\varphi}(x_i)} \circ \mathrm{right}_{\overline{\varphi}(y_i)} \circ \psi(\mathop{\mathrm{ext}}_{a_i,b_i}) \bigr) \circ \mathrm{left}_{\overline{\varphi}(x_h)} \circ \mathrm{right}_{\overline{\varphi}(y_h)} \,\,\text{.}\] For showing that \(\overline{\psi}\) is indeed a monoid morphism, one proves \(\overline{\psi}(\mathop{\mathrm{ext}}_{uu',v'v}) = \overline{\psi}(\mathop{\mathrm{ext}}_{u,v}) \circ \overline{\psi}(\mathop{\mathrm{ext}}_{u',v'})\) for all \(\mathop{\mathrm{ext}}_{u, v}, \mathop{\mathrm{ext}}_{u', v'} \in \mathcal{O}(\Sigma^\triangle)\) by observing simply that the unique stair factorization of \(\mathop{\mathrm{ext}}_{u u', v' v}\) is obtained by composing the unique stair factorizations of \(\mathop{\mathrm{ext}}_{u, v}\) and \(\mathop{\mathrm{ext}}_{u', v'}\).

We now show that \((\overline{\varphi},\overline{\psi})\) is in fact an \(\mathop{\mathrm{Ext}}\)-algebra morphism. The discussion above first shows that both \(\overline{\varphi}\colon\Sigma^\triangle\rightarrow R\) and \(\overline{\psi}\colon\mathcal{O}(\Sigma^\triangle)\rightarrow O\) are monoid morphisms. Next, let us prove that for all \(\mathop{\mathrm{ext}}_{u,v}\in\mathcal{O}(\Sigma^\triangle)\) and \(w\in\Sigma^\triangle\) we have \(\overline{\psi}(\mathop{\mathrm{ext}}_{u,v})(\overline{\varphi}(w))=\overline{\varphi}(\mathop{\mathrm{ext}}_{u,v}(w))\). Let \[\mathop{\mathrm{ext}}_{u,v} \quad=\quad \mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \quad\cdots\quad \circ \mathop{\mathrm{ext}}_{x_{h-1},y_{h-1}} \circ \mathop{\mathrm{ext}}_{a_{h-1},b_{h-1}} \circ \mathop{\mathrm{ext}}_{x_h,y_h}\] be the unique stair factorization of \(\mathop{\mathrm{ext}}_{u,v}\) provided by Lemma [lemma32ext]. If \(h = 1\), then \[\overline{\psi}(\mathop{\mathrm{ext}}_{u,v})(\overline{\varphi}(w)) = \mathrm{left}_{\overline{\varphi}(x_h)} \circ \mathrm{right}_{\overline{\varphi}(y_h)}(\overline{\varphi}(w)) = \overline{\varphi}(x_hwy_h) = \overline{\varphi}(\mathop{\mathrm{ext}}_{u, v}(w)) \,\,\text{.}\] Otherwise, we have \[\begin{align} & \overline{\psi}(\mathop{\mathrm{ext}}_{u,v})(\overline{\varphi}(w))\\ =& \bigcirc_{i=1}^{h-1} \bigl( \mathrm{left}_{\overline{\varphi}(x_i)} \circ \mathrm{right}_{\overline{\varphi}(y_i)} \circ \psi(\mathop{\mathrm{ext}}_{a_i,b_i}) \bigr) \circ \mathrm{left}_{\overline{\varphi}(x_h)}\circ\mathrm{right}_{\overline{\varphi}(y_h)} (\overline{\varphi}(w))\\ =& \bigcirc_{i=1}^{h-1} \bigl( \mathrm{left}_{\overline{\varphi}(x_i)} \circ \mathrm{right}_{\overline{\varphi}(y_i)} \circ \psi(\mathop{\mathrm{ext}}_{a_i,b_i}) \bigr) \bigl(\overline{\varphi}(x_hwy_h)\bigr)\\ =& \bigcirc_{i=1}^{h-2} \bigl( \mathrm{left}_{\overline{\varphi}(x_i)} \circ \mathrm{right}_{\overline{\varphi}(y_i)} \circ \psi(\mathop{\mathrm{ext}}_{a_i,b_i}) \bigr) \circ \\ & \mathrm{left}_{\overline{\varphi}(x_{h-1})}\circ\mathrm{right}_{\overline{\varphi}(y_{h-1})}\circ\psi(\mathop{\mathrm{ext}}_{a_{h-1},b_{h-1}}) \bigl(\overline{\varphi}(x_hwy_h)\bigr)\\ =& \bigcirc_{i=1}^{h-2} \bigl( \mathrm{left}_{\overline{\varphi}(x_i)} \circ \mathrm{right}_{\overline{\varphi}(y_i)} \circ \psi(\mathop{\mathrm{ext}}_{a_i,b_i}) \bigr) \circ \\ & \mathrm{left}_{\overline{\varphi}(x_{h-1})}\circ\mathrm{right}_{\overline{\varphi}(y_{h-1})} \bigl(\overline{\varphi}(a_{h-1}x_hwy_hb_{h-1})\bigr)\\ =& \bigcirc_{i=1}^{h-2} \bigl( \mathrm{left}_{\overline{\varphi}(x_i)} \circ \mathrm{right}_{\overline{\varphi}(y_i)} \circ \psi(\mathop{\mathrm{ext}}_{a_i,b_i}) \bigr) \bigl(\overline{\varphi}(x_{h-1}a_{h-1}x_hwy_hb_{h-1}y_{h-1})\bigr)\\ =& \cdots\\ =& \overline{\varphi}(x_1a_1\cdots x_{h-1}a_{h-1}x_hwy_hb_{h-1}y_{h-1}\cdots b_1y_1)\\ =& \overline{\varphi}(\mathop{\mathrm{ext}}_{u,v}(w)) \,\,\text{.} \end{align}\]

Let us prove that for all \(w\in\Sigma^\triangle\) we have \(\overline{\psi}(\mathrm{left}_{w})=\mathrm{left}_{\overline{\varphi}(w)}\). Noting that the unique stair factorization of \(\mathrm{left}_{w}\) is \(\mathop{\mathrm{ext}}_{w,\varepsilon}\) we obtain \[\overline{\psi}(\mathrm{left}_{w})= \overline{\psi}(\mathop{\mathrm{ext}}_{w,\varepsilon})= \mathrm{left}_{\overline{\varphi}(w)}\circ\mathrm{right}_{\overline{\varphi}(\varepsilon)}= \mathrm{left}_{\overline{\varphi}(w)}\circ\mathrm{right}_{1_R}= \mathrm{left}_{\overline{\varphi}(w)}\circ 1_O = \mathrm{left}_{\overline{\varphi}(w)} \,\,\text{.}\] One proves \(\overline{\psi}(\mathrm{right}_{w})=\mathrm{right}_{\overline{\varphi}(w)}\) for all \(w \in \Sigma^\triangle\) analogously.

Therefore, \((\overline{\varphi}, \overline{\psi})\) is an \(\mathop{\mathrm{Ext}}\)-algebra morphism and it is the unique one satisfying \(\overline{\varphi}(c) = \varphi(c)\) for each \(c \in \Sigma_\text{int}\) and \(\overline{\psi}(\mathop{\mathrm{ext}}_{a, b}) = \psi(\mathop{\mathrm{ext}}_{a, b})\) for each \(a \in \Sigma_\text{call}, b \in \Sigma_\text{ret}\). Take indeed any such \(\mathop{\mathrm{Ext}}\)-algebra morphism \((\varphi', \psi')\): using the properties of \(\mathop{\mathrm{Ext}}\)-algebra morphisms, it is straightforward to prove that then \(\overline{\varphi}(w) = \varphi'(w)\) for all \(w \in \Sigma^\triangle\) by structural induction on \(w\) and then to prove that \(\overline{\psi}(\mathop{\mathrm{ext}}_{u, v}) = \psi'(\mathop{\mathrm{ext}}_{u, v})\) for all \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\) by using the unique stair factorization of \(\mathop{\mathrm{ext}}_{u,v}\) provided by Lemma [lemma32ext]. ◻

Proof. Let \(u, v \in R\) such that \(u \sim v\). Take any \(x, y \in R\): we have that \[x u y = \mathrm{right}_{y} \circ \mathrm{left}_{x}(u) \sim \mathrm{right}_{y} \circ \mathrm{left}_{x}(v) = x v y\] by definition of congruence. Thus, \(\sim\) is a congruence on \(R\). This implies that \(R \mathclose{}/\mathopen{}\sim\) is a monoid.

Let \(e', f' \in O'\): this means there exist \(e, f \in O\) such that \(e'([r]_\sim) = [e(r)]_\sim\) and \(f'([r]_\sim) = [f(r)]_\sim\) for all \(r \in R\). Given any \(r \in R\), we thus have \[e' \circ f'([r]_\sim) = e'([f(r)]_\sim) = [e(f(r))]_\sim = [e \circ f(r)]_\sim \,\,\text{,}\] so that \(e' \circ f' \in O'\). Therefore, \(O'\) is a submonoid of \((R \mathclose{}/\mathopen{}\sim)^{R \mathclose{}/\mathopen{}\sim}\) that contains the functions \(\mathrm{left}_{[r]_{\sim}}\) and \(\mathrm{right}_{[r]_{\sim}}\) for all \([r]_\sim\in R\mathclose{}/\mathopen{}\sim\). Thus, \((R\mathclose{}/\mathopen{}\sim,O')\) is an \(\mathop{\mathrm{Ext}}\)-algebra.

Now define the functions \(\varphi\colon R \to R \mathclose{}/\mathopen{}\sim\) and \(\psi\colon O \to O'\) by respectively \(\varphi(r) = [r]_\sim\) for all \(r \in R\) and \(\psi(e) = e'\) with \(e' \in O'\) such that \(e'([r]_\sim) = [e(r)]_\sim\) for all \(r \in R\): this is well-defined because \(\sim\) is a congruence on \((R, O)\). Since \(\sim\) is a congruence on \(R\), \(\varphi\) is a surjective monoid morphism. Further, let \(e, f \in O\). We have \[\begin{align} \psi(e) \circ \psi(f) ([r]_\sim) & = \psi(e)([f(r)]_\sim)\\ & = [e(f(r))]_\sim\\ & = [e \circ f(r)]_\sim\\ & = \psi(e \circ f)([r]_\sim) \end{align}\] for all \(r \in R\), so that \(\psi(e) \circ \psi(f) = \psi(e \circ f)\). Therefore, as \(\psi(1_O)([r]_\sim) = [1_O(r)]_\sim = [r]_\sim\) for all \(r \in R\), it follows that \(\psi\) is also a monoid morphism, that is obviously surjective. By construction, we do of course have that \[\psi(e)(\varphi(r)) = \psi(e)([r]_\sim) = [e(r)]_\sim = \varphi(e(r))\] for all \(e \in O\) and \(r \in R\). Moreover, for all \(r \in R\), it holds that \[\psi(\mathrm{left}_{r})([x]_\sim) = [\mathrm{left}_{r}(x)]_\sim = [r x]_\sim = [r]_\sim [x]_\sim = \mathrm{left}_{\varphi(r)}([x]_\sim)\] for all \(x \in R\), so that \(\psi(\mathrm{left}_{r}) = \mathrm{left}_{\varphi(r)}\). Similarly, we can prove that \(\psi(\mathrm{right}_{r}) = \mathrm{right}_{\varphi(r)}\) for all \(r \in R\). Thus, \((\varphi, \psi)\) is a surjective morphism from \((R, O)\) to \((R \mathclose{}/\mathopen{}\sim, O')\). ◻

Proof. Let \(L \subseteq \Sigma^\triangle\) be a language recognized by \((R, O)\). This means that there exists a morphism \((\varphi, \psi)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (R, O)\) such that \(L = \varphi^{-1}(F)\) for some \(F \subseteq R\). We will prove the lemma by combining the following two points:

(1) if \((R,O)\) is a sub-\(\mathop{\mathrm{Ext}}\)-algebra of \((S,P)\), then so does \((S,P)\) recognize \(L\), and

(2) if \((R,O)\) is a quotient of \((S,P)\), then so does \((S,P)\) recognize \(L\).

For Point (1), assume that \((R, O)\) is a sub-\(\mathop{\mathrm{Ext}}\)-algebra of \((S, P)\). This means that \(R\) is a submonoid of \(S\) and that there exists a submonoid \(O'\) of \(P\) satisfying \(O = {O'|}_{R}\). Take an arbitrary function \(\sigma\colon O \to P\) such that \({\sigma(e)|}_{R} = e\) for all \(e \in O\). Let us consider the unique morphism \((\varphi', \psi')\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (S, P)\) such that \(\varphi'(c) = \varphi(c)\) for all \(c \in \Sigma_\text{int}\) and \(\psi'(\mathop{\mathrm{ext}}_{a, b}) = \sigma(\psi(\mathop{\mathrm{ext}}_{a, b}))\) for all \(a \in \Sigma_\text{call}, b \in \Sigma_\text{ret}\), given to us by Proposition [ptn:Freeness95Ext-algebras]. We can prove by induction on \(w\) that \(\varphi'(w) = \varphi(w)\) for all \(w \in \Sigma^\triangle\):

• \(w = \varepsilon\). Then \(\varphi'(w) = 1_S = 1_R = \varphi(w)\).

• \(w = c\) for some \(c \in \Sigma_\text{int}\). Then \(\varphi'(w) = \varphi'(c) = \varphi(c) = \varphi(w)\).

• \(w = a w' b\) for some \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\) and \(w' \in \Sigma^\triangle\). Then \[\begin{align} \varphi'(w) & = \varphi'(\mathop{\mathrm{ext}}_{a, b}(w'))\\ & = \psi'(\mathop{\mathrm{ext}}_{a, b})(\varphi'(w'))\\ & \stackrel{\text{IH}}{=}\sigma(\psi(\mathop{\mathrm{ext}}_{a, b}))(\varphi(w'))\\ & = {\sigma(\psi(\mathop{\mathrm{ext}}_{a, b}))|}_{R}(\varphi(w'))\\ & = \psi(\mathop{\mathrm{ext}}_{a, b})(\varphi(w'))\\ & = \varphi(\mathop{\mathrm{ext}}_{a, b}(w'))\\ & = \varphi(w) \,\,\text{.} \end{align}\]

• \(w = u v\) for some \(u, v \in \Sigma^\triangle \setminus \{\varepsilon\}\). Then \[\varphi'(w) = \varphi'(u) \varphi'(v) \stackrel{\text{IH}}{=} \varphi(u) \varphi(v) = \varphi(w) \,\,\text{.}\]

Thus, \(\varphi'^{-1}(F) = L\), which implies that \((S, P)\) recognizes \(L\).

For Point (2), assume that \((R, O)\) is a quotient of \((S, P)\). This means that there exists a surjective morphism \((\alpha, \beta)\colon (S, P) \to (R, O)\). Let us define an arbitrary function \(\rho\colon \Sigma_\text{int}\to S\) such that \(\rho(c) \in \alpha^{-1}(\varphi(c))\) for all \(c \in \Sigma_\text{int}\) as well as an arbitrary function \(\sigma\colon\{\mathop{\mathrm{ext}}_{a, b}\mid a \in \Sigma_\text{call}, b \in \Sigma_\text{ret}\} \to P\) such that \(\sigma(\mathop{\mathrm{ext}}_{a, b}) \in \beta^{-1}(\psi(\mathop{\mathrm{ext}}_{a, b}))\) for all \(a \in \Sigma_\text{call}, b \in \Sigma_\text{ret}\). Now, take the unique morphism \((\varphi', \psi')\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (S, P)\) given by Proposition [ptn:Freeness95Ext-algebras] for \(\rho\) and \(\sigma\): we claim that it is such that \(\alpha(\varphi'(w)) = \varphi(w)\) for all \(w \in \Sigma^\triangle\). We can prove it by induction on \(w\):

• \(w = \varepsilon\). Then \(\alpha(\varphi'(w)) = \alpha(1_S) = 1_R = \varphi(w)\).

• \(w = c\) for some \(c \in \Sigma_\text{int}\). Then \(\alpha(\varphi'(w)) = \alpha(\rho(c)) = \varphi(c) = \varphi(w)\).

• \(w = a w' b\) for some \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\) and \(w' \in \Sigma^\triangle\). Then \[\begin{align} \alpha(\varphi'(w)) & = \alpha\bigl(\varphi'(\mathop{\mathrm{ext}}_{a, b}(w'))\bigr)\\ & = \alpha\bigl(\psi'(\mathop{\mathrm{ext}}_{a, b})(\varphi'(w'))\bigr)\\ & = \beta(\psi'(\mathop{\mathrm{ext}}_{a, b}))\bigl(\alpha(\varphi'(w'))\bigr)\\ & \stackrel{\text{IH}}{=} \beta(\sigma(\mathop{\mathrm{ext}}_{a, b}))(\varphi(w'))\\ & = \psi(\mathop{\mathrm{ext}}_{a, b})(\varphi(w'))\\ & = \varphi(\mathop{\mathrm{ext}}_{a, b}(w'))\\ & = \varphi(w) \,\,\text{.} \end{align}\]

• \(w = u v\) for some \(u, v \in \Sigma^\triangle \setminus \{\varepsilon\}\). Then \[\alpha(\varphi'(w)) = \alpha(\varphi'(u)) \alpha(\varphi'(v)) \stackrel{\text{IH}}{=} \varphi(u) \varphi(v) = \varphi(w) \,\,\text{.}\]

Therefore, \(\varphi'^{-1}(\alpha^{-1}(F)) = L\), which implies that \((S, P)\) recognizes \(L\). ◻

Proof. Since \((R, O)\) recognizes \(L\) via \((\varphi, \psi)\), this means that there exists \(F \subseteq R\) such that \(\varphi^{-1}(F) = L\). We have that \(\varphi(\Sigma^\triangle)\) is a submonoid of \(R\) and \(\psi(\mathcal{O}(\Sigma^\triangle))\) is a submonoid of \(O\). Observe that for all \(e \in \psi(\mathcal{O}(\Sigma^\triangle))\) and \(r \in \varphi(\Sigma^\triangle)\), we have \[e(r) = \psi(\mathop{\mathrm{ext}}_{u, v})(\varphi(w)) = \varphi(u w v) \in \varphi(\Sigma^\triangle)\] because \(\psi(\mathop{\mathrm{ext}}_{u,v}) = e\) for \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\) and \(r = \varphi(w)\) for \(w \in \Sigma^\triangle\). Moreover, for all \(e, f \in \psi(\mathcal{O}(\Sigma^\triangle))\), it holds that \({e|}_{\varphi(\Sigma^\triangle)} \circ {f|}_{\varphi(\Sigma^\triangle)} = {(e \circ f)|}_{\varphi(\Sigma^\triangle)}\). Therefore, \({\psi(\mathcal{O}(\Sigma^\triangle))|}_{\varphi(\Sigma^\triangle)}\) is a submonoid of \(\varphi(\Sigma^\triangle)^{\varphi(\Sigma^\triangle)}\). In addition, for each \(r \in \varphi(\Sigma^\triangle)\), we have that \(r = \varphi(w)\) for some \(w \in \Sigma^\triangle\) and thus that \[\mathrm{left}_{r} = \mathrm{left}_{\varphi(w)} = {\psi(\mathrm{left}_{w})|}_{\varphi(\Sigma^\triangle)} = {\psi(\mathop{\mathrm{ext}}_{w, \varepsilon})|}_{\varphi(\Sigma^\triangle)}\] as well as \(\mathrm{right}_{r} = {\psi(\mathop{\mathrm{ext}}_{\varepsilon, w})|}_{\varphi(\Sigma^\triangle)}\). Thus, \(\bigl(\varphi(\Sigma^\triangle), {\psi(\mathcal{O}(\Sigma^\triangle))|}_{\varphi(\Sigma^\triangle)} \bigr)\) is a sub-\(\mathop{\mathrm{Ext}}\)-algebra of \((R, O)\).

It is clear that \(\varphi\) is a surjective monoid morphism from \(\Sigma^\triangle\) to \(\varphi(\Sigma^\triangle)\). Further, \[\begin{align} \psi'(\mathop{\mathrm{ext}}_{u, v}) \circ \psi'(\mathop{\mathrm{ext}}_{u', v'}) & = {\psi(\mathop{\mathrm{ext}}_{u, v})|}_{\varphi(\Sigma^\triangle)} \circ {\psi(\mathop{\mathrm{ext}}_{u', v'})|}_{\varphi(\Sigma^\triangle)}\\ & = \bigl(\psi(\mathop{\mathrm{ext}}_{u, v}) \circ \psi(\mathop{\mathrm{ext}}_{u', v'})\bigr) \big|_{\varphi(\Sigma^\triangle)}\\ & = {\psi(\mathop{\mathrm{ext}}_{u, v} \circ \mathop{\mathrm{ext}}_{u', v'})|}_{\varphi(\Sigma^\triangle)}\\ & = \psi'(\mathop{\mathrm{ext}}_{u, v} \circ \mathop{\mathrm{ext}}_{u', v'}) \end{align}\] for all \(\mathop{\mathrm{ext}}_{u, v}, \mathop{\mathrm{ext}}_{u', v'} \in \mathcal{O}(\Sigma^\triangle)\), hence since \(\psi'(\mathop{\mathrm{ext}}_{\varepsilon, \varepsilon}) = {1_O|}_{\varphi(\Sigma^\triangle)}\), it follows that \(\psi'\) is a surjective monoid morphism from \(\mathcal{O}(\Sigma^\triangle)\) to \({\psi(\mathcal{O}(\Sigma^\triangle))|}_{\varphi(\Sigma^\triangle)}\). Moreover, we have

• \(\psi'(\mathop{\mathrm{ext}}_{u, v})(\varphi(w)) = {\psi(\mathop{\mathrm{ext}}_{u, v})|}_{\varphi(\Sigma^\triangle)}(\varphi(w)) = \psi(\mathop{\mathrm{ext}}_{u, v})(\varphi(w)) = \varphi(\mathop{\mathrm{ext}}_{u, v}(w))\) for all \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\) and \(w \in \Sigma^\triangle\);

• \(\psi'(\mathrm{left}_{w}) = {\psi(\mathop{\mathrm{ext}}_{w, \varepsilon})|}_{\varphi(\Sigma^\triangle)} = \mathrm{left}_{\varphi(w)}\) and \(\psi'(\mathrm{right}_{w}) = \mathrm{right}_{\varphi(w)}\) for all \(w \in \Sigma^\triangle\).

Therefore, \((\varphi, \psi')\) is a surjective morphism recognizing \(L\). ◻

Proof. Assume first that there is a surjective morphism \((\alpha, \beta)\colon (R, O) \to (R_L, O_L)\) such that \(\varphi_L = \alpha \circ \varphi\). Then \[\varphi^{-1}\bigl(\alpha^{-1}(\varphi(L))\bigr) = (\alpha \circ \varphi)^{-1}\bigl(\varphi_L(L)) = \varphi_L^{-1}(\varphi_L(L)) = L \,\,\text{,}\] hence \((R, O)\) recognizes \(L\) via \((\varphi, \psi)\).

Assume now that \((R, O)\) recognizes \(L\) via \((\varphi, \psi)\). This means that there exists \(F \subseteq R\) satisfying \(\varphi^{-1}(F) = L\). Take \(w, w' \in \Sigma^\triangle\) such that \(\varphi(w) = \varphi(w')\). Then, given any \(e \in \mathcal{O}(\Sigma^\triangle)\), we have that \[\varphi(e(w)) = \psi(e)(\varphi(w)) = \psi(e)(\varphi(w')) = \varphi(e(w')) \,\,\text{.}\] Therefore, since \(\varphi^{-1}(F) = L\), it holds that \(w \sim_L w'\), that is, \(\varphi_L(w) = \varphi_L(w')\).

Take \(\mathop{\mathrm{ext}}_{u, v}, \mathop{\mathrm{ext}}_{u', v'} \in \mathcal{O}(\Sigma^\triangle)\) such that \(\psi(\mathop{\mathrm{ext}}_{u, v}) = \psi(\mathop{\mathrm{ext}}_{u', v'})\). Then, for each \(w \in \Sigma^\triangle\), we have that \[\varphi(\mathop{\mathrm{ext}}_{u, v}(w)) = \psi(\mathop{\mathrm{ext}}_{u, v})(\varphi(w)) = \psi(\mathop{\mathrm{ext}}_{u', v'})(\varphi(w)) = \varphi(\mathop{\mathrm{ext}}_{u', v'}(w)) \,\,\text{,}\] that is, \(\mathop{\mathrm{ext}}_{u, v}(w) \sim_L \mathop{\mathrm{ext}}_{u', v'}(w)\). Hence, \(\psi_L(\mathop{\mathrm{ext}}_{u, v}) = \psi_L(\mathop{\mathrm{ext}}_{u', v'})\).

We can now define the functions \(\alpha\colon R \to R_L\) and \(\beta\colon O \to O_L\) such that \(\alpha(\varphi(w)) = \varphi_L(w)\) for all \(w \in \Sigma^\triangle\) and \(\beta(\psi(\mathop{\mathrm{ext}}_{u, v})) = \psi_L(\mathop{\mathrm{ext}}_{u, v})\) for all \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\): those are well-defined by surjectivity of \((\varphi, \psi)\) and what we have proven just above. Since \((\varphi_L, \psi_L)\) is a surjective morphism from \((\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle))\) to \((R_L, O_L)\), we can easily prove that \((\alpha, \beta)\) is a surjective morphism from \((R, O)\) to \((R_L, O_L)\) that does of course satisfy \(\varphi_L = \alpha \circ \varphi\). ◻

Proof. Let \((R, O)\) be an \(\mathop{\mathrm{Ext}}\)-algebra and let \(L \subseteq \Sigma^\triangle\) be a language. Consider also its syntactic \(\mathop{\mathrm{Ext}}\)-algebra \((R_L,O_L)\) and its syntactic morphism \((\varphi_L, \psi_L)\).

3.2.0.0.1 Implication from right to left.

Assume that the syntactic \(\mathop{\mathrm{Ext}}\)-algebra \((R_L, O_L)\) of \(L\) divides \((R, O)\). We have that \((R_L,O_L)\) recognizes \(L\) and we then use Lemma [lem:Division95and95recognisability] to conclude that \((R, O)\) does also recognize \(L\).

3.2.0.0.2 Implication from left to right.

Assume that \((R, O)\) recognizes \(L\) through a morphism \((\varphi, \psi)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (R, O)\). By Lemma [lem:Surjective95recognition], we have that \(\bigl(\varphi(\Sigma^\triangle), {\psi(\mathcal{O}(\Sigma^\triangle))|}_{\varphi(\Sigma^\triangle)} \bigr) = (R', O')\) is a sub-\(\mathop{\mathrm{Ext}}\)-algebra of \((R, O)\) recognizing \(L\) via the surjective morphism \((\varphi, \psi')\) where \(\psi'(\mathop{\mathrm{ext}}_{u, v}) = {\psi(\mathop{\mathrm{ext}}_{u, v})|}_{\varphi(\Sigma^\triangle)}\) for all \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\). Then, by Lemma [lem:Factorization95surjective95recognition], there exists a surjective morphism \((\alpha, \beta)\colon (R', O') \to (R_L, O_L)\) such that \(\varphi_L = \alpha \circ \varphi\). Thus, we have that \((R_L, O_L)\) divides \((R, O)\). ◻

Proof. Let \(L \subseteq \Sigma^\triangle\) be a language. Before we prove the theorem we have the following claim, which can be easily proven by induction on \(|u|\) and structural induction on \(w\), respectively.

3.2.0.0.3 Claim.

Let \(A = (Q, \Sigma, \Gamma, \delta, q_0, F, \bot)\) be a DVPA. We denote by \(\pi_Q\) the projection of \(Q \times \Gamma^*\) on \(Q\) and by \(\pi_{\Gamma^*}\) the projection of \(Q \times \Gamma^*\) on \(\Gamma^*\). It holds that \(L\mathopen{}\left(A\right)\mathclose{} \subseteq \Sigma^\triangle\) and additionally we have that \[\widehat{\delta}(q, u v, \sigma) = \widehat{\delta}\bigl(\pi_Q(\widehat{\delta}(q, u, \sigma)), v, \pi_{\Gamma^*}(\widehat{\delta}(q, u, \sigma)) \bigr)\] and \[\widehat{\delta}(q, w, \alpha \sigma) = \bigl(\pi_Q(\widehat{\delta}(q, w, \alpha)), \alpha \sigma\bigr)\] for all \(q \in Q\), \(u, v \in \Sigma^*\), \(\sigma \in \Gamma^*\), \(w \in \Sigma^\triangle\) and \(\alpha \in \Gamma\).

3.2.0.0.4 Implication from left to right.

Assume that \(L\) is a VPL. This means there exists a DVPA \(A = (Q, \Sigma, \Gamma, \delta, q_0, F, \bot)\) such that \(L\mathopen{}\left(A\right)\mathclose{} = L\). Consider the operation \(*\) on \(R=Q^{Q \times \Gamma}\) defined so that for all \(f, g \in R\), we have \(f * g(q, \alpha) = g(f(q, \alpha), \alpha)\) for all \(q \in Q\) and \(\alpha \in \Gamma\). Observe that for all \(f, g, h \in Q^{Q \times \Gamma}\), we have \[(f * g) * h(q, \alpha) = h(f * g(q, \alpha), \alpha) = h(g(f(q, \alpha), \alpha), \alpha) = g * h(f(q, \alpha), \alpha) = f * (g * h)(q, \alpha)\] for all \(q \in Q\) and \(\alpha \in \Gamma\). Thus \(*\) is associative and since it also has \(i \in R\) with \(i(q, \alpha) = q\) for all \(q \in Q\) and \(\alpha \in \Gamma\) as an identity, we have that \(R = Q^{Q \times \Gamma}\) with operation \(*\) forms a monoid. Take \(O\) to be the monoid \(R^R\) (for composition). Since \(O\) clearly contains the functions \(\mathrm{left}_{r}\) and \(\mathrm{right}_{r}\) for all \(r\in R\), it follows that \((R, O)\) is a finite \(\mathop{\mathrm{Ext}}\)-algebra. We now prove that it recognizes \(L\). For each \(w \in \Sigma^\triangle\), define \(f_w \in R\) by \(f_w(q, \alpha) = \pi_Q(\widehat{\delta}(q, w, \alpha))\) for all \(q \in Q\) and \(\alpha \in \Gamma\). Let us consider the unique morphism \((\varphi, \psi)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (R, O)\), given by Proposition [ptn:Freeness95Ext-algebras], such that for each \(c \in \Sigma_\text{int}\), we have \(\varphi(c) = f_c\) and for each \(a \in \Sigma_\text{call}, b \in \Sigma_\text{ret}\), we have that \(\psi(\mathop{\mathrm{ext}}_{a, b})\) sends any \(f \in R\) to \(g \in R\) satisfying that \(g(q, \alpha) = \pi_Q\bigl(\delta(f(p, \beta), b, \beta)\bigr)\) with \(\delta(q, a, \alpha) = (p, \beta \alpha)\) for all \(q \in Q\) and \(\alpha \in \Gamma\). We claim that for all \(w \in \Sigma^\triangle\), we have that \(\varphi(w) = f_w\). We prove it by induction on \(w\).

• \(w = \varepsilon\). Then \(\varphi(w) = i = f_w\).

• \(w = c\) for some \(c \in \Sigma_\text{int}\). Then \(\varphi(w) = f_c = f_w\).

• \(w = a w' b\) for some \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\) and \(w' \in \Sigma^\triangle\). Then \[\varphi(w) = \varphi(\mathop{\mathrm{ext}}_{a, b}(w')) = \psi(\mathop{\mathrm{ext}}_{a, b})(\varphi(w')) \stackrel{\text{IH}}{ = } \psi(\mathop{\mathrm{ext}}_{a, b})(f_{w'}) \,\,\text{.}\] So \(\varphi(w) = g\) such that for all \(q \in Q\) and \(\alpha \in \Gamma\), if we set \(\delta(q, a, \alpha) = (p, \beta\alpha)\), we have, recalling that \(\widehat{\delta}\) extends \(\delta\), \[\begin{align} g(q, \alpha) & = \pi_Q\bigl(\delta(f_{w'}(p, \beta), b, \beta)\bigr)\\ & = \pi_Q\Bigl(\delta\bigl(\pi_Q(\widehat{\delta}(p,w',\beta)), b, \beta \bigr)\Bigr) \\ & = \pi_Q\Bigl(\widehat{\delta}\bigl(\pi_Q(\widehat{\delta}(p,w',\beta)), b, \beta \bigr)\Bigr) \\ & = \pi_Q\Bigl(\widehat{\delta} \bigl(\pi_Q(\widehat{\delta}(q, a w', \alpha)), b, \pi_{\Gamma^*}(\widehat{\delta}(q, a w', \alpha)) \bigr)\Bigr)\\ & = \pi_Q(\widehat{\delta}(q, a w' b, \alpha))\\ & = f_{a w' b}(q, \alpha)\\ & = f_w(q,\alpha) \,\,\text{.} \end{align}\] Thus \(\varphi(w) = f_w\).

• \(w = u v\) for some \(u, v \in \Sigma^\triangle \setminus \{\varepsilon\}\). Then \(\varphi(w) = \varphi(u) * \varphi(v) \stackrel{\text{IH}}{=} f_u * f_v\). But \[\begin{align} f_u * f_v(q, \alpha) & = f_v(f_u(q, \alpha), \alpha)\\ & = f_v\bigl(\pi_Q(\widehat{\delta}(q, u, \alpha)), \alpha\bigr)\\ & = \pi_Q\Bigl(\widehat{\delta} \bigl(\pi_Q(\widehat{\delta}(q, u, \alpha)), v, \alpha\bigr)\Bigr)\\ & = \pi_Q\Bigl(\widehat{\delta} \bigl(\pi_Q(\widehat{\delta}(q, u, \alpha)), v, \pi_{\Gamma^*}(\widehat{\delta}(q, u, \alpha)) \bigr)\Bigr)\\ & = \pi_Q(\widehat{\delta}(q, u v, \alpha))\\ & = f_{u v}(q, \alpha) \end{align}\] for all \(q \in Q\) and \(\alpha \in \Gamma\). Therefore \(\varphi(w) = f_w\).

Finally, set \(P = \{f \in R \mid f(q_0, \bot) \in F\}\). It holds that \[\begin{align} \varphi^{-1}(P) & = \{w \in \Sigma^\triangle \mid f_w(q_0, \bot) \in F\}\\ & = \{w \in \Sigma^\triangle \mid \pi_Q(\widehat{\delta}(q_0, w, \bot)) \in F\}\\ & = \{w \in \Sigma^\triangle \mid \widehat{\delta}(q_0, w, \bot) \in F \times \{\bot\}\}\\ & = L\mathopen{}\left(A\right)\mathclose{}\\ & = L \,\,\text{.} \end{align}\] Therefore, \((R, O)\) recognizes \(L\).

3.2.0.0.5 Implication from right to left.

Assume there exists a finite \(\mathop{\mathrm{Ext}}\)-algebra \((R, O)\) that recognizes \(L\). This means that there exists a morphism \((\varphi, \psi)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (R, O)\) such that \(L = \varphi^{-1}(F)\) for some \(F \subseteq R\). Let us now define the DVPA \[A = (Q, \Sigma, \Gamma, \delta, 1, F, \bot),\] where \(Q=R\), \(1=1_R\), \(\Gamma=R \times \Sigma_\text{call}\cup \{\bot\}\), and \[\delta(r, a, \alpha) = \begin{cases} (1, (r, a) \alpha) & \text{if a \in \Sigma_\text{call}}\\ (s \psi(\mathop{\mathrm{ext}}_{b, a})(r), \varepsilon) & \text{if a \in \Sigma_\text{ret} and \alpha = (s, b) \in R \times \Sigma_\text{call}}\\ (r, \varepsilon) & \text{if a \in \Sigma_\text{ret} and \alpha = \bot}\\ (r \varphi(c), \alpha) & \text{if a \in \Sigma_\text{int}} \end{cases}\] for all \(r \in R\), \(a \in \Sigma\) and \(\alpha \in \Gamma\). We prove that \(\widehat{\delta}(r, w, \sigma) = (r \varphi(w), \sigma)\) for all \(r \in R\), \(w \in \Sigma^\triangle\) and \(\sigma \in \Gamma^* \bot\) by induction on \(w\).

• \(w = \varepsilon\). Then \(\widehat{\delta}(r, w, \sigma) = (r, \sigma) = (r \varphi(w), \sigma)\).

• \(w = c\) for some \(c \in \Sigma_\text{int}\). Then \(\widehat{\delta}(r, w, \sigma) = (r \varphi(c), \sigma) = (r \varphi(w), \sigma)\).

• \(w = a w' b\) for some \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\) and \(w' \in \Sigma^\triangle\). Then \[\begin{align} \widehat{\delta}(r, w, \sigma) & = \widehat{\delta}(1, w' b, (r, a) \sigma)\\ & = \widehat{\delta}\bigl(\pi_Q(1, w', (r, a) \sigma), b, \pi_{\Gamma^*}(1, w', (r, a) \sigma) \bigr)\\ & \stackrel{\text{IH}}{=} \widehat{\delta}(\varphi(w'), b, (r, a) \sigma)\\ & = \bigl(r \psi(\mathop{\mathrm{ext}}_{a, b})(\varphi(w')), \sigma\bigr)\\ & = (r \varphi(w), \sigma) \,\,\text{.} \end{align}\]

• \(w = u v\) for some \(u, v \in \Sigma^\triangle \setminus \{\varepsilon\}\). Then \[\begin{align} \widehat{\delta}(r, w, \sigma) & = \widehat{\delta}\bigl(\pi_Q(\widehat{\delta}(r, u, \sigma)), v, \pi_{\Gamma^*}(\widehat{\delta}(r, u, \sigma))\bigr)\\ & \stackrel{\text{IH}}{=} \widehat{\delta}(r \varphi(u), v, \sigma)\\ & \stackrel{\text{IH}}{=} (r \varphi(u) \varphi(v), \sigma)\\ & = (r \varphi(w), \sigma) \,\,\text{.} \end{align}\]

Hence, \[\begin{align} L\mathopen{}\left(A\right)\mathclose{} & = \{w \in \Sigma^\triangle \mid \widehat{\delta}(1, w, \bot) \in F \times \{\bot\}\}\\ & = \{w \in \Sigma^\triangle \mid \pi_Q(\widehat{\delta}(1, w, \bot)) \in F\}\\ & = \{w \in \Sigma^\triangle \mid \varphi(w) \in F\}\\ & = \varphi^{-1}(F) = L \,\,\text{.} \end{align}\] Therefore, \(L\) is a VPL. ◻

Proof. For each \(r \in R\), let \(n_r \in \mathbb{N}_{>0}\) be the pumping constant for the context-free language \(\varphi^{-1}(r)\): it is a VPL and hence a context-free language by Theorem [thm:vpl:ext]. We set \(n = \max_{r \in R} n_r\). Let \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\) be such that there exists a factor \(w \in \Sigma^\triangle\) of \(u\) satisfying \(\mathopen{}\left|w\right|\mathclose{} \geq n\). Let \[\mathop{\mathrm{ext}}_{u,v} \quad=\quad \mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \quad\cdots\quad \circ \mathop{\mathrm{ext}}_{x_{h-1},y_{h-1}} \circ \mathop{\mathrm{ext}}_{a_{h-1},b_{h-1}} \circ \mathop{\mathrm{ext}}_{x_h,y_h}\] be the stair factorization of \(\mathop{\mathrm{ext}}_{u,v}\) provided by Lemma [lemma32ext]. Since no factor of \(u\) spanning one of the \(a_j\)’s in the factorization can be well-matched, there must exist some \(j \in [1, h]\) satisfying \(\mathopen{}\left|x_j\right|\mathclose{} \geq n\), so that if we set \(u' = x_1 a_1 \cdots x_{j - 1} a_{j - 1}\), \(v' = b_{j - 1} y_{j - 1} \cdots b_1 y_1\), \(u'' = a_j x_{j + 1} \cdots a_{h - 1} x_h\) and \(v'' = y_h b_{h - 1} \cdots y_{j + 1} b_j y_j\), we have \(u'v', u''v'' \in \Sigma^\triangle\) and \(\mathop{\mathrm{ext}}_{u, v} = \mathop{\mathrm{ext}}_{u', v'} \circ \mathop{\mathrm{ext}}_{x_j, \varepsilon} \circ \mathop{\mathrm{ext}}_{u'', v''}\). By the pumping lemma for context-free languages we have \(x_j = x' x z y y'\) with \(x', x, z, y, y' \in \Sigma^*\) such that \(\mathopen{}\left|x y\right|\mathclose{} \geq 1\), \(\mathopen{}\left|x z y\right|\mathclose{} \leq n\) and for all \(i \in \mathbb{N}\), \(x' x^i z y^i y' \in \Sigma^\triangle\) and \(\varphi(x_j) = \varphi(x' x^i z y^i y')\). This implies that if we set \(s = u' x'\) and \(t = y' u''\), then for all \(i \in \mathbb{N}\), we have \(s x^i z y^i t v = \mathop{\mathrm{ext}}_{u', v'} \circ \mathop{\mathrm{ext}}_{x' x^i z y^i y', \varepsilon} \circ \mathop{\mathrm{ext}}_{u'', v''}(\varepsilon) \in \Sigma^\triangle\) and \[\begin{align} \psi(\mathop{\mathrm{ext}}_{u, v}) & = \psi(\mathop{\mathrm{ext}}_{u', v'}) \circ \mathrm{left}_{\varphi(x_j)} \circ \psi(\mathop{\mathrm{ext}}_{u'', v''})\\ & = \psi(\mathop{\mathrm{ext}}_{u', v'}) \circ \mathrm{left}_{\varphi(x' x^i z y^i y')} \circ \psi(\mathop{\mathrm{ext}}_{u'', v''})\\ & = \psi(\mathop{\mathrm{ext}}_{u', v'}) \circ \psi(\mathop{\mathrm{ext}}_{x' x^i z y^i y', \varepsilon}) \circ \psi(\mathop{\mathrm{ext}}_{u'', v''})\\ & = \psi(\mathop{\mathrm{ext}}_{s x^i z y^i t, v}) \,\,\text{.} \end{align}\]

We handle the case where for \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\) there exists a factor \(w \in \Sigma^\triangle\) of \(v\) such that \(\mathopen{}\left|w\right|\mathclose{} \geq n\) symmetrically. ◻

Proof. Let \(F \subseteq R\) and \(P\) be a subsemigroup of \(O\). Assume all elements in \(P\) are \(F\)-reaching and \((\varphi,\psi)\) is \(F\)-weakly-length-synchronous.

Let \((u, v), (u', v) \in \mathsf{Con}(\Sigma)\) be such that \(\Delta(u), \Delta(u') > 0\) and \(\psi(\mathop{\mathrm{ext}}_{u, v}), \psi(\mathop{\mathrm{ext}}_{u', v}) \in P\). Set \(e = \psi(\mathop{\mathrm{ext}}_{u, v})\) and \(f = \psi(\mathop{\mathrm{ext}}_{u', v})\). By hypothesis, given \(\omega \in \mathbb{N}_{>0}\) the idempotent power of \(O\), we have \((e^\omega f^\omega)^\omega \in P\), hence \((e^\omega f^\omega)^\omega\) is an \(F\)-reaching idempotent and thus \(\mathcal{R}_{(e^\omega f^\omega)^\omega}\) is weakly length-synchronous. But \[\psi(\mathop{\mathrm{ext}}_{(u^{2\cdot\omega}u'^\omega)^\omega, v^{3\cdot\omega^2}}) = (e^\omega f^\omega)^\omega = \psi(\mathop{\mathrm{ext}}_{(u^{\omega}u'^{2\cdot\omega})^\omega, v^{3\cdot\omega^2}})\] so since \(\Delta((u^{2\cdot\omega}u'^\omega)^\omega) = \Delta((u^{\omega}u'^{2\cdot\omega})^\omega) > 0\), we obtain \[\arraycolsep=1.4pt\def\arraystretch{1.7} \begin{array}{lrcl} &\quad{\omega \cdot (2\cdot\omega\cdot |u|+ \omega\cdot |u'|)}& =& \omega\cdot(\omega\cdot|u|+2\cdot\omega\cdot |u'|)\\ \Longleftrightarrow\quad & {2\cdot|u|+|u'|} &=& {|u|+2\cdot|u'|}\\ \Longleftrightarrow\quad & |u| &=& |u'| \,\,\text{.} \end{array}\] In the same way, one can prove that for all \((u, v), (u, v') \in \mathsf{Con}(\Sigma)\) such that \(\Delta(u) > 0\) and \(\psi(\mathop{\mathrm{ext}}_{u, v}), \psi(\mathop{\mathrm{ext}}_{u, v'}) \in P\), we have \(\mathopen{}\left|v\right|\mathclose{} = \mathopen{}\left|v'\right|\mathclose{}\).

Therefore, \(\bigcup_{e \in P} \mathcal{R}_e\) is weakly length-synchronous. ◻

Proof. Let \(F \subseteq R\).

If \(\mathcal{U}_e=\{(u,v)\in\mathsf{Con}(\Sigma)\mid e\circ\psi(\mathop{\mathrm{ext}}_{u,v})=e\}\) is weakly length-synchronous for all \(F\)-reaching \(e\in O\), then in particular the set of contexts \(\mathcal{R}_e=\{(u,v)\in\mathsf{Con}(\Sigma)\mid \psi(\mathop{\mathrm{ext}}_{u,v})=e\}\) is weakly length-synchronous for all \(F\)-reaching idempotents \(e\in O\).

Conversely, assume that \((\varphi,\psi)\) is \(F\)-weakly-length-synchronous. Fix any \(F\)-reaching \(e\in O\). We need to prove that \(\mathcal{U}_e\) is weakly length-synchronous. It is clear that \(P = \{f \in O \mid e \circ f = e\}\) forms a subsemigroup of \(O\) whose elements are all \(F\)-reaching, by \(F\)-reachability of \(e\). Therefore, by Lemma [lem:Weak95length-synchronicity95subsemigroups], \(\bigcup_{f \in P} \mathcal{R}_f = \mathcal{U}_e\) is weakly length-synchronous. ◻

Proof. Let \(F \subseteq R\) and \(P\) be a subsemigroup of \(O\). Assume all elements in \(P\) are \(F\)-reaching and \((\varphi,\psi)\) is \(F\)-length-synchronous.

Let \((u, v), (u', v') \in \mathsf{Con}(\Sigma)\) be such that \(\Delta(u), \Delta(u') > 0\) and \(\psi(\mathop{\mathrm{ext}}_{u, v}), \psi(\mathop{\mathrm{ext}}_{u', v'}) \in P\). Set \(e = \psi(\mathop{\mathrm{ext}}_{u, v})\) and \(f = \psi(\mathop{\mathrm{ext}}_{u', v'})\). By hypothesis, given \(\omega \in \mathbb{N}_{>0}\) the idempotent power of \(O\), we have \((e^\omega f^\omega)^\omega \in P\), hence \((e^\omega f^\omega)^\omega\) is an \(F\)-reaching idempotent and thus \(\mathcal{R}_{(e^\omega f^\omega)^\omega}\) is length-synchronous. But \[\psi(\mathop{\mathrm{ext}}_{(u^{2 \cdot \omega} u'^\omega)^\omega, (v'^\omega v^{2 \cdot \omega})^\omega}) = (e^\omega f^\omega)^\omega = \psi(\mathop{\mathrm{ext}}_{(u^\omega u'^{2 \cdot \omega})^\omega, (v'^{2 \cdot \omega} v^\omega)^\omega})\] so since \(\Delta((u^{2\cdot\omega}u'^\omega)^\omega), \Delta((u^{\omega}u'^{2\cdot\omega})^\omega) > 0\), setting \((x, y) = ((u^{2 \cdot \omega} u'^\omega)^\omega, (v'^\omega v^{2 \cdot \omega})^\omega)\) and \((x', y') = ((u^\omega u'^{2 \cdot \omega})^\omega, (v'^{2 \cdot \omega} v^\omega)^\omega)\), we obtain (using that for \(a,b,c,d>0\) we have that \(\frac{a}{b}=\frac{c}{d}\) implies \(\frac{a}{b}=\frac{c}{d}=\frac{a+c}{b+d}\) and, if additionally \(a>c\), it implies \(\frac{a}{b}=\frac{c}{d}=\frac{a-c}{b-d}\)) \[\begin{align} \frac{|x|}{|y|}=\frac{|x'|}{|y'|} & \quad\Longrightarrow\quad & \frac{|x|}{|y|}=\frac{|x'|}{|y'|}=\frac{|x|+|x'|}{|y|+|y'|}= \frac{\omega^2\cdot(|u|+|u'|)}{\omega^2\cdot(|v|+|v'|)}\nonumber\\ &\quad\Longrightarrow\quad& \frac{|x|-\omega^2\cdot(|u|+|u'|)}{|y|-\omega^2\cdot(|v|+|v'|)}= \frac{|x'|-\omega^2\cdot(|u|+|u'|)}{|y'|-\omega^2\cdot(|v|+|v'|)} \label{E32square}\\ &\quad\Longrightarrow\quad& \frac{|u|}{|v|}= \frac{\omega^2\cdot|u|}{\omega^2\cdot|v|} \stackrel{(\ref{E32square})}{=} \frac{\omega^2\cdot|u'|}{\omega^2\cdot|v'|}= \frac{|u'|}{|v'|}\nonumber \,\,\text{.} \end{align}\tag{1}\]

Therefore, \(\bigcup_{e \in P} \mathcal{R}_e\) is length-synchronous. ◻

Proof. Let \(F \subseteq R\).

If \(\mathcal{U}_e=\{(u,v)\in\mathsf{Con}(\Sigma)\mid e\circ\psi(\mathop{\mathrm{ext}}_{u,v})=e\}\) is length-synchronous for all \(F\)-reaching \(e\in O\), then in particular the set of contexts \(\mathcal{R}_e=\{(u,v)\in\mathsf{Con}(\Sigma)\mid \psi(\mathop{\mathrm{ext}}_{u,v})=e\}\) is length-synchronous for all \(F\)-reaching idempotents \(e\in O\).

Conversely, assume that \((\varphi,\psi)\) is \(F\)-length-synchronous. Fix any \(F\)-reaching \(e\in O\). We need to prove that \(\mathcal{U}_e\) is length-synchronous. It is clear that \(P = \{f \in O \mid e \circ f = e\}\) forms a subsemigroup of \(O\) whose elements are all \(F\)-reaching, by \(F\)-reachability of \(e\). Therefore, by Lemma [lem:Length-synchronicity95subsemigroups], \(\bigcup_{f \in P} \mathcal{R}_f = \mathcal{U}_e\) is length-synchronous. ◻

Proof. The implication from Point 2 to Point 1 is trivial since Point 2 (a) implies Point 1.

Let us now prove that Point 1 implies Point 2. Fix any \(e\in O\) that is \(F\)-reaching and assume that \(\mathcal{U}_e\) is length-synchronous. Point 2 (a) follows immediately from length-synchronicity of \(\mathcal{U}_e\). We can hence write \(\alpha=\frac{A}{B}\) for some \(A,B\in\mathbb{N}_{>0}\).

For proving Point 2 (b), we define \(\beta= (n+1)\cdot(|O|+\max(A,B)+1)\), where \(n\) is the constant taken from Lemma [lem:Ext95pumping]. Let \((u,v)\in\mathcal{U}_e\) with \(\Delta(u) > 0\) and let \[\mathop{\mathrm{ext}}_{u,v}=\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ \dots \circ\mathop{\mathrm{ext}}_{x_{h-1},y_{h-1}}\circ\mathop{\mathrm{ext}}_{a_{h-1},b_{h-1}}\circ\mathop{\mathrm{ext}}_{x_h,y_h}\] be the stair factorization of \(\mathop{\mathrm{ext}}_{u,v}\) according to Lemma [lemma32ext]. Since our morphism \((\varphi,\psi)\) is \(F\)-weakly-length-synchronous by assumption, we have \(|x_i|,|y_i|\leq n\) by Lemma [ptn:hill95small]. Let \(u'\in\Sigma^*\) be a prefix of \(u\) and \(v'\) be a suffix of \(v\) such that \(\frac{|u'|}{|v'|}=\alpha\). If \((u',v')=(u,v)\) we are done since then \(\Delta(u')=-\Delta(v')\). Thus, it remains to consider the case when \(u'\) is a strict prefix of \(u\) and \(v'\) is a strict suffix of \(v\): indeed, due to \(\frac{|u|}{|v|}=\frac{|u'|}{|v'|}=\alpha\) we have that \(u'\) is a strict prefix of \(u\) if, and only if, \(v'\) is a strict suffix of \(v\).

Let \(j\in[1,h]\) be maximal such that \(x_1\cdots a_{j-1}x_j\) is a prefix of \(u'\) and \(y_jb_{j-1}\cdots y_1\) is a suffix of \(v'\). If \(j = 1\) we are done, since then \(\min\{\mathopen{}\left|u'\right|\mathclose{}, \mathopen{}\left|v'\right|\mathclose{}\} \leq n\), so that \(|\Delta(u')+\Delta(v')| \leq \mathopen{}\left|u'\right|\mathclose{} + \mathopen{}\left|v'\right|\mathclose{} \leq n + n \cdot \max(A, B) \leq \beta\). So assume now that \(j > 1\), which implies that \(\Delta(u'') > 0\). Note that \(j<h\) since \((u',v')\not=(u,v)\). Hence there exist unique words \(s,t\in\Sigma^*\) such that \(u'=u''s\) and \(v'=tv''\), where \(u''=x_1\cdots a_{j-1}x_j\) and \(v''=y_jb_{j-1}\cdots y_1\). By maximality of \(j\) we have \(\min\{|s|,|t|\}\leq n\). Setting \(f=\psi(\mathop{\mathrm{ext}}_{u'',v''})\) and \(g=\psi(\mathop{\mathrm{ext}}_{a_jx_{j+1}\cdots a_{h-1}x_h,y_h b_{h-1} \cdots y_{j+1}b_j})\) we have \(\psi(\mathop{\mathrm{ext}}_{u,v})=f\circ g\). We claim that there exist \(\mathop{\mathrm{ext}}_{x_g,y_g}\in\mathcal{O}(\Sigma^\triangle)\) such that \(\psi(\mathop{\mathrm{ext}}_{x_g,y_g})=g\) and \(|x_g|,|y_g|\leq |O|\cdot (n+1)\): indeed, by the pigeonhole principle and Lemma [ptn:hill95small] (as \(e \circ f \circ g = e\) and \(\Delta(u'') > 0\)), any \(\mathop{\mathrm{ext}}_{x,y}\in\mathcal{O}(\Sigma^\triangle)\) such that \(\psi(\mathop{\mathrm{ext}}_{x,y})=g\) and \(\max(|x|,|y|)>|O|\cdot (n+1)\) must have a stair factorization according to Lemma [lemma32ext] with an \(h > \left|O\right|\) and can thus be factorized as \(\mathop{\mathrm{ext}}_{x,y}=\mathop{\mathrm{ext}}_{x',y'}\circ\mathop{\mathrm{ext}}_{x'',y''}\circ\mathop{\mathrm{ext}}_{x''',y'''}\) such that \(\psi(\mathop{\mathrm{ext}}_{x,y})=\psi(\mathop{\mathrm{ext}}_{x',y'})\circ\psi(\mathop{\mathrm{ext}}_{x''',y'''})\), where moreover \((x'',y'')\in\Sigma^+\times\Sigma^+\). Thus, \(\psi(\mathop{\mathrm{ext}}_{u''x_g,y_gv''})=\psi(\mathop{\mathrm{ext}}_{u,v})\) and therefore \((u''x_g,y_gv'')\in\mathcal{U}_e\) with \(\Delta(u''x_g) > 0\). It follows \(\alpha=\frac{|u''x_g|}{|y_gv''|}= \frac{|u'|-|s|+|x_g|}{|y_g|+|v'|-|t|}\), or equivalently, using \(\frac{|u'|}{|v'|}=\alpha\): \[\begin{align} |s|&=&|u'|+|x_g|+\alpha(|t|-|y_g|-|v'|)= |x_g|+\alpha(|t|-|y_g|)\tag{2}\\ |t|&=&\frac{|s|-|u'|-|x_g|}{\alpha}+|y_g|+|v'|= \frac{|s|-|x_g|}{\alpha}+|y_g|\tag{3} \,\,\text{.} \end{align}\] Finally, we obtain \[\begin{align} |\Delta(u')+\Delta(v')| & = &|\Delta(u''s)+\Delta(tv'')|\\ &\stackrel{\Delta(u'')=-\Delta(v'')}{=}&|\Delta(s)+\Delta(t)|\\ &\leq & |s|+|t|\\ &=& \min(|s|,|t|)+\max(|s|,|t|)\\ &\leq& n+\max(|s|,|t|)\\ &\stackrel{(\ref{eq32s}),(\ref{eq32t})}{\leq}& n+\max\left(|x_g|+\alpha(n-|y_g|), \frac{n-|x_g|}{\alpha}+|y_g|\right)\\ &\leq& n+|O|\cdot (n+1)+n\cdot\max(A,B)\\ &\leq&(n+1)\cdot(|O|+\max(A,B)+1)\\ &=&\beta \,\,\text{.} \end{align}\] This proves Point 2 (b).

For Point 2 (c) and Point 2 (d) we set \(\gamma=(\lceil\frac{n}{2}\rceil+1)\cdot(n+1)+n\) and remark that \(\gamma\) does not depend on \(u\) nor \(v\). We only prove Point 2 (c), the proof of Point 2 (d) is analogous. As above, let \[\mathop{\mathrm{ext}}_{u,v}=\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ \dots \circ\mathop{\mathrm{ext}}_{x_{h-1},y_{h-1}}\circ\mathop{\mathrm{ext}}_{a_{h-1},b_{h-1}}\circ\mathop{\mathrm{ext}}_{x_h,y_h}\] be the stair factorization of \(\mathop{\mathrm{ext}}_{u,v}\) according to Lemma [lemma32ext]. Let \(u'\) with \(|u'|\geq\gamma\) be a factor of \(u\) and hence of \(x_1a_1x_2\cdots x_{h-1}a_{h-1}x_h\). By definition of stair factorization we have \(\Delta(x_i)=0\) for all \(i\in[1,h]\) and \(\Delta(a_i)=1\) for all \(i\in[1,h-1]\). Let \(w\) be the longest prefix of \(u'\) such that \(\Delta(w)=\min\{\Delta(x)\mid\text{x is a prefix of u'}\}\). Since \(|x_1|,|y_1|,\dots,|x_h|,|y_h|\leq n\), it immediately follows \(\Delta(w)\geq -\frac{n}{2}\) and \(|w|\leq n\). By the same reason, every prefix of the form \(ws\) of \(u'\) satisfies \(\Delta(ws)\geq \Delta(w)+\frac{|s|}{n+1}\). Thus we have \[\Delta(u')\geq \Delta(w)+\frac{|u'|-|w|}{n+1} \geq -\frac{n}{2}+ \frac{((\lceil\frac{n}{2}\rceil+1)\cdot(n+1)+n)-n}{n+1} \geq 1 \,\,\text{.} \qedhere\] ◻

Proof. Let \(L=L(G)\) for a vertically visibly pushdown grammar \(G=(V,\Sigma,P,S)\). Moreover, let \((\varphi_L,\psi_L)\colon (\mathcal{O}(\Sigma),\Sigma^\triangle)\to(R_L,O_L)\) be the syntactic morphism. For all \(e\in O_L\) recall the set of contexts \(\mathcal{R}_e=\{(u,v)\in\mathsf{Con}(\Sigma)\mid\psi_L(\mathop{\mathrm{ext}}_{u,v})=e\}\).

Let \(F=\{e\in O_L\mid\exists\mathop{\mathrm{ext}}_{u,v}\in\psi_L^{-1}(e) : (u,v) \in\mathcal{R}(G)\}\). Observe that \(F\) is a submonoid of \(O_L\) all of whose elements are \(\varphi_L(L)\)-reaching since \(G\) is vertically visibly pushdown. Also observe that \(\mathcal{R}(G)=\bigcup_{f \in F} \mathcal{R}_f\). We claim that since \(G\) is vertically visibly pushdown, there exists a constant \(C>0\) such that \(\frac{1}{C}\leq\frac{|x|}{|y|}\leq C\) for all \((x,y)\in\mathcal{R}(G)\setminus\{(\varepsilon,\varepsilon)\}\): indeed, one can take \(C=\frac{A}{B}\) where \(A = \max\bigl\{\max\{\mathopen{}\left|u\right|\mathclose{}, \mathopen{}\left|v\right|\mathclose{}\} \mathrel{\big|} T\rightarrow_GuT'v\bigr\}\) and \(B = \min\bigl\{\min\{\mathopen{}\left|u\right|\mathclose{}, \mathopen{}\left|v\right|\mathclose{}\} \mathrel{\big|} T\rightarrow_GuT'v\bigr\}\) since whenever \(T \Rightarrow_G^* x T' y\) thanks to a derivation comprising \(k \in \mathbb{N}_{>0}\) steps, we have \[\frac{1}{C} = \frac{k \cdot B}{k \cdot A} \leq \frac{\mathopen{}\left|x\right|\mathclose{}}{\mathopen{}\left|y\right|\mathclose{}} \leq \frac{k \cdot A}{k \cdot B} = C \,\,\text{.}\]

Next, we prove that for all \(\varphi_L(L)\)-reaching idempotents \(e\in O_L\) there exist \(g,h\in O_L\) such that \(g\circ e\circ h\in F\). Fix any such \(\varphi_L(L)\)-reaching idempotent \(e\in O_L\). Without loss of generality let us assume that \(e\) is not the identity in \(O_L\) (indeed, if \(e\) is the identity in \(O_L\), then we are done since we can then choose \(g=h=e\in F\)). Thus there exist \(g\in O_L\) and \(r\in R_L\) such that \((g\circ e)(r)\in\varphi_L(L)\). Moreover, let \(\mathop{\mathrm{ext}}_{u',v'}\in\psi_L^{-1}(g),\mathop{\mathrm{ext}}_{u,v}\in\psi_L^{-1}(e)\), and \(w\in\varphi_L^{-1}(r)\). Observe that we must have \((u,v)\not=(\varepsilon,\varepsilon)\) since \(\psi_L(\mathop{\mathrm{ext}}_{\varepsilon,\varepsilon})\) is the identity in \(O_L\). Since \(e\) is an idempotent we have that \(u'u^nwv^nv'\in L\) for all \(n\geq 1\). Fix a sufficiently large \(N\geq 1\) such that \(\frac{|u'|+|u|}{(N-1)|u|+|w|+N|v|+|v'|}\leq\frac{1}{C}\) and \(\frac{|u'|+N|u|+|w|+(N-1)|v|}{|v|+|v'|}\geq C\), which exists due to \((u,v)\not=(\varepsilon,\varepsilon)\). Since \(u'u^Nwv^Nv'\in L\) there exists \((x,y)\in\mathcal{R}(G)\setminus\{(\varepsilon,\varepsilon)\}\) such that \(xy=u'u^Nwv^Nv'\), \(S\Rightarrow_G^* xSy\), \(|x|\geq|u'u|\), and \(|y|\geq |vv'|\). Let \((x',y')\in\Sigma^*\times\Sigma^*\) be such that \((x,y)=(u'ux',y'vv')\). As \((u',v'),(u,v),(x,y)\in\mathsf{Con}(\Sigma)\), \(x'\in(\Sigma\setminus\Sigma_\text{ret})^*\), and \(y'\in(\Sigma\setminus\Sigma_\text{call})^*\), we can conclude \((x',y')\in\mathsf{Con}(\Sigma)\). That is, \((x,y)=(u',v')\circ(u,v)\circ(x',y')\in\mathcal{R}(G)\). Hence, \[g\circ e\circ\psi_L(\mathop{\mathrm{ext}}_{x',y'})=\psi_L(\mathop{\mathrm{ext}}_{u'ux',y'vv'})=\psi_L(\mathop{\mathrm{ext}}_{x,y})\in F.\]

We are now ready to prove Point 1. For the first direction, let us assume that \(L(G)\) is length-synchronous. Recalling that \(F\) is a submonoid of \(O_L\) all of whose elements are \(\varphi_L(L)\)-reaching, we obtain that \(R(G)=\bigcup_{f \in F} \mathcal{R}_f\) is length-synchronous by Lemma [lem:Length-synchronicity95subsemigroups].

Conversely, let us assume that \(\mathcal{R}(G)\) is length-synchronous. Assume by contradiction that \(L(G)\) is not length-synchronous. Hence \(\mathcal{R}_e\) is not length-synchronous for some \(\varphi_L(L)\)-reaching idempotent \(e\in O_L\), i.e. \(\psi_L(\mathop{\mathrm{ext}}_{u,v})=\psi_L(\mathop{\mathrm{ext}}_{u',v'})=e\) for some \(\mathop{\mathrm{ext}}_{u,v},\mathop{\mathrm{ext}}_{u',v'}\in\mathcal{O}(\Sigma^\triangle)\) such that \(\Delta(u),\Delta(u')>0\) and \(\frac{|u|}{|v|}\not=\frac{|u'|}{|v'|}\). Without loss of generality we may assume that \(|v|=|v'|\) (indeed, if \(|v|\not=|v'|\), then \(\mathop{\mathrm{ext}}_{u^{|v'|},v^{|v'|}},\mathop{\mathrm{ext}}_{(u')^{|v|},(v')^{|v|}}\) satisfies the desired property). As a consequence we have \(|u|\not=|u'|\), say \(|u|<|u'|\) without loss of generality. Since \(e\) is a \(\varphi_L(L)\)-reaching idempotent, as argued above, there exist \(g,h\in O_L\) such that \(g\circ e\circ h=f'\) for some \(f'\in F\). Let us fix \(\mathop{\mathrm{ext}}_{x_h,y_h}\in\psi_L^{-1}(h)\) and \(\mathop{\mathrm{ext}}_{x_g,y_g}\in\psi_L^{-1}(g)\). We have \(\psi_L(\mathop{\mathrm{ext}}_{x_gux_h,y_hvy_g}) = f' = \psi_L(\mathop{\mathrm{ext}}_{x_gu'x_h,y_hv'y_g})\). Since \(|x_g u x_h|<|x_g u' x_h|\) and \(|y_h v y_g|=|y_h v' y_g|\) it follows that \(\mathcal{R}_{f'}\) is not length-synchronous, contradicting our assumption that \(R(G)=\bigcup_{f \in F} \mathcal{R}_f\) is length-synchronous.

Let us next prove Point 2.

Let us first assume that \(L(G)\) is weakly length-synchronous. Again, since \(F\) is a submonoid of \(O_L\) all of whose elements are \(\varphi_L(L)\)-reaching, we obtain that \(R(G)=\bigcup_{f \in F} \mathcal{R}_f\) is weakly length-synchronous by Lemma [lem:Weak95length-synchronicity95subsemigroups].

Conversely, assume \(\mathcal{R}(G)\) is weakly length-synchronous. Assume by contradiction that \(\mathcal{R}_e\) is not weakly length-synchronous for some \(\varphi_L(L)\)-reaching idempotent \(e\in O_L\). Thus, \(\psi_L(\mathop{\mathrm{ext}}_{u,v})=\psi_L(\mathop{\mathrm{ext}}_{u',v'})=e\) for some \(\mathop{\mathrm{ext}}_{u,v},\mathop{\mathrm{ext}}_{u',v'}\in\mathcal{O}(\Sigma^\triangle)\) such that \(\Delta(u),\Delta(u')>0\) and moreover either \(u=u'\) and \(|v|\not=|v'|\) or \(v=v'\) and \(|u|\not=|u'|\). Without loss of generality let us assume that \(u=u'\) and \(|v|\not=|v'|\). As mentioned above, there exist \(g,h\in O_L\) such that \(g\circ e\circ h=f'\) for some \(f'\in F\). Fix some \(\mathop{\mathrm{ext}}_{x_g,y_g}\in\psi_L^{-1}(g)\) and some \(\mathop{\mathrm{ext}}_{x_h,y_h}\in\psi_L^{-1}(h)\). Analogously, as argued above, we have \(\psi_L(\mathop{\mathrm{ext}}_{x_gux_h,y_hvy_g})=\psi_L(\mathop{\mathrm{ext}}_{x_gux_h,y_hv'y_g})=f'\), \(\Delta(x_gux_h)>0\), and \(|y_hvy_g|\not=|y_hv'y_g|\), implying that \(\mathcal{R}_{f'}\) is not weakly length-synchronous, a contradiction to our assumption that \(\mathcal{R}(G)=\bigcup_{f\in F} \mathcal{R}_f\) is weakly length-synchronous. ◻

Proof. The proof goes by structural induction on \(w\).

• \(w = \varepsilon\). Then we are done because \(w\) contains only internal letters.

• \(w = c\) for a \(c \in \Sigma_\text{int}\). Then we are again done because \(w\) contains only internal letters.

• \(w = a w' b\) for \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\) and \(w' \in \Sigma^\triangle\). By using the inductive hypothesis, \(w'\) has a nesting-maximal stair factorization \(\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1, b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_{k},y_k}\circ\mathop{\mathrm{ext}}_{a_{k}, b_{k}} (w'')\). It directly follows that \(\mathop{\mathrm{ext}}_{a,b}\circ\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1, b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_{k},y_k}\circ\mathop{\mathrm{ext}}_{a_{k}, b_{k}} (w'')\) is a nesting-maximal stair factorization of \(w\).

• \(w = u v\) for \(u, v \in \Sigma^\triangle \setminus \{\varepsilon\}\). Then \(w\) can be decomposed as \(z_1 \cdots z_m\) with \(z_1, \ldots, z_m \in \Sigma_\text{call}\Sigma^\triangle \Sigma_\text{ret}\cup \Sigma_\text{int}\) and \(m \in \mathbb{N}, m \geq 2\). In this case, either \(z_i \in \Sigma_\text{int}\) for all \(i \in [1, m]\) and thus we are done because \(w\) contains only internal letters, or there exists some \(i \in [1, m]\) such that \(z_i \in \Sigma_\text{call}\Sigma^\triangle \Sigma_\text{ret}\) and has maximal nesting depth, i.e.\(\mathop{\mathrm{nd}}(w) = \mathop{\mathrm{nd}}(z_i)\). In this second subcase, we have that \(z_i = a z_i' b\) with \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\) and \(z_i' \in \Sigma^\triangle\). By using the inductive hypothesis, \(z_i'\) has a nesting-maximal stair factorization \(\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{ a_1, b_1}\circ \cdots \circ \mathop{\mathrm{ext}}_{x_k,y_k}\circ\mathop{\mathrm{ext}}_{a_k,b_k} (w'')\). Therefore, \[\mathop{\mathrm{ext}}_{z_1 \cdots z_{i - 1}, z_{i + 1} \cdots z_k}\circ \mathop{\mathrm{ext}}_{a,b}\circ\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ \dots\mathop{\mathrm{ext}}_{x_k,y_k}\circ\mathop{\mathrm{ext}}_{a_k,b_k}(w'')\] is a nesting-maximal stair factorization of \(w\).

 ◻

Proof. Let \(u_j=\mathop{\mathrm{ext}}_{a_j,b_j}\circ\mathop{\mathrm{ext}}_{x_{j+1},y_{j+1}} \circ\cdots\circ\; \mathop{\mathrm{ext}}_{a_{k},b_{k}}(u')\) for all \(j\in[1,k]\). Note that we have \(\mathop{\mathrm{nd}}(u)=\mathop{\mathrm{nd}}(u_1)=d>0\) by assumption. Moreover, \(\mathop{\mathrm{nd}}(u_{j})\geq\mathop{\mathrm{nd}}(u_{j+1})\) for all \(j\in[1,k-1]\) by definition of nesting depth. Thus, since \(\mathop{\mathrm{nd}}(u_k) = 1 > 0 = \mathop{\mathrm{nd}}(u_{k + 1})\), it follows that \[h=\min\{j\in[1,k]\mid\mathop{\mathrm{nd}}(u_j)>\mathop{\mathrm{nd}}(u_{j+1})\}\] is well-defined and \(\mathop{\mathrm{nd}}(u)=\mathop{\mathrm{nd}}(u_1)=\mathop{\mathrm{nd}}(u_h)=d\), thus showing Point 1. Since \[d=\mathop{\mathrm{nd}}(u_h)\leq\mathop{\mathrm{nd}}(u_{h+1})+1\] and \(\mathop{\mathrm{nd}}(u_{h+1})<\mathop{\mathrm{nd}}(u_h)=d\) it follows \(\mathop{\mathrm{nd}}(u_{h+1})=d-1\), thus showing Point 2. To prove Point 3, assume by contradiction that \(\mathop{\mathrm{nd}}(x_j)\geq d\) or \(\mathop{\mathrm{nd}}(y_j)\geq d\) for some \(j\in[1,h]\). Without loss of generality assume \(\mathop{\mathrm{nd}}(x_j)\geq d\). Since \(x_1=y_1=\varepsilon\) and \(d>0\) we must have \(j\in[2,h]\). It follows \[\mathop{\mathrm{nd}}(u)\geq\mathop{\mathrm{nd}}(u_{j-1})=\mathop{\mathrm{nd}}(a_{j-1}x_ju_jy_jb_{j-1})\geq \min(\mathop{\mathrm{nd}}(x_j),\mathop{\mathrm{nd}}(u_j))+1\geq d+1>d=\mathop{\mathrm{nd}}(u)\,\,\text{,}\] which is a contradiction. ◻

Proof of Proposition [ptn:Bounded95nesting-depth]. Let \(L\subseteq\Sigma^\triangle\) be a weakly length-synchronous VPL. We claim that \(\mathop{\mathrm{nd}}(L)\leq n+1\), where \(n\) is the pumping constant from Lemma [lem:Ext95pumping]. Assume by contradiction that \(\mathop{\mathrm{nd}}(u)=d\) for some \(u\in L\) and some \(d>n+1\). Let \[u=\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ\dots\circ \mathop{\mathrm{ext}}_{x_{k},y_{k}}\circ\mathop{\mathrm{ext}}_{a_k,b_k}(u')\] be a nesting-maximal stair factorization of \(u\) according to Lemma [lem:Maximal95stair95factorization]. According to Lemma [L32nesting32induction] there exists \(i\in[1,k]\) such that, setting \[u_j=\mathop{\mathrm{ext}}_{a_j,b_j}\circ\mathop{\mathrm{ext}}_{x_{j+1},y_{j+1}}\circ\cdots\circ \mathop{\mathrm{ext}}_{a_k,b_k}(u')\] for all \(j \in [1, k]\) and \(u_{k + 1} = u'\), we have \(\mathop{\mathrm{nd}}(u)=\mathop{\mathrm{nd}}(u_i)=d\) and \(\mathop{\mathrm{nd}}(u_{i+1})=d-1\). Since \(d - 1 > n > 0\), we must have \(i + 1 \leq k\), so that \(u_i=a_ix_{i+1}u_{i+1}y_{i+1}b_i\) with \(u_{i+1} \in \Sigma_\text{call}\Sigma^\triangle \Sigma_\text{ret}\) and \(\mathop{\mathrm{nd}}(x_{i+1}u_{i+1}y_{i+1})=\mathop{\mathrm{nd}}(u_{i+1})=d-1\). Hence it follows that \(\mathop{\mathrm{nd}}(x_{i+1})=d-1\) or \(\mathop{\mathrm{nd}}(y_{i+1})=d-1\). Without loss of generality let us assume \(\mathop{\mathrm{nd}}(y_{i+1})=d-1>n\). A simple induction shows that \(|x|\geq 2^{\mathop{\mathrm{nd}}(x)}-1\geq\mathop{\mathrm{nd}}(x)\) for all \(x\in\Sigma^\triangle\). Thus, we have \(|y_{i+1}|\geq\mathop{\mathrm{nd}}(y_{i+1})>n\), contradicting Proposition [ptn:hill95small]. ◻

Proof. Recall that \((R_L,O_L)=(\Sigma^\triangle,\mathcal{O}(\Sigma^\triangle))\mathclose{}/\mathopen{}\sim_L\) by Definition [def32syntactic]. Hence for all \((u,v),(u',v')\in\mathsf{Con}(\Sigma)\) we have \((u,v)\equiv_L(u',v')\) if, and only if, \(\psi_L(\mathop{\mathrm{ext}}_{u,v})=\psi_L(\mathop{\mathrm{ext}}_{u',v'})\).

First, let us assume that \((\varphi_L,\psi_L)\colon (\Sigma^\triangle,\mathcal{O}(\Sigma^\triangle))\rightarrow(R_L,O_L)\) is quasi-aperiodic. Assume by contradiction that \(L\) is not quasi-counterfree. Thus, there exists some \(\sigma=(u,v)\in\mathsf{Con}(\Sigma)\) such that \(\sigma^n\not\equiv_L\sigma^{n+1}\) for all \(n\in\mathbb{N}\) and \(\tau\equiv_L\sigma\circ\sigma\) for some \(\tau=(x,y)\in\mathsf{Con}(\Sigma)\cap\Sigma^{|u|}\times \Sigma^{|v|}\). The latter can equivalently be rephrased as \(\psi_L(\mathop{\mathrm{ext}}_{x,y})=\psi_L(\mathop{\mathrm{ext}}_{u^2,v^2})\). By choice of \(\sigma\) and the fact that \(\equiv_L\) has finite index there exist \(s\geq 1\) and \(t\geq 2\) such that \(\sigma^{s+i}\equiv_L\sigma^{s+i+t}\) for all \(i\geq 0\) and \(\sigma^{s+i}\not\equiv_L\sigma^{s+j}\) for all \(i,j\in[0,t-1]\) with \(i\not=j\). It follows that the set \(G=\psi_L(\{\mathop{\mathrm{ext}}_{u^{s+i},v^{s+i}}\mid i\in[0,t-1]\})\) is a non-trivial group with identity \(g_0=\psi_L(\mathop{\mathrm{ext}}_{u^{s+k},v^{s+k}})\in\psi_L(\mathcal{O}(\Sigma^\triangle)^{(s+k)|u|,(s+k)|v|})\), where \(k\) is the unique integer in \([0,t-1]\) such that \(s+k\) is divisible by \(t\). Also observe that \(G\) is a cyclic group that is generated by \(g_1=\psi_L(\mathop{\mathrm{ext}}_{u^{s+k+1},v^{s+k+1}})\). That is \(G=\{g_0,g_1,\dots,g_{t-1}\}\), where \(g_i=g_1^i\) for all \(i\in[2,t-1]\). But note that due to \(\psi_L(\mathop{\mathrm{ext}}_{x,y})=\psi_L(\mathop{\mathrm{ext}}_{u^2,v^2})\) we obtain \(g_1=\psi_L(\mathop{\mathrm{ext}}_{u^{s+k+1},v^{s+k+1}})=\psi_L(\mathop{\mathrm{ext}}_{xu^{s+k-1},v^{s+k-1}y})\) and thus \(g_0,g_1\in\psi_L(\mathcal{O}(\Sigma^\triangle)^{(s+k)|u|,(s+k)|v|})\) due to \(|x|=|u|\) and \(|y|=|v|\). Since \(g_i=g_0^{t-1-i}g_1^i\) for all \(i\in[0,t-1]\) we obtain that \(G=\{g_0,g_1,\dots,g_{t-1}\}\) is contained in \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{(t-1)(s+k)|u|,(t-1)(s+k)|v|})\), hereby contradicting quasi-aperiodicity of \((\varphi_L,\psi_L)\).

For the converse direction, let us assume that \(L\) is quasi-counterfree. Assume by contradiction that \((\varphi_L,\psi_L)\) is not quasi-aperiodic. That is, for some \(k,l\in\mathbb{N}\) the set \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k,l})\) contains a non-trivial group \(G\). Let \(g_0\in G\) be the identity of \(G\). Fix some \(g\in G\) with \(g\not=g_0\) and some \(\mathop{\mathrm{ext}}_{u,v}\in\mathcal{O}(\Sigma^\triangle)^{k,l}\) such that \(\psi_L(\mathop{\mathrm{ext}}_{u,v})=g\). Let \(\sigma=(u,v)\in\mathsf{Con}(\Sigma)\cap\Sigma^k\times\Sigma^l\). Since \(g\) is not the identity in \(G\) we have that \(\psi_L(\mathop{\mathrm{ext}}_{u^n,u^n})\not=\psi_L(\mathop{\mathrm{ext}}_{u^{n+1},v^{n+1}})\) for all \(n\in\mathbb{N}\), equivalently \(\sigma^n\not\equiv_L\sigma^{n+1}\) for all \(n\in\mathbb{N}\). But since moreover \(\psi_L(\mathop{\mathrm{ext}}_{u^n,v^n})\) is in \(G\) and thus in \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k,l})\) for all \(n\in\mathbb{N}\) it follows that \(\sigma\circ\sigma\equiv_L\tau\) for some \(\tau\in\mathsf{Con}(\Sigma)\cap\Sigma^{k}\times\Sigma^{l}\). We thus obtain a contradiction to our assumption that \(L\) is quasi-counterfree. ◻

Proof. To show the first point, let us fix some \(\varphi_L(L)\)-reaching \(r\in R_L\). Thus, there exist \(w_r\in\Sigma^\triangle\) and \((u_r,v_r)\in\mathsf{Con}(\Sigma)\) such that \(\varphi_L(w_r)=r\) and \(\varphi_L(u_rw_rv_r)\in \varphi_L(L)\). By definition of the syntactic morphism of \(L\) (Definition [def32syntactic]) for all \(r_1,r_2\in R_L\) with \(r_1\not=r_2\) there exists some \(e_{r_1,r_2}\in O_L\) such that \(e_{r_1,r_2}(r_1)\in \varphi_L(L)\Leftrightarrow e_{r_1,r_2}(r_2)\not\in \varphi_L(L)\). For each such \(e_{r_1,r_2}\in O_L\) fix \((u_{r_1,r_2},v_{r_1,r_2})\in\mathsf{Con}(\Sigma)\) with \(\psi_L(\mathop{\mathrm{ext}}_{u_{r_1,r_2},v_{r_1,r_2}})=e_{r_1,r_2}\).

Hence, for all \(w\in\Sigma^*\) we have \[w\in\varphi_L^{-1}(r)\quad\Longleftrightarrow\quad u_rwv_r\in L\;\wedge\; \bigwedge_{\substack{r'\in R_L\\r\not=r'}} u_{r,r'}wv_{r,r'}\in L\leftrightarrow u_{r,r'}w_rv_{r,r'}\in L \,\,\text{,}\] thus showing \(\varphi_L^{-1}(r)\leq_{\mathrm{cd}}L\).

For the second point, let us fix some \(\varphi_L(L)\)-reaching \(e\in O_L\). Fix some \((u_e,v_e)\in\mathsf{Con}(\Sigma)\) such that \(\psi_L(\mathop{\mathrm{ext}}_{u_e,v_e})=e\). Thus, again, there exist \(w_e\in\Sigma^\triangle\) and \((u_e',v_e')\in\mathsf{Con}(\Sigma)\) such that \(\varphi_L(u_e'u_ew_ev_ev_e')\in \varphi_L(L)\). Again by definition of the syntactic morphism of \(L\) (Definition [def32syntactic]), for all \(e_1,e_2\in O_L\) with \(e_1\not=e_2\) there exist some \(f_{e_1,e_2}\in O_L\) and some \(r_{e_1,e_2}\in R_L\) such that \(f_{e_1,e_2}(e_1(r_{e_1,e_2}))\in\varphi_L(L)\Leftrightarrow f_{e_1,e_2}(e_2(r_{e_1,e_2}))\not\in\varphi_L(L)\). For each such \(f_{e_1,e_2}\) and \(r_{e_1,e_2}\) fix, respectively, \((u_{e_1,e_2},v_{e_1,e_2})\in\mathsf{Con}(\Sigma)\) and \(w_{e_1,e_2}\in\Sigma^\triangle\) such that \(\psi_L(\mathop{\mathrm{ext}}_{u_{e_1,e_2},v_{e_1,e_2}}) = f_{e_1,e_2}\) and \(\varphi_L(w_{e_1,e_2})=r_{e_1,e_2}\), respectively. Hence, for all \(u\#v\in\Sigma^*\#\Sigma^*\) we have \[u\#v\in L_e\quad\Longleftrightarrow\quad\; u_e' u w_e v v_e' \in L\;\wedge\; \bigwedge_{\substack{e'\in O_L\\e\not=e'}} u_{e,e'} u w_{e,e'} v v_{e,e'}\in L\leftrightarrow u_{e,e'} u_e w_{e,e'} v_e v_{e,e'} \in L \,\,\text{,}\] thus showing \(L_e\leq_{\mathrm{cd}}L\). ◻

Proof. Recall that \((R_L, O_L)\) is the syntactic \(\mathop{\mathrm{Ext}}\)-algebra of \(L\) and \((\varphi_L, \psi_L)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (R_L, O_L)\) is its syntactic morphism. Assume that \((\varphi_L, \psi_L)\) is not \(\varphi_L(L)\)-weakly-length-synchronous.

Assume first there exist \(\mathop{\mathrm{ext}}_{u, v}, \mathop{\mathrm{ext}}_{u', v} \in \mathcal{O}(\Sigma^\triangle)\) satisfying that \(\psi_L(\mathop{\mathrm{ext}}_{u, v}) = \psi_L(\mathop{\mathrm{ext}}_{u', v})\) that is a \(\varphi_L(L)\)-reaching idempotent such that \(\Delta(u)\), \(\Delta(u') > 0\), but \(\mathopen{}\left|u\right|\mathclose{} \neq \mathopen{}\left|u'\right|\mathclose{}\). We exploit the fact that \(\mathopen{}\left|u\right|\mathclose{} \neq \mathopen{}\left|u'\right|\mathclose{}\) to reduce \(\mathrm{EQUALITY}=\bigl\{w\in\{0,1\}^* \mathrel{\big|}|w|_0=|w|_1\bigr\}\) to \(L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\). The constant-depth reduction works as follows on input \(w \in \{0, 1\}^*\):

1. Check if \(\mathopen{}\left|w\right|\mathclose{} = 2 n\) for some \(n \in \mathbb{N}\), reject if it is not the case.

2. Compute \(w'=\alpha(w)\), where \(\alpha\alpha\{0,1\}^*\rightarrow \Sigma^*\) is the length-multiplying morphism satisfying \(\alpha(1)=u^{\mathopen{}\left|u'\right|\mathclose{}}\) and \(\alpha(0)=u'^{\mathopen{}\left|u\right|\mathclose{}}\).

3. Accept whenever \(w' \# v^{n (\mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{})} \in L_{\psi(\mathop{\mathrm{ext}}_{u, v})}\).

Bearing in mind that \(0<\Delta(u)=-\Delta(v)=\Delta(u')\), the latter forms a valid reduction, because given a word \(w \in \{0, 1\}^*\) of length \(2 n\) for an \(n \in \mathbb{N}\) that contains \(k \in [0, 2 n]\) many \(1\)’s, for \(w' \# v^{n (\mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{})}\) to be in \(L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\), it is in particular required that \(w' v^{n (\mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{})}\) is well-matched, so it is necessary and sufficient that \[\begin{array}{lrll} &k \cdot \Delta(u) \cdot \mathopen{}\left|u'\right|\mathclose{} + (2 n - k) \cdot \Delta(u') \cdot \mathopen{}\left|u\right|\mathclose{} & =& -n \cdot \Delta(v) \cdot (\mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{})\\ \Longleftrightarrow\qquad& (k - n) \cdot \Delta(u) \cdot \mathopen{}\left|u'\right|\mathclose{} + (n - k) \cdot \Delta(u') \cdot \mathopen{}\left|u\right|\mathclose{} & = &0\\ \Longleftrightarrow\qquad& (k - n) \cdot \Delta(u) \cdot (\mathopen{}\left|u'\right|\mathclose{} - \mathopen{}\left|u\right|\mathclose{}) & = &0\\ \Longleftrightarrow\qquad&k & =& n \,\,\text{.} \end{array}\] Additionally applying Lemma [lemma32reduction32element] we obtain \(\mathrm{EQUALITY}\leq_{\mathrm{cd}}L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})} \leq_{\mathrm{cd}}L\). Assume now there exist \(\mathop{\mathrm{ext}}_{u, v}, \mathop{\mathrm{ext}}_{u, v'} \in \mathcal{O}(\Sigma^\triangle)\) satisfying that \(\psi_L(\mathop{\mathrm{ext}}_{u, v}) = \psi_L(\mathop{\mathrm{ext}}_{u, v'})\) is an \(\varphi_L(L)\)-reaching idempotent such that \(\Delta(u) > 0\) but \(\mathopen{}\left|v\right|\mathclose{} \neq \mathopen{}\left|v'\right|\mathclose{}\). Symmetrically, one can prove that we also have \(\mathrm{EQUALITY}\leq_{\mathrm{cd}}L\) in this case.

In conclusion, as \(\mathrm{EQUALITY}\) is \(\mathsf{TC}^0\)-complete under constant-depth reductions, it follows that \(L\) is \(\mathsf{TC}^0\)-hard under constant-depth reductions. ◻

Proof. Since \(L\) is not quasi-aperiodic, by Point 2 (a) Proposition [prop32effectivity] one can effectively compute \(k,l\in\mathbb{N}\) such that \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k,l})\) is not aperiodic. Thus, one can compute \(m\geq 2\) such that \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k,l})\) contains the additive group \(G=([0,m-1],+,0)\) of \(\mathbb{Z}/m\mathbb{Z}\) for some prime number \(m\). Moreover, there exist \(\mathop{\mathrm{ext}}_{u_0,v_0}, \mathop{\mathrm{ext}}_{u_1,v_1}\in\mathcal{O}(\Sigma^\triangle)^{k,l}\) such that \(\psi_L(\mathop{\mathrm{ext}}_{u_0,v_0})=0_G\) and \(\psi_L(\mathop{\mathrm{ext}}_{u_1,v_1})=1_G\). Since \(G\) is a group both \(\psi_L(\mathop{\mathrm{ext}}_{u_0,v_0})\) and \(\psi_L(\mathop{\mathrm{ext}}_{u_1,v_1})\) are \(\varphi_L(L)\)-reaching. Moreover there exist \(xy,z\in\Sigma^\triangle\) such that \(xu_0zv_0y\in L\) if, and only if, \(xu_1zv_1y\not\in L\). Let us assume without loss of generality that \(xu_0zv_0y\not\in L\) and \(xu_1zv_1y\in L\) (the case when \(xu_0zv_0y\in L\) and \(xu_1zv_1y\not\in L\) can be proven analogously). Let \(h_\uparrow,h_\downarrow\colon \{0,1\}^*\rightarrow\Sigma^*\) be the length-multiplying morphisms satisfying \(h_\uparrow(i)=u_i\) and \(h_\downarrow(i)=v_i\) for all \(i\in\{0,1\}\). We claim that \[w\in\text{MOD}_m\Longleftrightarrow \bigwedge_{i=1}^{m-1}xh_\uparrow(w)^{i^{m-2}} zh_\downarrow(w^R)^{i^{m-2}}y\not\in L.\] Let \(w_i=xh_\uparrow(w)^{i^{m-2}} zh_\downarrow(w^R)^{i^{m-2}}y\) for all \(i\in[1,m-1]\). Observe that \(w_i\in\Sigma^\triangle\) for all \(i\in[1,m-1]\) directly by definition of the morphisms \(h_\uparrow\) and \(h_\downarrow\).

To show the above equivalence, let us first assume that \(|w|_1\) is divisible by \(m\). Then we have \(\psi_L(\mathop{\mathrm{ext}}_{h^\uparrow(w),h^\downarrow(w^R)})= \psi_L(\mathop{\mathrm{ext}}_{u_0,v_0})=0_G\), and consequently \(\psi_L(\mathop{\mathrm{ext}}_{h^\uparrow(w)^{i^{m-2}},h^\downarrow(w)^{i^{m-2}}})=0_G\) for all \(i\in[1,m-1]\). It follows \(w_i\not\in L\) for all \(i\in[1,m-1]\), as desired. Conversely, assume that \(|w|_1\) is not divisible by \(m\), i.e. \(|w|_1\equiv i\text{ mod }m\) for some \(i\in[1,m-1]\). Hence \(\psi_L(\mathop{\mathrm{ext}}_{h^\uparrow(w),h^\uparrow(w^R)})=i_G\not=0_G\) and thus \(\psi_L(\mathop{\mathrm{ext}}_{h^\uparrow(w)^{i^{m-2}},h^\uparrow(w^R)^{i^{m-2}}})= (i^{m-1}\text{ mod } m)_G=1_G\) by Fermat’s Little Theorem. Hence \(w_i\in L\) as required.

Altogether we obtain \(\text{MOD}_m\leq_{\mathrm{cd}}L\). ◻

Proof of Proposition [prop32notsolvable]. Assume \((R_L,O_L)\) is not solvable. Then there exists a subset \(G\subseteq O_L\), where \(G\) is a non-trivial perfect group, i.e. \(G=\lbrack G,G\rbrack\). Let \(\omega\) be the idempotent power of \(G\). For all \(g,h\in G\) there exist \(\mathop{\mathrm{ext}}_{u_g,v_g},\mathop{\mathrm{ext}}_{u_h,v_h}\in\mathcal{O}(\Sigma^\triangle)\) such that \[\lbrack g,h\rbrack=ghg^{-1}h^{-1}=ghg^{\omega-1}h^{\omega-1}= \psi_L\left(\mathop{\mathrm{ext}}_{u_gu_hu_g^{\omega-1}u_h^{\omega-1},v_h^{\omega-1}v_g^{\omega-1}v_hv_g}\right)\] and \(1_G=g^\omega h^\omega=\psi_L(\mathop{\mathrm{ext}}_{u_g^\omega u_h^\omega,v_h^\omega v_g^\omega})\). Therefore, for all \(g,h\in G\) we have \[\lbrack g,h\rbrack=\psi_L\left( \mathop{\mathrm{ext}}_{u_gu_hu_g^{\omega-1}u_h^{\omega-1},v_h^{\omega-1}v_g^{\omega-1}v_hv_g}\circ\; \mathop{\bigcirc}_{\substack{(g',h')\in G^2\\(g',h')\not=(g,h)}} \mathop{\mathrm{ext}}_{u_{g'}^\omega u_{h'}^\omega,v_{h'}^\omega, v_{g'}^\omega}\right) \,\,\text{.}\] Hence, \(\{\lbrack g,h\rbrack \mid g,h\in G\}\subseteq\mathcal{O}(\Sigma^\triangle)^{k,l}\) for \[k=\sum_{(g,h)\in G^2}(|u_g|+|u_h|)\cdot\omega\quad\text{and}\quad l=\sum_{(g,h)\in G^2}(|v_h|+|v_g|)\cdot\omega\quad.\] Since \(G=\lbrack G,G\rbrack\) every element of \(G\) can be written as the product of at most \(|G|\) elements in \(\{\lbrack g,h\rbrack\mid g,h\in G\}\) and, in fact, even as the product of exactly \(|G|\) elements in \(\{\lbrack g,h\rbrack\mid g,h\in G\}\), since it contains the identity \(1_G\). Thus, we can conclude that \(G\subseteq\psi_L(\mathcal{O}(\Sigma^\triangle)^{k\cdot |G|,l\cdot|G|}\). Since the word problem of any non-solvable finite group is \(\mathsf{NC}^1\)-hard by [12] and \(G\subseteq\psi_L(\mathcal{O}(\Sigma^\triangle)^{k\cdot|G|,l\cdot|G|}\), it follows that the word problem for \(G\) is constant-depth reducible to \(L\). Hence \(L\) is \(\mathsf{NC}^1\)-hard and in particular \(\mathsf{TC}^0\)-hard. ◻

Proof. To prove Point 1 recall that \(\varphi_L^{-1}(r)\) is a VPL and hence a context-free language for all \(r\in R_L\). By Parikh’s Theorem [29] it follows that \(S_r=\bigl\{|w| \mathrel{\big|}w\in\Sigma^\triangle, \varphi_L(w)=r\bigr\}\subseteq\mathbb{N}\) is a semilinear set for all \(r\in R_L\). It follows that for all \(U\subseteq R_L\) the set \(S_U=\bigl\{|w| \mathrel{\big|}w\in\Sigma^\triangle, \varphi_L(w)\in U\bigr\}\subseteq \mathbb{N}\) is semilinear since semilinear sets are closed under union. Point 1 follows immediately from this observation.

Next we prove Point 2, Point 3 can be proven analogously. According to Lemma [lemma32Le] in Section 6.0.0.0.2 for \(\#\not\in\Sigma\) the language \(L_e=\{u\#v\mid uv\in\Sigma^\triangle : \psi_L(\mathop{\mathrm{ext}}_{u,v})=e\}\) is a VPL for all \(e\in O_L\). As the language \(K=\{u\#v\mid u,v\in\Sigma^\triangle\}\) is obviously a VPL, it follows that for all \(e\in O_L\) the language \[L_{e^\uparrow}=L_e\setminus K=\{u\#v\mid uv\in\Sigma^\triangle : \psi_L(\mathop{\mathrm{ext}}_{u,v})=e, \Delta(u)>0\}\subseteq L_e\] is a VPL as well. By Lemma [lemma32semilinear] in Section 6.0.0.0.2 the set \[S_e=\{(k,l)\in\mathbb{N}\times\mathbb{N}\mid \exists u\in\Sigma ^k, v\in^l : u \# v \in L_{e^\uparrow}\}\] is semilinear as well for all \(e\in O_L\). As a consequence we obtain that for all \(Y\subseteq O_L\) the set \[S_Y=\{(k,l)\in\mathbb{N}\times\mathbb{N}\mid \exists u\in\Sigma^k, v\in\Sigma^l,e\in Y : u \# v \in L_{e^\uparrow}\}\subseteq\mathbb{N}\times\mathbb{N}\] is semilinear as well since semilinear sets are closed under union. Since for all \(Y\subseteq O_L\) the set \(\{k\in\mathbb{N}\mid \psi_L(\mathcal{O}(\Sigma^\triangle)_\uparrow^{k,*}=Y\}\) is nothing but the projection of \(S_Y\) onto the first component and semilinear sets are closed under projection, Point 2 follows. ◻

Proof. Take \(t \in \mathbb{N}\) and \(p \in \mathbb{N}_{>0}\) given by Lemma [lem:Finite95Ext-algebra95morphisms95stability] such that \(\psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{i, *}_\uparrow\bigr) = \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{j, *}_\uparrow\bigr)\) for all \(i, j \in \mathbb{N}\) satisfying \(i, j \geq t\) and \(i \equiv j \pmod{p}\). Define \(\theta_{t, p}\colon \mathbb{N}\to \mathbb{N}\) as \[\theta_{t, p}(n) = \begin{cases} n & \text{if n < t}\\ \min\{n' \in \mathbb{N}\mid n' \geq t \wedge n' \equiv n \pmod{p}\} & \text{otherwise} \end{cases}\] for all \(n \in \mathbb{N}\). Take \(M\) to be the syntactic monoid of \(\mathcal{V}_{\psi_L}\) and \(h\colon \Gamma_{\psi_L}^* \to M\) to be its syntactic morphism.

If there exists \(f \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)_\uparrow\bigr)\) and \(k \in \mathbb{N}\) such that \(\$^k f \notin \mathcal{V}_{\psi_L}\), let us fix some \(f_\bot\) and \(k_\bot\) that satisfy this. Observe that for all \(k \in \mathbb{N}\), we have that \(h(\$^k) = h(\$^{\theta_{t, p}(k)})\). Further, for all \(n \in \mathbb{N}_{>0}\), \(k_1, \ldots, k_{n + 1} \in \mathbb{N}\) and \(f_1, \ldots, f_n \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)_\uparrow\bigr)\), we have \(h(\$^{k_1} f_1 \cdots \$^{k_n} f_n \$^{k_{n + 1}}) = h(\$^{\theta_{t, p}(k_1)} f_1 \alpha \$^{\theta_{t, p}(k_{n + 1})})\), where \[\alpha = \begin{cases} \varepsilon & \text{if \$^{k_2} f_2 \cdots \$^{k_n} f_n \in \mathcal{V}_{\psi_L}}\\ \$^{k_\bot} f_\bot & \text{otherwise} \,\,\text{.} \end{cases}\] Therefore, \(M\) is finite and thus \(\mathcal{V}_{\psi_L}\) is regular. Let \(l \in \mathbb{N}_{>0}\) be the stability index of \(h\) and take \(q \in\mathbb{N}_{>0}\) such that \(q\cdot l\geq t\) and \(q \cdot l \equiv 0 \pmod{p}\). By definition, we have \(h(\Gamma_{\psi_L}^l) = h(\Gamma_{\psi_L}^{q \cdot l})\). Thus, to show that \(h\) is quasi-aperiodic it is sufficient to prove that for all \(m \in h(\Gamma_{\psi_L}^{q \cdot l})\), we have \(m^2 = m^3\). Indeed, given \(m \in h(\Gamma_{\psi_L}^{q \cdot l})\), only the following three cases can occur.

1. \(m = h(\$^{q \cdot l})\). In this case, we have \[m^2 = h(\$^{2 \cdot q \cdot l}) = h(\$^{\theta_{t, p}(2 \cdot q \cdot l)}) = h(\$^{\theta_{t, p}(q \cdot l)}) = h(\$^{q \cdot l}) = m \,\,\text{,}\] where the third equality follows from \(\theta_{t,p}(2\cdot q\cdot l)=\theta_{t,p}(q\cdot l)\).

2. \(m = h(\$^{k_1} f \$^{k_\bot} f_\bot \$^{k_2})\) for \(f \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)_\uparrow\bigr)\) and \(k_1, k_2 \in \mathbb{N}\) satisfying \(\theta_{t, p}(k_1) = k_1\) and \(\theta_{t, p}(k_2) = k_2\). In this case, we have \[m^2 = h(\$^{k_1} f \$^{k_\bot} f_\bot \$^{k_1 + k_2} f \$^{k_\bot} f_\bot \$^{k_2}) = h(\$^{k_1} f \$^{k_\bot} f_\bot \$^{k_2}) = m \,\,\text{,}\] where the second equality follows from \(\$^{k_\bot} f_\bot \$^{k_1 + k_2} f \$^{k_\bot} f_\bot \notin \mathcal{V}_{\psi_L}\).

3. \(m = h(\$^{k_1} f \$^{k_2})\) for \(f \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)_\uparrow\bigr)\) and \(k_1, k_2 \in \mathbb{N}\) satisfying \(\theta_{t, p}(k_1) = k_1\) and \(\theta_{t, p}(k_2) = k_2\). If \(f \in \psi_L\bigr(\mathcal{O}(\Sigma^\triangle)^{k_1 + k_2 + 1, *}_\uparrow\bigl)\), then \[m^2 = h(\$^{k_1} f \$^{k_1 + k_2} f \$^{k_2}) = h(\$^{k_1} f \$^{k_2}) = m\] because \(\$^{k_1 + k_2} f \in \mathcal{V}_{\psi_L}\). Otherwise, \(f \notin \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{k_1 + k_2 + 1, *}_\uparrow\bigr)\) and then \[m^2 = h(\$^{k_1} f \$^{k_1 + k_2} f \$^{k_2}) = h(\$^{k_1} f \$^{k_\bot} f_\bot \$^{k_2})\] because \(\$^{k_1 + k_2} f \notin \mathcal{V}_{\psi_L}\), so \[m^3 = h(\$^{k_1} f \$^{k_\bot} f_\bot \$^{k_1 + k_2} f \$^{k_2}) = h(\$^{k_1} f \$^{k_\bot} f_\bot \$^{k_2}) = m^2\] because \(\$^{k_\bot} f_\bot \$^{k_1 + k_2} f \notin \mathcal{V}_{\psi_L}\).

Therefore, \(\mathcal{V}_{\psi_L}\) is a regular language whose syntactic morphism is quasi-aperiodic. ◻

Proof. We already know that for all \(r \in R_L\) and \(e \in O_L\), the languages \(\mathcal{E}_{\varphi_L, r}\) and \(\mathcal{E}_{\psi_L, e}\) are regular. To prove the lemma, we then just have to prove that

• if there exists \(r \in R_L\) such that the syntactic morphism of \(\mathcal{E}_{\varphi_L, r}\) is not quasi-aperiodic, then there exists \(k \in \mathbb{N}\) such that \(\varphi(\Sigma^\triangle \cap \Sigma^k)\) contains a semigroup that is not aperiodic;

• if there exists \(e \in O_L\) such that the syntactic morphism of \(\mathcal{E}_{\psi_L, e}\) is not quasi-aperiodic and for each \(\varphi_L(L)\)-reaching idempotent \(f \in O_L\) such that there exist \(f', f'' \in O_L\) satisfying \(e = f' \circ f \circ f''\) we have that \(\mathcal{R}_f = \{(u,v) \in \Sigma^* \times \Sigma^* \mid uv\in\Sigma^\triangle, \Delta(u)>0, \psi_L(\mathop{\mathrm{ext}}_{u,v})=f\}\) is length-synchronous, then there exist \(k, l \in \mathbb{N}\) such that \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k, l})\) contains a semigroup that is not aperiodic.

Indeed, the first point allows to conclude that \((\varphi_L, \psi_L)\) is not quasi-aperiodic, since if there exists a non-aperiodic semigroup \(S\) contained in \(\varphi_L(\Sigma^\triangle \cap \Sigma^k)\), then \(\{\mathrm{left}_{s} \mid s \in S\}\) is a semigroup contained in \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k, 0})\) (because for each \(s \in S\), there exists \(w \in \Sigma^\triangle \cap \Sigma^k\) satisfying \(\varphi_L(w) = s\), so that \(\psi_L(\mathop{\mathrm{ext}}_{w, \varepsilon}) = \mathrm{left}_{\varphi_L(w)} = \mathrm{left}_{s}\)). But this semigroup is non-aperiodic as well, since as \(S\) is non-aperiodic, it must be that for all \(i \in \mathbb{N}_{>0}\), there exists \(s \in S\) such that \(s^i \neq s^{i + 1}\), so that \({\mathrm{left}_{s}}^i \neq {\mathrm{left}_{s}}^{i + 1}\).

We only prove the second point, the first point can be proved in a similar way by leaving out the last paragraph of the following proof, that is the sole place where we need, given an \(e \in O_L\), length-synchronicity of \(\mathcal{R}_f\) for each \(\varphi_L(L)\)-reaching idempotent \(f \in O_L\) such that there exist \(f', f'' \in O_L\) satisfying \(e = f' \circ f \circ f''\).

Take \(t \in \mathbb{N}\) and \(p \in \mathbb{N}_{>0}\) given by Lemma [lem:Finite95Ext-algebra95morphisms95stability] such that \(\psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{i, *}_\uparrow\bigr) = \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{j, *}_\uparrow\bigr)\) for all \(i, j \in \mathbb{N}\) satisfying \(i, j \geq t\) and \(i \equiv j \pmod{p}\).

Assume there exists \(e \in O_L\) such that the syntactic morphism of \(\mathcal{E}_{\psi_L, e}\) is not quasi-aperiodic. Take \(M\) to be the syntactic monoid of \(\mathcal{E}_{\psi_L, e}\) and \(h\colon \Gamma_{\psi_L}^* \to M\) to be its syntactic morphism. Let \(s \in \mathbb{N}_{>0}\) be the stability index of \(h\) and let \(\omega \geq 2\) be a multiple both of the idempotent power of \(M\) and the idempotent power of \(O_L\). Non-quasi-aperiodicity of \(h\) implies that there exists \(g \in h(\Gamma_{\psi_L}^s)\) satisfying \(g^\omega \neq g^{\omega + 1}\).

By definition of the stability index, there exists \(w \in \Gamma_{\psi_L}^{q \cdot s}\) for \(q \in \mathbb{N}_{>0}\) such that \(q \cdot s \geq t\) and \(q \cdot s \equiv 0 \pmod{p}\) satisfying \(h(w) = g\). Since \(t \leq q \cdot s \leq q \cdot s \cdot \omega \leq q \cdot s \cdot (\omega + 1)\) and \(q \cdot s \equiv q \cdot s \cdot \omega \equiv q \cdot s \cdot (\omega + 1) \pmod{p}\), we cannot have \(w = \$^{q \cdot s}\), for otherwise we would have \(g^\omega = h(\$^{q \cdot s \cdot \omega}) = h(\$^{q \cdot s \cdot (\omega + 1)}) = g^{\omega + 1}\) because \(\psi_L\bigl( \mathcal{O}(\Sigma^\triangle)^{q \cdot s \cdot \omega + k + 1, *}_\uparrow \bigr) = \psi_L\bigl( \mathcal{O}(\Sigma^\triangle)^{q \cdot s \cdot (\omega + 1) + k + 1, *}_\uparrow \bigr)\) for all \(k \in \mathbb{N}\). Therefore, we have \(w = \$^{k_1} f_1 \cdots \$^{k_n} f_n \$^{k_{n + 1}}\) for \(n \in \mathbb{N}_{>0}\), \(k_1, \ldots, k_{n + 1} \in \mathbb{N}\) and \(f_1, \ldots, f_n \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)_\uparrow\bigr)\). Since \(g^\omega \neq g^{\omega + 1}\), there exist \(x, y \in \Gamma_{\psi_L}^*\) such that either \(x w^\omega y \in \mathcal{E}_{\psi_L, e}\) and \(x w^{\omega + 1} y \notin \mathcal{E}_{\psi_L, e}\), or \(x w^\omega y \notin \mathcal{E}_{\psi_L, e}\) and \(x w^{\omega + 1} y \in \mathcal{E}_{\psi_L, e}\). Assume the first case holds. Then we have \(x = x' \$^{k_x}\) and \(y = \$^{k_y} y'\) with \(k_x, k_y \in \mathbb{N}\) and \(x', y' \in \Gamma_{\psi_L}^*\) satisfying \(x', \$^{k_x + k_1} f_1, \$^{k_2} f_2, \ldots, \$^{k_n} f_n, \$^{k_{n + 1} + k_1} f_1, \$^{k_{n + 1} + k_y} y' \in \mathcal{V}_{\psi_L}\) and \(\mathop{\mathrm{eval}}_{\psi_L}(x')\circ (f_1 \circ \cdots \circ f_n)^\omega \circ \mathop{\mathrm{eval}}_{\psi_L}(y') = e\). Therefore, we also have \(x w^{\omega + 1} y \in \mathcal{V}_{\psi_L}\), hence since \(x w^{\omega + 1} y \notin \mathcal{E}_{\psi_L, e}\) we necessarily have \[\begin{align} e & = \mathop{\mathrm{eval}}_{\psi_L}(x') \circ (f_1 \circ \cdots \circ f_n)^\omega \circ \mathop{\mathrm{eval}}_{\psi_L}(y')\\ & \neq \mathop{\mathrm{eval}}_{\psi_L}(x w^{\omega + 1} y) = \mathop{\mathrm{eval}}_{\psi_L}(x') \circ (f_1 \circ \cdots \circ f_n)^{\omega + 1} \circ \mathop{\mathrm{eval}}_{\psi_L}(y') \,\,\text{.} \end{align}\] Thus we have \((f_1 \circ \cdots \circ f_n)^\omega \neq (f_1 \circ \cdots \circ f_n)^{\omega + 1}\) and \(\$^{k_{n + 1} + k_1} f_1 \$^{k_2} f_2 \cdots \$^{k_n} f_n \in \mathcal{V}_{\psi_L}\). This is also true for the case when \(x w^\omega y \notin \mathcal{E}_{\psi_L, e}\) and \(x w^{\omega + 1} y \in \mathcal{E}_{\psi_L, e}\).

Therefore, we have \((f_1 \circ \cdots \circ f_n)^\omega \neq (f_1 \circ \cdots \circ f_n)^{\omega + 1}\) with \[(f_1 \circ \cdots \circ f_n)^i \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{q \cdot s \cdot i, *}_\uparrow\bigr) = \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{q \cdot s, *}_\uparrow\bigr)\] for each \(i \in \mathbb{N}_{>0}\) because \(k_{n + 1} + k_1 + \cdots + k_n + n = q \cdot s \geq t\) and \(k_{n + 1} + k_1 + \cdots + k_n + n = q \cdot s \equiv 0 \pmod{p}\). But given \(\omega'\) the idempotent power of \(\{(f_1 \circ \cdots \circ f_n)^i \mid i \in \mathbb{N}_{>0}\}\), we have that \((f_1 \circ \cdots \circ f_n)^\omega = (f_1 \circ \cdots \circ f_n)^{\omega \omega'} = (f_1 \circ \cdots \circ f_n)^{\omega'}\), so that \((f_1 \circ \cdots \circ f_n)^{\omega'} \neq (f_1 \circ \cdots \circ f_n)^{\omega' + 1}\), hence \(\{(f_1 \circ \cdots \circ f_n)^i \mid i \in \mathbb{N}_{>0}\}\) is not aperiodic.

Assume additionally that for each \(\varphi_L(L)\)-reaching idempotent \(f \in O_L\) such that there exist \(f', f'' \in O_L\) satisfying \(e = f' \circ f \circ f''\) we have that \(\mathcal{R}_f = \{(u,v) \in \Sigma^* \times \Sigma^* \mid uv\in\Sigma^\triangle, \Delta(u)>0, \psi_L(\mathop{\mathrm{ext}}_{u,v})=f\}\) is length-synchronous. For each \(i \in \mathbb{N}_{>0}\), let \(\mathop{\mathrm{ext}}_{u_i, v_i} \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)^{q \cdot s, *}_\uparrow\bigr)\) such that \(\psi_L(\mathop{\mathrm{ext}}_{u_i, v_i}) = (f_1 \circ \cdots \circ f_n)^i\). If \((f_1 \circ \cdots \circ f_n)^\omega\) were not \(\varphi_L(L)\)-reaching, then it would imply that \(\mathop{\mathrm{ext}}_{u_\omega, v_\omega}\) is not \(L\)-reaching. This would in turn entail that for all \(z \in \Sigma^\triangle\) and \(\mathop{\mathrm{ext}}_{\alpha, \beta} \in \mathcal{O}(\Sigma^\triangle)\) we have \[\mathop{\mathrm{ext}}_{\alpha, \beta}(\mathop{\mathrm{ext}}_{u_\omega, v_\omega}(z)) \notin L \wedge \mathop{\mathrm{ext}}_{\alpha, \beta}(\mathop{\mathrm{ext}}_{u_1 u_\omega, v_\omega v_1}(z)) = \mathop{\mathrm{ext}}_{\alpha u_1, v_1 \beta}(\mathop{\mathrm{ext}}_{u_\omega, v_\omega}(z)) \notin L \,\,\text{,}\] so that it would follow that \[(f_1 \circ \cdots \circ f_n)^\omega = \psi_L(\mathop{\mathrm{ext}}_{u_\omega, v_\omega}) = \psi_L(\mathop{\mathrm{ext}}_{u_1 u_\omega, v_\omega v_1}) = (f_1 \circ \cdots \circ f_n)^{\omega + 1}\,\,\text{,}\] a contradiction. Hence, since \((f_1 \circ \cdots \circ f_n)^\omega\) is a \(\varphi_L(L)\)-reaching idempotent and \[e = \begin{cases} \mathop{\mathrm{eval}}_{\psi_L}(x') \circ (f_1 \circ \cdots \circ f_n)^\omega \circ \mathop{\mathrm{eval}}_{\psi_L}(y') & \text{if x w^\omega y \in \mathcal{E}_{\psi_L, e} and x w^{\omega + 1} y \notin \mathcal{E}_{\psi_L, e}}\\ \mathop{\mathrm{eval}}_{\psi_L}(x') \circ (f_1 \circ \cdots \circ f_n)^{\omega + 1} \circ \mathop{\mathrm{eval}}_{\psi_L}(y') & \text{o/w (x w^\omega y \notin \mathcal{E}_{\psi_L, e} and x w^{\omega + 1} y \in \mathcal{E}_{\psi_L, e})} \end{cases} \!\text{,}\] it follows that \(\mathcal{R}_{(f_1 \circ \cdots \circ f_n)^\omega}\) is length-synchronous. So for all \(i \in \mathbb{N}, i \geq 2\), since \(\psi_L(\mathop{\mathrm{ext}}_{u_1^\omega, v_1^\omega}) = \psi_L(\mathop{\mathrm{ext}}_{u_i^\omega, v_i^\omega}) = (f_1 \circ \cdots \circ f_n)^\omega\) with \(\Delta(u_1^\omega) > 0\) and \(\Delta(u_i^\omega) > 0\), since \(\mathopen{}\left|u_1\right|\mathclose{} = \mathopen{}\left|u_i\right|\mathclose{}\), we have \[\frac{\mathopen{}\left|u_1^\omega\right|\mathclose{}}{\mathopen{}\left|v_1^\omega\right|\mathclose{}} = \frac{\mathopen{}\left|u_i^\omega\right|\mathclose{}}{\mathopen{}\left|v_i^\omega\right|\mathclose{}} \Rightarrow \frac{\mathopen{}\left|u_1\right|\mathclose{}}{\mathopen{}\left|v_1\right|\mathclose{}} = \frac{\mathopen{}\left|u_i\right|\mathclose{}}{\mathopen{}\left|v_i\right|\mathclose{}} \Rightarrow \mathopen{}\left|v_1\right|\mathclose{} = \mathopen{}\left|v_i\right|\mathclose{} \,\,\text{.}\] To conclude, we obtain that the non-aperiodic semigroup \(\{(f_1 \circ \cdots \circ f_n)^i \mid i \in \mathbb{N}_{>0}\}\) is contained in \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{q \cdot s, \mathopen{}\left|v_1\right|\mathclose{}})\). ◻

Proof of Proposition [ptn:Approximate95matching95length-sync].. By assumption \((\varphi_L, \psi_L)\) is \(\varphi_L(L)\)-length-synchronous. Thus, the set of contexts \(\mathcal{U}_e\) is length-synchronous for all \(\varphi_L(L)\)-reaching \(e\in O_L\) by Proposition [prop32length32synchronous]. Moreover, there exists \(d_L \in \mathbb{N}\) bounding the nesting depth of the words in \(L\) Proposition [ptn:Bounded95nesting-depth]. For defining our desired formula \(\mu\), we will construct \(\ifthenelse{\equal{\Sigma}{\null}} { \mathsf{FO}[\mathsf{+}] } { \mathsf{FO}_{\Sigma}[\mathsf{+}] }\) formulas \(\mu_d\) and \(\mu_d^\uparrow\) for all \(0\leq d\leq d_L\) with the following properties: for all \(w \in \Sigma^+\) and for all \(i, j \in [1, \mathopen{}\left|w\right|\mathclose{}]\), we have

We therefore define \(\mu=\mu_{d_L}\). The construction of \(\mu_d^\uparrow\) and \(\mu_d\) is by induction on \(d\). We set \[\mu_0(i,j)=\bot \text{ and } \mu_0(i,j)=\forall z \bigl(x \leq z \leq y \rightarrow \Sigma_\text{int}(z)\bigr).\] Let us assume \(d>0\). The formula \(\mu_d\) is easily defined assuming \(\mu_d^\uparrow\). We define \[\begin{align} \mu_d(x,y)&\!\!=\!\!&\forall z\biggl[x\leq z\leq y\rightarrow\\ &&\quad\Bigl(\Sigma_\text{int}(z)\vee\exists z'\bigl( \begin{aligned}[t] & (\Sigma_\text{call}(z)\wedge\Sigma_\text{ret}(z')\wedge \mu_d^\uparrow(z,z'))\vee\\ & (\Sigma_\text{call}(z')\wedge\Sigma_\text{ret}(z)\wedge \mu_d^\uparrow(z',z)) \bigr)\Bigr)\biggl] \,\,\text{.} \end{aligned} \end{align}\] It remains to define \(\mu_d^\uparrow\). Let us assume \(u=w_i\dots w_j\in\Sigma^\triangle\), that \(i\) is matched to \(j\) in \(w\) and that \(\mathop{\mathrm{nd}}(u)=d>0\). Hence, \(u=a_1vb_1\in\Sigma^\triangle\) for some \(a_1\in\Sigma_\text{call}\), \(b_1\in\Sigma_\text{ret}\), and \(v\in\Sigma^\triangle\). We then apply Lemma [L32nesting32induction] which states that \(u\) has a nesting-maximal stair factorization \(u=\mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ\dots \mathop{\mathrm{ext}}_{x_{k},y_{k}}\circ\mathop{\mathrm{ext}}_{a_{k},b_{k}}(u')\) such that for some \(h\in[1,k]\), setting \(u_\ell=\mathop{\mathrm{ext}}_{a_\ell,b_\ell}\circ\mathop{\mathrm{ext}}_{x_{\ell+1},y_{\ell+1}} \circ\cdots\circ\; \mathop{\mathrm{ext}}_{a_k,b_k}(u')\) for all \(\ell \in [1, k]\) and \(u_{k + 1} = u'\), we have

1. \(\mathop{\mathrm{nd}}(u)=\mathop{\mathrm{nd}}(u_h)=d\),

2. \(\mathop{\mathrm{nd}}(u_{h+1})=d-1\), and

3. \(\mathop{\mathrm{nd}}(x_1),\mathop{\mathrm{nd}}(y_1),\dots,\mathop{\mathrm{nd}}(x_h),\mathop{\mathrm{nd}}(y_h)<d\).

We remark that \(x_1=y_1=\varepsilon\). Let \(i=i_1<\dots<i_h\) and \(j_h<\dots<j_1=j\) be the positions that correspond to the positions of the letters \(a_1,\dots,a_h\in\Sigma_\text{call}\) and \(b_1,\dots, b_h\in\Sigma_\text{ret}\) of \(u\) in \(w\), respectively: more precisely \(i_\ell=i+\mathopen{}\left|x_1\cdots a_{\ell-1}x_\ell\right|\mathclose{}\) and \(j_\ell=\mathopen{}\left|x_1a_1\cdots x_ka_ku'b_ky_k\cdots b_{\ell+1}y_{\ell+1}\right|\mathclose{}+1\) for all \(\ell\in[1,h]\). The formula \(\mu_{d}^\uparrow\) could guess the positions \(i=i_1<\dots<i_h\) and \(j_h<\dots<j_1=j\) and verify the following (recalling that \(x_1=y_1=\varepsilon\)):

(a) the infix \(w_{i_h+1}\cdots w_{j_h-1}=\mathop{\mathrm{ext}}_{x_{h+1},y_{h+1}}(u_{h+1})\) is well-matched, and

(b) the word \(w_{i_1}\cdots w_{i_{h}} w_{j_h}\cdots w_{j_1}\) is well-matched.

Point (a) can be realized via the formula \(\mu_{d-1}\) by making use of Point 2 from above, whereas Point (b) can be realized by the following ad-hoc formula, this time making use of Point 3 and from above: \[\kappa_h(x,x',y',y)=\exists x_1\cdots x_h\exists y_1\cdots y_h \biggl( \begin{align}[t] & x=x_1\wedge x'=x_h\wedge y'=y_h\wedge y=y_h\wedge\\ & \bigwedge_{t=1}^h \bigl(\Sigma_\text{call}(x_t)\wedge \Sigma_\text{ret}(y_t)\bigr)\wedge\\ & \bigwedge_{t=1}^{h-1} \bigl(\mu_{d-1}(x_t+1,x_{t+1}-1)\wedge \mu_{d-1}(y_{t+1}+1,y_t-1)\bigr) \biggr) \text{.} \end{align}\]

The problem with this approach is that the size of the formula depends on the size of \(w\). For instance, for \(a\in\Sigma_\text{call}\), \(b\in\Sigma_\text{ret}\), \(c\in\Sigma_\text{int}\), and \(u=a^ncb^n\) we have \(\mathop{\mathrm{nd}}(u)=\mathop{\mathrm{nd}}(acb)=1\) for all \(n\geq 1\). Hence we would have \(h=n-1\), so \(h\) would depend on \(u\) which is problematic. Therefore, towards expressing Point (b) by a formula whose size only depends on \(|O_L|\), let us define, for all \(\ell,\ell'\in[1,h]\), the product \[e_{\ell,\ell'}=\psi_L(\mathop{\mathrm{ext}}_{x_\ell,y_\ell}\circ \mathop{\mathrm{ext}}_{a_{\ell},b_{\ell}}\cdots\mathop{\mathrm{ext}}_{x_{\ell'},y_{\ell'}} \circ\mathop{\mathrm{ext}}_{a_{\ell'},b_{\ell'}})\quad\text{and}\quad e_\ell=e_{1,\ell}.\] We remark that all \(e_{\ell,\ell'}\) are \(\varphi_L(L)\)-reaching since \(w\) is assumed to be in \(L\). We say an interval \(I=[s,t]\subseteq[1,h]\) is repetitive if \(s<t\) and \(e_s=e_t\).

Proof of the Claim. For all \(z\in[1,h]\) let \(\lambda(z)=\max\{\ell\in[1,h]\mid e_\ell=e_z\}\). Observe \(\lambda(z)\geq z\) for all \(z\in[1,h]\) and that \(|\lambda([1,h])|\leq|O_L|\). We define \(t_0=1\). Let \(p>0\) and assume that we have already defined \(t_{p-1}\). In case \(t_{p-1}=h\) we are done and define \(q=p-1\) and \(s_{q+1}=h\). So let us assume \(t_{p-1}<h\). In case there exists \(z\in[t_{p-1},h]\) such that \(z<\lambda(z)\) we define \(s_p=\min\{z\in[t_{p-1},h]\mid z<\lambda(z)\}\) and \(t_p=\lambda(s_p)\), otherwise (i.e.in case \(z=\lambda(z)\) for all \(z\in[t_{p-1},h]\)) we are done and define \(q=p-1\) and \(s_{q+1}=h\). Immediately by definition we have \(1=t_0\leq s_1<t_1<s_2<t_2<\dots<s_q<t_q\leq s_{q+1}=h\) (because if we had \(t_{p-1} = s_p\) for a \(p \in [2, q]\), we would have \(e_{s_{p-1}} = e_{t_{p-1}} = e_{s_p}\), so \(\lambda(s_p) = \lambda(s_{p-1}) = t_{p-1} = s_p < \lambda(s_p)\), a contradiction) and \(e_{s_p}=e_{t_p}\) for all \(p \in [1, q]\). Moreover, the intervals \([s_1,t_1],\dots,[s_q,t_q]\) are indeed all repetitive. Since moreover \(t_p\in\lambda([1,h])\) for all \(p\in[1,q]\) and \(|\lambda([1,h])|\leq|O_L|\) we must have \(q\leq|O_L|\). Now let \(D_0=[t_0,s_1],D_1=[t_1,s_2],\dots,D_q=[t_q,s_{q+1}]\). Clearly, these sets are pairwise disjoint. Moreover, by construction, the only elements \(z \in \bigcup_{p = 0}^q D_p\) such that \(z < \lambda(z)\) are those in \(X=\{s_1, \ldots, s_q\}\), so that all elements \(z \in (\bigcup_{p = 0}^q D_p) \setminus X\) satisfy \(z=\lambda(z)\), i.e.are elements from \(\lambda([1,h])\). Thus, we obtain \(q+\sum_{p=0}^{q}\left|D_p\right| = q + \left|\bigcup_{p=0}^q D_p\right| \leq \left|O_L\right|+\left|X\right|+\left|\lambda([1,h])\right|=3\left|O_L\right|\). 0◻

Let \(1=t_0\leq s_1<t_1<s_2<t_2<\cdots< s_q<t_q\leq s_{q+1}=h\) be the indices satisfying Claim [claim32pigeon] along with \(D_0=[t_0,s_1],D_1=[t_1,s_2],\dots,D_q=[t_q,s_{q+1}]\). Let \(d_p=|D_p|\) for all \(p\in[0,q]\). Since, for all \(p\in[1,q]\), the non-empty interval \([s_p,t_p]\) is repetitive, we have \(e_{s_p}=e_{t_p}\) and thus obtain \[e_{s_p}=e_{t_p}= e_{s_p}\circ \psi_L(\mathop{\mathrm{ext}}_{x_{s_p+1}\cdots a_{t_p},b_{t_p}\cdots y_{s_p+1}}).\] Hence, we have \(w\models\pi_{e_{s_p}}(i_{s_p}+1,i_{t_p},j_{t_p},j_{s_p}-1)\) where \(\pi_{e_{s_p}}\) is the formula given by Lemma [lem:Synchronous95element95matching] (recall that \(e_{s_p}\) is \(\varphi_L(L)\)-reaching and that \(\mathcal{U}_{e_{s_p}}\) is length-synchronous). We can therefore use the formula \(\pi_{e_{s_p}}\) to witness that \(w_{i_{s_p}+1}\cdots w_{i_{t_p}}w_{j_{t_p}}\cdots w_{j_{s_p}-1}\) is indeed a well-matched word. It will thus remain to verify that \(w_{i_{t_p}}\cdots w_{i_{s_{p+1}}}w_{j_{s_{p+1}}}\cdots w_{i_{t_p}}\) is well-matched for all \(p\in[0,q]\): this can be guaranteed by evaluating \(\kappa_{d_p}(i_{t_p},i_{s_{p+1}},j_{s_{p+1}},i_{t_p})\). We can now define our final formula \(\mu_d^\uparrow\): \[\begin{align} \mu_d^\uparrow(x,y) = & \bigvee_{\substack{q\in[0,|O_L|]\\ d_0,\dots,d_q\geq 1:\\ q+d_0+\dots+d_q\leq 3|0|}}\exists x_1\dots x_{q+1}\exists x_0'\dots x_q' \exists y_1\dots y_{q+1}\exists y_1'\dots y_0'\\ & \biggl[ \begin{aligned}[t] & x_0\leq x_1<x_1'<x_2<\dots<x_q'<y_q'<y_q<\dots<y_1'<y_1\leq y_0'\wedge \\ & x_0'=x\wedge y_0'=y\wedge \mu_{d-1}(x_{q+1}+1,y_{q+1}-1)\wedge\\ & \bigwedge_{p=1}^q\left(\bigvee_{e\in O_L \text{ \varphi_L(L)-reaching}} \pi_e(x_p+1,x_p',y_p',y_p-1)\right) \wedge\\ & \bigwedge_{p=0}^{q} \kappa_{d_p}(x_p',x_{p+1},y_{p+1},y_p') \biggr] \,\,\text{.} & \qedhere \end{aligned} \end{align}\] ◻

Proof. By hypothesis, there exists \(d_L \in \mathbb{N}\) bounding the nesting depth of the words in \(L\).

By hypothesis also, for each \(\varphi_L(L)\)-reaching \(r \in R_L\), the language \(\mathcal{E}_{\varphi_L, r}\) is regular and its syntactic morphism is quasi-aperiodic. This implies, by [2], that for each \(\varphi_L(L)\)-reaching \(r \in R_L\), there exists an \(\mathsf{FO}_{\Gamma_{\varphi_L}}[<, \mathsf{MOD}]\)-sentence \(\nu_{\varphi_L, r}\) defining \(\mathcal{E}_{\varphi_L, r}\).

Finally, by hypothesis, for each \(\varphi_L(L)\)-reaching \(e \in O_L\), the language \(\mathcal{E}_{\psi_L, e}\) is regular and its syntactic morphism is quasi-aperiodic. Again, by [2], for each \(\varphi_L(L)\)-reaching \(e \in O_L\), there exists an \(\mathsf{FO}_{\Gamma_{\psi_L}}[<, \mathsf{MOD}]\)-sentence \(\nu_{\psi_L, e}\) defining \(\mathcal{E}_{\psi_L, e}\).

5.3.5.0.1 Auxiliary formulas.

We introduce a few auxiliary formulas that all assume access to the full matching relation \(M^\triangle(w)\), represented by the relational symbol \(\leftrightsquigarrow\).

First let us define a formula \(A\) such that for all \(w \in \Sigma^\triangle\) and \(i, j, k \in [1, \mathopen{}\left|w\right|\mathclose{}]\) satisfying \(w_i \cdots w_j \in \Sigma^\triangle\), we have that \((w, M^\triangle\left(w\right)) \models A(i, j, k)\) if, and only if, \(i \leq k < j\) and \(\Delta(w_i \cdots w_k) > 0\). We let \[A(x, y, z) = \exists x' \exists y' (x \leq x' \leq z < y' \leq y \wedge x' \leftrightsquigarrow y') \,\,\text{.}\]

Next, we define a formula \(U\) such that for all \(w \in \Sigma^\triangle\) and \(i, i', k \in [1, \mathopen{}\left|w\right|\mathclose{}]\), we have that \((w, M^\triangle\left(w\right)) \models U(i, i', k)\) if, and only if, \(i \leq k \leq i'\) and \(k\) is matched to some position larger than \(i'\) in \(w\). We let \[U(x, x', z) = x \leq z \leq x' \wedge \exists t (z \leftrightsquigarrow t \wedge x' < t) \,\,\text{.}\]

The last formulas we introduce are \(N_d\) which express that the infix \(w_i\cdots w_j\in\Sigma^\triangle\) of \(w\in\Sigma^\triangle\) has nesting depth at least \(d\geq 0\). More precisely, for all \(d \in \mathbb{N}\), we introduce auxiliary formulas \(N_d\) such that for all \(w \in \Sigma^\triangle\) and \(i, j \in [1, \mathopen{}\left|w\right|\mathclose{}]\) satisfying \(w_i \cdots w_j \in \Sigma^\triangle\), we have that \((w, M^\triangle\left(w\right)) \models N_d(i, j)\) if, and only if, \(\mathop{\mathrm{nd}}(w_i \cdots w_j) \geq d\). The case \(d=0\) is trivial since we can set \(N_0(i,j) = \top\).

Take \(w \in \Sigma^\triangle\) such that \(\mathop{\mathrm{nd}}(w) = d' \geq 1\). Note that then \(w\) can be factorized as \(w=w_1uw_2\) such that \(w_1, w_2 \in \Sigma^\triangle\), \(u\in\Sigma_\text{call}\Sigma^\triangle\Sigma_\text{ret}\) and \(\mathop{\mathrm{nd}}(w)=\mathop{\mathrm{nd}}(u) = d'\). This means that \(u=a_1vb_1\) for \(a_1\in\Sigma_\text{call}\), \(b_1\in\Sigma_\text{ret}\) and \(v\in\Sigma^\triangle\). We then apply Lemma [lem:Maximal95stair95factorization] and Lemma [L32nesting32induction] implying that \(u\) has a nesting-maximal stair factorization \[u = \mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_k,y_k} \circ \mathop{\mathrm{ext}}_{a_k,b_k}(u')\] for which there exists \(h\in[1,k]\) such that, setting \(u_i=\mathop{\mathrm{ext}}_{a_i,b_i}\circ\mathop{\mathrm{ext}}_{x_{i+1},y_{i+1}} \circ\cdots\circ\; \mathop{\mathrm{ext}}_{a_k,b_k}(u')\) for all \(i \in [1, k]\) and \(u_{k + 1} = u'\), we have \(\mathop{\mathrm{nd}}(u)=\mathop{\mathrm{nd}}(u_h) = d'\) and \[\mathop{\mathrm{nd}}(\mathop{\mathrm{ext}}_{x_{h+1},y_{h+1}} \circ \mathop{\mathrm{ext}}_{a_{h+1}, b_{h+1}} \circ \cdots \circ \mathop{\mathrm{ext}}_{a_k,b_k}(u')) = \mathop{\mathrm{nd}}(u_{h+1}) = d'-1\,\,\text{.}\] Thus, by definition of the nesting depth of a well-matched word, \(u_h=a_hz_1z_2b_h\) for \(z_1,z_2\in\Sigma^\triangle\) satisfying \(\mathop{\mathrm{nd}}(z_1) = \mathop{\mathrm{nd}}(z_2) = d'-1\).

Hence, we set \[N_1(x, y) = \exists x' \exists y' (x \leq x' < y' \leq y \wedge x' \leftrightsquigarrow y')\] and for \(d\geq 2\) we set \[N_d(x, y) = \exists x' \exists y' \exists z \bigl( \begin{align}[t] & x \leq x' < z < y' \leq y \wedge x' \leftrightsquigarrow y' \wedge \neg A(x'+1, y'-1, z) \wedge\\ & N_{d - 1}(x'+1, z) \wedge N_{d - 1}(z+1, y'-1) \bigr) \,\,\text{.} \end{align}\]

Main construction.

To build the \(\ifthenelse{\equal{\Sigma, \leftrightsquigarrow}{\null}} { \mathsf{FO}[\mathsf{+}] } { \mathsf{FO}_{\Sigma, \leftrightsquigarrow}[\mathsf{+}] }\)-sentence \(\eta\), we build \(\ifthenelse{\equal{\Sigma, \leftrightsquigarrow}{\null}} { \mathsf{FO}[\mathsf{+}] } { \mathsf{FO}_{\Sigma, \leftrightsquigarrow}[\mathsf{+}] }\)-formulas

• \(\eta_{d, r}^\uparrow(x, y)\) for all \(d \in \mathbb{N}\) and all \(\varphi_L(L)\)-reaching \(r \in R_L\) and

• \(\eta_{d, r}(x, y)\) for all \(d\in\mathbb{N}\) and all \(\varphi_L(L)\)-reaching \(r\in R_L\)

that also assume access to the full matching relation \(M^\Delta(w)\). They will have the following properties for all \(w\in\Sigma^\triangle\) and all \(i,j\in[1,\mathopen{}\left|w\right|\mathclose{}]\):

• if \(i\) is matched to \(j\) in \(w\), then \((w, M^\triangle\left(w\right)) \models \eta_{d, r}^\uparrow(i, j)\) if, and only if, \(\mathop{\mathrm{nd}}(w_i \cdots w_j) \leq d\) and \(\varphi_L(w_i \cdots w_j) = r\) and

• if \(w_i \cdots w_j \in \Sigma^\triangle\), then \((w, M^\triangle\left(w\right)) \models \eta_{d, r}(i, j)\) if, and only if, \(\mathop{\mathrm{nd}}(w_i \cdots w_j) \leq d\) and \(\varphi_L(w_i \cdots w_j) = r\).

Let the formula \(E\) be defined as \(\forall x (x \neq x)\) if \(\varepsilon\in L\) and \(\bot=\exists x (x\neq x)\) otherwise. Observe that \(w\models \forall x (x \neq x)\) if, and only if, \(w=\varepsilon\). Our final formula \(\eta\) will then be defined as \[\begin{align} \eta = & \forall z \exists t \bigl( (\Sigma_\text{call}(z) \rightarrow z \leftrightsquigarrow t) \wedge (\Sigma_\text{ret}(z) \rightarrow t \leftrightsquigarrow z) \bigr) \wedge\\ & \Bigl( E \vee \exists x \exists y \bigl( \neg \exists x' (x' < x) \wedge \neg \exists y' (y < y') \wedge \bigvee_{r \in \varphi_L(L)} \eta_{d_L, r}(x, y) \bigr) \Bigr). \end{align}\]

It now remains to build \(\eta_{d, r}^\uparrow(x, y)\) and \(\eta_{d, r}(x, y)\) for all \(d \in \mathbb{N}\) and \(\varphi_L(L)\)-reaching \(r \in R_L\). The construction is by induction on \(d\). Let \(r \in R_L\) that is \(\varphi_L(L)\)-reaching. We define \(\eta_{0,r}^\uparrow(x,y)=\bot\). We define \(\eta_{0,r}\) as \[\eta_{0,r}(x,y) = \neg N_1(x,y) \wedge \tau_0(\nu_{\varphi_L,r}) \,\,\text{,}\] where the translation \(\tau_0\) is inductively defined as follows:

• \(\tau_0(z<z')=z<z'\);

• \(\tau_0(s(z))= \bigvee_{c \in \varphi_L^{-1}(s) \cap \Sigma_\text{int}} c(z)\) for all \(s \in \varphi_L(\Sigma^\triangle \setminus \{\varepsilon\})\);

• \(\tau_0(\mathsf{MOD}_m(z))= \exists t \bigl((z = x \rightarrow 1 = t \cdot m) \wedge (z \neq x \rightarrow z - x + 1 = t \cdot m)\bigr)\) for all \(m \in \mathbb{N}_{>0}\);

• \(\tau_0(\$(z))=\bot\);

• \(\tau_0(\rho_1(\boldsymbol{z}_1) \wedge \rho_2(\boldsymbol{z}_2))= \tau_0(\rho_1(\boldsymbol{z}_1))\wedge \tau_0(\rho_1(\boldsymbol{z}_2))\);

• \(\tau_0(\neg\rho(\boldsymbol{z}))=\neg\tau_0(\rho(\boldsymbol{z}))\);

• \(\tau_0(\exists z \rho(z,\boldsymbol{z}))= \exists z \bigl(x \leq z \leq y \wedge \tau_0(\rho(z,\boldsymbol{z}))\bigr)\).

Now let \(d>0\). Let us first define \(\eta_{d,r}\) when assuming that we have already defined \(\eta_{d,r}^\uparrow\). Given \(w\in\Sigma^\triangle \setminus \{\varepsilon\}\) and \(i,j\in[1,\mathopen{}\left|w\right|\mathclose{}]\) such that \(w_i \cdots w_j \in \Sigma^\triangle \setminus \{\varepsilon\}\), note that in case \(\mathop{\mathrm{nd}}(w_i \cdots w_j)\leq d\), then one can factorize \(w_i \cdots w_j\) as \(w_i \cdots w_j = u_1 \cdots u_m\) such that \(u_\ell\in\Sigma_\text{int}\cup \Sigma_\text{call}\Sigma^\triangle\Sigma_\text{ret}\) and \(\mathop{\mathrm{nd}}(u_\ell)\leq d\) for all \(\ell\in[1,m]\). Note also that if \(\varphi_L(w_i \cdots w_j) = r\), as \(r\) is \(\varphi_L(L)\)-reaching, then \(\varphi_L(u_\ell)\) is \(\varphi_L(L)\)-reaching for all \(\ell \in [1, m]\). Using these observations we define \[\eta_{d,r}(x,y) = \neg N_{d+1}(x,y) \wedge \forall z \Bigl( x \leq z \leq y \rightarrow \bigl( \tau_1(\$(z)) \vee \bigvee_{\substack{s \in \varphi_L(\Sigma^\triangle \setminus \{\varepsilon\})\\ \text{\varphi_L(L)-reaching}}} \tau_1(s(z)) \bigl) \Bigr) \wedge \tau_1(\nu_{\varphi_L,r}) \,\,\text{,}\] where the translation \(\tau_1\) agrees with the above translation \(\tau_0\) (where, as expected, occurrences of \(\tau_0\) are replaced by \(\tau_1\)) except for the following kinds of subformulas:

• \(\tau_1(\$(z))=A(x,y,z)\);

• \(\tau_1(s(z)) = \neg A(x, y, z) \wedge \Bigl(\bigvee_{c \in \varphi_L^{-1}(s) \cap \Sigma_\text{int}} c(z) \vee \exists t \bigl(x \leq t \leq y \wedge t \leftrightsquigarrow z \wedge \eta_{d, s}^\uparrow(t, z)\bigr) \Bigr)\) if \(s\) is \(\varphi_L(L)\)-reaching, \(\tau_1(s(z)) = \bot\) otherwise.

It remains to define \(\eta_{d,r}^\uparrow\).

We first construct for all \(\varphi_L(L)\)-reaching \(e\in O_L\) a formula \(\chi_{d,e}(x,x',y',y)\) such that for all \(w \in \Sigma^\triangle\) and \(i, i', j', j \in [1, \mathopen{}\left|w\right|\mathclose{}], i \leq i' < j' \leq j\) we have that if \(w_i \cdots w_{i'} w_{j'} \cdots w_j \in \Sigma^\triangle\) and \(i'\) is matched to \(j'\) in \(w\), then given \[\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}= \mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ\cdots\circ \mathop{\mathrm{ext}}_{x_k,y_k}\circ\mathop{\mathrm{ext}}_{a_k,b_k}\] the stair factorization of \(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}\) provided by Lemma [lemma32ext], we have \((w, M^\triangle\left(w\right)) \models \chi_{d,e}(i,i',j',j)\) if, and only if, \(\mathop{\mathrm{nd}}(x_\ell), \mathop{\mathrm{nd}}(y_\ell) < d\) for all \(\ell \in [1, k]\) and \(\psi_L(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j})=e\). Given \(w, i, i', j', j\) and the associated stair factorization as above, note that whenever \(\psi_L(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}) = e\), as \(e\) is \(\varphi_L(L)\)-reaching, then \(\varphi_L(x_\ell)\) and \(\varphi_L(y_\ell)\) are \(\varphi_L(L)\)-reaching for all \(\ell \in [1, k]\). If additionally \(\mathop{\mathrm{nd}}(x_\ell), \mathop{\mathrm{nd}}(y_\ell) < d\) for all \(\ell \in [1, k]\), we can inductively make use of the formulas \(\{\eta_{d-1,r'}\mid r'\in R_L \text{ \varphi_L(L)-reaching}\}\) in order to evaluate \(\varphi_L(x_1), \varphi_L(y_1), \ldots, \varphi_L(x_k), \varphi_L(y_k)\). Let \(p_1, \ldots, p_k \in [i, i']\) be the positions in \(w_i \cdots w_{i'}\) where, respectively, \(a_1, \ldots, a_k\) in the above factorization of \(\mathop{\mathrm{ext}}_{w_i \cdots w_{i'}, w_{j'} \cdots w_j}\) appear: the formula \(\chi_{d,e}\) will verify if \(\sigma_i\cdots\sigma_{i'}\in\mathcal{E}_{\psi_L,e}\), where \[\sigma_q= \begin{cases} \mathrm{left}_{\varphi_L(x_m)}\circ\mathrm{right}_{\varphi_L(y_m)} \circ\psi_L(\mathop{\mathrm{ext}}_{a_m,b_m}) & \text{if q = p_m for m \in [1, k]}\\ \$ & \text{otherwise} \end{cases}\] for all \(q \in [i, i']\). Hence we set \[\chi_{d, e}(x, x', y', y) = \forall z \Bigl( x \leq z \leq x' \rightarrow \bigl( \tau_2(\$(z)) \vee \bigvee_{\substack{f \in \psi_L \bigl( \mathcal{O}(\Sigma^\triangle)_\uparrow \bigr)\\ \text{\varphi_L(L)-reaching}}} \tau_2(f(z)) \bigl) \Bigr) \wedge \tau_2(\nu_{\psi_L,e}) \,\,\text{,}\] where the translation \(\tau_2\) agrees with translation \(\tau_0\) (where, as expected, occurrences of \(\tau_0\) are replaced by \(\tau_2\)) with the following exceptions:

• \(\tau_2(\exists z \rho(z,\boldsymbol{z}))= \exists z \bigl(x \leq z \leq x' \wedge \tau_2(\rho(z,\boldsymbol{z}))\bigr)\)

• \(\tau_2(\$(z))=\neg U(x,x',z)\)

• \(\tau_2(f(z)) = \begin{cases} \exists t \Bigl( \begin{aligned}[t] & U(x, x', z) \wedge z \leftrightsquigarrow t \wedge\\ & \bigl(\iota_{d,f}(x,x',y',y,z,t)\vee \zeta_{d,f}(x,x',z,t)\bigr) \Bigr) \end{aligned} & \text{if f is \varphi_L(L)-reaching}\\ \bot & \text{otherwise} \end{cases}\) for each \(f \in \psi_L\bigl(\mathcal{O}(\Sigma^\triangle)_\uparrow\bigr)\), where \[\begin{align} \iota_{d,f}(x,x',y',y,z,t) = & \neg \exists z' \bigl(U(x, x', z') \wedge z' < z\bigl) \wedge\\ & \begin{aligned}[t] & \bigvee_{\substack{a \in \Sigma_\text{call}, b \in \Sigma_\text{ret}, r', r'' \in R_L\\ f=\mathrm{left}_{r'} \circ \mathrm{right}_{r''}\circ \psi_L(\mathop{\mathrm{ext}}_{a, b})}} \biggl( \begin{align}[t] & a(z) \wedge b(t) \wedge\\ & \Bigl(\bigl(x < z \wedge \eta_{d - 1, r'}(x, z - 1)\bigr) \vee F_{r'}(x, z)\Bigr) \wedge\\ & \Bigl(\bigl(t < y \wedge \eta_{d - 1, r''}(t + 1, y)\bigr) \vee F_{r''}(y, t)\Bigr) \biggr) \end{aligned} \end{align} \end{align}\] with \(F_s(x, z) = \begin{cases} x = z & \text{if s = 1_{R_L}}\\ \bot & \text{otherwise} \end{cases}\) for all \(\varphi_L(L)\)-reaching \(s \in R_L\) and \[\zeta_{d,f}(x,x',z,t) = \exists z' \exists t' \biggl( \begin{align}[t] & U(x, x', z') \wedge z' < z \wedge \neg \exists z'' \bigl(z' < z'' < z \wedge U(x, x', z'')\bigr) \wedge z' \leftrightsquigarrow t' \wedge\\ & \bigvee_{\substack{a \in \Sigma_\text{call}, b \in \Sigma_\text{ret}, r', r'' \in R_L\\ f=\mathrm{left}_{r'} \circ \mathrm{right}_{r''}\circ \psi_L(\mathop{\mathrm{ext}}_{a, b})}} \Bigl( \begin{aligned}[t] a(z) \wedge b(t) \wedge \, & \eta_{d - 1, r'}(z' + 1, z - 1) \wedge\\ & \eta_{d - 1, r''}(t + 1, t' - 1) \Bigr)\biggr) \,\,\text{.} \end{aligned} \end{align}\]

We now construct \(\eta_{d,r}^\uparrow\) itself. Given \(w\in\Sigma^\triangle \setminus \{\varepsilon\}\) and \(i,j\in[1,\mathopen{}\left|w\right|\mathclose{}]\) such that \(i\) is matched to \(j\) in \(w\), observe first that the infix \(w_i \cdots w_j\) is of the form \(w_i \cdots w_j=a_1vb_1\in\Sigma^\triangle\) for some \(a_1\in\Sigma_\text{call}\), \(b_1\in\Sigma_\text{ret}\), and \(v\in\Sigma^\triangle\). As above, we can directly express \(\mathop{\mathrm{nd}}(w_i \cdots w_j)\leq d\) via the formula \(\neg N_{d+1}\). Assuming this holds, towards expressing that \(\varphi_L(w_i \cdots w_j)=r\), we make use of Lemma [lem:Maximal95stair95factorization] and Lemma [L32nesting32induction]: for the infix \(w_i \cdots w_j\) there is a nesting-maximal stair factorization \[w_i \cdots w_j = \mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_k,y_k} \circ \mathop{\mathrm{ext}}_{a_k,b_k}(u')\] such that we have

1. \(\mathop{\mathrm{nd}}(x_1),\mathop{\mathrm{nd}}(y_1),\dots,\mathop{\mathrm{nd}}(x_k),\mathop{\mathrm{nd}}(y_k)<d\); and

2. if \(\varphi_L(w_i \cdots w_j) = r\), as \(r\) is \(\varphi_L(L)\)-reaching, then \(\psi_L(\mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_k,y_k} \circ \mathop{\mathrm{ext}}_{a_k,b_k})\) and \(\varphi_L(u')\) are \(\varphi_L(L)\)-reaching.

By these points, we can use the formulas \(\{\chi_{d,e}(x,x',y',y) \mid e \in O_L \text{ \varphi_L(L)-reaching}\}\) to evaluate \(\psi_L(\mathop{\mathrm{ext}}_{x_1,y_1} \circ \mathop{\mathrm{ext}}_{a_1,b_1} \circ \cdots \circ \mathop{\mathrm{ext}}_{x_k,y_k} \circ \mathop{\mathrm{ext}}_{a_k,b_k})\) and the formulas \(\{\eta_{0,r'}\mid r'\in R_L \text{ \varphi_L(L)-reaching}\}\) to evaluate \(\varphi_L(u')\). We are now ready to give the formula \(\eta_{d,r}^\uparrow\). We set \[\eta_{d, r}^\uparrow(x, y) = \neg N_{d + 1}(x, y) \wedge \exists x' \exists y' \Bigl( \begin{align}[t] & x \leq x' < y' \leq y \wedge x' \leftrightsquigarrow y' \wedge\\ & \bigvee_{\substack{r' \in R_L, e \in O_L\\e(r') = r}} \bigl( \chi_{d, e}(x, x', y', y) \wedge \eta_{0, r'}(x' + 1, y' - 1) \bigl) \Bigr) \,\,\text{.} & \qedhere \end{align}\] ◻

Proof. Let \(e\in\mathcal{Z}\). For showing that \(N_e\) is an intermediate VPL we first show that \(N_e\) is quasi-counterfree. To this end we show that the syntactic morphism \((\varphi_{N_e},\psi_{N_e})\) of \(N_e\) is quasi-aperiodic, which is equivalent by Proposition [prop32quasi-counterfree].

Assume by contradiction that \((\varphi_{N_e},\psi_{N_e})\) is not quasi-aperiodic. Then there exist \(k,l\in\mathbb{N}\) such that \(\psi_{N_e}(\mathcal{O}(\Upsilon^\triangle)^{k,l})\) contains a non-trivial group, say \(G\subseteq O_{N_e}\). Let \(g_0\) be the identity of \(G\) and let \(g_1\in G\) be such that \(g_1\not=g_0\). Thus, we have \(g_1^{i+1}\not=g_1^i\) for all \(\mathbb{N}_{>0}\). We claim that all \(g\in G\) are \(\varphi_{N_e}(N_e)\)-reaching: indeed, if \(g\in G\) were not \(\varphi_{N_e}(N_e)\)-reaching, then the same would hold for all \(g'\in G\) since \(g'=g'g^{-1}g\), hence implying that \(g'\) is the (one and only) zero of \(O_{N_e}\), contradicting that \(G\) is non-trivial. Fix some \(\mathop{\mathrm{ext}}_{u_0,v_0},\mathop{\mathrm{ext}}_{u_1,v_1}\in\mathcal{O}(\Upsilon^\triangle)^{k,l}\) such that \(\psi_{N_e}(\mathop{\mathrm{ext}}_{u_0,v_0})=g_0\) and \(\psi_{N_e}(\mathop{\mathrm{ext}}_{u_1,v_1})=g_1\). Note that we must have \(k>0\) or \(l>0\) for otherwise we would have \(u_0=u_1=\varepsilon\) and \(v_0=v_1=\varepsilon\), a contradiction to \(g_0\not=g_1\). We moreover claim that \(u_0,u_1\not\in\widetilde{\Sigma}^*\) and hence \(v_0,v_1\not\in\overline{\Sigma}^*\): indeed, a consequence of Remark [remark32flat] is that \(\mathop{\mathrm{ext}}_{u,v}\in\psi_{N_e}^{-1}(f)\cap\widetilde{\Sigma}^s\times \overline{\Sigma}^t\) implies \(s,t\leq n\) for all \(\varphi_{N_e}(N_e)\)-reaching \(f\in O_{N_e}\), yet the fact that \(\psi_{N_e}(\mathop{\mathrm{ext}}_{u^i,v^i})\) is in \(G\) and thus \(\varphi_{N_e}(N_e)\)-reaching for all \(i\geq 1\) contradicts this (recall that \(|u_1|>0\) or \(|v_1|>0\)). In other words, both \(u_0\) and \(u_1\) contain at least one letter from \(\Sigma_\text{call}\) and both \(v_0\) and \(v_1\) contain a letter from \(\Sigma_\text{ret}\).

Next we claim that neither \(u_0\) nor \(u_1\) contain any letter from \(\Sigma_\text{ret}\): indeed, without loss of generality if \(u_1\) were to contain a letter from \(\Sigma_\text{ret}\) then \(\psi_{N_e}(\mathop{\mathrm{ext}}_{u_1^2,v_1^2})\) would be the zero of \(O_{N_e}\), contradicting that \(\psi_{N_e}(\mathop{\mathrm{ext}}_{u_1^2,v_1^2})\) is in \(G\). It follows that \(u_0,u_1\in(\widetilde{\Sigma}^*\Sigma_\text{call}\widetilde{\Sigma}^*)^+\) and hence that \(v_0,v_1\in(\overline{\Sigma}^*\Sigma_\text{ret}\overline{\Sigma}^*)^+\).

Let \(u_0'=\widetilde{\vartheta}^{-1}(u_0)\), \(u_1'=\widetilde{\vartheta}^{-1}(u_1)\), \(v_0'=\overline{\vartheta}^{-1}(v_0)\), \(v_1'=\overline{\vartheta}^{-1}(v_1)\) and note that \(\mathop{\mathrm{ext}}_{u_0',v_0'},\mathop{\mathrm{ext}}_{u_1',v_1'} \in\mathcal{O}(\Sigma^{k,l})\). Since \(\mathfrak{P}(O_L)\) forms a monoid there exists \(p \in \mathbb{N}_{>0}\) such that \[\psi_L(\{\mathop{\mathrm{ext}}_{u_0', v_0'}, \mathop{\mathrm{ext}}_{u_1', v_1'}\})^p = \psi_L(\{\mathop{\mathrm{ext}}_{u_0', v_0'}, \mathop{\mathrm{ext}}_{u_1', v_1'}\})^{2 p} \,\,\text{.}\] This implies that for all \(i \in \mathbb{N}_{>0}\), we have \[\psi_L(\mathop{\mathrm{ext}}_{u_0'^{p - 1} u_1', v_1' v_0'^{p - 1}})^i \in \psi_L(\{\mathop{\mathrm{ext}}_{u_0', v_0'}, \mathop{\mathrm{ext}}_{u_1', v_1'}\})^{i p} = \psi_L(\{\mathop{\mathrm{ext}}_{u_0', v_0'}, \mathop{\mathrm{ext}}_{u_1', v_1'}\})^p \,\,\text{.}\] Hence, as \(\mathopen{}\left|u_0\right|\mathclose{}=\mathopen{}\left|u_1\right|\mathclose{}=\mathopen{}\left|u_0'\right|\mathclose{} = \mathopen{}\left|u_1'\right|\mathclose{} = k\) and \(\mathopen{}\left|v_0\right|\mathclose{}=\mathopen{}\left|v_1\right|\mathclose{}=\mathopen{}\left|v_0'\right|\mathclose{} = \mathopen{}\left|v_1'\right|\mathclose{} = l\), the semigroup \(\{\psi_L(\mathop{\mathrm{ext}}_{u_0'^{p - 1} u_1', v_1' v_0'^{p - 1}})^i \mid i \in \mathbb{N}_{>0}\}\) is contained in \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k p, l p})\). We show that the latter semigroup is not aperiodic by showing \(\psi_L(\mathop{\mathrm{ext}}_{u_0'^{p - 1} u_1', v_1' v_0'^{p - 1}})^i\not= \psi_L(\mathop{\mathrm{ext}}_{u_0'^{p - 1} u_1', v_1' v_0'^{p - 1}})^{i+1}\) for all \(i\in\mathbb{N}_{>0}\). Indeed, since \[\psi_{N_e}\left(\left(\mathop{\mathrm{ext}}_{u_0^{p-1}u_1,v_1v_0^{p-1}}\right)^{i+1}\right)=g_1^{i+1}\not= g_1^{i+2}=\psi_{N_e}\left(\left(\mathop{\mathrm{ext}}_{u_0^{p-1}u_1,v_1v_0^{p-1}} \right)^{i+2}\right)\] there exist \(\mathop{\mathrm{ext}}_{x,y}\in\mathcal{O}(\Upsilon^\triangle)\) and \(w\in\Upsilon^\triangle\) such that, without loss of generality \[\left(\mathop{\mathrm{ext}}_{x,y}\circ \left(\mathop{\mathrm{ext}}_{u_0^{p-1}u_1,v_1v_0^{p-1}}\right)^{i+1}\right)(w)\in N_e \;\:\text{and}\;\: \left(\mathop{\mathrm{ext}}_{x,y}\circ \left(\mathop{\mathrm{ext}}_{u_0^{p-1}u_1,v_1v_0^{p-1}}\right)^{i+2}\right)(w)\not\in N_e \,\,\text{.}\] Now since \(u_0,u_1\in(\widetilde{\Sigma}^*\Sigma_\text{call}\widetilde{\Sigma}^*)^+\) there exists a factorization \(u_0^{p-1}u_1wv_1v_0^{p-1}=x'y'\) such that \[\left(\mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x),\overline{\vartheta}^{-1}(y)}\circ \left(\mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(u_0^{p-1}u_1), \overline{\vartheta}^{-1}(v_1v_0^{p-1})}\right)^{i}\right)( \widetilde{\vartheta}^{-1}(x')\#\overline{\vartheta}^{-1}(y'))\in M_e\] and \[\left(\mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x),\overline{\vartheta}^{-1}(y)}\circ \left(\mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(u_0^{p-1}u_1), \overline{\vartheta}^{-1}(v_1v_0^{p-1})}\right)^{i+1}\right)( \widetilde{\vartheta}^{-1}(x')\#\overline{\vartheta}^{-1}(y'))\not\in M_e\] By definition of \(M_e\) we obtain \[\begin{align} e&=&e\circ\psi_L\left(\mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x(u_0^{p-1}u_1)^ix'), \overline{\vartheta}^{-1}(y'(v_1v_0^{p-1})^iy)}\right)\\ &=&e\circ\psi_L\left( \mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x),\overline{\vartheta}^{-1}(y)} \right) \circ \psi_L\left( \mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(u_0^{p-1}u_1), \overline{\vartheta}^{-1}(v_1v_0^{p-1})}\right)^i \circ \psi_L\left( \mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x'),\overline{\vartheta}^{-1}(y')} \right) \end{align}\] and \[\begin{align} e&\not=&e\circ\psi_L\left(\mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x(u_0^{p-1}u_1)^{i+1}x'), \overline{\vartheta}^{-1}(y'(v_1v_0^{p-1})^{i+1}y)}\right)\\ &=&e\circ\psi_L\left( \mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x),\overline{\vartheta}^{-1}(y)} \right) \circ \psi_L\left( \mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(u_0^{p-1}u_1), \overline{\vartheta}^{-1}(v_1v_0^{p-1})}\right)^{i+1} \circ \psi_L\left( \mathop{\mathrm{ext}}_{\widetilde{\vartheta}^{-1}(x'),\overline{\vartheta}^{-1}(y')} \right)\!. \end{align}\] Thus, we must have \(\psi_L(\mathop{\mathrm{ext}}_{u_0'^{p - 1} u_1', v_1' v_0'^{p - 1}})^i\not= \psi_L(\mathop{\mathrm{ext}}_{u_0'^{p - 1} u_1', v_1' v_0'^{p - 1}})^{i+1}\), as required. As this is true for each \(i \in \mathbb{N}_{>0}\), the semigroup \(\{\psi_L(\mathop{\mathrm{ext}}_{u_0'^{p - 1} u_1', v_1' v_0'^{p - 1}})^i \mid i \in \mathbb{N}_{>0}\}\) that is contained in \(\psi_L(\mathcal{O}(\Sigma^\triangle)^{k p, l p})\) is not aperiodic, contradicting quasi-aperiodicity of \((\varphi_L, \psi_L)\).

It remains to show that one can compute a vertically visibly pushdown grammar \(G_e\) with \(L(G_e)=N_e\) such that \(\mathcal{R}(G_e)\) is weakly length-synchronous but not length-synchronous. By Remark [remark32flat] each non-empty word in \(N_e\) is of the form \[(u\#v)^\ddagger= \mathop{\mathrm{ext}}_{\widetilde{\vartheta}(x_1),\overline{\vartheta}(y_1)} \circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ\cdots\circ \mathop{\mathrm{ext}}_{\widetilde{\vartheta}(x_{k}),\overline{\vartheta}(y_{k})} \circ\mathop{\mathrm{ext}}_{a_k,b_k}\circ \mathop{\mathrm{ext}}_{\widetilde{\vartheta}(x_{k+1}),\overline{\vartheta}(y_{k+1})}(\varepsilon)\] for some \(k\geq 1\) and some words \(x_1,\dots,x_{k+1},y_1,\dots,y_{k+1}\in\Sigma^\triangle\) all of which have length at most \(n\) such that moreover \(e\circ\psi_L(\mathop{\mathrm{ext}}_{u,v})=e\). We construct the grammar \(G_e=(V,\Upsilon,P,S_e)\) as follows. The set of nonterminals is \(V=\{S_f\mid f\in O_L\}\), \(S_e\in V\) is the start nonterminal, the set of productions consists of the union of \(\{S_e\rightarrow_{G_e}\varepsilon\}\) and \[\begin{align} \left\{\biggl.S_f\rightarrow_{G_e}\widetilde{\vartheta}(x_1)a\widetilde{\vartheta}(x_2)S_g \overline{\vartheta}(y_2)b\overline{\vartheta}(y_1)\right. \!\!\!&\bigm|&\!\!\! f,g\in O_L, x_1,x_2,y_1,y_2\in\Sigma^\triangle, |x_1|,|x_2|,|y_1|,|y_2|\leq n, \\ &&\!\!\! a\in\Sigma_\text{call},b\in\Sigma_\text{ret}, \left.\biggl.f\circ\psi_L(\mathop{\mathrm{ext}}_{x_1ax_2,y_2by_1})=g\right\}. \end{align}\] As a consequence we obtain \[\begin{align} \mathcal{R}(G_e)=\left\{\biggl.\left(\widetilde{\vartheta}(x_1)\dots a_k\widetilde{\vartheta}(x_{x+1}), \overline{\vartheta}(y_{k+1})b_k\dots \overline{\vartheta}(y_1)\right)\right. \!\!\!&\big|&\!\!\! x_1,\dots,x_{k+1},x_1,\dots,y_{k+1}\in\Sigma^\triangle,\\ && \!\!\!a_1,\dots,a_{k}\in\Sigma_\text{call}, b_1,\dots,b_{k}\in\Sigma_\text{ret},\\ &&\!\!\! \left.e\circ\psi_L(\mathop{\mathrm{ext}}_{a_1\dots a_{k}x_{k+1},y_{k+1}b_k\dots y_1})=e \biggl.\right\} \end{align}\] \[\begin{align} \phantom{\mathcal{R}(G_e)}=\left\{\biggl.\left(\widetilde{\vartheta}(x_1)\dots a_k\widetilde{\vartheta}(x_{x+1}), \overline{\vartheta}(y_{k+1})b_k\dots \overline{\vartheta}(y_1)\right)\right. \!\!\!&\big|&\!\!\! x_1,\dots,x_{k+1},x_1,\dots,y_{k+1}\in\Sigma^\triangle,\\ && \!\!\!a_1,\dots,a_{k}\in\Sigma_\text{call}, b_1,\dots,b_{k}\in\Sigma_\text{ret},\\ &&\!\!\! \left.\left(x_1\dots a_{k}x_{k+1},y_{k+1}b_k\dots y_1\right)\in \mathcal{U}_e\biggl.\right\}\!. \end{align}\] It follows that \(\mathcal{R}(G_e)\) is weakly length-synchronous since \(\mathcal{U}_e\) is: indeed, if \(\mathcal{R}(G_e)\) were not weakly length-synchronous and without loss of generality there were to exist \((u,v),(u',v')\in\mathcal{R}(G_e)\) with \(u=u'\) and \(|v|\not=|v'|\), then both \((\widetilde{\vartheta}^{-1}(u),\overline{\vartheta}^{-1}(v))\) and \((\widetilde{\vartheta}^{-1}(u'),\overline{\vartheta}^{-1}(v'))\) would be in \(\mathcal{U}_e\) by definition. Yet \(\widetilde{\vartheta}^{-1}(u)= \widetilde{\vartheta}^{-1}(u')\) and \(|\overline{\vartheta}^{-1}(v)|=|v|\not=|v'|=\overline{\vartheta}^{-1}(v')\), so this would contradict that \(\mathcal{U}_e\) is indeed weakly length-synchronous. Analogously it follows that \(\mathcal{R}(G_e)\) is not length-synchronous since \(\mathcal{U}_e\) is not length-synchronous by assumption. ◻

Proof. Assume we are given \(w\in\Upsilon^*\). To decide if \(w\in N_e\) using an oracle to \(M_e\) we do the following constant-depth computation:

1. Accept if \(w = \varepsilon\), otherwise continue.

2. Check if \(w=uv\) for some \(u\in(\widetilde{\Sigma}\cup\Sigma_\text{call})^*\) and some \(v\in(\overline{\Sigma}\cup\Sigma_\text{ret})^*\), reject if this is not the case.

3. Check whether \(u\) can be factorized as \(u=x_1a_1\cdots x_ka_kx_{k+1}\), where \(k\geq 1\), \(x_1,\dots,x_{k+1}\in \{x \in \widetilde{\Sigma}^* \mid \mathopen{}\left|x\right|\mathclose{} \leq n \wedge \widetilde{\vartheta}^{-1}(x) \in \Sigma^\triangle\}\) and \(a_1,\dots,a_k\in\Sigma_\text{call}\) and whether \(v\) can be factorized as \(v=y_{l+1}b_ly_l\cdots a_1y_1\), where \(l\geq 1\), \(y_1,\dots,y_{l+1}\in \{y \in \overline{\Sigma}^* \mid \mathopen{}\left|y\right|\mathclose{} \leq n \wedge \overline{\vartheta}^{-1}(y) \in \Sigma^\triangle\}\) and \(b_1,\dots,b_l\in\Sigma_\text{ret}\). Reject if it is not possible. (Observe that this is doable by a constant depth and polynomial size circuit family since we test membership in finite sets that do not depend on the input.)

4. Finally accept if, and only if, the word \[\widetilde{\vartheta}^{-1}(x_1)a_1\cdots \widetilde{\vartheta}^{-1}(x_{k-1}) a_k \widetilde{\vartheta}^{-1}(x_{k+1}) \# \overline{\vartheta}^{-1}(y_{l+1})b_l \overline{\vartheta}^{-1}(y_{l+1}) \cdots b_1 \overline{\vartheta}^{-1}(y_{1})\] is in \(M_e\).

 ◻

Proof. Assume we are given \(w\in(\Sigma\cup\{\#\})^*\), where \(w=w_1\cdots w_m\) and where \(w_i\in\Sigma\cup\{\#\}\) for all \(i\in[1,m]\). To decide if \(w\in M_e\) using an oracle to \(N_e\) we do the following constant-depth computation:

1. Check if \(w=u\#v\) for some \(u\in\Sigma^+\) and some \(v\in\Sigma^+\), reject otherwise.

2. For all return letters \(b\in\Sigma_\text{ret}\) and all positions \(j\) within \(u\) at which \(b\) appears, check whether there exists a position \(i\) within \(u\) such that \(1 \leq j - i \leq n - 1\) and the infix \(w_i\cdots w_j\) is in \(\Sigma^\triangle\). (As above, this is doable by a constant depth and polynomial size circuit family since we check well-matchedness of at most a fixed number of words that does not depend on the input.) Reject if it is not the case.

3. For all call letters \(a\in\Sigma_\text{call}\) and all positions \(i\) within \(v\) at which \(a\) appears, check whether there exists a position \(j\) within \(v\) such that \(1 \leq j - i \leq n - 1\) and the infix \(w_i \cdots w_j\) is in \(\Sigma^\triangle\). Reject if it is not the case.

4. For each position \(i\) within \(u\), compute \(P_\text{call}(i)\) where \(P_\text{call}\) is the unary predicate defined by \(w\models P_\text{call}(i)\) if, and only if, \(i\) is a position within \(u\), \(w_i\in\Sigma_\text{call}\), and there does not exist any position \(j\) within \(u\) such that \(1 \leq j - i \leq n - 1\) and the infix \(w_i\cdots w_j\) is in \(\Sigma^\triangle\).

5. For each position \(j\) within \(v\), compute \(P_\text{ret}(j)\) where \(P_\text{ret}\) is the unary predicate defined by \(w\models P_\text{ret}(j)\) if, and only if, \(j\) is a position within \(v\), \(w_j\in\Sigma_\text{ret}\), and there does not exist any position \(i\) within \(v\) such that \(1 \leq j - i \leq n - 1\) and the infix \(w_i\cdots w_j\) is in \(\Sigma^\triangle\).

6. Let \(1\leq i_1<i_2\dots <i_k\leq|u|\) be an enumeration of \(\{i\in[1,|u|]\mid w\models P_\text{call}(i)\}\) and let \(|u|+2\leq j_l<j_{l-1}\dots <j_1\leq m\) be an enumeration of \(\{j\in[|u|+2,m]\mid w\models P_\text{ret}(j)\}\). Build \[u'=\widetilde{\vartheta} (w_{1}\cdots w_{i_1-1})w_{i_1} \cdots \widetilde{\vartheta}(w_{i_{k-1}+1}\cdots w_{i_k-1})w_{i_k} \widetilde{\vartheta}(w_{i_{k+1}+1}\cdots w_{|u|})\] and \[v'=\overline{\vartheta}(w_{|u|+2}\cdots w_{j_{l+1}-1}) w_{j_l}\cdots \overline{\vartheta} (w_{j_2}+1\cdots w_{j_1-1})w_{j_1} \overline{\vartheta} (w_{j_1}+1\cdots w_{m}).\]

7. Accept if, and only if, the word \(u'v'\) is in \(N_e\).

 ◻

Proof. Note that the following equivalence holds: \[u\#v \in M_e\quad\Longleftrightarrow\quad \text{\exists f\in O_L that is \varphi_L(L)-reaching}: e\circ f=e\wedge u\#v\in L_f\wedge \Delta(u)>0 \,\,\text{.}\] This holds because for \(\mathop{\mathrm{ext}}_{u, v} \in \mathcal{O}(\Sigma^\triangle)\) satisfying \(e \circ \psi_L(\mathop{\mathrm{ext}}_{u, v}) = e\), as \(e\) is \(\varphi_L(L)\)-reaching, \(\psi_L(\mathop{\mathrm{ext}}_{u, v})\) must also be \(\varphi_L(L)\)-reaching. Assume we are given \(w\in(\Sigma\cup\{\#\})^*\). To decide if \(w\in M_e\) we do the following constant-depth computation using oracles to \(\biguplus_{\text{f\in O_L is \varphi_L(L)-reaching}} L_f\):

1. Check if \(w=u\#v\) for some \(u,v\in\Sigma^*\), reject otherwise.

2. Check if \(u\#v\in L_f\) for some \(\varphi_L(L)\)-reaching \(f\in O_L\) satisfying \(e\circ f=e\), reject otherwise.

3. Finally, accept if, and only if for all \(\varphi_L(L)\)-reaching \(f\in O_L\) we have \(u\#\not\in L_f\).

If the second check is successful, then \(\psi_L(\mathop{\mathrm{ext}}_{u,v})\) is necessarily \(\varphi_L(L)\)-reaching, so in that case when \(\Delta(u)=0\) it holds that \(u \in \Sigma^\triangle\) and \(\psi_L(\mathop{\mathrm{ext}}_{u, \varepsilon})\) is \(\varphi_L(L)\)-reaching. Hence, in combination with the second check, the third check is successful if, and only if \(\Delta(u)>0\). ◻

Proof. By assumption \(L\) is weakly length-synchronous but not length-synchronous, and its syntactic morphism \((\varphi_L,\psi_L)\) is quasi-aperiodic. There is a constant \(d_L\) such that all words in \(L\) have nesting depth at most \(d_L\) by Proposition [ptn:Bounded95nesting-depth].

By the first point of Proposition [ptn:Quasi-aperiodicity95eval95languages] we may assume that the evaluation language \(\mathcal{E}_{\varphi_L,r}\) is regular and its syntactic morphism is quasi-aperiodic for all \(\varphi_L(L)\)-reaching \(r\in R_L\). This implies, by [2], that for each \(\varphi_L(L)\)-reaching \(r \in R_L\), there exists an \(\mathsf{FO}_{\Gamma_{\varphi_L}}[<, \mathsf{MOD}]\)-sentence \(\nu_{\varphi_L, r}\) defining \(\mathcal{E}_{\varphi_L, r}\).

As \(L\) is not length-synchronous we cannot assume analogous sentences for the evaluation languages \(\mathcal{E}_{\psi_L,e}\) for all \(\varphi_L(L)\)-reaching \(e\in O_L\). Indeed, Remark [remark32not32weakly] provides an example of a weakly length-synchronous but non-length-synchronous VPL whose syntactic morphism is quasi-aperiodic but for which some evaluation language \(\mathcal{E}_{\psi_L,e}\) for \(e \in O_L\) that is \(\varphi_L(L)\)-reaching has a non-quasi-aperiodic syntactic morphism.

However, let \(e \in O_L\) be such that \(\mathcal{R}_e = \{(u,v) \in \mathsf{Con}(\Sigma) \mid\psi_L(\mathop{\mathrm{ext}}_{u,v})=e\}\) is length-synchronous. Take any \(\varphi_L(L)\)-reaching idempotent \(f \in O_L\) such that there exist \(g, h \in O_L\) satisfying \(e = g \circ f \circ h\). There exist \(\mathop{\mathrm{ext}}_{x_g, y_g}, \mathop{\mathrm{ext}}_{x_h, y_h} \in \mathcal{O}(\Sigma^\triangle)\) such that \(\psi_L(\mathop{\mathrm{ext}}_{x_g, y_g}) = g\) and \(\psi_L(\mathop{\mathrm{ext}}_{x_h, y_h}) = h\). Let \((u, v), (u', v') \in\mathsf{Con}(\Sigma)\) such that \(\Delta(u), \Delta(u') > 0\) and \(\psi_L(\mathop{\mathrm{ext}}_{u, v}) = \psi_L(\mathop{\mathrm{ext}}_{u', v'}) = f\). Because \(f\) is idempotent, we have that \(\psi_L(\mathop{\mathrm{ext}}_{u^{\mathopen{}\left|v'\right|\mathclose{}}, v^{\mathopen{}\left|v'\right|\mathclose{}}}) = \psi_L(\mathop{\mathrm{ext}}_{u'^{\mathopen{}\left|v\right|\mathclose{}}, v'^{\mathopen{}\left|v\right|\mathclose{}}}) = f\), thus \(\psi_L(\mathop{\mathrm{ext}}_{x_g u^{\mathopen{}\left|v'\right|\mathclose{}} x_h, y_h v^{\mathopen{}\left|v'\right|\mathclose{}} y_g}) = \psi_L(\mathop{\mathrm{ext}}_{x_g u'^{\mathopen{}\left|v\right|\mathclose{}} x_h, y_h v'^{\mathopen{}\left|v\right|\mathclose{}} y_g}) = e\). Therefore, because of length-synchronicity of \(\mathcal{R}_e\), it follows that \[\begin{align} \frac{\mathopen{}\left|x_g u^{\mathopen{}\left|v'\right|\mathclose{}} x_h\right|\mathclose{}}{\mathopen{}\left|y_h v^{\mathopen{}\left|v'\right|\mathclose{}} y_g\right|\mathclose{}} & = \frac{\mathopen{}\left|x_g u'^{\mathopen{}\left|v\right|\mathclose{}} x_h\right|\mathclose{}}{\mathopen{}\left|y_h v'^{\mathopen{}\left|v\right|\mathclose{}} y_g\right|\mathclose{}}\\ \frac{\mathopen{}\left|x_g\right|\mathclose{} + \mathopen{}\left|v'\right|\mathclose{} \cdot \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|x_h\right|\mathclose{}}{\mathopen{}\left|y_h\right|\mathclose{} + \mathopen{}\left|v'\right|\mathclose{} \cdot \mathopen{}\left|v\right|\mathclose{} + \mathopen{}\left|y_g\right|\mathclose{}} & = \frac{\mathopen{}\left|x_g\right|\mathclose{} + \mathopen{}\left|v\right|\mathclose{} \cdot \mathopen{}\left|u'\right|\mathclose{} + \mathopen{}\left|x_h\right|\mathclose{}}{\mathopen{}\left|y_h\right|\mathclose{} + \mathopen{}\left|v\right|\mathclose{} \cdot \mathopen{}\left|v'\right|\mathclose{} + \mathopen{}\left|y_g\right|\mathclose{}}\\ \mathopen{}\left|v'\right|\mathclose{} \cdot \mathopen{}\left|u\right|\mathclose{} & = \mathopen{}\left|v\right|\mathclose{} \cdot \mathopen{}\left|u'\right|\mathclose{}\\ \frac{\mathopen{}\left|u\right|\mathclose{}}{\mathopen{}\left|v\right|\mathclose{}} & = \frac{\mathopen{}\left|u'\right|\mathclose{}}{\mathopen{}\left|v'\right|\mathclose{}} \,\,\text{.} \end{align}\] So we can conclude that \(\mathcal{R}_f = \{(u,v) \in \mathsf{Con}(\Sigma)\mid\psi_L(\mathop{\mathrm{ext}}_{u,v})=f\}\) is length-synchronous. Thus, by the second point of Proposition [ptn:Quasi-aperiodicity95eval95languages] we may assume that the evaluation language \(\mathcal{E}_{\psi_L,e}\) is regular and its syntactic morphism is quasi-aperiodic for all \(\varphi_L(L)\)-reaching \(e\in O_L\) with \(\mathcal{R}_e\) length-synchronous. This implies again, by [2], that for each \(\varphi_L(L)\)-reaching \(e \in O_L\) with \(\mathcal{R}_e\) length-synchronous, there exists an \(\mathsf{FO}_{\Gamma_{\psi_L}}[<, \mathsf{MOD}]\)-sentence \(\nu_{\psi_L, e}\) defining \(\mathcal{E}_{\psi_L, e}\).

For proving \(L\leq_{\mathrm{cd}}\biguplus_{e\in\mathcal{Z}} M_e\) we must thus make use of the oracles to \(\biguplus_{e\in\mathcal{Z}} M_e\). All of the following predicates can be computed by a circuit family of constant depth and polynomial size with access to these oracles. More concretely, by accessing oracles to \(\biguplus_{e\in\mathcal{Z}} M_e\), for all \(e\in\mathcal{Z}\) we may assume that we have a predicate \(\pi_e^{\mathsf{exact}}\) such that for all \(w \in \Sigma^+\) and \(i, i', j', j \in [1, \mathopen{}\left|w\right|\mathclose{}], i \leq i' < j' \leq j\) the following holds: \[\begin{align} \label{P321} w\models\pi_e^{\mathsf{exact}}(i,i',j',j)&\quad\Longleftrightarrow\quad& w_i\cdots w_{i'} w_{j'} \cdots w_j\in\Sigma^\triangle,\\ && e\circ\psi_L(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j})=e \text{ and }\nonumber\\&&\Delta(w_i\cdots w_{i'})>0\nonumber \end{align}\tag{4}\]

For all \(\varphi_L(L)\)-reaching \(e\in O_L\) that are not in \(\mathcal{Z}\) we may assume, by Lemma [lem:Synchronous95element95matching], that we have the \(\ifthenelse{\equal{\null}{\null}} { \mathsf{FO}[\mathsf{+}] } { \mathsf{FO}_{\null}[\mathsf{+}] }\)-definable (and hence constant-depth computable) predicate \(\pi_e\) at hand. It has the following properties: for all \(w \in \Sigma^+\) and \(i, i', j', j \in [1, \mathopen{}\left|w\right|\mathclose{}], i \leq i' < j' \leq j\):

• if \(w\models \pi_e(i, i', j', j)\), then \(w_i \cdots w_{i'} w_{j'} \cdots w_j \in \Sigma^\triangle\) and

• if \(w_i \cdots w_{i'} w_{j'} \cdots w_j \in \Sigma^\triangle\), \(\Delta(w_i \cdots w_{i'}) > 0\) and \(e \circ \psi_L(\mathop{\mathrm{ext}}_{w_i \cdots w_{i'}, w_{j'} \cdots w_j}) = e\), then \(w\models \pi_e(i, i', j', j)\).

We can first build an approximate matching \(\mu\) relative to \(L\). This is done totally analogously as done in Section 5.3.4.1 by replacing the there appearing \(\pi_e\) for each \(e\in\mathcal{Z}\) by our predicate \(\pi_e^{\mathsf{exact}}\): indeed, Remark [remark32up] states that the predicates \(\pi_e\) from of Lemma [lem:Synchronous95element95matching] could have been replaced by the predicate \(\pi_e^{\mathsf{exact}}\).

Thus, as in the proof of Proposition [ptn:Eval95languages95and95bounded95nesting-depth] we may assume that we have full access to the matching relation \(M^\Delta(w)\) of our input word \(w\).

For verifying if a given word \(w\in\Sigma^\triangle\) is in \(L\) we follow the same approach as the main construction in Section 5.3.5. It is however important to stress that this time we cannot assume quasi-aperiodicity of the syntactic morphisms of the evaluation languages \(\mathcal{E}_{\psi_L,e}\) for all \(\varphi_L(L)\)-reaching \(e\in O_L\). Still, we build formulas

• \(\overline{\eta}_{d, r}^\uparrow(x, y)\) for all \(d\in[0,d_L]\) and all \(\varphi_L(L)\)-reaching \(r \in R_L\) and

• \(\overline{\eta}_{d, r}(x, y)\) for all \(d\in[0,d_L]\) and all \(\varphi_L(L)\)-reaching \(r\in R_L\)

that will have the following properties (as \(\eta_{d,r}\) and \(\eta_{d,r}^\uparrow\)) for all \(w\in\Sigma^\triangle\) and all \(i,j\in[1,\mathopen{}\left|w\right|\mathclose{}]\):

• if \(i\) is matched to \(j\) in \(w\), then \((w, M^\triangle\left(w\right)) \models \overline{\eta}_{d, r}^\uparrow(i, j)\) if, and only if, \(\mathop{\mathrm{nd}}(w_i \cdots w_j) \leq d\) and \(\varphi_L(w_i \cdots w_j) = r\);

• if \(w_i \cdots w_j \in \Sigma^\triangle\), then \((w, M^\triangle\left(w\right)) \models \overline{\eta}_{d, r}(i, j)\) if, and only if, \(\mathop{\mathrm{nd}}(w_i \cdots w_j) \leq d\) and \(\varphi_L(w_i \cdots w_j) = r\).

It remains to define the formulas \(\overline{\eta}_{d,r}\) and \(\overline{\eta}_{d,r}^\uparrow\) for all \(d\in[0,d_L]\) and all \(\varphi_L(L)\)-reaching \(r\in R_L\). For the definition of the \(\overline{\eta}_{0,r}^\uparrow\) and the \(\overline{\eta}_{0,r}\) we can simply reuse \(\eta_{0,r}\) and \(\eta_{0,r}^\uparrow\) as in the proof of Proposition [ptn:Eval95languages95and95bounded95nesting-depth] respectively (\(\eta_{0,r}\) will make use of our sentence \(\nu_{\varphi_L,r}\)). So let us assume \(d>0\).

We first construct for all \(\varphi_L(L)\)-reaching \(e\in O_L\) a formula \(\overline{\chi}_{d,e}(x,x',y',y)\) such that for all \(w \in \Sigma^\triangle\) and \(i, i', j', j \in [1, \mathopen{}\left|w\right|\mathclose{}], i \leq i' < j' \leq j\) we have that if \(w_i \cdots w_{i'} w_{j'} \cdots w_j \in \Sigma^\triangle\) and \(i'\) is matched to \(j'\) in \(w\), then given \[\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}= \mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ\cdots\circ \mathop{\mathrm{ext}}_{x_k,y_k}\circ\mathop{\mathrm{ext}}_{a_k,b_k}\] the stair factorization of \(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}\) provided by Lemma [lemma32ext], we have \((w, M^\triangle\left(w\right)) \models \overline{\chi}_{d,e}(i,i',j',j)\) if, and only if, \(\mathop{\mathrm{nd}}(x_\ell), \mathop{\mathrm{nd}}(y_\ell) < d\) for all \(\ell \in [1, k]\) and \(\psi_L(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j})=e\). Given \(w, i, i', j', j\) and the associated stair factorization as above, note that whenever \(\psi_L(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}) = e\), as \(e\) is \(\varphi_L(L)\)-reaching, then \(\varphi_L(x_\ell)\) and \(\varphi_L(y_\ell)\) are \(\varphi_L(L)\)-reaching for all \(\ell \in [1, k]\). If additionally \(\mathop{\mathrm{nd}}(x_\ell), \mathop{\mathrm{nd}}(y_\ell) < d\) for all \(\ell \in [1, k]\), we can inductively make use of the formulas \(\{\overline{\eta}_{d-1,r'}\mid r'\in R_L \text{ \varphi_L(L)-reaching}\}\) in order to evaluate \(\varphi_L(x_1), \varphi_L(y_1), \ldots, \varphi_L(x_k), \varphi_L(y_k)\).

As expected, the problems are, firstly, that we cannot necessarily access our evaluation languages \(\mathcal{E}_{\psi_L,e}\) and, secondly, that we have to build a formula that may not depend on \(k\). As in Section 5.3.4.1 we define the product \[e_{\ell,\ell'}= \psi_L(\mathop{\mathrm{ext}}_{x_\ell,y_\ell}\circ\mathop{\mathrm{ext}}_{a_{\ell},b_{\ell}}\circ\cdots\circ \mathop{\mathrm{ext}}_{x_{\ell'},y_{\ell'}}\circ\mathop{\mathrm{ext}}_{a_{\ell'},b_{\ell'}})\quad \text{and}\quad e_\ell=e_{1,\ell}\] for all \(\ell,\ell'\in[1,k]\). We say an interval \(I=[s,t]\subseteq[1,k]\) is repetitive if \(s<t\) and \(e_s=e_t\).

By Claim [claim32pigeon] there exist indices \(1=t_0\leq s_1<t_1<s_2<t_2<\cdots<s_q<t_q\leq s_{q+1}=k\) such that \([s_1,t_1],\ldots, [s_q,t_q]\) are all repetitive and for \(D_0=[t_0,s_1],D_1=[t_1,s_2],\dots,D_q=[t_q,s_{q+1}]\) we have \(q+\sum_{p=0}^q\left|D_p\right|\leq 3\left|O_L\right|\). Let \(i=i_1<\cdots<i_k\) and \(j_k<\cdots<j_1=j\) be the positions that correspond to the positions of the letters \(a_1,\dots,a_k\in\Sigma_\text{call}\) and \(b_k,\dots, b_1\in\Sigma_\text{ret}\) of the factorization of \(\mathop{\mathrm{ext}}_{w_i \cdots w_{i'}, w_{j'} \cdots w_j}\) in \(w\), respectively: more precisely \(i_\ell=i+\mathopen{}\left|x_1\cdots a_{\ell-1}x_\ell\right|\mathclose{}\) and \(j_\ell=\mathopen{}\left|x_1 a_1 \cdots x_k a_k w_{i'+1} \cdots w_{j'-1} b_k y_{k} \cdots b_{\ell+1} y_{\ell+1}\right|\mathclose{}+1\) for all \(\ell\in[1,k]\). Since the non-empty interval \([s_p,t_p]\) is repetitive for all \(p\in[1,q]\), we have \(e_{s_p}=e_{t_p}\) and thus obtain \[e_{s_p}=e_{t_p}= e_{s_p}\circ\psi(\mathop{\mathrm{ext}}_{x_{s_p+1}\cdots a_{t_p},b_{t_p}\cdots y_{s_p+1}}) \,\,\text{.}\] Given \(p \in [1, q]\), if \(e_{s_p} \in \mathcal{Z}\), we can use the predicate \(\pi_{e_{s_p}}^{\mathsf{exact}}\) to check the above equality; we set \(\theta_{d, e_{s_p}}(x, x', y', y) = \pi_{e_{s_p}}^{\mathsf{exact}}(x, x', y', y)\). If \(e_{s_p}\notin\mathcal{Z}\) and is \(\varphi_L(L)\)-reaching, then \(\mathcal{U}_{e_{s_p}}\) is length-synchronous, so for all \(e' \in O_L\) such that \(e_{s_p} \circ e' = e_{s_p}\), we have that \(e'\) is \(\varphi_L(L)\)-reaching and \(\mathcal{R}_{e'} = \{(u,v) \in \mathsf{Con}(\Sigma) \mid \psi_L(\mathop{\mathrm{ext}}_{u,v})=e'\}\) is length-synchronous. So to check the above equality, we can use the formula \(\theta_{d, e_{s_p}}(x, x', y', y)\) built by taking the disjunction over all \(e' \in O_L\) such that \(e_{s_p} \circ e' = e_{s_p}\) of the formulas defined inductively completely analogously as \(\chi_{d, e'}(x, x', y', x')\) in Section 5.3.5 (using the sentence \(\nu_{\psi_L, e'}\) defining \(\mathcal{E}_{\psi_L, e'}\)): we simply replace every occurrence of \(\eta_{d-1,r}\) by \(\overline{\eta}_{d-1,r}\).

Next, for all \(m>0\) and all \(\varphi_L(L)\)-reaching \(f\in O_L\) we will construct a formula \(\alpha_{d, m, f}(x,x',y',y)\) such that for all \(w \in \Sigma^\triangle\) and \(i, i', j', j \in [1, \mathopen{}\left|w\right|\mathclose{}], i \leq i' < j' \leq j\) we have that if \(w_i \cdots w_{i'} w_{j'} \cdots w_j \in \Sigma^\triangle\) and \(i'\) is matched to \(j'\) in \(w\), then given \[\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}= \mathop{\mathrm{ext}}_{x_1,y_1}\circ\mathop{\mathrm{ext}}_{a_1,b_1}\circ\cdots\circ \mathop{\mathrm{ext}}_{x_k,y_k}\circ\mathop{\mathrm{ext}}_{a_k,b_k}\] the stair factorization of \(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j}\) provided by Lemma [lemma32ext], we have \((w, M^\triangle\left(w\right)) \models \alpha_{d,m,f}(i,i',j',j)\) if, and only if, \(\mathop{\mathrm{nd}}(x_\ell), \mathop{\mathrm{nd}}(y_\ell) < d\) for all \(\ell \in [1, k]\), \(\Delta(w_i \cdots w_{i'})=-\Delta(w_{j'} \cdots w_j)=m\) and \(\psi_L(\mathop{\mathrm{ext}}_{w_i\cdots w_{i'},w_{j'}\cdots w_j})=e\). For \(\boldsymbol{\sigma}=(\boldsymbol{\sigma}_1,\dots,\boldsymbol{\sigma}_m)\in{\Sigma_\text{call}}^m\), \(\boldsymbol{\xi}=(\boldsymbol{\xi}_1\dots,\boldsymbol{\xi}_m)\in{\Sigma_\text{ret}}^m\), \(\boldsymbol{r}=(\boldsymbol{r}_1,\dots,\boldsymbol{r}_m)\in {R_L}^m\), and \(\boldsymbol{r}^\dagger=(\boldsymbol{r}_1^\dagger,\dots,\boldsymbol{r}_m^\dagger)\in {R_L}^m\) we define \[\prod(\boldsymbol{\sigma},\boldsymbol{\xi},\boldsymbol{r},\boldsymbol{r}^\dagger)= \bigcirc_{g=1}^{m}\mathrm{left}_{\boldsymbol{r}_g}\circ \mathrm{right}_{\boldsymbol{r}_g^\dagger}\circ \psi_L(\mathop{\mathrm{ext}}_{\boldsymbol{\sigma}_g,\boldsymbol{\xi}_g}).\] The formula \(\alpha_{d, m, f}\) can be expressed as follows: \[\begin{align} \alpha_{d,m,f}(x,x',y',y) = & \bigvee_{\substack{\boldsymbol{\sigma} \in {\Sigma_\text{call}}^m, \boldsymbol{\xi}\in {\Sigma_\text{ret}}^m\\ \boldsymbol{r},\boldsymbol{r}^\dagger\in {R_L}^m: f=\prod(\boldsymbol{\sigma},\boldsymbol{\xi},\boldsymbol{r},\boldsymbol{r}^\dagger)}} \exists x_1,\dots, x_m\exists y_1,\dots,y_m\\ & \biggl( \begin{aligned}[t] & x'=x_m \wedge y'=y_m \wedge x\leq x_1<\cdots<x_m<y_m<\cdots<y_1\leq y\wedge\\ & \bigwedge_{g=1}^m \bigl(\boldsymbol{\sigma}_g(x_g) \wedge \boldsymbol{\xi}_g(y_g) \wedge x_g \leftrightsquigarrow y_g\bigr) \wedge\\ & \forall z \bigl((x \leq z \leq x' \wedge \bigwedge_{g=1}^m z \neq x_g) \rightarrow \neg U(x, x', z)\bigr) \wedge\\ & \Bigl(\bigl(x < x_1 \wedge \overline{\eta}_{d-1,\boldsymbol{r}_1}(x,x_1-1)\bigr) \vee F_{\boldsymbol{r}_1}(x, x_1)\Bigr) \wedge\\ & \Bigl(\bigl(y_1 < y \wedge \overline{\eta}_{d-1,\boldsymbol{r}_1^\dagger}(y_1+1,y)\bigr) \vee F_{\boldsymbol{r}_1^\dagger}(y_1, y)\Bigr) \wedge\\ & \bigwedge_{g=2}^m \overline{\eta}_{d-1,\boldsymbol{r}_g}(x_{g-1}+1,x_g-1) \wedge \bigwedge_{g=2}^m \overline{\eta}_{d-1,\boldsymbol{r}_g^\dagger}(y_g+1,y_{g-1}-1) \biggr) \end{aligned} \end{align}\] with \(F_s(x, z) = \begin{cases} x = z & \text{if s = 1_{R_L}}\\ \bot & \text{otherwise} \end{cases}\) for all \(\varphi_L(L)\)-reaching \(s \in R_L\).

We are now ready to define the formula \(\overline{\chi}_{d,e}\): \[\begin{align} \overline{\chi}_{d,e}(x,x',y',x) & = & \bigvee_{\substack{q\in[0,\left|O_L\right|]\\ m_0, \dots, m_{q-1}\geq 1 \wedge m_q \geq 0:\\ q+m_0+\dots+m_q\leq 3\left|O_L\right|}} \quad \bigvee_{\substack{e_0,f_0,e_1,\dots,f_{q-1},e_q,f_q\in O_L\\ e_0=1_{O_L}\wedge\forall j\in[1,q]:e_j=e_{j-1}\circ f_{j-1}\\ e=e_q\circ f_q}}\\ && \exists x_1, \dots, x_{q+1}\exists x_0', \dots, x_q' \exists y_1, \dots, y_{q+1}\exists y_1', \dots, y_0'\\ &&\Biggl( \begin{aligned} x_0'\leq x_1<x_1'<x_2<\dots<x_q' \leq x_{q+1}<\\ y_{q+1} \leq y_q'<y_q<\dots<y_1'<y_1\leq y_0' \end{aligned}\wedge \\ &&\quad x_0'=x\wedge y_0'=y\wedge x_{q+1}=x'\wedge y_{q+1}=y'\wedge\\ &&\quad \bigwedge_{p=1}^q (x_p \leftrightsquigarrow y_p \wedge x_p' \leftrightsquigarrow y_p') \wedge\\ &&\quad \forall z \Bigl(\bigl(x \leq z < x' \wedge \bigwedge_{p=1}^q (z \neq x_p \wedge z \neq x_p')\bigr) \rightarrow \neg U(x, x', z)\Bigr) \wedge\\ &&\quad \bigwedge_{p=1}^q\theta_{d, e_p}(x_p+1,x_p',y_p',y_p-1) \wedge\\ &&\quad \alpha_{d, m_0, f_0}(x_0',x_1,y_1,y_0') \wedge \bigwedge_{p=1}^{q-1} \alpha_{d, m_p,f_p}(x_p'+1,x_{p+1},y_{p+1},y_p'-1) \wedge\\ &&\quad \Bigl( \begin{align}[t] \bigl(x_q' < x_{q+1} \wedge \alpha_{d, m_q, f_q}(x_q'+1,x_{q+1},y_{q+1},y_q'-1)\bigr) \vee\\ F'_{q, m_q, f_q}(x_q',x_{q+1})\Bigr) \Biggr) \end{align} \end{align}\] with \(F'_{q, m, f}(x, z) = \begin{cases} \top & \text{if q = 0}\\ x = z & \text{if q > 0, m = 0 and f = 1_{O_L}}\\ \bot & \text{otherwise} \end{cases}\) for all \(q \in [0, \left|O_L\right|]\), \(m \in [0, 3\left|O_L\right|]\) and \(f \in O_L\).

The inductive definition of \(\overline{\eta}_{d,r}^\uparrow\) is completely analogous to the definition of \(\eta_{d,r}\) in Section 5.3.5: we simply replace every occurrence of \(\eta_{d-1,r}\) by \(\overline{\eta}_{d-1,r}\) and every occurrence of \(\chi_{d,e}\) by \(\overline{\chi}_{d,e}\).

The inductive definition of \(\overline{\eta}_{d,r}\) is completely analogous to the definition of \(\eta_{d,r}\) in Section 5.3.5: we access the horizontal evaluation languages \(\mathcal{E}_{\varphi_L,r}\) for all \(\varphi_L(L)\)-reaching \(r\in R_L\) by making use of the sentence \(\nu_{\varphi, r}\) and the already defined \(\overline{\eta}_{d,r}^\uparrow\). ◻

Proof. Let \(L \subseteq \Sigma^\triangle\) be a weakly length-synchronous VPL that is not length-synchronous. According to Point 2 (b) of Proposition [prop32effectivity] one can effectively compute a quadruple \((k_0,l_0,k_0',l_0')\in\mathbb{N}_{>0}^4\) for which there exist \(\mathop{\mathrm{ext}}_{u, v}, \mathop{\mathrm{ext}}_{u', v'} \in \mathcal{O}(\Sigma^\triangle)\) such that

• \(|u|=k_0\), \(|v|=l_0\), \(|u'|=k_0'\), \(|v'|=l_0'\),

• \(\psi_L(\mathop{\mathrm{ext}}_{u, v}) = \psi_L(\mathop{\mathrm{ext}}_{u', v'})\) is a \(\varphi_L(L)\)-reaching idempotent,

• \(\Delta(u), \Delta(u') > 0\), and

• \(\frac{k_0}{l_0}=\frac{\mathopen{}\left|u\right|\mathclose{}}{\mathopen{}\left|v\right|\mathclose{}} \neq \frac{\mathopen{}\left|u'\right|\mathclose{}}{\mathopen{}\left|v'\right|\mathclose{}}=\frac{k_0'}{l_0'}\).

We can explicitly compute such \(\mathop{\mathrm{ext}}_{u, v}\) and \(\mathop{\mathrm{ext}}_{u', v'}\) by just doing an exhaustive search. This enables us to assume without loss of generality while maintaining effective computability that \(\Delta(u)=\Delta(u')\): indeed, in case \(\Delta(u)\not=\Delta(u')\), we can consider \(\mathop{\mathrm{ext}}_{u_1,v_1}=\mathop{\mathrm{ext}}_{u^{\Delta(u')},v^{\Delta(u')}}\) and \(\mathop{\mathrm{ext}}_{u_2,v_2}=\mathop{\mathrm{ext}}_{(u')^{\Delta(u)},(v')^{\Delta(u)}}\) satisfying the desired properties.

Let us now define Green’s relations on \(O_L\) (see [25]). Let us consider two elements \(x,y\) of \(O_L\).

• We write \(x \leq_{\mathfrak{J}}y\) whenever there are elements \(e,f\) of \(O_L\) such that \(x = e \circ y \circ f\). We write \(x \mathrel{\mathfrak{J}}y\) if \(x \leq_{\mathfrak{J}}y\) and \(y \leq_{\mathfrak{J}}x\). We write \(x <_{\mathfrak{J}}y\) if \(x \leq_{\mathfrak{J}}y\) and \(x \not\mathrel{\mathfrak{J}}y\).

• We write \(x \leq_{\mathfrak{R}}y\) whenever there is an element \(e\) of \(O_L\) such that \(x = y \circ e\). We write \(x \mathrel{\mathfrak{R}}y\) if \(x \leq_{\mathfrak{R}}y\) and \(y \leq_{\mathfrak{R}}x\).

• We write \(x \leq_{\mathfrak{L}}y\) whenever there is an element \(e\) of \(O_L\) such that \(x = e \circ y\). We write \(x \mathrel{\mathfrak{L}}y\) if \(x \leq_{\mathfrak{L}}y\) and \(y \leq_{\mathfrak{L}}x\).

• We write \(x \mathrel{\mathfrak{H}}y\) if \(x \mathrel{\mathfrak{R}}y\) and \(x \mathrel{\mathfrak{L}}y\).

Observe that because \(\Delta(u) = \Delta(u')\), we have that \(u v' \in \Sigma^\triangle\) and \(u' v \in \Sigma^\triangle\), so that we can consider the elements \(\mathop{\mathrm{ext}}_{u u u, v v' v} = \mathop{\mathrm{ext}}_{u, v} \circ \mathop{\mathrm{ext}}_{u, v'} \circ \mathop{\mathrm{ext}}_{u, v}\) and \(\mathop{\mathrm{ext}}_{u u' u, v v v} = \mathop{\mathrm{ext}}_{u, v} \circ \mathop{\mathrm{ext}}_{u', v} \circ \mathop{\mathrm{ext}}_{u, v}\) in \(\mathcal{O}(\Sigma^\triangle)\). These elements satisfy \(\psi_L(\mathop{\mathrm{ext}}_{u u u, v v' v}) \leq_{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{u, v})\) and \(\psi_L(\mathop{\mathrm{ext}}_{u u' u, v v v}) \leq_{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{u, v})\). We claim that we actually have \(\psi_L(\mathop{\mathrm{ext}}_{u u u, v v' v}) <_{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{u, v})\) and \(\psi_L(\mathop{\mathrm{ext}}_{u u' u, v v v}) <_{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{u, v})\). Indeed, assume we had \(\psi_L(\mathop{\mathrm{ext}}_{u u' u, v v v}) \mathrel{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{u, v})\). Set \(x = \psi_L(\mathop{\mathrm{ext}}_{u, v})\) and \(y = \psi_L(\mathop{\mathrm{ext}}_{u', v})\). By a classical property of Green’s relations (see [25]), since it would hold that \(x \circ y \circ x \leq_{\mathfrak{R}}x\) and \(x \circ y \circ x \mathrel{\mathfrak{J}}x\), we would have \(x \circ y \circ x \mathrel{\mathfrak{R}}x\) and dually, since it would hold that \(x \circ y \circ x \leq_{\mathfrak{L}}x\) and \(x \circ y \circ x \mathrel{\mathfrak{J}}x\), we would have \(x \circ y \circ x \mathrel{\mathfrak{L}}x\). Therefore, we would have \(x \circ y \circ x \mathrel{\mathfrak{H}}x\). By another classical result on Green’s relations [25], as \(x\) is an idempotent, its \(\mathrel{\mathfrak{H}}\)-class is a group, hence for \(\omega \in \mathbb{N}_{>0}\) the idempotent power of \(O_L\), we would have \((x \circ y \circ x)^\omega = x^\omega = x\) (as the only idempotent element in a group is the identity). This would finally entail that \(\psi_L(\mathop{\mathrm{ext}}_{(u u' u)^\omega, (v v v)^\omega}) = \psi_L(\mathop{\mathrm{ext}}_{(u u u)^\omega, (v v v)^\omega})\) is a \(\varphi_L(L)\)-reaching idempotent and \(\Delta((u u' u)^\omega) = \Delta((u u u)^\omega) > 0\) but \(\mathopen{}\left|(u u' u)^\omega\right|\mathclose{} \neq \mathopen{}\left|(u u u)^\omega\right|\mathclose{}\), a contradiction to the fact that \((\varphi_L, \psi_L)\) is \(\varphi_L(L)\)-weakly-length-synchronous. Symmetrically, we can prove that if we had \(\psi_L(\mathop{\mathrm{ext}}_{u u u, v v' v}) \mathrel{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{u, v})\), this would contradict the fact that \((\varphi_L, \psi_L)\) is \(\varphi_L(L)\)-weakly-length-synchronous.

We distinguish three cases. In each of these we prove that there exist \(k, l \in \mathbb{N}_{>0}, k \neq l\) such that \(\mathcal{L}_{k, l} \leq_{\mathrm{cd}}L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\), so that since \(L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})} \leq_{\mathrm{cd}}L\) (by Lemma [lemma32reduction32element]) and by transitivity of \(\leq_{\mathrm{cd}}\) we have \(\mathcal{L}_{k, l} \leq_{\mathrm{cd}}L\).

Case \(\mathopen{}\left|v\right|\mathclose{} = \mathopen{}\left|v'\right|\mathclose{}\).

In that case, we necessarily have \(\mathopen{}\left|u\right|\mathclose{} \neq \mathopen{}\left|u'\right|\mathclose{}\). Then, we can exploit the fact that matching \(u^3\) with \(v v' v\) or \(u u' u\) with \(v^3\) makes us fall down to a smaller \(\mathrel{\mathfrak{J}}\)-class to reduce \(\mathcal{L}_{3 \mathopen{}\left|u\right|\mathclose{}, 2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{}}\) to \(L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\). The constant-depth reduction works as follows on input \(w \in \Sigma^*\):

1. check if \(w = x y\) with \(x \in (ac^{3 \mathopen{}\left|u\right|\mathclose{} - 1} + ac^{2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{} - 1})^*\) and \(y \in (b_1 + b_2)^*\), reject if it’s not the case;

2. build \(x'\) by sending \(ac^{3 \mathopen{}\left|u\right|\mathclose{} - 1}\) to \(u^3\), \(ac^{2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{} - 1}\) to \(u u' u\) and \(y'\) by sending \(b_1\) to \(v^3\) and \(b_2\) to \(v v' v\);

3. accept whenever \(x' \# y' \in L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\).

This forms a valid reduction. Indeed, take a word \(w = x y\) with \(x \in (ac^{3 \mathopen{}\left|u\right|\mathclose{} - 1} + ac^{2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{} - 1})^n\) for \(n \in \mathbb{N}\) and \(y \in (b_1 + b_2)^m\) for \(m \in \mathbb{N}\) and consider \(x' \# y'\) produced by the reduction with \(x' \in (u^3 + u u' u)^n\) and \(y' \in (v^3 + v v' v)^m\). If \(w \in \mathcal{L}_{3 \mathopen{}\left|u\right|\mathclose{}, 2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{}}\), then it easily follows that \(x' \# y' \in L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\). Otherwise, if \(w \notin \mathcal{L}_{3 \mathopen{}\left|u\right|\mathclose{}, 2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{}}\), then either \(n \neq m\) and thus \(x' y'\) is not well-matched because \(\Delta(x') = n \cdot 3 \cdot \Delta(u)\) and \(\Delta(y') = m \cdot 3 \cdot \Delta(v)\), or \(n = m\) and thus \(x' y'\) is well-matched, so \(\mathop{\mathrm{ext}}_{x', y'} = \mathop{\mathrm{ext}}_{z_1', t_1'} \circ \cdots \circ \mathop{\mathrm{ext}}_{z_n', t_n'}\) with \(z_1', \ldots, z_n' \in \{u^3, u u' u\}\) and \(t_1', \ldots, t_n' \in \{v^3, v v' v\}\) such that there exists \(i \in [1, n]\) satisfying \(\mathop{\mathrm{ext}}_{z_i', t_i'} \in \{\mathop{\mathrm{ext}}_{u^3, v v' v}, \mathop{\mathrm{ext}}_{u u' u, v^3}\}\), thereby implying \[\psi_L(\mathop{\mathrm{ext}}_{x', y'}) \leq_{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{z_i', t_i'}) <_{\mathfrak{J}} \psi_L(\mathop{\mathrm{ext}}_{u, v}) \,\,\text{.}\] Our algorithm therefore outputs the pair \((k,l)=(3k_0,2k_0+k_0')\).

Case \(\mathopen{}\left|u\right|\mathclose{} = \mathopen{}\left|u'\right|\mathclose{}\).

This case is symmetric to the previous case. Our algorithm outputs the pair \((k,l)=(2l_0+l_0',3l_0)\).

Case \(\mathopen{}\left|u\right|\mathclose{} \neq \mathopen{}\left|u'\right|\mathclose{}\) and \(\mathopen{}\left|v\right|\mathclose{} \neq \mathopen{}\left|v'\right|\mathclose{}\).

Then, we can again exploit the fact that matching \(u^3\) with \(v v' v\) or \(u u' u\) with \(v^3\) makes us fall down to a smaller \(\mathrel{\mathfrak{J}}\)-class to reduce \(\mathcal{L}_{A \cdot B', A' \cdot B}\) where \(A = 3 \mathopen{}\left|u\right|\mathclose{}=3k_0\), \(A' = 2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{}=2k_0+k_0'\), \(B = 3 \mathopen{}\left|v\right|\mathclose{}=3l_0\) and \(B' = 2 \mathopen{}\left|v\right|\mathclose{} + \mathopen{}\left|v'\right|\mathclose{}=2l_0+l_0'\) to \(L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\). Indeed, we have \(A \cdot B' \neq A' \cdot B\) because otherwise we would have \[\begin{align} 3 \mathopen{}\left|u\right|\mathclose{} \cdot (2 \mathopen{}\left|v\right|\mathclose{} + \mathopen{}\left|v'\right|\mathclose{}) & = (2 \mathopen{}\left|u\right|\mathclose{} + \mathopen{}\left|u'\right|\mathclose{}) \cdot 3 \mathopen{}\left|v\right|\mathclose{}\\ 6 \mathopen{}\left|u\right|\mathclose{} \mathopen{}\left|v\right|\mathclose{} + 3 \mathopen{}\left|u\right|\mathclose{} \mathopen{}\left|v'\right|\mathclose{} & = 6 \mathopen{}\left|u\right|\mathclose{} \mathopen{}\left|v\right|\mathclose{} + 3 \mathopen{}\left|u'\right|\mathclose{} \mathopen{}\left|v\right|\mathclose{}\\ \mathopen{}\left|u\right|\mathclose{} \mathopen{}\left|v'\right|\mathclose{} & = \mathopen{}\left|u'\right|\mathclose{} \mathopen{}\left|v\right|\mathclose{} \,\,\text{.} \end{align}\] The constant-depth reduction works as follows on input \(w \in \Sigma^*\):

1. check if \(w = x y\) with \(x \in (ac^{A \cdot B' - 1} + ac^{A' \cdot B - 1})^*\) and \(y \in (b_1 + b_2)^*\), reject if it is not the case;

2. build \(x'\) by sending \(ac^{A \cdot B' - 1}\) to \((u^3)^{B'}\), \(ac^{A' \cdot B - 1}\) to \((u u' u)^B\) and \(y'\) by sending \(b_1\) to \((v^3)^{B'}\) and \(b_2\) to \((v v' v)^B\);

3. accept whenever \(x' \# y' \in L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\).

This forms a valid reduction. Indeed, take a word \(w = x y\) with \(x = z_1 \cdots z_n\) where \(n \in \mathbb{N}\) and \(z_1, \ldots, z_n \in \{ac^{A \cdot B' - 1}, ac^{A' \cdot B - 1}\}\) and \(y = t_1 \cdots t_m\) where \(m \in \mathbb{N}\) and \(t_1, \ldots, t_m \in \{b_1, b_2\}\). Consider \(x' \# y'\) produced by the reduction with \(x' = z_1' \cdots z_n'\) where \(z_1', \ldots, z_n' \in \{(u^3)^{B'}, (u u' u)^B\}\) and \(y' = t_1' \cdots t_m'\) where \(t_1', \ldots, t_m' \in \{(v^3)^{B'}, (v v' v)^B\}\). If \(w \in \mathcal{L}_{A \cdot B', A' \cdot B}\), then it easily follows that \(x' \# y' \in L_{\psi_L(\mathop{\mathrm{ext}}_{u, v})}\). Otherwise, if \(w \notin \mathcal{L}_{A \cdot B', A' \cdot B}\), three situations can occur.

• There exists \(i \in [1, \min\{n, m\}]\) such that \(z_1 \cdots z_{i - 1} t_{i - 1} \cdots t_1 \in \mathcal{L}_{A \cdot B', A' \cdot B}\) but it holds that \((z_i, t_i) \in \{(ac^{A \cdot B' - 1}, b_2), (ac^{A' \cdot B - 1}, b_1)\}\). Assume first \((z_i, t_i) = (ac^{A' \cdot B - 1}, b_1)\). In this case, let \(\tilde{x}' = (u u' u)^{B - 1} z_{i + 1}' \cdots z_n'\) and \(\tilde{y}' = t_n' \cdots t_{i + 1}' (v^3)^{B' - 1}\). If \(\Delta(\tilde{x}' \tilde{y}') \neq 0\), then \[\Delta(x' y') = \Delta(z_1' \cdots z_{i - 1}' (u u' u) v^3 t_{i - 1}' \cdots t_1') + \Delta(\tilde{x}' \tilde{y}') = \Delta(\tilde{x}' \tilde{y}') \neq 0 \,\,\text{,}\] thus \(x' y'\) is not well-matched. Otherwise, if \(\Delta(\tilde{x}' \tilde{y}') = 0\), we can show that \(\tilde{x}' \tilde{y}'\) is well-matched. Indeed, since \(u v \in \Sigma^\triangle\), for all \(j \in [1, \mathopen{}\left|u\right|\mathclose{}]\), we have \(\Delta(u_1 \cdots u_j) \geq 0\) and for all \(j \in [1, \mathopen{}\left|v\right|\mathclose{}]\), we have \(\Delta(v_j \cdots v_{\mathopen{}\left|v\right|\mathclose{}}) = -\Delta(u v_1 \cdots v_{j - 1}) \leq 0\). Similarly, since \(u' v' \in \Sigma^\triangle\), for all \(j \in [1, \mathopen{}\left|u'\right|\mathclose{}]\), we have \(\Delta(u'_1 \cdots u'_j) \geq 0\) and for all \(j \in [1, \mathopen{}\left|v'\right|\mathclose{}]\), we have \(\Delta(v'_j \cdots v'_{\mathopen{}\left|v'\right|\mathclose{}}) = -\Delta(u' v'_1 \cdots v'_{j - 1}) \leq 0\). This implies that for all \(j \in [1, \mathopen{}\left|\tilde{x}'\right|\mathclose{}]\), we have \(\Delta(\tilde{x}'_1 \cdots \tilde{x}'_j) \geq 0\) and for all \(j \in [1, \mathopen{}\left|\tilde{y}'\right|\mathclose{}]\), we have \(\Delta(\tilde{x}' \tilde{y}'_1 \cdots \tilde{y}'_{j - 1}) = -\Delta(\tilde{y}'_j \cdots \tilde{y}'_{\mathopen{}\left|\tilde{y}'\right|\mathclose{}}) \geq 0\). Therefore, \(\tilde{x}' \tilde{y}' \in \Sigma^\triangle\). Hence \(x' y'\) is well-matched and \[\mathop{\mathrm{ext}}_{x', y'} = \mathop{\mathrm{ext}}_{z_1' \cdots z_{i - 1}', t_{i - 1}' \cdots t_1'} \circ \mathop{\mathrm{ext}}_{z_i', t_i'} \circ \mathop{\mathrm{ext}}_{\tilde{x}', \tilde{y}'} \,\,\text{,}\] so that \[\psi_L(\mathop{\mathrm{ext}}_{x', y'}) \leq_{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{z_i', t_i'}) <_{\mathfrak{J}} \psi_L(\mathop{\mathrm{ext}}_{u, v}) \,\,\text{.}\]

  If we assume that \((z_i, t_i) = (ac^{A \cdot B' - 1}, b_2)\), then we prove in the same way that either \(x' y'\) is not well-matched or it is well-matched and \(\psi_L(\mathop{\mathrm{ext}}_{x', y'}) <_{\mathfrak{J}}\psi_L(\mathop{\mathrm{ext}}_{u, v})\).

• It holds that \(n < m\) and \(z_1 \cdots z_n t_n \cdots t_1 \in \mathcal{L}_{A \cdot B', A' \cdot B}\). This entails that \(\Delta(x' t_n' \cdots t_1') = \Delta(z_1' \cdots z_n' t_n' \cdots t_1') = 0\), so that \[\Delta(x' y') = \Delta(x' t_n' \cdots t_1') + \Delta(t_m' \cdots t_{n + 1}') = \Delta(t_m' \cdots t_{n + 1}') < 0\] because \(m > n\) and \(\Delta(v) < 0\) as well as \(\Delta(v') < 0\). Therefore, \(x' y'\) is not well-matched.

• It holds that \(n > m\) and \(z_1 \cdots z_m t_m \cdots t_1 \in \mathcal{L}_{A \cdot B', A' \cdot B}\). Symmetrically to the previous case, we can also show that then, \(x' y'\) is not well-matched.

Hence, our algorithm outputs the pair \((k,l)=(A\cdot B',A'\cdot B)=(3k_0(2l_0+l_0'),(2k_0+k_0')3l_0)\) in this last case. ◻

Proof of the Claim.. The proof of Theorem [thm:vpl:ext] shows that one can effectively compute DVPAs \(A_1\) and \(A_2\) such that \(L(A_1)=\varphi_1^{-1}(F_1)\) and \(L(A_2)=\varphi_2^{-1}(F_2)\). By [7] one can effectively decide if \(L(A_1)=L(A_2)\) by deciding \(L(A_1)\subseteq L(A_2)\) and \(L(A_2)\subseteq L(A_1)\). ◻

Proof of Proposition [prop32ext32alg]. By Theorem [thm:vpl:ext] we first compute from our DVPA \(A\) on the visibly pushdown alphabet \(\Sigma\) an \(\mathop{\mathrm{Ext}}\)-algebra \((R_A,O_A)\), a morphism \((\varphi_A,\psi_A)\colon(\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle))\to (R_A,O_A)\), and a subset \(F_A \subseteq R_A\) such that \(L(A) = \varphi_A^{-1}(F_A)\). For an \(\mathop{\mathrm{Ext}}\)-algebra \((R,O)\) define \(\#(R,O)=(\left|R\right|,\left|O\right|)\). Let \(\prec\subseteq(\mathbb{N}\times\mathbb{N})^2\) be the lexicographic order on \(\mathbb{N}\times\mathbb{N}\), i.e.\((i,j)\prec(k,l)\) if, and only if either \(i<k\), or \(i=k\) and \(j<l\).

Observe that since \((R_A, O_A)\) recognizes \(L\), we have that the syntactic \(\mathop{\mathrm{Ext}}\)-algebra \((R_L, O_L)\) of \(L\) divides \((R_A, O_A)\) by Proposition [prop:syntactic:recognizes], so that \(\#(R_L, O_L) \leq \#(R_A, O_A)\). In fact, we have that any \(\mathop{\mathrm{Ext}}\)-algebra \((R, O)\) having \([1, i]\) for \(i \in [1, \left|R_L\right|]\) as base set, satisfying \(\#(R, O) \leq \#(R_L, O_L)\) and recognizing \(L\) via a morphism \((\varphi, \psi)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (R, O)\) is a presentation of \((R_L, O_L)\) with \((\varphi, \psi)\) and \(F\) presentations of, respectively, \((\varphi_L, \psi_L)\) and \(\varphi_L(L)\). Indeed, since such an \(\mathop{\mathrm{Ext}}\)-algebra recognizes \(L\), by Proposition [prop:syntactic:recognizes] it is divided by \((R_L, O_L)\): this implies that \(\#(R_L, O_L) \leq \#(R, O)\), but as also \(\#(R, O) \leq \#(R_L, O_L)\), we have \(\#(R, O) = \#(R_L, O_L)\). The morphism \((\varphi, \psi)\) must be surjective, otherwise, by Lemma [lem:Surjective95recognition], \(\bigl(\varphi(\Sigma^\triangle), {\psi(\mathcal{O}(\Sigma^\triangle))|}_{\varphi(\Sigma^\triangle)} \bigr)\) would be a sub-\(\mathop{\mathrm{Ext}}\)-algebra of \((R, O)\) recognizing \(L\) such that \(\#\bigl(\varphi(\Sigma^\triangle), {\psi(\mathcal{O}(\Sigma^\triangle))|}_{\varphi(\Sigma^\triangle)} \bigr) < \#(R, O) = \#(R_L, O_L)\) while \((R_L, O_L)\) divides \(\bigl(\varphi(\Sigma^\triangle), {\psi(\mathcal{O}(\Sigma^\triangle))|}_{\varphi(\Sigma^\triangle)} \bigr)\), which is contradictory. Therefore, by Lemma [lem:Factorization95surjective95recognition], there is a surjective morphism \((\alpha, \beta)\colon (R, O) \to (R_L, O_L)\), that must be bijective, such that \(\varphi_L = \alpha \circ \varphi\), so that \((R, O)\) is a presentation of \((R_L, O_L)\) with \((\varphi, \psi)\) and \(F\) presentations of, respectively, \((\varphi_L, \psi_L)\) and \(\varphi_L(L)\).

Under the assumption that such an \(\mathop{\mathrm{Ext}}\)-algebra exists, we compute \((R_L, O_L)\), \((\varphi_L, \psi_L)\) and \(\varphi_L(L)\) by enumerating all the finitely many triples made of a finite \(\mathop{\mathrm{Ext}}\)-algebra \((R, O)\), a morphism \((\varphi,\psi)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle))\to(R,O)\) and a subset \(F \subseteq R\) such that \(R\) has \([1, i]\) for \(i \in [1, \left|R_A\right|]\) as base set and \(\#(R, O) \leq \#(R_A, O_A)\). For each of these we test whether \(\varphi^{-1}(F)=\varphi_A^{-1}(F_A)\), which is possible by the above claim and take \((R, O)\), \((\varphi, \psi)\) and \(F\) from a triple validating this test with \(\#(R, O)\) minimal with respect to \(\prec\).

It remains to prove that an \(\mathop{\mathrm{Ext}}\)-algebra \((R, O)\) having \([1, i]\) for \(i \in [1, \left|R_L\right|]\) as base set, satisfying \(\#(R, O) \leq \#(R_L, O_L)\) and recognizing \(L\) exists. Take any bijection \(\alpha\colon R_L \to [1, \left|R_L\right|]\). We define \(R\) to be the monoid with base set \([1, \left|R_L\right|]\) and operation defined by \(x \cdot y = \alpha\bigl(\alpha^{-1}(x) \alpha^{-1}(y)\bigr)\) for all \(x, y \in [1, \left|R_L\right|]\). This is a monoid because

• \(x \cdot \alpha(1_R) = \alpha\bigl(\alpha^{-1}(x) \alpha^{-1}(\alpha(1_R))\bigr) = \alpha(\alpha^{-1}(x)) = \alpha\bigl(\alpha^{-1}(\alpha(1_R)) \alpha^{-1}(x)\bigr) = \alpha(1_R) \cdot x\) for all \(x \in R\); and

• for all \(x, y, z \in R\), we have \[\begin{align} x \cdot (y \cdot z) & = \alpha \biggl( \alpha^{-1}(x) \alpha^{-1}\Bigl(\alpha\bigl(\alpha^{-1}(y) \alpha^{-1}(z)\bigr)\Bigr) \biggr)\\ & = \alpha\bigl(\alpha^{-1}(x) \alpha^{-1}(y) \alpha^{-1}(z)\bigr)\\ & = \alpha \biggl( \alpha^{-1}\Bigl(\alpha\bigl(\alpha^{-1}(x) \alpha^{-1}(y)\bigr)\Bigr) \alpha^{-1}(z) \biggr)\\ & = (x \cdot y) \cdot z \,\,\text{.} \end{align}\]

Define the function \(\beta\colon O_L \to R^R\) by \(\beta(f')(x) = \alpha\bigl(f'(\alpha^{-1}(x))\bigr)\) for all \(f' \in O_L\) and \(x \in R\). Set \(O\) to be the monoid with base set \(\beta(O_L)\) and with composition as operation. This is a monoid because

• \(\beta(1_O)(x) = \alpha\bigl(1_O(\alpha^{-1}(x))\bigr) = x = \mathrm{id}_R(x)\) for all \(x \in R\); and

• for all \(f', g' \in O_L\), \[\beta(f') \circ \beta(g')(x) = \alpha \Biggl( f' \biggl( \alpha^{-1} \Bigl( \alpha\bigl(g'(\alpha^{-1}(x))\bigr) \Bigr) \biggr) \Biggr) = \alpha\bigl(f' \circ g'(\alpha^{-1}(x))\bigr) = \beta(f' \circ g')(x)\] for all \(x \in R\), so that \(\beta(f') \circ \beta(g') \in O\).

Then \((R, O)\) is an \(\mathop{\mathrm{Ext}}\)-algebra, because for all \(r' \in R_L\), we have \[\beta(\mathrm{left}_{r'})(x) = \alpha\bigl(\mathrm{left}_{r'}(\alpha^{-1}(x))\bigr) = \alpha\bigl(\alpha^{-1}(\alpha(r')) \alpha^{-1}(x)\bigr) = \alpha(r') \cdot x = \mathrm{left}_{\alpha(r')}(x)\] for all \(x \in R\) and \(\beta(\mathrm{right}_{r'})(x) = \mathrm{right}_{\alpha(r')}(x)\) for all \(x \in R\), so that \(\mathrm{left}_{r}, \mathrm{right}_{r} \in O\) for all \(r \in R\) by surjectivity of \(\alpha\).

We now define \((\varphi, \psi)\colon (\Sigma^\triangle, \mathcal{O}(\Sigma^\triangle)) \to (R, O)\) as the unique morphism satisfying \(\varphi(c) = \alpha(\varphi_L(c))\) for all \(c \in \Sigma_\text{int}\) and \(\psi(\mathop{\mathrm{ext}}_{a, b}) = \beta(\psi_L(\mathop{\mathrm{ext}}_{a, b}))\) for all \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\) given by Proposition [ptn:Freeness95Ext-algebras]. It is easy to show that then, \(\varphi(w) = \alpha(\varphi_L(w))\) for all \(w \in \Sigma^\triangle\) by structural induction on \(w\). Hence, by injectivity of \(\alpha\), we have \[\begin{align} \varphi^{-1}\bigl(\alpha(\varphi_L(L))\bigr) & = \{w \in \Sigma^\triangle \mid \alpha(\varphi_L(w)) \in \alpha(\varphi_L(L))\}\\ & = \{w \in \Sigma^\triangle \mid \varphi_L(w) \in \varphi_L(L)\} = \varphi_L^{-1}(\varphi_L(L)) = L \,\,\text{,} \end{align}\] thus \((R, O)\) recognizes \(L\). ◻

Proof. Let \(\Sigma'\) be the alphabet that emerges from \(\Sigma\) by additionally declaring \(\#\) as an internal letter. We will construct an \(\mathop{\mathrm{Ext}}\)-algebra \((R',O')\) and a morphism \((\varphi',\psi')\colon(\Sigma'^\triangle,\mathcal{O}(\Sigma')^\triangle)\to(R',O')\) such that for some element \(r'\in R'\) we have \(L_e=\varphi'^{-1}(r')\).

We define \(R'=R\cup O\cup\{\bot\}\), for some fresh zero \(\bot\), where multiplication between two elements in \(R'\) is defined as follows:

• multiplication between two elements in \(R\) is inherited from the monoid \(R\);

• \(r\cdot f=\mathrm{left}_{r}\circ f\) and \(f\cdot r=\mathrm{right}_{r}\circ f\) for all \(r\in R\) and all \(f\in O\);

• \(\bot\) acts as a zero, i.e.\(\bot\cdot r'=r'\cdot\bot=\bot\) for all \(r'\in R'\);

• \(f\cdot g=\bot\) for all \(f,g\in O\).

Clearly the identity of \(R\) is the identity of \(R'\). Associativity is immediate except for products of the form \(r_1\cdot f\cdot r_2, r_1\cdot r_2\cdot f\), and \(f\cdot r_1\cdot r_2\), where \(f\in O\) and \(r_1,r_2\in R\). In the first case we have \[\begin{align} (r_1\cdot f)\cdot r_2 & = (\mathrm{left}_{r_1}\circ f)\cdot r_2 = \mathrm{right}_{r_2}\circ(\mathrm{left}_{r_1}\circ f) = (\mathrm{right}_{r_2}\circ\mathrm{left}_{r_1})\circ f\\ & = (\mathrm{left}_{r_1}\circ\mathrm{right}_{r_2})\circ f = r_1\cdot (\mathrm{right}_{r_2}\circ f) = r_1\cdot (f\cdot r_2) \,\,\text{.} \end{align}\] In the second case we have \[(r_1\cdot r_2)\cdot f = \mathrm{left}_{r_1 r_2}\circ f = (\mathrm{left}_{r_1}\circ\mathrm{left}_{r_2})\circ f = \mathrm{left}_{r_1}\circ(\mathrm{left}_{r_2}\circ f) = r_1\cdot(r_2\cdot f)\] and in the third case we have \[f\cdot (r_1\cdot r_2)=\mathrm{right}_{r_1r_2}\circ f= (\mathrm{right}_{r_2}\circ\mathrm{right}_{r_1})\circ f= \mathrm{right}_{r_2}\circ(\mathrm{right}_{r_1}\circ f)= (f\cdot r_1)\cdot r_2 \,\,\text{.}\] We define \(O'=(R')^{R'}\) which is clearly a monoid for composition and thus directly get that \((R', O')\) is an \(\mathop{\mathrm{Ext}}\)-algebra. Applying Proposition [ptn:Freeness95Ext-algebras], we define the morphism \[(\varphi',\psi')\colon (\Sigma'^\triangle,\mathcal{O}(\Sigma')^\triangle)\to(R',O')\] as the unique one satisfying \(\varphi'(c)=\varphi(c)\) for all \(c\in\Sigma_\text{int}\), \(\varphi'(\#)=\mathrm{id}_O\) and where for all \(a \in \Sigma_\text{call}\), \(b \in \Sigma_\text{ret}\), we have \[\psi'(\mathop{\mathrm{ext}}_{a,b})(x)= \begin{cases} \psi(\mathop{\mathrm{ext}}_{a,b})(x) & \text{if x\in R}\\ \psi(\mathop{\mathrm{ext}}_{a,b})\circ x & \text{if x\in O}\\ \bot & \text{otherwise (i.e.\;if x=\bot)} \end{cases}\] for all \(x\in R'\). It suffices to prove the following claim, which directly implies the desired equality \(\varphi'^{-1}(e)= \{u\#v\mid uv \in \Sigma^\triangle \text{ s.t.\;} \psi(\mathop{\mathrm{ext}}_{u,v})=e\}\). For all \(w\in\Sigma'^\triangle\) we have \[\varphi'(w)= \begin{cases} \varphi(w)& \text{ if w\in\Sigma^\triangle}\\ \psi(\mathop{\mathrm{ext}}_{u,v}) & \text{ if w=u\#v for some uv\in\Sigma^\triangle}\\ \bot & \text{ otherwise.} \end{cases}\] We prove it by structural induction on \(w\). The cases when \(w = \varepsilon\) or \(w=c\in\Sigma_\text{int}\) follow immediately from the definition of \(\varphi'\). In case \(w=\#=\varepsilon\#\varepsilon\), we have \(\varphi'(w)=\mathrm{id}_O=\psi(\mathop{\mathrm{ext}}_{\varepsilon,\varepsilon})\).

For the inductive step first assume \(w=aw'b\) for some \(w'\in\Sigma'^\triangle\). If \(w'\) is neither in \(\Sigma^\triangle\) nor of the form \(u\#v\) with \(uv \in \Sigma^\triangle\), then \(\varphi'(w') = \bot\) by induction hypothesis and thus \(\varphi'(w) = \psi'(\mathop{\mathrm{ext}}_{a,b})(\varphi'(w'))=\psi'(\mathop{\mathrm{ext}}_{a,b})(\bot) = \bot\) as required. If \(w'\in\Sigma^\triangle\), then \(\varphi'(w')=\varphi(w')\in R\) by induction hypothesis, and hence \(\varphi'(w)=\psi'(\mathop{\mathrm{ext}}_{a,b})(\varphi'(w'))=\psi'(\mathop{\mathrm{ext}}_{a,b})(\varphi(w'))= \psi(\mathop{\mathrm{ext}}_{a,b})(\varphi(w'))=\varphi(w)\) as required. If \(w'=u\#v\) with \(uv\in\Sigma^\triangle\), i.e.\(w = a u\#v b\), then \(\varphi'(w')=\psi(\mathop{\mathrm{ext}}_{u,v})\in O\) by induction hypothesis. Hence, we have \(\varphi'(w)=\psi'(\mathop{\mathrm{ext}}_{a,b})(\varphi'(w'))= \psi'(\mathop{\mathrm{ext}}_{a,b})(\psi(\mathop{\mathrm{ext}}_{u,v}))=\psi(\mathop{\mathrm{ext}}_{a,b})\circ\psi(\mathop{\mathrm{ext}}_{u,v})= \psi(\mathop{\mathrm{ext}}_{au,vb})\).

Finally assume \(w=xy\) for some \(x,y\in\Sigma'^\triangle\setminus\{\varepsilon\}\). The case when \(x\) or \(y\) is neither in \(\Sigma^\triangle\) nor of the form \(u\#v\) with \(uv \in \Sigma^\triangle\) is easily handled by applying the induction hypothesis and observing that \(\bot\) is a zero in \(R'\). Two other immediate cases are when both \(x\) and \(y\) are in \(\Sigma^\triangle\) and when both \(x\) and \(y\) are of the form \(u\#v\) with \(uv \in \Sigma^\triangle\). Consider the case when \(x\in\Sigma^\triangle\setminus\{\varepsilon\}\) and \(y=u\#v\) with \(uv \in \Sigma^\triangle\), hence \(w=xu\#v\). The induction hypothesis yields \(\varphi'(x)=\varphi(x)\in R\) and \(\varphi'(y)=\psi(\mathop{\mathrm{ext}}_{u,v})\in O\). We obtain \[\varphi'(xy)=\varphi'(x)\cdot\varphi'(y)= \varphi(x)\cdot \psi(\mathop{\mathrm{ext}}_{u,v})= \mathrm{left}_{\varphi(x)}\circ\psi(\mathop{\mathrm{ext}}_{u,v})=\psi(\mathop{\mathrm{ext}}_{xu,v})\] as required. Finally, let us treat the case when \(x=u\#v\) with \(uv\in\Sigma^\triangle\) and \(y\in\Sigma^\triangle\setminus\{\varepsilon\}\), i.e.\(w=u\#vy\). The induction hypothesis yields \(\varphi'(x)=\psi(\mathop{\mathrm{ext}}_{u,v})\in O\) and \(\varphi'(y)=\varphi(y)\in R\). We obtain \[\varphi'(xy)=\varphi'(x)\cdot\varphi'(y)= \psi(\mathop{\mathrm{ext}}_{u,v})\cdot\varphi(y)= \mathrm{right}_{\varphi(y)}\circ\psi(\mathop{\mathrm{ext}}_{u,v})=\psi(\mathop{\mathrm{ext}}_{u,vy})\] as required. ◻

Proof. We first compute a PDA \(A'\) accepting the same language as \(A\), i.e. \(L(A')=L(A)\). Let us assume without loss of generality that \(0,1\not\in\Sigma'\). We claim that from \(A'=(Q,\Sigma',\Gamma,\Omega,q_0,F,\bot)\) one can compute a PDA \(A''\) such that \[L(A'')=\{0^{|u|}\#1^{|v|}\mid u\#v\in L(A')\} \,\,\text{.}\] Indeed, the PDA \(A''\) can simply be computed as follows: we set \[A''=(Q\times\{0,1\},\{0,1,\#\},\Gamma,\Omega',\langle q_0,0\rangle,F\times\{1\},\bot) \,\,\text{,}\] where \(\Omega'\) is the union of \(\bigl\{(\langle p,i\rangle,i,X,\langle q,i\rangle,\alpha) \mathrel{\big|} i\in\{0,1\}, \exists c\in\Sigma' \setminus \{\#\} : (p,c,X,q,\alpha)\in\Omega\bigr\}\) and \(\{(\langle p,0\rangle,\#,X,\langle q,1\rangle,\alpha)\mid (p,\#,X,q,\alpha)\in\Omega\}\). Finally, we apply Parikh’s Theorem, cf. [29], which implies that the set \(\{(m,n)\in\mathbb{N}\times\mathbb{N}\mid 0^m\#1^n\in L(A'')\}=P(L(A))\) is effectively semilinear. ◻

Proof of Proposition [prop32quasi]. Let \(e\in O\). By Lemma [lemma32Le] we first compute a finite \(\mathop{\mathrm{Ext}}\)-algebra recoginizing \(L_e\), along with an associated morphism and subset. From the latter we can compute (by Theorem [thm:vpl:ext]) a DVPA \(A_e\) accepting \(L_e\). We then use Lemma [lemma32semilinear] to conclude that the set \[P(L_e) = \{(k,l)\in\mathbb{N}\times\mathbb{N}\mid \exists u\in\Sigma^k,v\in\Sigma^l : uv\in\Sigma^\triangle, \psi(\mathop{\mathrm{ext}}_{u,v})=e\}\] is effectively semilinear, and this holds for all \(e \in O\).

We make use of the folklore fact that semilinear sets are effectively closed under Boolean operations, cf. [30] for a recent study. To decide whether \((\varphi, \psi)\) is quasi-aperiodic, we go through all possible subsets \(U \subseteq O\): if it is a subsemigroup of \(O\) that is a non-trivial group, we compute the set \(\bigcap_{e\in U} P(L_e)\) and reject if it is non-empty (which is easy to check given a semilinear presentation of the set), otherwise we continue. If we were able to go through all those subsets without rejecting, we accept.

Thus, if \((\varphi,\psi)\) is not quasi-aperiodic we can find a subset \(U\subseteq O\) that contains a non-trivial group and output a pair \((k,l)\in \bigcap_{e\in U} P(L_e)\); it witnesses that \(\psi(\mathcal{O}(\Sigma^\triangle)^{k,l})\) is not aperiodic. ◻

Proof. First assume that \(\vec{x}_{i,j}\) and \(\vec{x}_{i',j'}\) are co-linear for all \(i,i'\in I\), \(j\in[0,t_i]\), and \(j'\in [0,t_{i'}]\). Let \((k,l),(k',l')\in S\). That is, \((k,l)=\vec{x}_{i,0}+ n_1\vec{x}_{i,1}+\dots+n_{t_i}\vec{x}_{i,t_i}\) and \((k',l')=\vec{x}_{i',0}+n_1'\vec{x}_{i',1}+\dots+n_{t_{i'}}'\vec{x}_{i',t_{i'}}\) for some \(i,i'\in I\) and some \(n_1,\dots,n_{t_i},n_1',\dots,n_{t_{i'}}'\in \mathbb{N}\). But due to pairwise co-linearity there exist \(\alpha,\alpha'\in\mathbb{Q}_{>0}\) such that \((k,l)=\alpha\vec{x}_{i,0}\) and \((k',l')=\alpha'\vec{x}_{i,0}\), thus implying \(\frac{k}{l}=\frac{k'}{l'}\).

Conversely assume that there exist two vectors \((k,l)=\vec{x}_{i,j}\) and \((k',l')=\vec{x}_{i',j'}\) that are not co-linear. In case this is possible when \(i\not= i'\) and \(j=j'=0\) we are done, since then \((k,l),(k',l')\in S\) and thus \(\frac{k}{l}\not=\frac{k'}{l'}\). Otherwise \(\vec{x}_{i,0}\) and \(\vec{x}_{i',0}\) are co-linear for all \(i,i'\in I\), so there must exist \(i\in I\) and \(j\in[0,t_i]\) such that \(\vec{x}_{i,0}\) and \(\vec{x}_{i,j}\) are not co-linear. Then \(\vec{x}_{i,0}\) and \(\vec{x}_{i,0}+\vec{x}_{i,j}\) are in \(S\) but also not co-linear: indeed, if \(\alpha\vec{x}_{i,0}=\vec{x}_{i,0}+\vec{x}_{i,j}\) for some \(\alpha\in\mathbb{Q}_{>0}\), then \(\vec{x}_{i,j}=(\alpha-1)\vec{x}_{i,0}\) with \(\alpha-1>0\) due to \(\vec{x}_{i,0},\vec{x}_{i,j}\in\mathbb{N}^2\setminus\{(0,0)\}\), a contradiction. Hence there exist \((k,l),(k',l')\in S\) that are not co-linear, and therefore \(\frac{k}{l}\not=\frac{k'}{l'}\). ◻

Proof of Proposition [prop32length32effectivity]. Let us fix the \(\mathop{\mathrm{Ext}}\)-algebra morphism \((\varphi,\psi)\colon (\Sigma^\triangle,\mathcal{O}(\Sigma^\triangle))\to(R,O)\), where \((R, O)\) is a finite \(\mathop{\mathrm{Ext}}\)-algebra and where \(F\subseteq R\).

Recall that over the alphabet \(\Sigma'\), obtained from \(\Sigma\) by declaring a fresh letter \(\#\) as internal, the language \[L_{e \uparrow} = \{u\#v\mid uv \in \Sigma^\triangle : \Delta(u) > 0, \psi(\mathop{\mathrm{ext}}_{u,v})=e\} = L_e \cap \{u\#v\mid uv \in \Sigma^\triangle : \Delta(u) > 0\}\] is given for all \(e \in O\). The language \(\{u\#v\mid uv \in \Sigma^\triangle : \Delta(u) > 0\}\) is a clearly a VPL. Thus, for all \(e \in O\), we have that the set \[P(L_{e \uparrow}) = \left\{(k,l)\in\mathbb{N}\times\mathbb{N}\mid \exists u\in\Sigma^k,v\in\Sigma^l : uv\in\Sigma^\triangle, \Delta(u) > 0, \psi(\mathop{\mathrm{ext}}_{u,v})=e\right\}\] is effectively semilinear: indeed, given \(e \in O\), using Lemma [lemma32Le] and Theorem [thm:vpl:ext], we can as in the proof of Point 2 (a) of Proposition [prop32effectivity] compute a DVPA \(A_e\) accepting \(L_e\); we then compute a DVPA \(A_{e \uparrow}\) accepting \(L_{e \uparrow} = L(A_e) \cap L(A)\) by using the effective construction given in [7] and finally use Lemma [lemma32semilinear] to conclude.

Observe that \((\varphi,\psi)\) is \(F\)-length-synchronous if, and only if, for each \(F\)-reaching idempotent \(e \in O\) for which \(P(L_{e\uparrow})\) is non-empty we have \(|\{\frac{k}{l}\mid (k,l)\in P(L_{e \uparrow})\}|=1.\) The latter condition is easily seen to be decidable by the characterization provided in Lemma [lemma32collinear]. Hence, for deciding if \((\varphi,\psi)\) is length-synchronous our algorithm verifies if for all \(F\)-reaching \(e\in O\) for which \(P(L_{e\uparrow})\) is non-empty we have \(|\{\frac{k}{l}\mid (k,l)\in P(L_{e \uparrow})\}|=1.\) On the other hand, if this verification fails, i.e. in case \((\varphi,\psi)\) is not \(F\)-length-synchronous, our algorithm outputs, again using the characterization of Lemma [lemma32collinear], a quadruple \((k,l,k',l')\in\mathbb{N}_{>0}^4\) such that for some \(F\)-reaching idempotent \(e\in O\) we have \((k,l),(k',l')\in P(L_{e\uparrow})\) and \(\frac{k}{l}\not=\frac{k'}{l'}\). ◻

Proof of Lemma [lemma32Ke]. Let \(\Sigma'\) be the alphabet that emerges from \(\Sigma \cup \overline{\Sigma}\) by additionally declaring \(\#\) as an internal letter. We will construct an \(\mathop{\mathrm{Ext}}\)-algebra \((R',O')\) and a morphism \((\varphi',\psi')\) from \((\Sigma'^\triangle,\mathcal{O}(\Sigma')^\triangle)\) to \((R',O')\) such that for some subset \(F \subseteq R'\) we have \(K_e=\varphi'^{-1}(F)\).

Let \(\overline{R} = \{\overline{r} \mid r \in R\}\). We define \(R' = R \cup \overline{R} \cup \mathfrak{P}(O^2) \setminus \emptyset \cup \{\bot, 1\}\), for some fresh zero \(\bot\) and identity \(1\), where multiplication between two elements in \(R'\) is defined as follows:

• for all \(r_1, r_2 \in R\), \[\begin{align} r_1 \cdot r_2 & = r_1 r_2 & \overline{r_1} \cdot r_2 & = \bot\\ \overline{r_1} \cdot \overline{r_2} & = \overline{r_2 r_1} & r_1 \cdot \overline{r_2} & = \bot \,\,\text{;} \end{align}\]

• for all \(r \in R\) and \(E \in \mathfrak{P}(O^2) \setminus \emptyset\), \[\begin{align} r \cdot E & = \{(\mathrm{left}_{r} \circ e_1, e_2) \mid (e_1, e_2) \in E\} & E \cdot r & = \bot\\ E \cdot \overline{r} & = \{(e_1, \mathrm{left}_{r} \circ e_2) \mid (e_1, e_2) \in E\} & \overline{r} \cdot E & = \bot \,\,\text{;} \end{align}\]

• for all \(E_1, E_2 \in \mathfrak{P}(O^2) \setminus \emptyset\), we have \(E_1 \cdot E_2 = \bot\);

• \(\bot\) acts as a zero, i.e.\(\bot\cdot r'=r'\cdot\bot=\bot\) for all \(r'\in R'\);

• \(1\) acts as an identity, i.e.\(1 \cdot r' = r' \cdot 1 = r'\) for all \(r'\in R'\).

Associativity is immediate except for products of the form \(\overline{r_1} \cdot \overline{r_2} \cdot \overline{r_3}\), \(r_1 \cdot E \cdot \overline{r_2}\), \(r_1 \cdot r_2 \cdot E\) and \(E \cdot \overline{r_1} \cdot \overline{r_2}\), where \(E \in \mathfrak{P}(O^2) \setminus \emptyset\) and \(r_1, r_2, r_3 \in R\). In the first case we have \[(\overline{r_1} \cdot \overline{r_2}) \cdot \overline{r_3} = \overline{r_2 r_1} \cdot \overline{r_3} = \overline{r_3 r_2 r_1} = \overline{r_1} \cdot \overline{r_3 r_2} = \overline{r_1} \cdot (\overline{r_2} \cdot \overline{r_3}) \,\,\text{.}\] In the second case we have \[\begin{align} (r_1 \cdot E) \cdot \overline{r_2} & = \{(\mathrm{left}_{r_1} \circ e_1, e_2) \mid (e_1, e_2) \in E\} \cdot \overline{r_2}\\ & = \{(\mathrm{left}_{r_1} \circ e_1, \mathrm{left}_{r_2} \circ e_2) \mid (e_1, e_2) \in E\}\\ & = r_1 \cdot \{(e_1, \mathrm{left}_{r_2} \circ e_2) \mid (e_1, e_2) \in E\} = r_1 \cdot (E \cdot \overline{r_2}) \,\,\text{.} \end{align}\] In the third case we have \[\begin{align} (r_1 \cdot r_2) \cdot E & = \{(\mathrm{left}_{r_1 r_2} \circ e_1, e_2) \mid (e_1, e_2) \in E\}\\ & = \{(\mathrm{left}_{r_1} \circ \mathrm{left}_{r_2} \circ e_1, e_2) \mid (e_1, e_2) \in E\}\\ & = r_1 \cdot \{(\mathrm{left}_{r_2} \circ e_1, e_2) \mid (e_1, e_2) \in E\} = r_1 \cdot (r_2 \cdot E) \end{align}\] and in the fourth case we have \[\begin{align} E \cdot (\overline{r_1} \cdot \overline{r_2}) & = \{(e_1, \mathrm{left}_{r_2 r_1} \circ e_2) \mid (e_1, e_2) \in E\}\\ & = \{(e_1, \mathrm{left}_{r_2} \circ \mathrm{left}_{r_1} \circ e_2) \mid (e_1, e_2) \in E\}\\ & = \{(e_1, \mathrm{right}_{r_1} \circ e_2) \mid (e_1, e_2) \in E\} \cdot \overline{r_2} = (E \cdot \overline{r_1}) \cdot \overline{r_2} \,\,\text{.} \end{align}\] We define \(O'=(R')^{R'}\) which is clearly a monoid for composition and thus directly get that \((R', O')\) is a finite \(\mathop{\mathrm{Ext}}\)-algebra. Applying Proposition [ptn:Freeness95Ext-algebras], we define the morphism \((\varphi',\psi')\colon (\Sigma'^\triangle,\mathcal{O}(\Sigma')^\triangle)\to(R',O')\) as the unique one satisfying \(\varphi'(c)=\varphi(c)\) and \(\varphi'(\overline{c}) = \overline{\varphi(c)}\) for all \(c\in\Sigma_\text{int}\), \(\varphi'(\#)= \{(\psi(\mathop{\mathrm{ext}}_{\varepsilon, v}), \psi(\mathop{\mathrm{ext}}_{\varepsilon, v})) \mid v \in \Sigma^\triangle\}\) and where for all \(a, a' \in \Sigma_\text{call}\), \(b, b' \in \Sigma_\text{ret}\), we have \[\begin{align} \psi'(\mathop{\mathrm{ext}}_{a,b})(x) & = \begin{cases} \psi(\mathop{\mathrm{ext}}_{a,b})(1_R) & \text{if x=1}\\ \psi(\mathop{\mathrm{ext}}_{a,b})(x) & \text{if x\in R}\\ \bot & \text{otherwise} \end{cases}\\ \psi'(\mathop{\mathrm{ext}}_{\overline{b'},\overline{a'}})(x) & = \begin{cases} \overline{\psi(\mathop{\mathrm{ext}}_{a',b'})(1_R)} & \text{if x=1}\\ \overline{\psi(\mathop{\mathrm{ext}}_{a',b'})(x')} & \text{if x=\overline{x'} for x'\in R}\\ \bot & \text{otherwise} \end{cases}\\ \psi'(\mathop{\mathrm{ext}}_{a,\overline{a'}})(x) & = \begin{cases} \bigcup_{\substack{b \in \Sigma_\text{ret}\\z \in \Sigma^\triangle\\ (e_1, e_2) \in x}} \{(\psi(\mathop{\mathrm{ext}}_{a,bz}) \circ e_1, \psi(\mathop{\mathrm{ext}}_{a',bz}) \circ e_2)\} & \text{if x \in \mathfrak{P}(O^2) \setminus \emptyset}\\ \bot & \text{otherwise} \end{cases}\\ \psi'(\mathop{\mathrm{ext}}_{\overline{b'},b})(x) & = \bot \end{align}\] for all \(x\in R'\). Note that \((\varphi', \psi')\) is computable because \[\begin{align} \{(\psi(\mathop{\mathrm{ext}}_{\varepsilon, v}), \psi(\mathop{\mathrm{ext}}_{\varepsilon, v})) \mid v \in \Sigma^\triangle\} & = \{(\mathrm{right}_{\varphi(v)}, \mathrm{right}_{\varphi(v)}) \mid v \in \Sigma^\triangle\}\\ & = \{(\mathrm{right}_{r}, \mathrm{right}_{r}) \mid r \in R\} \end{align}\] and \[\begin{align} & \bigcup_{\substack{b \in \Sigma_\text{ret}\\z \in \Sigma^\triangle\\ (e_1, e_2) \in x}} \{(\psi(\mathop{\mathrm{ext}}_{a,bz}) \circ e_1, \psi(\mathop{\mathrm{ext}}_{a',bz}) \circ e_2)\}\\ = & \bigcup_{\substack{b \in \Sigma_\text{ret}\\z \in \Sigma^\triangle\\ (e_1, e_2) \in x}} \{(\mathrm{right}_{\varphi(z)} \circ \psi(\mathop{\mathrm{ext}}_{a,b}) \circ e_1, \mathrm{right}_{\varphi(z)} \circ \psi(\mathop{\mathrm{ext}}_{a',b}) \circ e_2)\}\\ = & \bigcup_{\substack{b \in \Sigma_\text{ret}\\r \in R\\ (e_1, e_2) \in x}} \{(\mathrm{right}_{r} \circ \psi(\mathop{\mathrm{ext}}_{a,b}) \circ e_1, \mathrm{right}_{r} \circ \psi(\mathop{\mathrm{ext}}_{a',b}) \circ e_2)\} \end{align}\] for all \(x \in \mathfrak{P}(O^2) \setminus \emptyset\) and \(a, a' \in \Sigma_\text{call}\).

Now define the set of pairs \(P = \{(u, u') \in \Sigma^* \times \Sigma^* \mid \exists v \in \Sigma^* : uv \in \Sigma^\triangle, u'v \in \Sigma^\triangle\}\); it is not difficult to check that for all \(w \in \Sigma'^*\), \(w \in \Sigma'^\triangle \cap \Sigma^* \# \overline{\Sigma}^*\) if and only if \(w = u\#\overline{u'}\) for \((u, u') \in P\). It suffices to prove the following claim, which directly implies the desired equality \[\begin{align} & \varphi'^{-1}(\{E \in \mathfrak{P}(O^2) \setminus \emptyset \mid (e, e) \in E\})\\ = & \{u\#\overline{u'} \mid (u, u') \in P, \exists v \in \Sigma^* : uv \in \Sigma^\triangle, u'v \in \Sigma^\triangle, \psi(\mathop{\mathrm{ext}}_{u, v}) = \psi(\mathop{\mathrm{ext}}_{u', v}) = e\}\\ = & \{u\#\overline{u'} \mid u, u' \in \Sigma^*, \exists v \in \Sigma^* : uv \in \Sigma^\triangle, u'v \in \Sigma^\triangle, \psi(\mathop{\mathrm{ext}}_{u,v})=\psi(\mathop{\mathrm{ext}}_{u',v})=e\} \,\,\text{.} \end{align}\] For all \(w\in\Sigma'^\triangle\) we have \[\varphi'(w)= \begin{cases} 1 & \text{if w = \varepsilon}\\ \varphi(w) & \text{if w\in\Sigma^\triangle\setminus\{\varepsilon\}}\\ \overline{\varphi(w')} & \text{if w = \overline{w'} for w' \in \Sigma^\triangle\setminus\{\varepsilon\}}\\ \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\} & \text{if w=u\#\overline{u'} for (u, u') \in P}\\ \bot & \text{otherwise.} \end{cases}\] We prove it by structural induction on \(w\). The cases when \(w = \varepsilon\) or \(w=c\in\Sigma_\text{int}\) or \(w=\overline{c}\in\overline{\Sigma}_\text{int}\) follow immediately from the definition of \(\varphi'\). In case \(w=\#=\varepsilon\#\varepsilon\), we have \[\varphi'(w)= \{(\psi(\mathop{\mathrm{ext}}_{\varepsilon, v}), \psi(\mathop{\mathrm{ext}}_{\varepsilon, v})) \mid v \in \Sigma^\triangle\} = \{(\psi(\mathop{\mathrm{ext}}_{\varepsilon, v}), \psi(\mathop{\mathrm{ext}}_{\varepsilon, v})) \mid v \in \Sigma^*, \varepsilon v \in \Sigma^\triangle\}\] as required.

For the inductive step first assume \(w=\alpha w' \beta\) for \(w'\in\Sigma'^\triangle\), \(\alpha \in \Sigma_\text{call}\cup \overline{\Sigma}_\text{call}\) and \(\beta \in \Sigma_\text{ret}\cup \overline{\Sigma}_\text{ret}\). If \(w'\) is neither in \(\Sigma^\triangle \cup \overline{\Sigma}^\triangle\) nor of the form \(u\#\overline{u'}\) with \((u, u') \in P\), then \(\varphi'(w') = \bot\) by induction hypothesis and thus \(\varphi'(w) = \psi'(\mathop{\mathrm{ext}}_{\alpha,\beta})(\varphi'(w')) = \psi'(\mathop{\mathrm{ext}}_{\alpha,\beta})(\bot) = \bot\) as required, since \(w\) is also neither in \(\Sigma^\triangle \cup \overline{\Sigma}^\triangle\) nor of the form \(u\#\overline{u'}\) with \((u, u') \in P\). If \(w' = \varepsilon\), then \(\varphi'(w') = 1\) and hence \[\begin{align} \varphi'(w) & = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta})(\varphi'(w'))\\ & = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta})(1)\\ & = \begin{cases} \psi(\mathop{\mathrm{ext}}_{\alpha, \beta})(1_R) = \varphi(w) & \text{if \alpha \in \Sigma_\text{call} and \beta \in \Sigma_\text{ret}}\\ \overline{\psi(\mathop{\mathrm{ext}}_{a, b})(1_R)} = \overline{\varphi(a b)} & \text{if \alpha = \overline{b} \in \overline{\Sigma}_\text{call} and \beta = \overline{a} \in \overline{\Sigma}_\text{ret}}\\ \bot & \text{otherwise} \end{cases} \end{align}\] as required, because \(w = \overline{b} \, \overline{a} = \overline{a b}\) in the second case. If \(w' \in \Sigma^\triangle \setminus \{\varepsilon\}\), then \(\varphi'(w') = \varphi(w') \in R\) by induction hypothesis, and hence \[\begin{align} \varphi'(w) = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta})(\varphi'(w')) & = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta})(\varphi(w'))\\ & = \begin{cases} \psi(\mathop{\mathrm{ext}}_{\alpha, \beta})(\varphi(w')) = \varphi(w) & \text{if \alpha \in \Sigma_\text{call} and \beta \in \Sigma_\text{ret}}\\ \bot & \text{otherwise} \end{cases} \end{align}\] as required. If \(w' \in \overline{\Sigma}^\triangle \setminus \{\varepsilon\}\), then \(w' = \overline{w''}\) for \(w'' \in \Sigma^\triangle \setminus \{\varepsilon\}\), so \(\varphi'(w') = \overline{\varphi(w'')} \in \overline{R}\) by induction hypothesis, and hence \[\begin{align} \varphi'(w) & = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta})(\varphi'(w'))\\ & = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta})(\overline{\varphi(w'')})\\ & = \begin{cases} \overline{\psi(\mathop{\mathrm{ext}}_{a, b})(\varphi(w''))} = \overline{\varphi(a w'' b)} & \text{if \alpha = \overline{b} \in \overline{\Sigma}_\text{call} and \beta = \overline{a} \in \overline{\Sigma}_\text{ret}}\\ \bot & \text{otherwise} \end{cases} \end{align}\] as required, because \(w = \overline{b} \, \overline{w''} \, \overline{a} = \overline{a w'' b}\) in the first case. If \(w'=u\#u'\) with \((u, u') \in P\), i.e.\(w = \alpha u\#u' \beta\), then \[\varphi'(w') = \{(\psi(\mathop{\mathrm{ext}}_{u,v'}), \psi(\mathop{\mathrm{ext}}_{u', v'})) \mid v' \in \Sigma^*, uv', u'v' \in \Sigma^\triangle\} \in \mathfrak{P}(O^2) \setminus \emptyset\] by induction hypothesis. Hence, we have \[\begin{align} \varphi'(w) & = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta})(\varphi'(w'))\\ & = \psi'(\mathop{\mathrm{ext}}_{\alpha, \beta}) (\{(\psi(\mathop{\mathrm{ext}}_{u,v'}), \psi(\mathop{\mathrm{ext}}_{u', v'})) \mid v' \in \Sigma^*, uv', u'v' \in \Sigma^\triangle\})\\ & = \bigcup_{\substack{b \in \Sigma_\text{ret}\\z \in \Sigma^\triangle}} \{(\psi(\mathop{\mathrm{ext}}_{au,v'bz}), \psi(\mathop{\mathrm{ext}}_{a'u',v'bz})) \mid v' \in \Sigma^*, uv', u'v' \in \Sigma^\triangle\}\\ & = \{(\psi(\mathop{\mathrm{ext}}_{au,v}), \psi(\mathop{\mathrm{ext}}_{a'u', v})) \mid v \in \Sigma^*, auv, a'u'v \in \Sigma^\triangle\} \end{align}\] if \(\alpha = a \in \Sigma_\text{call}\) and \(\beta = \overline{a'} \in \overline{\Sigma}_\text{ret}\) (where the last inclusion from right to left follows by considering the unique stair factorizations given by Lemma [lemma32ext] for the elements of each pair) and \(\varphi'(w) = \bot\) otherwise, as required.

Finally assume \(w=xy\) for some \(x, y \in \Sigma'^\triangle \setminus \{\varepsilon\}\). The case when \(x\) or \(y\) is neither in \(\Sigma^\triangle \cup \overline{\Sigma}^\triangle\) nor of the form \(u\#\overline{u'}\) with \((u, u') \in P\) is easily handled by applying the induction hypothesis and observing that \(\bot\) is a zero in \(R'\). Four other immediate cases are when both \(x\) and \(y\) are in \(\Sigma^\triangle\), when \(x\) is in \(\Sigma^\triangle\) and \(y\) in \(\overline{\Sigma}^\triangle\), when \(x\) is in \(\overline{\Sigma}^\triangle\) and \(y\) in \(\Sigma^\triangle\) and when both \(x\) and \(y\) are of the form \(u\#u'\) with \((u, u') \in P\). For the case when both \(x\) and \(y\) are in \(\overline{\Sigma}^\triangle\), we have that \(x = \overline{x'}\) and \(y = \overline{y'}\) for \(x', y' \in \Sigma^\triangle\), so that \(\varphi'(x) = \overline{\varphi(x')} \in \overline{R}\) and \(\varphi'(y) = \overline{\varphi(y')} \in \overline{R}\) by induction hypothesis, hence \[\varphi'(x y) = \varphi'(x) \cdot \varphi'(y) = \overline{\varphi(x')} \cdot \overline{\varphi(y')} = \overline{\varphi(y') \varphi(x')} = \overline{\varphi(y' x')}\] as required, because \(x y = \overline{x'} \, \overline{y'} = \overline{y' x'}\). Consider the case when \(x \in (\Sigma^\triangle \cup \overline{\Sigma}^\triangle) \setminus \{\varepsilon\}\) and \(y = u\#\overline{u'}\) with \((u, u') \in P\), hence \(w = x u\#\overline{u'}\). The induction hypothesis yields \[\varphi'(x) = \begin{cases} \varphi(x) \in R & \text{if x \in \Sigma^\triangle \setminus \{\varepsilon\}}\\ \overline{\varphi(x')} \in \overline{R} & \text{if x = \overline{x'} for x' \in \Sigma^\triangle \setminus \{\varepsilon\}} \end{cases}\] and \(\varphi'(y) = \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\} \in \mathfrak{P}(O^2) \setminus \emptyset\). We obtain \[\begin{align} \varphi'(w) & = \varphi'(x) \cdot \varphi'(y)\\ & = \varphi(x) \cdot \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\}\\ & = \{(\mathrm{left}_{\varphi(x)} \circ \psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\}\\ & = \{(\psi(\mathop{\mathrm{ext}}_{x u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, xuv, u'v \in \Sigma^\triangle\} \end{align}\] if \(x \in \Sigma^\triangle \setminus \{\varepsilon\}\) and \(\varphi'(w) = \overline{\varphi(x')} \cdot \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\} = \bot\) if \(x = \overline{x'}\) for \(x' \in \Sigma^\triangle \setminus \{\varepsilon\}\), as required. Eventually, let us treat the case when \(x = u\#u'\) with \((u, u') \in P\) and \(y \in (\Sigma^\triangle \cup \overline{\Sigma}^\triangle) \setminus \{\varepsilon\}\), hence \(w = u\#\overline{u'} y\). The induction hypothesis yields \(\varphi'(x) = \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\} \in \mathfrak{P}(O^2) \setminus \emptyset\) and \(\varphi'(y) = \begin{cases} \varphi(y) \in R & \text{if y \in \Sigma^\triangle \setminus \{\varepsilon\}}\\ \overline{\varphi(y')} \in \overline{R} & \text{if y = \overline{y'} for y' \in \Sigma^\triangle \setminus \{\varepsilon\}} \end{cases}\). We obtain \[\begin{align} \varphi'(w) & = \varphi'(x) \cdot \varphi'(y)\\ & = \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\} \cdot \overline{\varphi(y')}\\ & = \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \mathrm{left}_{\varphi(y')} \circ \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\}\\ & = \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{y' u', v})) \mid v \in \Sigma^*, uv, y'u'v \in \Sigma^\triangle\} \end{align}\] if \(y = \overline{y'}\) for \(y' \in \Sigma^\triangle \setminus \{\varepsilon\}\) and \(\varphi'(w) = \{(\psi(\mathop{\mathrm{ext}}_{u,v}), \psi(\mathop{\mathrm{ext}}_{u', v})) \mid v \in \Sigma^*, uv, u'v \in \Sigma^\triangle\} \cdot \varphi(y) = \bot\) if \(x \in \Sigma^\triangle \setminus \{\varepsilon\}\), as required, because \(\overline{y' u'} = \overline{u'} \, \overline{y'}\) in the first case. ◻