$\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}},\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}},\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}$,
and
$\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{1.0pt}{$\neq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\dot{=}$}}}}}{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{1.0pt}{$\neq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\dot{=}$}}}}}{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\neq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}}}}{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{0.6pt}{{\tiny$\neq$}}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}}}}$.
We also note that, for all words, adding a factor in
$\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}$
cannot change the accessibility in $\mathcal{A}$ since reading such a factor
has no effect on the stack or the current state. Additionally, reading several
$c$ in a row triggers a self loop and reading several $r$ is not possible in
$\mathcal{A}$. As a consequence, the base predicates mentioned in Example 4.2
hold, that is,
$\mathfrak{B}(\\{cr\\}\leqslant_{\mathcal{A}}\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}})$,
$\mathfrak{B}(\\{c\\}\leqslant_{\mathcal{A}}\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}})$,
$\mathfrak{B}(\\{r\\}\leqslant_{\mathcal{A}}\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}})$,
and
$\mathfrak{B}(\\{rc\\}\leqslant_{\mathcal{A}}\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{1.0pt}{$\neq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\dot{=}$}}}}}{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{1.0pt}{$\neq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\dot{=}$}}}}}{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\neq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}}}}{\makebox[5.60002pt]{\makebox[0.0pt]{\raisebox{0.6pt}{{\tiny$\neq$}}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}}}})$.
Yet, we have that $cr\leqslant_{\mathcal{A}}\varepsilon$ because
$(q_{0},cr,\bot)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to11.78pt{\vbox to2.68pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.3381pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}} {{}{}{}{}}
{{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@curveto{0.46236pt}{0.0pt}{0.69353pt}{1.1381pt}{1.15588pt}{1.1381pt}\pgfsys@curveto{1.49062pt}{1.1381pt}{1.77913pt}{0.58272pt}{2.0806pt}{0.0pt}\pgfsys@curveto{2.38205pt}{-0.5827pt}{2.67056pt}{-1.1381pt}{3.00531pt}{-1.1381pt}\pgfsys@curveto{3.34004pt}{-1.1381pt}{3.62856pt}{-0.58272pt}{3.93002pt}{0.0pt}\pgfsys@curveto{4.23148pt}{0.5827pt}{4.51999pt}{1.1381pt}{4.85474pt}{1.1381pt}\pgfsys@curveto{5.18947pt}{1.1381pt}{5.47798pt}{0.58272pt}{5.77945pt}{0.0pt}\pgfsys@curveto{6.0809pt}{-0.5827pt}{6.36942pt}{-1.1381pt}{6.70416pt}{-1.1381pt}\pgfsys@lineto{6.70416pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}^{*}(q_{2},\varepsilon,\langle
c,q_{0}\rangle)$ but
$(q_{0},\varepsilon,\bot)\mathrel{\raisebox{-2.0pt}[0.0pt][0.0pt]{
\leavevmode\hbox to11.78pt{\vbox
to13.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-6.83301pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}}
}}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@curveto{0.46236pt}{0.0pt}{0.69353pt}{1.1381pt}{1.15588pt}{1.1381pt}\pgfsys@curveto{1.49062pt}{1.1381pt}{1.77913pt}{0.58272pt}{2.0806pt}{0.0pt}\pgfsys@curveto{2.38205pt}{-0.5827pt}{2.67056pt}{-1.1381pt}{3.00531pt}{-1.1381pt}\pgfsys@curveto{3.34004pt}{-1.1381pt}{3.62856pt}{-0.58272pt}{3.93002pt}{0.0pt}\pgfsys@curveto{4.23148pt}{0.5827pt}{4.51999pt}{1.1381pt}{4.85474pt}{1.1381pt}\pgfsys@curveto{5.18947pt}{1.1381pt}{5.47798pt}{0.58272pt}{5.77945pt}{0.0pt}\pgfsys@curveto{6.0809pt}{-0.5827pt}{6.36942pt}{-1.1381pt}{6.70416pt}{-1.1381pt}\pgfsys@lineto{6.70416pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.94055pt}{-1.25pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\raisebox{-0.5pt}[0.0pt][0.0pt]{\scriptsize$/$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}^{*}(q_{2},\varepsilon,\langle
c,q_{0}\rangle)$.

###  4.2 Fixpoint Characterization of Languages and Inclusion

In order to formulate our inclusion algorithm, it remains to give an effective
computation of a query-basis. We do so through a fixpoint characterization of
the languages recognized by OPAs. We introduce the function Cat to construct
words that follow the runs of the given OPA. Iterating the Cat function
$n\in\mathbb{N}$ times captures all words of length up to $n$, and the
fixpoint of the iteration captures the entire language of a given OPA.

Let $\mathcal{A}=(Q,I,F,\Delta)$ be an OPA. Consider a vector of set of words
$\vec{X}$ that accesses its fields with two states $s,t\in Q$, and three
letters $a,b,c\in\widehat{\Sigma}\cup\\{\varepsilon\\}$. Intuitively, we aim
at constructing $\vec{X}$ iteratively such that, reading any
$w\in\vec{X}^{a,b,c}_{s,t}$ from the configuration $(s,wc,\alpha)$ where
$\alpha^{\top}=a$ allows reaching $(t,c,\beta)$ where $\beta^{\top}=b$ in
$\mathcal{A}$. We recall that $\bot^{\top}=\varepsilon$. As the base case, we
take $\vec{X}^{a,b,c}_{s,t}=\varepsilon$ when $a=b$ and $s=t$, otherwise
$\vec{X}^{a,b,c}_{s,t}=\varnothing$. Then, we introduce operations (more
explicitly, functions from sets of words to sets of words) that use the
transitivity of ${\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to11.78pt{\vbox to2.68pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.3381pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}} {{}{}{}{}}
{{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@curveto{0.46236pt}{0.0pt}{0.69353pt}{1.1381pt}{1.15588pt}{1.1381pt}\pgfsys@curveto{1.49062pt}{1.1381pt}{1.77913pt}{0.58272pt}{2.0806pt}{0.0pt}\pgfsys@curveto{2.38205pt}{-0.5827pt}{2.67056pt}{-1.1381pt}{3.00531pt}{-1.1381pt}\pgfsys@curveto{3.34004pt}{-1.1381pt}{3.62856pt}{-0.58272pt}{3.93002pt}{0.0pt}\pgfsys@curveto{4.23148pt}{0.5827pt}{4.51999pt}{1.1381pt}{4.85474pt}{1.1381pt}\pgfsys@curveto{5.18947pt}{1.1381pt}{5.47798pt}{0.58272pt}{5.77945pt}{0.0pt}\pgfsys@curveto{6.0809pt}{-0.5827pt}{6.36942pt}{-1.1381pt}{6.70416pt}{-1.1381pt}\pgfsys@lineto{6.70416pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}^{*}}$ in
$\mathcal{A}$ to extend the sets of $\vec{X}$. We first introduce:

$\texttt{CatShift}(\vec{X}^{a,b,c}_{s,t})=\left\\{\begin{array}[]{c@{~}|@{~}c}ub^{\prime}v\hfil\leavevmode\nobreak\
\vrule\leavevmode\nobreak\
&\begin{array}[]{l}a^{\prime},b^{\prime}\in\Sigma,\,q,s^{\prime},t^{\prime}\in
Q,\,u\in\vec{X}^{a,a^{\prime},b^{\prime}}_{s,s^{\prime}},\,v\in\vec{X}^{b^{\prime},b,c}_{t^{\prime},t},\\\
(s^{\prime},\langle
a^{\prime},q\rangle\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{
\leavevmode\hbox to11.78pt{\vbox
to13.02pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.64948pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$b^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(t^{\prime},\langle
b^{\prime},q\rangle\bot)\end{array}\end{array}\right\\}$

Essentially, CatShift adds $ub^{\prime}v$ to $\vec{X}^{a,b,c}_{s,t}$ when some
run over $u$ can be appended with $b^{\prime}$ thanks to a shift-transition,
and some run of $v$ requires starting with $b^{\prime}$ at the top of the
stack. Next, we introduce:

$\texttt{CatChain}(\vec{X}^{a,b,c}_{s,t})=\left\\{\begin{array}[]{c@{~}|@{~}c}ub^{\prime}v\hfil\leavevmode\nobreak\
\vrule\leavevmode\nobreak\
&\begin{array}[]{l}a^{\prime},b^{\prime},c^{\prime}\in\Sigma,\,q,s^{\prime},t^{\prime}\in
Q,\,u\in\vec{X}^{a,b,b^{\prime}}_{s,q},\,v\in\vec{X}^{b^{\prime},c^{\prime},c}_{s^{\prime},t^{\prime}},\\\
b\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}b^{\prime}\,\land\,(q,\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{
\leavevmode\hbox to11.78pt{\vbox
to13.02pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.64948pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$b^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(s^{\prime},\langle
b^{\prime},q\rangle\bot)\,\land\,(t^{\prime},\langle
c^{\prime},q\rangle\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{
\leavevmode\hbox to12.78pt{\vbox
to10.58pt{\pgfpicture\makeatletter\hbox{\hskip 0.7pt\lower-0.7pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.4pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.08115pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.17592pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$c$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(t,\bot)\end{array}\end{array}\right\\}$

Intuitively, CatChain adds $ub^{\prime}v$ to $\vec{X}^{a,b,c}_{s,t}$ when some
run over $u$ can be appended with $b^{\prime}$ thanks to a push-transition,
and some run of $v$ requires starting with $b^{\prime}$ at the top of the
stack. Additionally, $b^{\prime}$ is guaranteed to be removed from the stack
thanks to a pop-transition on the incoming letter $c$. Finally, we define:

$\texttt{Cat}(\vec{X}^{a,b,c}_{s,t})=\vec{X}^{a,b,c}_{s,t}\cup\texttt{CatShift}(\vec{X}^{a,b,c}_{s,t})\cup\texttt{CatChain}(\vec{X}^{a,b,c}_{s,t})$

Note that the function Cat never removes words from the sets of $\vec{X}$,
i.e., $\vec{X}^{a,b,c}_{s,t}\subseteq\texttt{Cat}(\vec{X}^{a,b,c}_{s,t})$.
Iterating the Cat function $n\in\mathbb{N}$ times allows us to extend the sets
of $\vec{X}$ to words of length at most $n$ that follow some run of
$\mathcal{A}$. In particular, Cat characterizes the language of $\mathcal{A}$
by $w\in L(\mathcal{A})$ if and only if
$w\in\texttt{Cat}^{*}(\vec{X}^{\varepsilon,\varepsilon,\varepsilon}_{q_{I},q_{F}})$
for some $q_{I}\in I$ and $q_{F}\in F$. This is formalized by the following
lemma.

######  Lemma 4.10.

Let $\mathcal{A}=(Q,I,F,\Delta)$ be an OPA, and let $\Gamma=\Sigma\times Q$.
Considering $\vec{U}^{a,b,c}_{s,t}=\varepsilon$ when $a=b$ and $s=t$,
otherwise $\vec{U}^{a,b,c}_{s,t}=\varnothing$. The following holds for all
$n>0$:

$\texttt{Cat}^{n}(\vec{U}^{a,b,c}_{s,t}){=}\big{\\{}u\mid(s,uc,\alpha){\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{
\leavevmode\hbox to11.78pt{\vbox to2.68pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.3381pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}} {{}{}{}{}}
{{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@curveto{0.46236pt}{0.0pt}{0.69353pt}{1.1381pt}{1.15588pt}{1.1381pt}\pgfsys@curveto{1.49062pt}{1.1381pt}{1.77913pt}{0.58272pt}{2.0806pt}{0.0pt}\pgfsys@curveto{2.38205pt}{-0.5827pt}{2.67056pt}{-1.1381pt}{3.00531pt}{-1.1381pt}\pgfsys@curveto{3.34004pt}{-1.1381pt}{3.62856pt}{-0.58272pt}{3.93002pt}{0.0pt}\pgfsys@curveto{4.23148pt}{0.5827pt}{4.51999pt}{1.1381pt}{4.85474pt}{1.1381pt}\pgfsys@curveto{5.18947pt}{1.1381pt}{5.47798pt}{0.58272pt}{5.77945pt}{0.0pt}\pgfsys@curveto{6.0809pt}{-0.5827pt}{6.36942pt}{-1.1381pt}{6.70416pt}{-1.1381pt}\pgfsys@lineto{6.70416pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}^{*}}(t,c,\beta),|u|=n,\alpha\in\varTheta_{a},\beta\in\varTheta_{b},au\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}},uc\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}},u^{\triangleright}=b\big{\\}}$

where, for all $a\in\widehat{\Sigma}$, the set of stack symbols
$\varTheta_{a}\subseteq\Gamma\cup\\{\bot\\}$ is defined by
$\varTheta_{a}=\\{\bot\\}$ if $a=\varepsilon$, and $\varTheta_{a}=\\{\langle
a,q\rangle\mid q\in Q\\}$ otherwise.

We continue Example 4.2, showing that Cat agrees with the considered query-
basis.

######  Example 4.11.

Let $\vec{U}^{a,b,c}_{s,t}=\varepsilon$ when $a=b$ and $s=t$, otherwise
$\vec{U}^{a,b,c}_{s,t}=\varnothing$. Thanks to Lemma 4.10, we have that
$L(\mathcal{B})=\texttt{Cat}^{*}(\vec{U}^{\varepsilon,\varepsilon,\varepsilon}_{p_{0},p_{0}})$.
First observe that
$c,r\notin\texttt{Cat}^{*}(\vec{U}^{\varepsilon,\varepsilon,\varepsilon}_{p_{0},p_{0}})$.
This comes from Lemma 4.10 and the fact that there is no run of $\mathcal{B}$
from $p_{0}$ to $p_{0}$ that reads a single letter. Next, we prove that
$cr,rc\in\texttt{Cat}^{2}(\vec{U}^{\varepsilon,\varepsilon,\varepsilon}_{p_{0},p_{0}})$.

We show that
$r\in\texttt{Cat}(\vec{U}^{\varepsilon,\varepsilon,c}_{p_{0},p_{1}})$ by
CatChain. Indeed, we have
$\varepsilon\in\vec{U}^{\varepsilon,\varepsilon,r}_{p_{0},p_{0}}$,
$\varepsilon\in\vec{U}^{r,r,c}_{p_{1},p_{1}}$,
$\varepsilon\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}r$,
and $(p_{0},\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to11.78pt{\vbox to10.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.01428pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$r$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(p_{1},\langle
r,p_{1}\rangle\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to12.78pt{\vbox to10.58pt{\pgfpicture\makeatletter\hbox{\hskip
0.7pt\lower-0.7pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.4pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.08115pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.17592pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$c$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(p_{1},\bot)$. Then,
$rc\in\texttt{Cat}^{2}(\vec{U}^{\varepsilon,\varepsilon,\varepsilon}_{p_{0},p_{0}})$
by CatChain since
$r\in\texttt{Cat}(\vec{U}^{\varepsilon,\varepsilon,c}_{p_{0},p_{1}})$,
$\varepsilon\in\vec{U}^{c,c,\varepsilon}_{p_{0},p_{0}}$,
$\varepsilon\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}c$,
and $(p_{1},\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to11.78pt{\vbox to10.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.17592pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$c$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(p_{0},\langle
c,p_{1}\rangle\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to12.78pt{\vbox to10.58pt{\pgfpicture\makeatletter\hbox{\hskip
0.7pt\lower-0.7pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.4pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.08115pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.05844pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$\varepsilon$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(p_{1},\bot)$.

We show that $r\in\texttt{Cat}(\vec{U}^{c,r,\varepsilon}_{p_{1},p_{0}})$ by
CatShift. Indeed, we have $\varepsilon\in\vec{U}^{c,c,r}_{p_{1},p_{1}}$,
$\varepsilon\in\vec{U}^{r,r,\varepsilon}_{p_{0},p_{0}}$, and $(p_{1},\langle
c,p\rangle\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to11.78pt{\vbox to10.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.01428pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$r$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(p_{0},\langle
r,p\rangle\bot)$, for all $p\in\\{p_{0},p_{1}\\}$. Then,
$cr\in\texttt{Cat}^{2}(\vec{U}^{\varepsilon,\varepsilon,\varepsilon}_{p_{0},p_{0}})$
by CatChain since
$\varepsilon\in\vec{U}^{\varepsilon,\varepsilon,c}_{p_{0},p_{0}}$,
$r\in\texttt{Cat}(\vec{U}^{c,r,\varepsilon}_{p_{1},p_{0}})$,
$\varepsilon\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}c$,
$(p_{0},\bot)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to11.78pt{\vbox to10.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.17592pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$c$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(p_{1},\langle
c,p_{0}\rangle\bot)$, and $(p_{0},\langle
r,p_{0}\rangle)\mathrel{\raisebox{-0.4pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to12.78pt{\vbox to10.58pt{\pgfpicture\makeatletter\hbox{\hskip
0.7pt\lower-0.7pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.4pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.08115pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.08115pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.05844pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\normalsize{\scriptsize$\varepsilon$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}(p_{0},\bot)$.

The computation of a query-basis for deciding whether $L_{1}$ is a subset of
$L_{2}$ consists of iterating Cat to collect enough words to obtain a vector
of finite bases with respect to the quasi-order $\preccurlyeq$ that is a
language abstraction of $L_{2}$. In other words, we search for
$n\in\mathbb{N}$ such that $\texttt{Cat}^{n}(\vec{X}^{a,b,c}_{s,t})$ is a
basis for $\lim_{k\mapsto\infty}\texttt{Cat}^{k}(\vec{U}^{a,b,c}_{s,t})$ with
respect to $\preccurlyeq$. The following lemma shows that when
$\mathfrak{B}(\texttt{Cat}^{n}(\vec{X}^{a,b,c}_{s,t})\preccurlyeq\texttt{Cat}^{n+1}(\vec{X}^{s,b,c}_{s,t}))$
holds for some $n\in\mathbb{N}$, then
$\mathfrak{B}(\texttt{Cat}^{n}(\vec{X}^{a,b,c}_{s,t})\preccurlyeq\lim_{k\mapsto\infty}\texttt{Cat}^{k}(\vec{X}^{a,b,c}_{s,t}))$
holds also, as long as the used quasi-order is chain-monotonic.

######  Lemma 4.12.

Let $\preccurlyeq$ be a chain-monotonic quasi-order over
$\widehat{\Sigma}^{*}$. For every $A=(Q,I,F,\Delta)$ and $\vec{X},\vec{Y}$
such that
$\mathfrak{B}(\vec{X}^{a,b,c}_{s,t}\preccurlyeq\vec{Y}^{a,b,c}_{s,t})$ holds
for all $s,t\in Q$ and all $a,b,c\in\Sigma\cup\\{\varepsilon\\}$, we have
$\mathfrak{B}(\texttt{Cat}(\vec{X}^{a,b,c}_{s,t})\preccurlyeq\texttt{Cat}(\vec{Y}^{a,b,c}_{s,t}))$
holds also for all $s,t\in Q$ and all $a,b,c\in\Sigma\cup\\{\varepsilon\\}$.

Input: an OPL $L_{1}$ given by the OPA $(Q,I,F,\Delta)$

Input: a language $L_{2}$ with a procedure deciding if $w\in L_{2}$

Input: a quasi-order $\preccurlyeq$ that is a language abstraction of $L_{2}$

Output: Returns ok if $L_{1}\subseteq L_{2}$ and ko otherwise

1

2Function  __:

3 let  _$\vec{U}$_ as  _$\vec{U}^{a,b,c}_{s,t}\coloneqq\varepsilon$_ if
$a=b\land s=t$ else $\vec{U}^{a,b,c}_{s,t}\coloneqq\varnothing$

4 $\vec{X}\coloneqq\vec{U}$

5 repeat

6 let  _$\vec{X}$_ as
$\vec{X}^{a,b,c}_{s,t}\coloneqq\texttt{Cat}(\vec{X}^{a,b,c}_{s,t})$

7 until
_$\mathfrak{B}(\vec{X}^{a,b,c}_{s,t}\preccurlyeq\texttt{Cat}(\vec{X}^{a,b,c}_{s,t}))$
for all $s,t\in Q$ and all $a,b,c\in\Sigma\cup\\{\varepsilon\\}$_

8 for each  _$(q_{I},q_{F})\in I\times F$_ do

9 for each
_$w\in\vec{X}^{\varepsilon,\varepsilon,\varepsilon}_{q_{I},q_{F}}$_ do

10 if  _$w\notin L_{2}$_ then return ko

11

12

13 return ok

Figure 7: Antichain inclusion algorithm.

Our inclusion algorithm is given in Figure 7. We can prove that it always
terminates thanks to the finite base property of language abstractions.
Additionally, its correctness is based on the following: Lemmas 4.10 and 4.12
ensure that the repeat-until loop computes a basis of the language $L_{1}$
given by an OPA while the language saturation ensures the completeness of this
basis with respect to the inclusion problem.

######  Theorem 4.13.

The algorithm from Figure 7 terminates and decides language inclusion.

We establish that our inclusion algorithm for OPAs is in ExpTime as a
consequence of Lemma 3.9, Remark 4.5, the facts that the vector $\vec{X}$
maintains polynomially many sets of words and the membership problem for OPAs
is in PTime (Remark 2.17). We recall that inclusion and universality are
ExpTime-C for both OPLs and VPLs [3, 43].

######  Theorem 4.14.

For all OPAs $\mathcal{A},\mathcal{B}$ with respectively
$n_{\mathcal{A}},n_{\mathcal{B}}$ states and $m$ input letters, the inclusion
algorithm from Figure 7 with ${\leqslant_{\mathcal{B}}}$ as the language
abstraction quasi-order decides if $L(\mathcal{A})\subseteq L(\mathcal{B})$ in
time $\mathcal{O}(m\times n_{\mathcal{A}})^{\mathcal{O}(m\times
n_{\mathcal{B}})^{\mathcal{O}(1)}}$.

##  5 Conclusion

We provided, for the first time, a syntactic congruence that characterizes
operator precedence languages (OPLs) in the following exact sense: for any
language $L$, the syntactic congruence has finitely many equivalence classes
if and only if $L$ is an OPL. Second, we gave sufficient conditions for a
quasi-order to yield an antichain algorithm for solving the universality and
language inclusion problems for nondeterministic automata. These conditions
are satisfied by our syntactic congruence, which, like any finite congruence,
is monotonic for structured words (i.e., chain-monotonic) and saturates its
language. This results in an exponential-time antichain algorithm for the
inclusion of operator precedence automata (OPAs), which is the optimal worst-
case complexity for the ExpTime-hard problem. This will allow efficient
symbolic implementations of antichain algorithms to be extended to OPLs.

The possibility of future research directions regarding OPLs is still vast.
One promising direction is to study OPAs from a runtime verification [6]
perspective. For example, extending the runtime approaches for visibly
pushdown automata [10, 49], one can study the monitor synthesis and right-
universality problems for OPAs to establish them as an expressively powerful
class of monitors. Also other methods developed for visibly pushdown automata
may be generalizable to OPAs based on our syntactic congruence, such as
learning algorithms [41].

While OPLs characterize the weakest known restrictions on stack operations
which enable decidability of the inclusion problem, one may try to push the
frontier of decidability by relaxing the restrictions on stack operations
further. Investigating similar restrictions in the context of observability
for counter automata can also provide new decidability results. For example,
[7] shows that hardcoding the counter operations (increments and decrements)
in the input letters yields decidable inclusion for one-counter automata.
Another natural direction is to investigate quantitative versions of OPAs, for
instance, through the addition of Presburger acceptance constraints, and to
identify decidable fragments thereof [27].

## References

  * [1] Rajeev Alur and Dana Fisman.  Colored nested words.  Formal Methods Syst. Des., 58(3):347–374, 2021.  URL: https://doi.org/10.1007/s10703-021-00384-2, doi:10.1007/s10703-021-00384-2.
  * [2] Rajeev Alur, Viraj Kumar, P. Madhusudan, and Mahesh Viswanathan.  Congruences for visibly pushdown languages.  In Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi, and Moti Yung, editors, Automata, Languages and Programming, 32nd International Colloquium,/pdf/0907.2130.pdf ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings, volume 3580 of Lecture Notes in Computer Science, pages 1102–1114. Springer, 2005.  URL: https://doi.org/10.1007/11523468_89, doi:10.1007/11523468\\_89.
  * [3] Rajeev Alur and P. Madhusudan.  Visibly pushdown languages.  In László Babai, editor, Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, pages 202–211. ACM, 2004.  URL: https://doi.org/10.1145/1007352.1007390, doi:10.1145/1007352.1007390.
  * [4] André Arnold.  A syntactic congruence for rational omega-language.  Theor. Comput. Sci., 39:333–335, 1985.  URL: https://doi.org/10.1016/0304-3975(85)90148-3, doi:10.1016/0304-3975(85)90148-3.
  * [5] Alessandro Barenghi, Stefano Crespi-Reghizzi, Dino Mandrioli, and Matteo Pradella.  Parallel parsing of operator precedence grammars.  Inf. Process. Lett., 113(7):245–249, 2013.  URL: https://doi.org/10.1016/j.ipl.2013.01.008, doi:10.1016/j.ipl.2013.01.008.
  * [6] Ezio Bartocci and Yliès Falcone, editors.  Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science.  Springer, 2018.  doi:10.1007/978-3-319-75632-5.
  * [7] Benedikt Bollig.  One-counter automata with counter observability.  In Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen, editors, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India, volume 65 of LIPIcs, pages 20:1–20:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.  URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2016.20, doi:10.4230/LIPIcs.FSTTCS.2016.20.
  * [8] Ahmed Bouajjani, Peter Habermehl, Lukás Holík, Tayssir Touili, and Tomás Vojnar.  Antichain-based universality and inclusion testing over nondeterministic finite tree automata.  In Oscar H. Ibarra and Bala Ravikumar, editors, Implementation and Applications of Automata, 13th International Conference, CIAA 2008, San Francisco, California, USA, July 21-24, 2008. Proceedings, volume 5148 of Lecture Notes in Computer Science, pages 57–67. Springer, 2008.  URL: https://doi.org/10.1007/978-3-540-70844-5_7, doi:10.1007/978-3-540-70844-5\\_7.
  * [9] Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, and Jean-François Raskin.  Antichain-based QBF solving.  In Tevfik Bultan and Pao-Ann Hsiung, editors, Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings, volume 6996 of Lecture Notes in Computer Science, pages 183–197. Springer, 2011.  URL: https://doi.org/10.1007/978-3-642-24372-1_14, doi:10.1007/978-3-642-24372-1\\_14.
  * [10] Véronique Bruyère, Marc Ducobu, and Olivier Gauwin.  Right-universality of visibly pushdown automata.  In Axel Legay and Saddek Bensalem, editors, Runtime Verification \- 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013\. Proceedings, volume 8174 of Lecture Notes in Computer Science, pages 76–93. Springer, 2013.  URL: https://doi.org/10.1007/978-3-642-40787-1_5, doi:10.1007/978-3-642-40787-1\\_5.
  * [11] Véronique Bruyère, Marc Ducobu, and Olivier Gauwin.  Visibly pushdown automata: Universality and inclusion via antichains.  In Adrian-Horia Dediu, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 7th International Conference, LATA 2013, Bilbao, Spain, April 2-5, 2013. Proceedings, volume 7810 of Lecture Notes in Computer Science, pages 190–201. Springer, 2013.  URL: https://doi.org/10.1007/978-3-642-37064-9_18, doi:10.1007/978-3-642-37064-9\\_18.
  * [12] Véronique Bruyère, Guillermo A. Pérez, and Gaëtan Staquet.  Learning realtime one-counter automata.  In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 244–262. Springer, 2022.  URL: https://doi.org/10.1007/978-3-030-99524-9_13, doi:10.1007/978-3-030-99524-9\\_13.
  * [13] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin.  Algorithms for omega-regular games with imperfect information${}^{\mbox{, }}$.  In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 287–302. Springer, 2006.  URL: https://doi.org/10.1007/11874683_19, doi:10.1007/11874683\\_19.
  * [14] Michele Chiari, Dino Mandrioli, and Matteo Pradella.  Operator precedence temporal logic and model checking.  Theor. Comput. Sci., 848:47–81, 2020.  URL: https://doi.org/10.1016/j.tcs.2020.08.034, doi:10.1016/j.tcs.2020.08.034.
  * [15] Christian Choffrut.  Minimizing subsequential transducers: a survey.  Theor. Comput. Sci., 292(1):131–143, 2003.  URL: https://doi.org/10.1016/S0304-3975(01)00219-5, doi:10.1016/S0304-3975(01)00219-5.
  * [16] Patrick Cousot and Radhia Cousot.  Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.  In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238–252. ACM, 1977.  URL: https://doi.org/10.1145/512950.512973, doi:10.1145/512950.512973.
  * [17] Stefano Crespi-Reghizzi, Giovanni Guida, and Dino Mandrioli.  Operator precedence grammars and the noncounting property.  SIAM J. Comput., 10(1):174–191, 1981.  URL: https://doi.org/10.1137/0210013, doi:10.1137/0210013.
  * [18] Stefano Crespi-Reghizzi, Violetta Lonati, Dino Mandrioli, and Matteo Pradella.  Toward a theory of input-driven locally parsable languages.  Theor. Comput. Sci., 658:105–121, 2017.  URL: https://doi.org/10.1016/j.tcs.2016.05.003, doi:10.1016/j.tcs.2016.05.003.
  * [19] Stefano Crespi-Reghizzi and Dino Mandrioli.  Algebraic properties of structured context-free languages: old approaches and novel developments.  CoRR, abs/0907.2130, 2009.  URL: http://arxiv.org/abs/0907.2130, arXiv:0907.2130.
  * [20] Stefano Crespi-Reghizzi and Dino Mandrioli.  Operator precedence and the visibly pushdown property.  J. Comput. Syst. Sci., 78(6):1837–1867, 2012.  URL: https://doi.org/10.1016/j.jcss.2011.12.006, doi:10.1016/j.jcss.2011.12.006.
  * [21] Stefano Crespi-Reghizzi, Dino Mandrioli, and David F. Martin.  Algebraic properties of operator precedence languages.  Inf. Control., 37(2):115–133, 1978.  URL: https://doi.org/10.1016/S0019-9958(78)90474-6, doi:10.1016/S0019-9958(78)90474-6.
  * [22] Stefano Crespi-Reghizzi and Matteo Pradella.  Beyond operator-precedence grammars and languages.  J. Comput. Syst. Sci., 113:18–41, 2020.  URL: https://doi.org/10.1016/j.jcss.2020.04.006, doi:10.1016/j.jcss.2020.04.006.
  * [23] Aldo de Luca and Stefano Varricchio.  Well quasi-orders and regular languages.  Acta Informatica, 31(6):539–557, 1994.  URL: https://doi.org/10.1007/BF01213206, doi:10.1007/BF01213206.
  * [24] Kyveli Doveri, Pierre Ganty, and Luka Hadži-Ðokić.  Antichains Algorithms for the Inclusion Problem Between $\omega$-VPL.  In TACAS’23: Proc. 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 13993 of LNCS. Springer, 2023.
  * [25] Kyveli Doveri, Pierre Ganty, and Nicolas Mazzocchi.  Forq-based language inclusion formal testing.  In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 109–129. Springer, 2022.  URL: https://doi.org/10.1007/978-3-031-13188-2_6, doi:10.1007/978-3-031-13188-2\\_6.
  * [26] Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato.  Inclusion testing of büchi automata based on well-quasiorders.  In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 3:1–3:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.3, doi:10.4230/LIPIcs.CONCUR.2021.3.
  * [27] Manfred Droste, Stefan Dück, Dino Mandrioli, and Matteo Pradella.  Weighted operator precedence languages.  Inf. Comput., 282:104658, 2022.  URL: https://doi.org/10.1016/j.ic.2020.104658, doi:10.1016/j.ic.2020.104658.
  * [28] Tomás Fiedor, Lukás Holík, Ondrej Lengál, and Tomás Vojnar.  Nested antichains for WS1S.  In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pages 658–674. Springer, 2015.  URL: https://doi.org/10.1007/978-3-662-46681-0_59, doi:10.1007/978-3-662-46681-0\\_59.
  * [29] Tomás Fiedor, Lukás Holík, Ondrej Lengál, and Tomás Vojnar.  Nested antichains for WS1S.  Acta Informatica, 56(3):205–228, 2019.  URL: https://doi.org/10.1007/s00236-018-0331-z, doi:10.1007/s00236-018-0331-z.
  * [30] Emmanuel Filiot, Olivier Gauwin, and Nathan Lhote.  Logical and algebraic characterizations of rational transductions.  Log. Methods Comput. Sci., 15(4), 2019.  URL: https://doi.org/10.23638/LMCS-15(4:16)2019, doi:10.23638/LMCS-15(4:16)2019.
  * [31] Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin.  An antichain algorithm for LTL realizability.  In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 263–277. Springer, 2009.  URL: https://doi.org/10.1007/978-3-642-02658-4_22, doi:10.1007/978-3-642-02658-4\\_22.
  * [32] Michael J. Fischer.  Some properties of precedence languages.  In Patrick C. Fischer, Seymour Ginsburg, and Michael A. Harrison, editors, Proceedings of the 1st Annual ACM Symposium on Theory of Computing, May 5-7, 1969, Marina del Rey, CA, USA, pages 181–190. ACM, 1969\.  URL: https://doi.org/10.1145/800169.805432, doi:10.1145/800169.805432.
  * [33] Robert W. Floyd.  Syntactic analysis and operator precedence.  J. ACM, 10(3):316–333, 1963.  URL: https://doi.org/10.1145/321172.321179, doi:10.1145/321172.321179.
  * [34] Pierre Ganty, Elena Gutiérrez, and Pedro Valero.  A congruence-based perspective on automata minimization algorithms.  In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 77:1–77:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.77, doi:10.4230/LIPIcs.MFCS.2019.77.
  * [35] Pierre Ganty, Francesco Ranzato, and Pedro Valero.  Language inclusion algorithms as complete abstract interpretations.  In Bor-Yuh Evan Chang, editor, Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11822 of Lecture Notes in Computer Science, pages 140–161. Springer, 2019.  URL: https://doi.org/10.1007/978-3-030-32304-2_8, doi:10.1007/978-3-030-32304-2\\_8.
  * [36] Pierre Ganty, Francesco Ranzato, and Pedro Valero.  Complete abstractions for checking language inclusion.  ACM Trans. Comput. Log., 22(4):22:1–22:40, 2021.  URL: https://doi.org/10.1145/3462673, doi:10.1145/3462673.
  * [37] Ferenc Gécseg.  Classes of tree languages determined by classes of monoids.  Int. J. Found. Comput. Sci., 18(6):1237–1246, 2007.  URL: https://doi.org/10.1142/S0129054107005285, doi:10.1142/S0129054107005285.
  * [38] Jelena Ignjatovic, Miroslav Ciric, and Stojan Bogdanovic.  Determinization of fuzzy automata with membership values in complete residuated lattices.  Inf. Sci., 178(1):164–180, 2008.  URL: https://doi.org/10.1016/j.ins.2007.08.003, doi:10.1016/j.ins.2007.08.003.
  * [39] Barbara Jobstmann and Roderick Bloem.  Optimizations for LTL synthesis.  In Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings, pages 117–124. IEEE Computer Society, 2006.  URL: https://doi.org/10.1109/FMCAD.2006.22, doi:10.1109/FMCAD.2006.22.
  * [40] Nils Klarlund, Anders Møller, and Michael I. Schwartzbach.  MONA implementation secrets.  Int. J. Found. Comput. Sci., 13(4):571–586, 2002.  URL: https://doi.org/10.1142/S012905410200128X, doi:10.1142/S012905410200128X.
  * [41] Viraj Kumar, P. Madhusudan, and Mahesh Viswanathan.  Minimization, learning, and conformance testing of boolean programs.  In Christel Baier and Holger Hermanns, editors, CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings, volume 4137 of Lecture Notes in Computer Science, pages 203–217. Springer, 2006.  URL: https://doi.org/10.1007/11817949_14, doi:10.1007/11817949\\_14.
  * [42] Martin Lange.  P-hardness of the emptiness problem for visibly pushdown languages.  Inf. Process. Lett., 111(7):338–341, 2011.  URL: https://doi.org/10.1016/j.ipl.2010.12.013, doi:10.1016/j.ipl.2010.12.013.
  * [43] Violetta Lonati, Dino Mandrioli, Federica Panella, and Matteo Pradella.  Operator precedence languages: Their automata-theoretic and logic characterization.  SIAM J. Comput., 44(4):1026–1088, 2015.  URL: https://doi.org/10.1137/140978818, doi:10.1137/140978818.
  * [44] Oded Maler and Ludwig Staiger.  On syntactic congruences for omega-languages.  Theor. Comput. Sci., 183(1):93–112, 1997.  URL: https://doi.org/10.1016/S0304-3975(96)00312-X, doi:10.1016/S0304-3975(96)00312-X.
  * [45] Dino Mandrioli and Matteo Pradella.  Generalizing input-driven languages: Theoretical and practical benefits.  Comput. Sci. Rev., 27:61–87, 2018.  URL: https://doi.org/10.1016/j.cosrev.2017.12.001, doi:10.1016/j.cosrev.2017.12.001.
  * [46] Jakub Michaliszyn and Jan Otop.  Learning deterministic visibly pushdown automata under accessible stack.  In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 of LIPIcs, pages 74:1–74:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.74, doi:10.4230/LIPIcs.MFCS.2022.74.
  * [47] Jean-Eric Pin.  Profinite methods in automata theory.  In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 of LIPIcs, pages 31–50. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009.  URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1856, doi:10.4230/LIPIcs.STACS.2009.1856.
  * [48] Francesco Pontiggia, Michele Chiari, and Matteo Pradella.  Verification of programs with exceptions through operator precedence automata.  In Radu Calinescu and Corina S. Pasareanu, editors, Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings, volume 13085 of Lecture Notes in Computer Science, pages 293–311. Springer, 2021.  URL: https://doi.org/10.1007/978-3-030-92124-8_17, doi:10.1007/978-3-030-92124-8\\_17.
  * [49] Grigore Rosu, Feng Chen, and Thomas Ball.  Synthesizing monitors for safety properties: This time with calls and returns.  In Martin Leucker, editor, Runtime Verification, 8th International Workshop, RV 2008, Budapest, Hungary, March 30, 2008. Selected Papers, volume 5289 of Lecture Notes in Computer Science, pages 51–68. Springer, 2008.  URL: https://doi.org/10.1007/978-3-540-89247-2_4, doi:10.1007/978-3-540-89247-2\\_4.
  * [50] Nguyen Van Tang and Hitoshi Ohsaki.  On model checking for visibly pushdown automata.  In Adrian-Horia Dediu and Carlos Martín-Vide, editors, Language and Automata Theory and Applications - 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012. Proceedings, volume 7183 of Lecture Notes in Computer Science, pages 408–419. Springer, 2012.  URL: https://doi.org/10.1007/978-3-642-28332-1_35, doi:10.1007/978-3-642-28332-1\\_35.
  * [51] Niklaus Wirth and Helmut Weber.  EULER: a generalization of ALGOL and it formal definition: Part 1\.  Commun. ACM, 9(1):13–25, 1966.  URL: https://doi.org/10.1145/365153.365162, doi:10.1145/365153.365162.
  * [52] Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin.  Antichains: A new algorithm for checking universality of finite automata.  In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 17–30. Springer, 2006.  URL: https://doi.org/10.1007/11817963_5, doi:10.1007/11817963\\_5.
  * [53] Martin De Wulf, Laurent Doyen, Nicolas Maquet, and Jean-François Raskin.  Antichains: Alternative algorithms for LTL satisfiability and model-checking.  In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 63–77. Springer, 2008.  URL: https://doi.org/10.1007/978-3-540-78800-3_6, doi:10.1007/978-3-540-78800-3\\_6.

##  Appendix A Omitted Proofs

#### Proposition 3.3

*Statement. $\approx$ is a chain-monotonic equivalence relation with finitely many classes.

######  Proof A.1.

The reflexivity, symmetry, and transitivity of ${\approx}$ is trivial, and the
chain-monotonicity follows from the definitions. We prove here that
${\approx}$ has finitely many equivalence classes.

Consider $w\in\widehat{\Sigma}^{+}$ for which $\lambda(w)$ is of the form
$a_{1}\dots a_{\ell}b_{1}\dots b_{m}c_{1}\dots c_{n}$ for some
$\ell,m,n\in\mathbb{N}$ and such that

$a_{1}\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}a_{2}\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}\ldots\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}a_{\ell}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}b_{1}\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}b_{2}\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}\ldots\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}b_{m}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}c_{1}\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}c_{2}\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}\ldots\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}c_{n}$

where $a_{i},b_{j},c_{k}\in\Sigma$ for all $i,j,k$. Let
$P_{w}^{\triangleleft}=\\{a_{1},b_{1}\\}\cup\\{a_{i+1}\mid
a_{i}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a_{i+1}\\}$
and $P_{w}^{\triangleright}=\\{b_{m},c_{n}\\}\cup\\{c_{i}\mid
c_{i}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}c_{i+1}\\}$.
By convention, we define
$P_{\varepsilon}^{\triangleleft}=P_{\varepsilon}^{\triangleright}=\\{\varepsilon\\}$.
We can define the profile of a word as
$P_{w}=(w^{\triangleleft},w^{\triangleright},P_{w}^{\triangleleft},P_{w}^{\triangleright})$.
Note that there are at most $|\widehat{\Sigma}|^{2}\times
2^{2|\widehat{\Sigma}|}$ distinct profiles. We show that $P_{x}=P_{y}$ implies
$x\approx y$ for all $x,y\in\widehat{\Sigma}^{*}$.

Let $x,y\in\widehat{\Sigma}^{*}$ be such that $P_{x}=P_{y}$. By the equality
of profiles, we directly get $x^{\triangleleft}=y^{\triangleleft}$ and
$x^{\triangleright}=y^{\triangleright}$. Now, let
$u_{0},v_{0}\in\widehat{\Sigma}^{*}$ be such that
$u_{0}x^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and
$x^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$.
Since $x$ and $y$ agree on the first and last letters, we $u_{0}$ and $v_{0}$
also satisfy
$u_{0}y^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and
$y^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$.
Now, let $u,v\in\widehat{\Sigma}^{*}$ be arbitrary. We want to show that
${{}^{u}[u_{0}xv_{0}]^{v}}$ iff ${{}^{u}[u_{0}yv_{0}]^{v}}$. Note that
$\lambda(x)$ is of the form given above, and since
$u_{0}x^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and
$x^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
the word $u_{0}xv_{0}$ is also of the same form. Moreover, since $y$ has the
same profile as $x$, the same holds for $u_{0}yv_{0}$ as well. In particular,
$P_{u_{0}xv_{0}}=P_{u_{0}yv_{0}}$. Then, if ${{}^{u}[u_{0}xv_{0}]^{v}}$, we
have
$u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}a$
for all $a\in P_{u_{0}xv_{0}}^{\triangleleft}$ and
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}v^{\triangleleft}$
for all $b\in P_{u_{0}xv_{0}}^{\triangleright}$. Since the same holds for
$u_{0}yv_{0}$, we get ${{}^{u}[u_{0}yv_{0}]^{v}}$. The other direction is
similar.

#### Theorem 3.6

*Statement. For every $L\subseteq\widehat{\Sigma}^{*}$, $\equiv_{L}$ is a chain-monotonic equivalence relation.

######  Proof A.2.

The reflexivity, symmetry, and transitivity of ${\equiv_{L}}$ is trivial. We
prove that ${\equiv_{L}}$ is chain-monotonic. Let us define the following
relation over $\widehat{\Sigma}^{*}$:

$x\sim y\iff\forall
u,v,u_{0},v_{0}\in\widehat{\Sigma}^{*}\begin{cases}\begin{array}[]{c}\big{(}u_{0}x^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}\land
x^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}\land{{}^{u}[u_{0}xv_{0}]^{v}}\big{)}\\\
\Downarrow\\\ \big{(}uu_{0}xv_{0}v\in L\Leftrightarrow uu_{0}yv_{0}v\in
L\big{)}\end{array}\end{cases}$

Recall that for every $x,y\in\widehat{\Sigma}^{*}$ we have $x\equiv_{L}y$ if
and only if both $x\approx y$ and $x\sim y$ holds, where ${\approx}$ is the
chain equivalence.

Let $x,y\in\widehat{\Sigma}^{*}$ such that $x\equiv_{L}y$, and let
$u,v,u_{0},v_{0}\in\widehat{\Sigma}^{*}$ such that
$u_{0}x^{\triangleleft},u_{0}y^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$x^{\triangleright}v_{0},y^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
${{}^{u}[u_{0}xv_{0}]^{v}}$, and ${{}^{u}[u_{0}yv_{0}]^{v}}$. We claim that
$uu_{0}xv_{0}v\equiv_{L}uu_{0}yv_{0}v$. Since the chain equivalence $\approx$
is chain-monotonic, we get $uu_{0}xv_{0}v\approx uu_{0}yv_{0}v$. Then, we only
need to show that $uu_{0}xv_{0}v\sim uu_{0}yv_{0}v$. In particular, for every
$u^{\prime},v^{\prime},u_{0}^{\prime},v_{0}^{\prime}\in\widehat{\Sigma}^{*}$
such that
$u_{0}^{\prime}(uu_{0}xv_{0}v)^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$(uu_{0}xv_{0}v)^{\triangleright}v_{0}^{\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
${{}^{u^{\prime}}[u_{0}^{\prime}uu_{0}xv_{0}vv_{0}^{\prime}]^{v^{\prime}}}$ we
have $u^{\prime}u_{0}^{\prime}uu_{0}xv_{0}vv_{0}^{\prime}v^{\prime}\in L$ iff
$u^{\prime}u_{0}^{\prime}uu_{0}yv_{0}vv_{0}^{\prime}v^{\prime}\in L$.

Let
$u^{\prime},v^{\prime},u_{0}^{\prime},v_{0}^{\prime}\in\widehat{\Sigma}^{*}$
be such that
$u_{0}^{\prime}(uu_{0}xv_{0}v)^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$(uu_{0}xv_{0}v)^{\triangleright}v_{0}^{\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
and
${{}^{u^{\prime}}[u_{0}^{\prime}uu_{0}xv_{0}vv_{0}^{\prime}]^{v^{\prime}}}$.
Furthermore, since $uu_{0}xv_{0}v\approx uu_{0}yv_{0}v$, we have
$u_{0}^{\prime}(uu_{0}yv_{0}v)^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$(uu_{0}yv_{0}v)^{\triangleright}v_{0}^{\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
and
${{}^{u^{\prime}}[u_{0}^{\prime}uu_{0}yv_{0}vv_{0}^{\prime}]^{v^{\prime}}}$.

Now, take $u_{0}^{\prime\prime}=u_{0}$,
$u^{\prime\prime}=u^{\prime}u_{0}^{\prime}u$, $v_{0}^{\prime\prime}=v_{0}$,
and $v^{\prime\prime}=vv_{0}^{\prime}v^{\prime}$. Observe that since
$x\equiv_{L}y$ and thanks to the choice of
$u,v,u_{0},v_{0}\in\widehat{\Sigma}^{*}$ given above, we have
$u_{0}^{\prime\prime}x^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$u_{0}^{\prime\prime}y^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$x^{\triangleright}v_{0}^{\prime\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
$y^{\triangleright}v_{0}^{\prime\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
${{}^{u^{\prime\prime}}[u_{0}^{\prime\prime}xv_{0}^{\prime\prime}]^{v^{\prime\prime}}}$,
and
${{}^{u^{\prime\prime}}[u_{0}^{\prime\prime}yv_{0}^{\prime\prime}]^{v^{\prime\prime}}}$.
Moreover,
$u^{\prime\prime}u_{0}^{\prime\prime}xv_{0}^{\prime\prime}v^{\prime\prime}\in
L$ iff
$u^{\prime\prime}u_{0}^{\prime\prime}yv_{0}^{\prime\prime}v^{\prime\prime}\in
L$, which is the same as
$u^{\prime}u_{0}^{\prime}uu_{0}xv_{0}vv_{0}^{\prime}v^{\prime}\in L$ iff
$u^{\prime}u_{0}^{\prime}uu_{0}yv_{0}vv_{0}^{\prime}v^{\prime}\in L$. Then,
$uu_{0}xv_{0}v\sim uu_{0}yv_{0}v$, and thus
$uu_{0}xv_{0}v\equiv_{L}uu_{0}yv_{0}v$. Therefore, ${\equiv_{L}}$ is chain-
monotonic.

#### Lemma 3.9

*Statement. For every OPA $\mathcal{A}$ with $n$ states and $m$ input letters, the structural congruence $\equiv_{\mathcal{A}}$ has at most $\mathcal{O}(m)^{\mathcal{O}(m\times n)^{\mathcal{O}(1)}}$ equivalence classes.

######  Proof A.3.

Suppose that $L$ is an OPL over $\widehat{\Sigma}$, and let
$\mathcal{A}=(Q,\\{q_{I}\\},F,\Delta)$ be a complete deterministic OPA with
the unique initial state $q_{I}$ such that $L(\mathcal{A})=L$. For every
$w\in\widehat{\Sigma}^{*}$ the functions $f_{w}$ and $g_{w}$ have a finite
input domain and a finite output range. The functions $\varPhi_{w}$ however,
have a finite input domain but an infinite output range. Nevertheless, only
the top of the output stack of $\varPhi_{w}$ is used in $\equiv_{\mathcal{A}}$
and, for all $w\in\widehat{\Sigma}^{*}$, the functions
$(q,\gamma)\mapsto(\varPhi(q,\gamma))^{\top}$ do have a finite output range.
Then, it is easy to see that $\equiv_{\mathcal{A}}$ has finitely many
equivalence classes, thanks to Proposition 3.3. In fact, it has at most:

$\big{(}|\widehat{\Sigma}|^{2}\times
2^{2|\widehat{\Sigma}|}\big{)}\times\big{(}2^{|Q|}\big{)}^{|Q|\times(|\Gamma|+1)}\times\big{(}2^{|Q|}\big{)}^{|Q|^{2}\times(|\Gamma|+1)}\times\big{(}2^{|\Gamma|+1}\big{)}^{|Q|\times(|\Gamma|+1)}$

equivalence classes. We recall that $\Gamma=\widehat{\Sigma}\times Q$. Hence,
in Landau’s notation we obtain
$|{\equiv_{\mathcal{A}}}|\leq\mathcal{O}(|\widehat{\Sigma}|)^{\mathcal{O}(|\Sigma|\times|Q|)^{\mathcal{O}(1)}}$.

#### Lemma 3.10

*Statement. For every OPA $\mathcal{A}$, the congruence $\equiv_{L(\mathcal{A})}$ is coarser than the congruence $\equiv_{\mathcal{A}}$.

######  Proof A.4.

We claim that every class of $\equiv_{\mathcal{A}}$ is contained in a class of
$\equiv_{L}$, thus establishing that $\equiv_{L}$ also has finitely many
equivalence classes. Consider $x,y,u,v,u_{0},v_{0}\in\widehat{\Sigma}^{*}$
such that $x\equiv_{\mathcal{A}}y$. Assume that
$u_{0}x^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$x^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
and ${{}^{u}[u_{0}xv_{0}]^{v}}$ hold. Then, since $x\approx y$, we have that
$u_{0}y^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$y^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$
and ${{}^{u}[u_{0}yv_{0}]^{v}}$ hold for all
$u,v,u_{0},v_{0}\in\widehat{\Sigma}^{*}$ as well. Next, we prove that all
configurations $(t,v,\theta)$ where $t\in Q$ and
$\theta\in\varPhi_{u}(q_{I},\bot)$ reachable from $(q_{I},uu_{0}xv_{0}v,\bot)$
is also reachable from $(q_{I},uu_{0}yv_{0}v,\bot)$. As the role of $x$ and
$y$ is symmetrical, it implies that $uu_{0}xv_{0}v\in L\Leftrightarrow
uu_{0}yv_{0}v\in L$. There are four cases, depending on the precedences
between
$u_{0}^{\triangleright}\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}x^{\triangleleft}$
and
$x^{\triangleright}\mathrel{\mathchoice{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[8.00003pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}v_{0}^{\triangleleft}$.

We have
$u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}u_{0}^{\triangleleft}$
by definition, and we consider only the case where
$u_{0}^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}x^{\triangleleft}$
and
$x^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}v_{0}^{\triangleleft}$,
as the other can be tackled similarly. From $(q_{I},uu_{0}xv_{0}v,\bot)$ all
configurations that $\mathcal{A}$ can reach after reading $u$ are of the from
$(q_{u},u_{0}xv_{0}v,\theta_{u}\cdot\bot)$ where $q_{u}\in f_{u}(q_{I},\bot)$
and $\theta_{u}\in\varPhi_{u}(q_{I},\bot)$, because
$\varepsilon\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}u^{\triangleleft}$.
After reading $u_{0}$, $\mathcal{A}$ can reach configurations of the form
$(q_{u_{0}},xv_{0}v,\theta_{u_{0}}\cdot\theta_{u}\cdot\bot)$ where
$q_{u_{0}}\in f_{u_{0}}(q_{u},\bot)$ and
$\theta_{u_{0}}\in\varPhi_{u_{0}}(q_{u},\bot)$, due to
$u^{\triangleright}u_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$.
Observe that we have been able to abstract the stack $\theta_{u}\cdot\bot$
with $\bot$ thanks to
$u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}u_{0}^{\triangleleft}$.
Then $\mathcal{A}$ must performs pop-transitions since
$u_{0}x^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$.
After popping $\theta_{u_{0}}$, the reachable configurations are of the form
$(p_{u_{0}},xv_{0}v,\theta_{u}\cdot\bot)$ where $p_{u_{0}}\in
g_{u_{0}}(q_{u},q_{u_{0}},\bot)$. Observe that, the stack is clear from the
computation of $u_{0}$ due to
$u_{0}^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}x^{\triangleleft}$,
in fact ${{}^{u}[u_{0}]^{x}}$. All configurations that $\mathcal{A}$ can reach
after reading $x$ are of the form
$(q_{x},v_{0}v,\theta_{x}\cdot\theta_{u}\cdot\bot)$ where $q_{x}\in
f_{x}(p_{u_{0}},\bot)$ and $\theta_{x}\in\varPhi_{x}(p_{u_{0}},\bot)$, because
$u^{\triangleright}x\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$.
Once again, we have been able to abstract the stack $\theta_{u}\cdot\bot$ with
$\bot$, this time it is thanks to
$u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}x^{\triangleleft}$.
Now, as we are dealing with
$x^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}v_{0}^{\triangleleft}$,
$\mathcal{A}$ must clear the stack from the computation of $x$ after reading
$v_{0}$, and so the function $g_{x}$ must be called after reading $g_{v_{0}}$.
We emphasize that the stack $\theta_{x}\cdot\theta_{u}\cdot\bot$ cannot be
abstracted by $\bot$. However, since
$x^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
it can be abstracted by its top symbol, denoted by $\theta_{x}^{\top}$.
Observe that, in the case where
$x^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}v_{0}^{\triangleleft}$,
we must have $\theta_{x}\neq\bot$, and thus the top of $\theta_{x}$ indeed
correspond to the top of $\theta_{x}\cdot\theta_{u}\cdot\bot$. Let
$\theta^{\prime}_{x}$ be defined by
$\theta_{x}=\theta_{x}^{\top}\theta^{\prime}_{x}$. After reading $v_{0}$,
$\mathcal{A}$ can reach configurations of the from
$(q_{v_{0}},v,\theta_{v_{0}}\cdot\theta^{\prime}_{x}\cdot\theta_{u}\cdot\bot)$.
where $q_{v_{0}}\in f_{v_{0}}(q_{x},\theta_{x}^{\top})$ and
$\theta_{v_{0}}\in\varPhi_{v_{0}}(q_{x},\theta_{x}^{\top})$, because
$x^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$.
It is worth noticing that the top of the stack $\theta_{x}^{\top}$ may have
been modified while reading $v_{0}$, due to
$x^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}v_{0}^{\triangleleft}$.
For instance, it is the case when $v_{0}$ is a single letter. Then
$\mathcal{A}$ must performs pop-transitions since
$v_{0}v^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$.
After popping $\theta_{v_{0}}$, the reachable configurations are of the form
$(p_{v_{0}},v,\theta^{\prime}_{x}\cdot\theta_{u}\cdot\bot)$ where
$p_{v_{0}}\in g_{v_{0}}(q_{x},q_{v_{0}},\theta_{x}^{\top})$. Observe that, the
stack is clear from the computation of $v_{0}$ due to
$v_{0}^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}v^{\triangleleft}$.
Moreover, $g_{v_{0}}$ pops the modified top of $\theta_{x}$. More pop-
transitions must be performed since
$xv^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$.
After popping $\theta^{\prime}_{x}$, the reachable configurations are of the
form $(p_{x},v,\theta_{u}\cdot\bot)$ where
$p_{x}=g_{x}(p_{u_{0}},p_{v_{0}},\bot)$. This time, the stack is clear from
the computation of $x$ due to
$x^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}v^{\triangleleft}$.
We emphasize that $g_{x}$ is used as it have been defined for. Indeed, $g_{x}$
takes as parameters the current state $p_{v_{0}}$ and the parameters on which
$f_{x}$ have been previously called, i.e., $p_{u_{0}}$ and $\bot$. By taking
$t=p_{x}$ and $\theta=\theta_{u}\cdot\bot$, we established that
$(q_{I},uu_{0}xv_{0}v,\bot)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{
\leavevmode\hbox to11.78pt{\vbox to2.68pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.3381pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}} {{}{}{}{}}
{{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@curveto{0.46236pt}{0.0pt}{0.69353pt}{1.1381pt}{1.15588pt}{1.1381pt}\pgfsys@curveto{1.49062pt}{1.1381pt}{1.77913pt}{0.58272pt}{2.0806pt}{0.0pt}\pgfsys@curveto{2.38205pt}{-0.5827pt}{2.67056pt}{-1.1381pt}{3.00531pt}{-1.1381pt}\pgfsys@curveto{3.34004pt}{-1.1381pt}{3.62856pt}{-0.58272pt}{3.93002pt}{0.0pt}\pgfsys@curveto{4.23148pt}{0.5827pt}{4.51999pt}{1.1381pt}{4.85474pt}{1.1381pt}\pgfsys@curveto{5.18947pt}{1.1381pt}{5.47798pt}{0.58272pt}{5.77945pt}{0.0pt}\pgfsys@curveto{6.0809pt}{-0.5827pt}{6.36942pt}{-1.1381pt}{6.70416pt}{-1.1381pt}\pgfsys@lineto{6.70416pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}^{*}(t,v,\theta)$.
As a direct consequence of $x\equiv_{\mathcal{A}}y$, making the above
reasoning with $y$ instead of $x$ results dealing with identical intermediate
sets of states and sets of stacks. Hence, we proved that all configurations of
the from $(t,v,\theta)$ where $t\in Q$ and $\theta\in\varPhi_{u}(q_{I},\bot)$
reachable from $(q_{I},uu_{0}xv_{0}v,\bot)$ is also reachable from
$(q_{I},uu_{0}yv_{0}v,\bot)$.

#### Lemma 3.12

*Statement. For every $L\subseteq\widehat{\Sigma}^{*}$, if $\equiv_{L}$ has finite index then $L$ is a $\widehat{\Sigma}$-OPL.

######  Proof A.5.

Consider a language $L\subseteq\widehat{\Sigma}^{*}$ such that $\equiv_{L}$
has finitely many equivalence classes. We construct a deterministic OPA that
recognizes $L$ and whose states are based on the equivalence classes of
${\equiv_{L}}$. Given $w\in\widehat{\Sigma}^{*}$, we denote $[w]$ its
equivalence class with respect to ${\equiv_{L}}$. We construct
$\mathcal{A}=(Q,\\{q_{0}\\},F,\Delta)$ with the set of states
$Q=\\{([u],[v])\mid u,v\in\widehat{\Sigma}^{*}\\}$, the initial state
$q_{0}=([\varepsilon],[\varepsilon])$, the set of accepting states
$F=\\{([\varepsilon],[w])\mid w\in L\\}$, and the $\widehat{\Sigma}$-driven
transition function $\Delta\colon
Q\times\Sigma\times(\Gamma^{+}\cup\\{\bot\\})\rightarrow
Q\times(\Sigma\cup\\{\varepsilon\\})\times(\Gamma^{+}\cup\\{\bot\\})$, where
$\Gamma=\Sigma\times Q$, is defined as follows: $\Delta$ maps
$(([u],[v]),a,\langle b,([u^{\prime}],[v^{\prime}])\rangle\theta)$ to
$(([a],[\varepsilon]),\varepsilon,\langle a,([u],[v])\rangle\langle
b,([u^{\prime}],[v^{\prime}])\rangle\theta)$ if
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}a$,
it returns $(([uva],[\varepsilon]),\varepsilon,\langle
a,([u^{\prime}],[v^{\prime}])\rangle\theta)$ if
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}a$,
and $(([u^{\prime}],[v^{\prime}uv]),a,\theta)$ if
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$.

##### Invariants.

We show that the automaton $\mathcal{A}$ satisfies the following invariants
after reaching the state $([u],[v])\in Q$ from the initial state $q_{0}$:

  1. 1.

The top of the stack is $u^{\triangleright}$ if $u\neq\varepsilon$, and $\bot$
otherwise.

  2. 2.

All outgoing on $a\in\Sigma$ satisfies
$va\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and $v\neq\varepsilon\Rightarrow
v^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$.

  3. 3.

$u\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}$.

  4. 4.

$u^{\triangleright}v\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$
and $v\neq\varepsilon\Rightarrow
u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}v^{\triangleleft}$.

We prove all invariants together by induction on the length of the run from
$q_{0}$ that reaches the state $([u],[v])\in Q$. The run starts in
$q_{0}=([\varepsilon],[\varepsilon])$ which trivially satisfies all
invariants. By induction we assume the invariants to hold for all run of
length $n>0$. Let $([u],[v])$ be the state reached after $n$ transitions,
$a\in\Sigma$ be the incoming letter and $(b,([u^{\prime}],[v^{\prime}]))$ be
the top of the stack.

If
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}a$,
the automaton $\mathcal{A}$ performs a push-transition to reach
$([a],[\varepsilon])$, which satisfies (1) by definition of push-transition.
The invariants (2, 3, 4) hold trivially.

If
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}a$,
the automaton $\mathcal{A}$ performs a shift-transition to reach
$([uva],[\varepsilon])$, which satisfies (1) by definition of the shift-
transition. Since a shift-transition is triggered, the stack is not $\bot$. By
the induction hypothesis, (1) ensures that $u^{\triangleright}=b$ and (2)
ensures that
$va\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$.
Consequently and because
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}a$,
we have that
$uva\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}$,
i.e., (3) is preserved. The invariants (2, 4) hold trivially.

If
$b\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$,
the automaton $\mathcal{A}$ performs a pop-transition to reach
$([u^{\prime}],[v^{\prime}uv])$. Since a pop-transition is triggered, the
stack is not $\bot$. By the induction hypothesis, (1) ensures that
$u^{\triangleright}=b$, thus
$u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$.
In particular $u\neq\varepsilon$, and thus $u^{\triangleleft}\in\Sigma$.
Additionally, the induction hypothesis gives us that
$va\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and $v\neq\varepsilon\Rightarrow
v^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$
by (2). We have that
$uva\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
because
$u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$,
$u\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}$
and ${{}^{u}[v]^{a}}$ from (2, 3, 4). Finally, (4) ensures that
$u^{\triangleright}v\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$.

Since $([u^{\prime}],[v^{\prime}])$ is on the stack, there exists a strict
prefix of the current run that ends in $([u^{\prime}],[v^{\prime}])$ and such
that popping $(b,([u^{\prime}],[v^{\prime}]))$ recovers its stack. By the
induction hypothesis on such smaller run, (1) ensures that if
$u^{\prime}=\varepsilon$ then the stack is $\bot$ otherwise the top is
$u^{\prime\triangleright}$, and (3) ensures that
$u^{\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}$.
So, (1) and (3) are directly preserved. Continuing the induction hypothesis,
(2) ensures that
$v^{\prime}u^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and (4) ensures that
$u^{\prime\triangleright}v^{\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$
and $v^{\prime}\neq\varepsilon\Rightarrow
u^{\prime\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}v^{\prime\triangleleft}$.
In the case where $u^{\prime}\neq\varepsilon$ and $v^{\prime}=\varepsilon$, we
get that $v^{\prime}uv\neq\varepsilon\Rightarrow
u^{\prime\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}(v^{\prime}uv)^{\triangleleft}$
since
$u^{\prime\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}u^{\triangleleft}$
as the automaton $\mathcal{A}$ pushed $([u^{\prime}],[v^{\prime}])$ on the
stack while reading $u^{\triangleleft}$. The other cases are immediate.
Moreover,
$u^{\prime\triangleright}v^{\prime}uv\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$
comes as we established that
$u^{\prime\triangleright}v^{\prime}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
$u\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}$
,
$u^{\triangleright}v\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
and
$u^{\prime\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}u^{\triangleleft}$.
Hence (4) is preserved. For the invariant (2), we established that
$uva\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and
$v^{\prime}u^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
which implies that
$v^{\prime}uva\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$.
We also established that $v\neq\varepsilon\Rightarrow
v^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$
and
$u^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$,
which implies that
$(v^{\prime}uv)^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$.
In particular, the invariant (2) is preserved.

##### Determinism.

For all states $([a],[\varepsilon]),([b],[\varepsilon])\in Q$ reachable in
$\mathcal{A}$ with a push-transition, if $a\neq b$ then $a\not\approx b$ which
implies that $a\not\equiv_{L}b$. Reciprocally, if $a\equiv_{L}b$ then
$a\approx b$, which implies that $a=b$.

For all states $([u_{1}],[v_{1}]),([u_{2}],[v_{2}])\in Q$ and all
$a\in\Sigma$, let
$([u_{1}v_{1}a],[\varepsilon]),([u_{2}v_{2}a],[\varepsilon])$ be two states
reachable in $\mathcal{A}$ with a shift-transition. We show that, if
$u_{1}\equiv_{L}u_{2}$ and $v_{1}\equiv_{L}v_{2}$ then
$u_{1}v_{2}a\equiv_{L}u_{2}v_{2}a$. If $v_{1}=\varepsilon$, then
$v_{2}\equiv_{L}v_{1}$ implies $v_{2}=\varepsilon$. Also
$u_{1}\equiv_{L}u_{2}$ implies $u_{1}a\equiv_{L}u_{2}a$ by chain-monotonicity
of ${\equiv_{L}}$. Otherwise, if $v_{1}\neq\varepsilon$, then
$v_{2}\equiv_{L}v_{1}$ implies $v_{2}\neq\varepsilon$. Furthermore,
${{}^{u_{1}}[v_{1}]^{a}}$ and ${{}^{u_{1}}[v_{2}]^{a}}$, since $u_{1}\approx
u_{2}$ and the invariants (2) and (4) hold. In particular,
$u_{1}^{\triangleright}v_{2}a\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}}$.
By chain-monotonicity of ${\equiv_{L}}$, we have $v_{1}\equiv_{L}v_{2}$
implies $u_{1}v_{1}a\equiv_{L}u_{1}v_{2}a$, and $u_{1}\equiv_{L}u_{2}$ implies
$u_{1}v_{2}a\equiv_{L}u_{2}v_{2}a$ Hence, $u_{1}v_{1}a\equiv_{L}u_{2}v_{2}a$,
by transitivity of ${\equiv_{L}}$.

For all states $([u_{1}],[v_{1}])$, $([u_{2}],[v_{2}])$,
$([u^{\prime}_{1}],[v^{\prime}_{1}])$, $([u^{\prime}_{2}],[v^{\prime}_{2}])\in
Q$, we let $([u^{\prime}_{1}],[v^{\prime}_{1}u_{1}v_{1}])$ and
$([u^{\prime}_{2}],[v^{\prime}_{2}u_{2}v_{2}])$ be two states reachable in
$\mathcal{A}$ with a pop-transition. We show that, if $u_{1}\equiv_{L}u_{2}$,
$v_{1}\equiv_{L}v_{2}$, and $v^{\prime}_{1}\equiv_{L}v^{\prime}_{2}$, then
$v^{\prime}_{1}u_{1}v_{1}\equiv_{L}v^{\prime}_{2}u_{2}v_{2}$. As a direct
consequence of the invariants, we have that
${{}^{v^{\prime}_{1}u_{1}}[u_{1}]^{\varepsilon}}$,
${{}^{v^{\prime}_{1}u_{1}}[u_{2}]^{\varepsilon}}$,
${{}^{\varepsilon}[v^{\prime}_{1}u_{1}v_{2}]^{\varepsilon}}$,
${{}^{\varepsilon}[v^{\prime}_{1}u_{2}v_{2}]^{\varepsilon}}$,
${{}^{\varepsilon}[v^{\prime}_{1}]^{u_{2}v_{2}}}$, and
${{}^{\varepsilon}[v^{\prime}_{2}]^{u_{2}v_{2}}}$. Additionally,
$v^{\prime}_{1}u^{\triangleleft},v^{\prime}_{1}u_{2}^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$
and
$u_{1}^{\triangleright}v_{2},u_{2}^{\triangleright}v_{2}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$.
By chain-monotonicity of ${\equiv_{L}}$, we have $v_{1}\equiv_{L}v_{2}$
implies $v^{\prime}_{1}u_{1}v_{1}\equiv_{L}v^{\prime}_{1}u_{1}v_{2}$,
${\equiv_{L}}$, $u_{1}\equiv_{L}u_{2}$ implies
$v^{\prime}_{1}u_{1}v_{2}\equiv_{L}v^{\prime}_{1}u_{2}v_{2}$, and
$v^{\prime}_{1}\equiv_{L}v^{\prime}_{2}$ implies
$v^{\prime}_{1}u_{2}v_{2}\equiv_{L}v^{\prime}_{2}u_{2}v_{2}$. Hence,
$v^{\prime}_{1}u_{1}v_{1}\equiv_{L}v^{\prime}_{2}u_{2}v_{2}$, by transitivity
of ${\equiv_{L}}$.

##### Correctness.

We have $L(\mathcal{A})=L$ since $[w]\cap L=\varnothing$ or $[w]\subseteq L$,
for all $w\in\Sigma^{*}$. More precisely, every $w\in\widehat{\Sigma}^{*}$
admits a unique run
$(([\varepsilon],[\varepsilon]),w,\bot)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{
\leavevmode\hbox to11.78pt{\vbox to2.68pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.3381pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}} {{}{}{}{}}
{{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@curveto{0.46236pt}{0.0pt}{0.69353pt}{1.1381pt}{1.15588pt}{1.1381pt}\pgfsys@curveto{1.49062pt}{1.1381pt}{1.77913pt}{0.58272pt}{2.0806pt}{0.0pt}\pgfsys@curveto{2.38205pt}{-0.5827pt}{2.67056pt}{-1.1381pt}{3.00531pt}{-1.1381pt}\pgfsys@curveto{3.34004pt}{-1.1381pt}{3.62856pt}{-0.58272pt}{3.93002pt}{0.0pt}\pgfsys@curveto{4.23148pt}{0.5827pt}{4.51999pt}{1.1381pt}{4.85474pt}{1.1381pt}\pgfsys@curveto{5.18947pt}{1.1381pt}{5.47798pt}{0.58272pt}{5.77945pt}{0.0pt}\pgfsys@curveto{6.0809pt}{-0.5827pt}{6.36942pt}{-1.1381pt}{6.70416pt}{-1.1381pt}\pgfsys@lineto{6.70416pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}^{*}(([\varepsilon],[w^{\prime}]),\varepsilon,\bot)$
since $\mathcal{A}$ is deterministic. By induction we prove that, for all
$x,y\in\Sigma^{*}$, all $\theta\in\Gamma^{+}\cup\\{\bot\\}$, if
$(q_{0},xy,\bot)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{ \leavevmode\hbox
to11.78pt{\vbox to2.68pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.3381pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}} {{}{}{}{}}
{{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@curveto{0.46236pt}{0.0pt}{0.69353pt}{1.1381pt}{1.15588pt}{1.1381pt}\pgfsys@curveto{1.49062pt}{1.1381pt}{1.77913pt}{0.58272pt}{2.0806pt}{0.0pt}\pgfsys@curveto{2.38205pt}{-0.5827pt}{2.67056pt}{-1.1381pt}{3.00531pt}{-1.1381pt}\pgfsys@curveto{3.34004pt}{-1.1381pt}{3.62856pt}{-0.58272pt}{3.93002pt}{0.0pt}\pgfsys@curveto{4.23148pt}{0.5827pt}{4.51999pt}{1.1381pt}{4.85474pt}{1.1381pt}\pgfsys@curveto{5.18947pt}{1.1381pt}{5.47798pt}{0.58272pt}{5.77945pt}{0.0pt}\pgfsys@curveto{6.0809pt}{-0.5827pt}{6.36942pt}{-1.1381pt}{6.70416pt}{-1.1381pt}\pgfsys@lineto{6.70416pt}{0.0pt}\pgfsys@lineto{9.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.38113pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}^{*}(([u_{0}],[v_{0}],y,\theta)$
then there exist $n\in\mathbb{N}$, and
$(a_{i},([u_{i}],[v_{i}]))_{i\in\\{1\dots n\\}}$ such that $\theta=\langle
a_{1},([u_{1}],[v_{1}])\rangle...\langle a_{n},([u_{n}],[v_{n}])\rangle\bot$
and $x\equiv_{L}u_{n}v_{n}\dots u_{0}v_{0}$. In particular, we get that
$w\equiv_{L}w^{\prime}$ implying that $w\in L(\mathcal{A})$ iff
$([\varepsilon],[w^{\prime}])\in F$ iff $w^{\prime}\in L$ iff $w\in L$. The
base case, when the run has length $n=0$, is trivial since $x=\varepsilon$ and
$\theta=\bot$. Suppose that the property holds for all runs of length $n$, we
prove that it holds for runs of length $n+1$. Let $z=u_{n}v_{n}\dots
u_{0}v_{0}$. In the case where the last transition is a push-transition that
reads $a\in\widehat{\Sigma}$ from $([u_{0}],[v_{0}])$. If $z=\varepsilon$ then
$x=\varepsilon$ since $x\equiv_{L}z$. Hence $xa\equiv_{L}za$ holds trivially.
Otherwise $z\neq\varepsilon$. Since a push-transition is triggered and
$u_{0}^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$
by invariant (2), we have that ${{}^{\varepsilon}[z]^{a}}$. Since
$x\equiv_{L}z$ and ${{}^{\varepsilon}[x]^{a}}$ holds as well then we get
$xa\equiv_{L}za$ by chain-monotonicity. In the case where the last transition
is a pop-transition from $([u_{0}],[v_{0}])$. Then the reached state is
$([u_{1}],[v_{1}u_{0}v_{0}])$ and the property is trivially preserved. In the
case where the last transition is a shift-transition that reads
$a\in\widehat{\Sigma}$ from $([u_{0}],[v_{0}])$. Since a shift-transition is
triggered, we that the
$u_{0}^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{1.0pt}{$\dot{=}$}}{\raisebox{0.8pt}{\scriptsize$\dot{=}$}}{\raisebox{0.6pt}{\tiny$\dot{=}$}}}a$
by invariant (1). In particular $u_{0}\neq\varepsilon$. By invariant (2), if
$v_{0}\neq\varepsilon$ then
$v_{0}^{\triangleright}\mathrel{\mathchoice{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{1.0pt}{$\gtrdot$}}{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}{\raisebox{0.6pt}{\tiny$\gtrdot$}}}a$.
Due to $x\equiv_{L}z$, we have that
$x^{\triangleright}=v_{0}^{\triangleright}$. So, $xa\equiv_{L}za$ since
${{}^{\varepsilon}[x]^{a}}$ and ${{}^{\varepsilon}[z]^{a}}$. Otherwise if
$v_{0}=\varepsilon$. Due to $x\equiv_{L}z$ and $u_{0}\neq\varepsilon$, we have
that $x^{\triangleright}=u_{0}^{\triangleright}$. So, $xa\equiv_{L}za$ since
${{}^{\varepsilon}[x]^{a}}$ and ${{}^{\varepsilon}[z]^{a}}$.

#### Proposition 4.6

*Statement. For every OPA $\mathcal{A}$, $\leqslant_{\mathcal{A}}$ is a computable chain-monotonic well quasi-order.

######  Proof A.6.

Let $\widehat{\Sigma}$ be an operator precedence alphabet, and
$\mathcal{A}=(Q,I,F,\Delta)$ be an OPA. We only show that the structural
quasi-order $\leqslant_{\mathcal{A}}$ is chain-monotonic since the rest is
argued before the statement in the main body of the paper. Let us define the
following relation over $\widehat{\Sigma}^{*}$:

$x\ll y\iff\forall q\in
Q,\forall\gamma\in\Gamma\cup\\{\bot\\}\bigwedge\begin{cases}f_{x}(q,\gamma)\subseteq
f_{y}(q,\gamma)\\\ g_{x}(q,q^{\prime},\gamma)\subseteq
g_{y}(q,q^{\prime},\gamma)\\\
(\varPhi_{x}(q,\gamma))^{\top}\subseteq(\varPhi_{y}(q,\gamma))^{\top}\end{cases}$

Recall that for every $x,y\in\widehat{\Sigma}^{*}$ we have
$x\leqslant_{\mathcal{A}}y$ iff $x\approx y$ and $x\ll y$, where ${\approx}$
is the chain equivalence. In particular, we want to show that for every
$x,y,u,v,u_{0},v_{0}\in\widehat{\Sigma}^{*}$ such that
$u_{0}x^{\triangleleft},u_{0}y^{\triangleleft}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\geq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\geq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\gtrdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\geq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\gtrdot$}}}}}}}$,
$x^{\triangleright}v_{0},y^{\triangleright}v_{0}\in\widehat{\Sigma}^{*}_{\mathrel{\mathchoice{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{$\leq$}}{\makebox[0.0pt]{\raisebox{1.0pt}{$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\scriptsize$\leq$}}{\makebox[0.0pt]{\raisebox{0.8pt}{\scriptsize$\lessdot$}}}}}{\makebox[5.60002pt]{{\makebox[0.0pt]{\tiny$\leq$}}{\makebox[0.0pt]{\raisebox{0.6pt}{\tiny$\lessdot$}}}}}}}$,
${{}^{u}[u_{0}xv_{0}]^{v}}$, ${{}^{u}[u_{0}yv_{0}]^{v}}$, and
$x\leqslant_{\mathcal{A}}y$, we have
$uu_{0}xv_{0}v\leqslant_{\mathcal{A}}uu_{0}yv_{0}v$. Since the chain
equivalence ${\approx}$ is chain-monotonic, we only need to show that ${\ll}$
is chain-monotonic, i.e., we have $uu_{0}xv_{0}v\ll uu_{0}yv_{0}v$ for every
$x,y,u,v,u_{0},v_{0}\in\widehat{\Sigma}^{*}$ as above.

Let $\star\notin\Sigma$ be a fresh letter for which we extend the precedence
relation with
$a\mathrel{\mathchoice{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{1.0pt}{$\lessdot$}}{\raisebox{0.8pt}{\scriptsize$\lessdot$}}{\raisebox{0.6pt}{\tiny$\lessdot$}}}\star$
for all $a\in\Sigma$. Let $w\in\widehat{\Sigma}^{*}$, $q,q^{\prime}\in Q$, and
$\gamma\in\Gamma\cup\\{\bot\\}$. Recall the following:

$f_{w}(q,\gamma)=\\{q_{w}\in
Q\mid\exists\gamma_{w}\in\Gamma^{+}\cup\\{\bot\\},(q,w\star,\gamma)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{
\leavevmode\hbox to11.78pt{\vbox to2.68pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.3381pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} }{{{{}{}{{}} }}{{}} {{}{}{}{}}
{{}{}{}{}} }{{{{}{}{{}} }}{{}} {{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}
{{}{}{}{}} {{}{}{}{}} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}