Max Planck Institute for Software Systems (MPI-SWS), Germanyashwani@mpi-
sws.orghttps://orcid.org/0000-0002-1825-0097Max Planck Institute for Software
Systems (MPI-SWS), Germanygeorg@mpi-
sws.orghttps://orcid.org/0000-0002-6421-4388 Ashwani Anand and Georg Zetzsche
Theory of computation Models of computation [3cm]eu-erc.pdfFunded by the
European Union (ERC, FINABIS, 101077902). Views and opinions expressed are
however those of the author(s) only and do not necessarily reflect those of
the European Union or the European Research Council Executive Agency. Neither
the European Union nor the granting authority can be held responsible for
them.

###### Acknowledgements.

The authors are grateful to Yousef Shakiba for discussions on the block
downward closure of regular languages. Guillermo A. Pérez and Jean-François
Raskin 2 34th International Conference on Concurrency Theory (CONCUR 2023)
CONCUR 2023 CONCUR 2023 September 18–23, 2023 Antwerp, Belgium 279 39

# Priority Downward Closures

Ashwani Anand  Georg Zetzsche

###### Abstract

When a system sends messages through a lossy channel, then the language
encoding all sequences of messages can be abstracted by its downward closure,
i.e. the set of all (not necessarily contiguous) subwords. This is useful
because even if the system has infinitely many states, its downward closure is
a regular language. However, if the channel has congestion control based on
priorities assigned to the messages, then we need a finer abstraction: The
downward closure with respect to the priority embedding. As for subword-based
downward closures, one can also show that these priority downward closures are
always regular.

While computing finite automata for the subword-based downward closure is well
understood, nothing is known in the case of priorities. We initiate the study
of this problem and provide algorithms to compute priority downward closures
for regular languages, one-counter languages, and context-free languages.

###### keywords:

downward closure, priority order, pushdown automata, non-deterministic finite
automata, abstraction, computability

###### category:

##  1 Introduction

When analyzing infinite-state systems, it is often possible to replace
individual components by an overapproximation based on (subword) downward
closures. Here, the _(subword) downward closure_ of a language
$L\subseteq\Sigma^{*}$ is the set of all words that appear as (not necessarily
contiguous) subwords of members of $L$. This overapproximation is usually
possible because the verified properties are not changed when we allow
additional behaviors resulting from subwords. Furthermore, this
overapproximation simplifies the system because a well-known result by Haines
is that for _every language $L\subseteq\Sigma^{*}$_, its subword downward
closure is regular.

This idea has been successfully applied to many verification tasks, such as
the verification of restricted lossy channel systems [1], concurrent programs
with dynamic thread spawning and bounded context-switching [2, 6],
asynchronous programs (safety, termination, liveness [25], but also context-
free refinement verification [7]), the analysis of thread pools [8], and
safety of parameterized asynchronous shared-memory systems [28]. For these
reasons, there has been a substantial amount of interest in algorithms to
compute finite automata for subword downward closures of given infinite-state
sytems [29, 12, 18, 31, 30, 5, 32, 19, 11, 4, 34, 15, 3].

One situation where downward closures are useful is that of systems that send
messages through a lossy channel, meaning that every message can be lost on
the way. Then clearly, the downward closure of the set of sequences of
messages is exactly the set of sequences observed by the receiver. This works
as long as all messages can be dropped arbitrarily.

#### Priorities

However, if the messages are not dropped arbitrarily but as part of congestion
control, then taking the set of all subwords would be too coarse an
abstraction: Suppose we want to prioritize critical messages that can only be
dropped if there are no lower-priority messages in the channel. For example,
RFC 2475 describes an architecture that allows specifying relative priority
among the IP packets from a finite set of priorities and allows the network
links to drop lower priority packets to accommodate higher priority ones when
the congestion in the network reaches a critical point [10]. As another
example, in networks with an Asynchronous Transfer Mode layer, cells carry a
priority in order to give preferences to audio or video packages over less
time-critical packages [24]. In these situations, the subword downward closure
would introduce behaviors that are not actually possible in the system.

To formally capture the effect of dropping messages by priorities, Haase,
Schmitz and Schnoebelen [17] introduced _Priority Channel Systems (PCS)_.
These feature an ordering on words (i.e. channel contents), called the
_Prioritised Superseding Order (PSO)_ , which allows the messages to have an
assigned priority, such that higher priority messages can supersede lower
priority ones. This order indeed allows the messages to be treated
discriminatively, but the superseding is asymmetric. A message can be
superseded only if there is a higher priority letter coming in the channel
later. This means, PSO are the “priority counterpart” of the subword order for
channels with priorities. In particular, in these systems, components can be
abstracted by their _priority downward closure_ , the downward closure with
respect to the PSO. Fortunately, just as for subwords, priority downward
closures are also always regular.

This raises the question of whether it is possible to compute finite automata
for the priority downward closure for given infinite-state systems. For
example, consider a recursive program that sends messages into a lossy channel
with congestion control. Then, the set of possible message sequences that can
arrive is exactly the priority downward closure
$S\mathord{\downarrow_{\mathsf{P}}}$ of the language $S$ of sent messages.
Since $S$ is context-free in this case, we would like to compute a finite
automaton for $S\mathord{\downarrow_{\mathsf{P}}}$. While this problem is
well-understood for subwords, nothing is known for priority downward closures.

#### Contribution

We initiate the study of computing priority downward closures. We show two
main results. On the one hand, we study the setting above—computing priority
downward closures of context-free languages. Here, we show that one can
compute a doubly-exponential-sized automaton for its priority downward
closure. On the other hand, we consider a natural restriction of context-free
languages: We show that for one-counter automata, there is a polynomial-time
algorithm to compute the priority downward closure.

#### Key technical ingredients

The first step is to consider a related order on words, which we call _block
order_ , which also has priorities assigned to letters, but imposes them more
symmetrically. Moreover, we show that under mild assumptions, computing
priority downward closures reduces to computing block downward closures.

Both our constructions—for one-counter automata and context-free
languages—require new ideas. For one-counter automata, we modify the subword-
based downward closures construction from [3] in a non-obvious way to block
downward closures. Crucially, our modification relies on the insight that, in
some word, repeating existing factors will always yield a word that is larger
in the block order. For context-free languages, we present a novel inductive
approach: We decompose the input language into finitely many languages with
fewer priority levels and apply the construction recursively.

#### Outline of the paper

We fix notation in Section 2 and introduce the block order and show its
relationship to the priority order in Section 3. In Sections 4, 5 and 6, we
then present methods for computing block and priority downward closures for
regular languages, one-counter languages, and context-free languages,
respectively.

##  2 Preliminaries

We will use the convention that $[i,j]$ denotes the set
$\\{i,i+1,\ldots,j\\}$. By $\Sigma$, we represent a finite alphabet.
$\Sigma^{*}\ (\Sigma^{+})$ denotes the set of (non-empty) words over $\Sigma$.
When defining the priority order, we will equip $\Sigma$ with a set of
priorities with total order $(\mathcal{P},\lessdot)$, i.e. there exists a
fixed priority mapping from $\Sigma$ to $\mathcal{P}$. The set of priority
will be the set of integers $[0,d]$, with the canonical total order. By sets
$\Sigma_{=p}$ ($p\in\mathcal{P}$), we denote the set of letters in $\Sigma$
with priority $p$. For priority $p\in\mathcal{P}$, $\Sigma_{\leq
p}=\Sigma_{=0}\cup\cdots\cup\Sigma_{=p}$, i.e. the set of letters smaller than
or equal to $p$. For a word $w=a_{0}a_{1}\cdots a_{k}$, where
$a_{i}\in\Sigma$, by $w[i,j]$, we denote the infix $a_{i}a_{i+1}\cdots
a_{j-1}a_{j}$, and by $w[i]$, we denote $a_{i}$.

#### Finite automata and regular languages

A _non-deterministic finite state automaton ( NFA)_ is a tuple ${\rm
NewA}=(Q,\Sigma,\delta,q_{0},F)$, where $Q$ is a finite set of _states_ ,
$\Sigma$ is its _input alphabet_ , $\delta$ is its set of _edges_ i.e. a
finite subset of $Q\times\Sigma\cup\\{\epsilon\\}\times Q$, $q_{0}\in Q$ is
its _initial state_ , and $F\subseteq Q$ is its set of _final states_. A word
is accepted by ${\rm NewA}$ if it has a run from the initial state ending in a
final state. The language _recognized_ by an NFA ${\rm NewA}$ is called a
regular language, and is denoted by $\mathcal{L}({\rm NewA})$. The _size of a
NFA_, denoted by $|{\rm NewA}|$, is the number of states in the NFA.

#### (Well-)quasi-orders

A _quasi-order_ , denoted as $(X,\leq)$, is a set $X$ with a reflexive and
transitive relation $\leq$ on $X$. If $x\leq y$ (or equivalently, $y\geq x$),
we say that $x$ is smaller than $y$, or $y$ is greater than $x$. If $\leq$ is
also anti-symmetric, then it is called a _partial order_. If every pair of
elements in $X$ is comparable by $\leq$, then it is called a _total_ or
_linear_ order. Let $(X,\leq_{1})$ and $(Y,\leq_{2})$ be two quasi orders, and
$h:X\rightarrow Y$ be a function. We call $h$ a _monomorphism_ if it is one-
to-one and $x_{1}\leq_{1}x_{2}\iff h(x_{1})\leq_{2}h(x_{2})$.

A quasi order $(X,\leq)$ is called a _well-quasi order ( WQO)_, if any
infinite sequence of elements $x_{0},x_{1},x_{2},\ldots$ from $X$ contains an
increasing pair $x_{i}\leq x_{j}$ with $i<j$. If $X$ is the set of words over
some alphabet, then a WQO $(X,\leq)$ is called _multiplicative_ if $\forall
u,u^{\prime},v,v^{\prime}\in X$, $u\leq u^{\prime}$ and $v\leq v^{\prime}$
imply that $uv\leq u^{\prime}v^{\prime}$.

#### Subwords

For $u,v\in\Sigma^{*},$ we say $u\preccurlyeq v$, which we refer to as
_subword order_ , if $u$ is a subword (not necessarily, contiguous) of $v$,
i.e. if

$\displaystyle u$ $\displaystyle=$ $\displaystyle u_{1}u_{2}\cdots u_{k}$
$\displaystyle\text{and, }v$ $\displaystyle=$ $\displaystyle
v_{0}u_{1}v_{1}u_{2}v_{2}\cdots v_{k-1}u_{k}v_{k}$

where $u_{i}\in\Sigma$ and $v_{i}\in\Sigma^{*}$. In simpler words,
$u\preccurlyeq v$ if some letters of $v$ can be dropped to obtain $u$. For
example, let $\Sigma=[0,1]$. Then, $0\preccurlyeq 00\preccurlyeq
010\not\preccurlyeq 110$; $0$ and $00$ can be obtained by dropping letters
from $00$ and $010$, respectively. But $010$ cannot be obtained from $110$, as
the latter does not have sufficiently many $0$s. If $u\preccurlyeq v$, we say
that $u$ is subword smaller than $v$, or simply that $u$ is a subword of $v$.
And we call a mapping from the positions in $u$ to positions in $v$ that
witnesses $u\preccurlyeq v$ as the _witness position mapping_.

Since $\Sigma$ is a WQO with the equality order, by Higman’s lemma,
$\Sigma^{*}$ is a WQO with the subword order. It is in fact a multiplicative
WQO: if $u\preccurlyeq u^{\prime}$ and $v\preccurlyeq v^{\prime}$, then
dropping the same letters from $u^{\prime}v^{\prime}$ gives us $uv$.

#### Priority order

We take an alphabet $\Sigma$ with priorities totally ordered by $\lessdot$. We
say $u\preccurlyeq_{\mathsf{P}}v$, which we refer to as _priority order_ , if
$u=\epsilon$ or,

$\displaystyle u$ $\displaystyle=$ $\displaystyle u_{1}u_{2}\cdots u_{k}$
$\displaystyle\text{and, }v$ $\displaystyle=$ $\displaystyle
v_{1}u_{1}v_{2}u_{2}\cdots v_{k}u_{k},$

such that $\forall i\in[1,k]$, $u_{i}\in\Sigma$ and $v_{i}\in\Sigma_{\leq
u_{i}}^{*}$. It is easy to observe that the priority order is multiplicative,
and is finer than the subword order, i.e. $\forall
u,v\in\Sigma^{*},u\preccurlyeq_{\mathsf{P}}v\implies u\preccurlyeq v$. As
shown in [17, Theorem 3.6], the priority order on words over a finite alphabet
with priorities is a well-quasi ordering:

######  Lemma 2.1.

$(\Sigma^{*},\preccurlyeq_{\mathsf{P}})$ is a WQO.

#### Downward closure

We define the subword downward closure and priority downward closure for a
language $L\subseteq\Sigma^{*}$ as follows:

$\displaystyle L\mathord{\downarrow}$
$\displaystyle:=\\{u\in\Sigma^{*}\,\mid\exists\ v\in L\colon u\ \preccurlyeq\
v\\},$ $\displaystyle L\mathord{\downarrow_{\mathsf{P}}}$
$\displaystyle:=\\{u\in\Sigma^{*}\mid\exists\ v\in L\colon u\
\preccurlyeq_{\mathsf{P}}\ v\\}.$

The following is the starting point for our investigation: It shows that for
every language $L$, there exist finite automata for its downward closures
w.r.t. $\preccurlyeq$ and $\preccurlyeq_{\mathsf{P}}$.

######  Lemma 2.2.

Every subword downward closed sets and every priority downward closed set is
regular.

For the subword order, this was shown by Haines [20]. The same idea applies to
the priority ordering: A downward closed set is the complement of an upward
closed set. Therefore, and since every upward closed set in a well-quasi
ordering has finitely many minimal elements, it suffices to show that the set
of all words above a single word is a regular language. This, in turn, is
shown using a simple automaton construction. In Appendix A, we prove an
analogue of this for the block ordering (Lemma 3.7).

We stress that Lemma 2.2 is not effective: It does not guarantee that finite
automata for downward closures can be computed for any given language. In
fact, there are language classes for which they are not computable, such as
reachability sets of lossy channel systems and Church-Rosser languages [26,
16]. Therefore, our focus will be on the question of how to effectively
compute automata for priority downward closures.

##  3 The Block Order

We first define the block order formally and then give the intuition behind
the definition. Let $\Sigma$ be a finite alphabet, and $\mathcal{P}=[0,d]$ be
a set of priorities with a total order $\lessdot$. Then for
$u,v\in\Sigma^{*}$, where maximum priority occurring among $u$ and $v$ is $p$,
we say $u\preccurlyeq_{\mathsf{B}}v$, if

  1. i.

if $u,v\in\Sigma_{=p}^{*}$, and $u\preccurlyeq v$, or

  2. ii.

if

$\displaystyle u$ $\displaystyle=$ $\displaystyle u_{0}x_{0}u_{1}x_{1}\cdots
x_{n-1}u_{n}$ $\displaystyle\text{and, }v$ $\displaystyle=$ $\displaystyle
v_{0}y_{0}v_{1}y_{1}\cdots y_{m-1}v_{m}$

where $x_{0},\ldots x_{n-1},y_{0},\ldots,y_{m-1}\in\Sigma_{=p}$, and for all
$i\in[0,n]$, we have $u_{i},v_{i}\in\Sigma_{\leq p-1}^{*}$ (the $u_{i}$ and
$v_{i}$ are called _sub- $p$_ blocks), and there exists a strictly
monotonically increasing map $\phi:[0,n]\rightarrow[0,m]$, which we call the
_witness block map_ , such that

    1. (a)

$u_{i}\preccurlyeq_{\mathsf{B}}v_{\phi(i)}$, $\forall i$,

    2. (b)

$\phi(0)=0$,

    3. (c)

$\phi(n)=m$, and

    4. (d)

$x_{i}\preccurlyeq v_{\phi(i)}y_{\phi(i)}v_{\phi(i)+1}\cdots v_{\phi(i+1)}$,
$\forall i\in[0,n-1]$.

Intuitively, we say that $u$ is _block smaller_ than $v$, if either

  * •

both words have letters of same priority, and $u$ is a subword of $v$, or,

  * •

the largest priority occurring in both words is $p$. Then we split both words
along the priority $p$ letters, to obtain sequences of sub-$p$ blocks of
words, which have words of strictly less priority. Then by item iia, we embed
the sub-$p$ blocks of $u$ to those of $v$, such that they are recursively
block smaller. Then with items iib and iic, we ensure that the first (and
last) sub-$p$ block of $u$ is embedded in the first (resp., last) sub-$p$
block of $v$. We will see later that this constraint allows the order to be
multiplicative. Finally, by item iid, we ensure that the letters of priority
$p$ in $u$ are preserved in $v$, i.e. every $x_{i}$ indeed occurs between the
embeddings of the sub-$p$ block $u_{i}$ and $u_{i+1}$.

######  Example 3.1.

Consider the alphabet $\Sigma=\\{0^{a},0^{b},1^{a},1^{b},2^{a},2^{b}\\}$ with
priority set $\mathcal{P}=[0,2]$ and $\Sigma_{=i}=\\{i^{a},i^{b}\\}$. In the
following examples, the color helps to identify the largest priority occurring
in the words. First, notice that
$\epsilon\preccurlyeq_{\mathsf{B}}0^{a}\preccurlyeq_{\mathsf{B}}0^{a}0^{b}$,
and hence

$\displaystyle{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}1^{b}}0^{a}\preccurlyeq_{\mathsf{B}}0^{a}{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}1^{b}}0^{a}0^{a}1^{a}0^{a}0^{b},$
but
$\displaystyle{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}1^{b}}0^{a}\not\preccurlyeq_{\mathsf{B}}0^{a}{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}1^{b}}0^{a}0^{a}{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}1^{a}}0^{b}0^{b}.$

This is because $0^{a}\not\preccurlyeq_{\mathsf{B}}0^{b}0^{b}$, i.e. the last
sub-$1$ block of the former word cannot be mapped to the last sub-$1$ block of
the latter word. As another example, we have

$\displaystyle{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}2^{a}}1^{b}0^{a}\preccurlyeq_{\mathsf{B}}0^{a}{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}2^{a}}0^{a}1^{b}0^{a}0^{a}1^{a}0^{a}0^{b},$
but
$\displaystyle{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}2^{a}}1^{b}0^{a}\not\preccurlyeq_{\mathsf{B}}0^{a}{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}2^{b}}0^{a}1^{b}0^{a}0^{a}1^{a}0^{a}0^{b}.$

This is because $2^{a}$ does not exist in the latter word, violating item iid.
Finally, notice that

$1^{a}1^{b}\not\preccurlyeq_{\mathsf{B}}1^{a}{\color[rgb]{1,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.4,0.4}2^{a}}1^{b},$
(1)

because the sub-$2$ block $1^{a}1^{b}$ would have to be mapped to a single
sub-$2$ block in the right-hand word; but none of them can accomodate
$1^{a}1^{b}$.

Note that by items iid and iia, we have that
$u\preccurlyeq_{\mathsf{B}}v\implies u\preccurlyeq v$, for all
$u,v\in\Sigma^{*}$. Then there exists a position mapping $\rho$ from $[0,|u|]$
to $[0,|v|]$ such that $u[i]=v[\rho(i)]$, for all $i$. We say that a position
mapping _respects block order_ if for all $i$, $v[\rho(i),\rho(i+1)]$ contains
letters of priorities smaller than $u[i]$ and $u[i+1]$. It is easy to observe
that if $u\preccurlyeq_{\mathsf{B}}v$, then there exists a position mapping
from $u$ to $v$ respecting the block order. The following is a straightforward
repeated application of Higman’s Lemma [22] (see Appendix A).

######  Theorem 3.2.

$(\Sigma^{*},\preccurlyeq_{\mathsf{B}})$ is a WQO.

In fact, the block order is multiplicative, i.e. for all
$u,v,u^{\prime},v^{\prime}\in\Sigma^{*}$ such that
$u\preccurlyeq_{\mathsf{B}}u^{\prime}$ and
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$, it holds that
$uv\preccurlyeq_{\mathsf{B}}u^{\prime}v^{\prime}$.

######  Lemma 3.3.

$(\Sigma^{*},\preccurlyeq_{\mathsf{B}})$ is a multiplicative WQO.

######  Proof 3.4.

For singleton $\mathcal{P}$, the result trivially holds because it coincides
with the subword order. Let $(\Sigma_{\leq
p-1}^{*},\preccurlyeq_{\mathsf{B}})$ be multiplicative. Now we show that
$(\Sigma_{\leq p}^{*},\preccurlyeq_{\mathsf{B}})$ is multiplicative. To this
end, let $u\preccurlyeq_{\mathsf{B}}u^{\prime}$,
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$, and $\phi,\psi$ be the witnessing
block maps respectively. We assume

$\displaystyle u$ $\displaystyle=$ $\displaystyle
u_{0}x_{0}u_{1}x_{1}u_{2}x_{2}\cdots x_{k-1}u_{k}$ $\displaystyle v$
$\displaystyle=$ $\displaystyle v_{0}y_{0}v_{1}y_{1}v_{2}y_{2}\cdots
y_{l-1}v_{l}$ $\displaystyle u^{\prime}$ $\displaystyle=$ $\displaystyle
u^{\prime}_{0}x^{\prime}_{0}u^{\prime}_{1}x^{\prime}_{1}u^{\prime}_{2}x^{\prime}_{2}\cdots
x^{\prime}_{k-1}u^{\prime}_{k^{\prime}}$ $\displaystyle v^{\prime}$
$\displaystyle=$ $\displaystyle
v^{\prime}_{0}y^{\prime}_{0}v^{\prime}_{1}y^{\prime}_{1}v^{\prime}_{2}y^{\prime}_{2}\cdots
y^{\prime}_{l-1}v^{\prime}_{l^{\prime}}$

where $x_{i},y_{i},x_{i}^{\prime},y_{i}^{\prime}\in\Sigma_{=p}$. Consider the
function $\delta\colon[0,k+l-1]\rightarrow[0,k^{\prime}+l^{\prime}-1]$ with

$i\mapsto\begin{cases}\phi(i),\text{ if }1\leq i\leq k\\\ \psi(i-k+1),\text{
if }k<i\leq k+l-1\end{cases}$

Since the $k^{th}$ sub-$p$ block of $u$ and the $1^{st}$ sub-$p$ block of $v$
combines in $uv$ to form one sub-$p$ block, we have $k+l-1$ sub-$p$ blocks.
Similarly, $u^{\prime}v^{\prime}$ has $k^{\prime}+l^{\prime}-1$ sub-$p$
blocks. And hence
$u_{k}v_{1}\preccurlyeq_{\mathsf{B}}u^{\prime}_{k^{\prime}}v^{\prime}_{1}$, by
induction hypothesis. The recursive embedding is obvious for other sub-$p$
blocks. We also have that $\delta(0)=0$ and
$\delta(k+l-1)=k^{\prime}+l^{\prime}-1$. By monotonicity of $\phi$ and $\psi$,
$\delta$ is also strictly monotonically increasing. Hence, $\delta$ witnesses
$uv\preccurlyeq_{\mathsf{B}}u^{\prime}v^{\prime}$.

#### Pumping

In the subword ordering, an often applied property is that for any words
$u,v,w$, we have $uw\preccurlyeq uvw$, i.e. inserting any word leads to a
superword. This is not true for the block ordering, as we saw in Example 3.1,
(1). However, one of our key observations about the block order is the
following property: If the word we insert is just a repetition of an existing
factor, then this yields a larger word in the block ordering. This will be
crucial for our downward closure construction for one-counter automata in
Section 5.

######  Lemma 3.5 (Pumping Lemma).

For any $u,v,w\in\Sigma^{*}$, we have $uvw\preccurlyeq_{\mathsf{B}}uvvw$.

Before we prove Lemma 3.5, let us note that by applying Lemma 3.5 multiple
times, this implies that we can also repeat multiple factors. For instance, if
$w=w_{1}w_{2}w_{3}w_{4}w_{5}$, then
$w\preccurlyeq_{\mathsf{B}}w_{1}w_{2}^{2}w_{3}w_{4}^{3}w_{5}$. Figure 1 shows
an example on how to choose the witness block map.

######  Proof 3.6.

We proceed by induction on the number of priorities. If there is just a single
priority (i.e. $\mathcal{P}=\\{0\\}$), then $\preccurlyeq_{\mathsf{B}}$
coincides with $\preccurlyeq$ and the statement is trivial. Let us assume the
Lemma is established for words with up to $n$ priorities. We distinguish two
cases.

  * •

Suppose $v$ contains only letters of priorities $[0,n]$. Then repeating $v$
means repeating a factor inside a sub-$(n+1)$ block, which is a word with
priorities in $[0,n]$. Hence, the statement follows by induction: Formally,
this means we can use the embedding mapping that sends block $i$ of $uvw$ to
block $i$ of $uvvw$.

  * •

Suppose $v$ contains a letter of priority $n+1$. write
$v=v_{0}x_{1}v_{1}\cdots x_{m}v_{m}$, where $x_{1},\ldots,x_{m}$ are the
letters of priority $n+1$ in $v$ and $v_{0},\ldots,v_{m}$ are the sub-$(n+1)$
blocks of $v$. Then:

$\displaystyle uvw$ $\displaystyle=uv_{0}x_{1}\cdots v_{m-1}x_{m}v_{m}w,$
$\displaystyle uvvw$ $\displaystyle=uv_{0}x_{1}\cdots
v_{m-1}x_{m}\underbrace{v_{m}v_{0}x_{1}\cdots
v_{m-1}x_{m}}_{\text{skipped}}v_{m}w.$

The idea is simple: Our witness block map just skips the $m$ sub-$(n+1)$
blocks inside of $v_{m}v_{0}x_{1}\cdots v_{m-1}x_{m}$. Thus, the sub-$(n+1)$
blocks in $uv_{0}x_{1}\cdots v_{m-1}x_{m}$ are mapped to the same blocks in
$uv_{0}x_{1}\cdots v_{m-1}x_{m}$, and the sub-$(n+1)$ blocks in $v_{m}w$ are
mapped to the same blocks in $v_{m}w$. This is clearly a valid witness block
map, since the first (resp. last) sub-$(n+1)$ block is mapped to the first
(resp. last), and each sub-$(n+1)$ block is mapped to an identical sub-$(n+1)$
block.

${w^{\prime}=}$${1}$${2}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${2}$${1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${0}$${w=}$${1}$${2}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${2}$${1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2}$${\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${0}$
Figure 1: Here $\Sigma=[0,2]$, $\mathcal{P}=[0,2]$, and $A_{i}=\\{i\\}$,
$w=12(01)21(121)0$ and $w^{\prime}=12(01)^{2}21(121)^{3}0$. The repeated
segments are marked in  red, and the arrows denote the witness block map.

#### Regular downward closures

As for $\preccurlyeq$ and $\preccurlyeq_{\mathsf{P}}$, we define
$L\mathord{\downarrow_{\mathsf{B}}}=\\{u\in\Sigma^{*}\mid\exists v\in L\colon
u\preccurlyeq_{\mathsf{B}}v\\}$ for any $L\subseteq\Sigma^{*}$.

######  Lemma 3.7.

For every $L\subseteq\Sigma^{*}$, $L\mathord{\downarrow_{\mathsf{B}}}$ is a
regular language.

For the proof of Lemma 3.7, one can argue as mentioned above: The complement
$\Sigma^{*}\setminus(L\mathord{\downarrow_{\mathsf{B}}})$ of
$L\mathord{\downarrow_{\mathsf{B}}}$ is upward closed. And since
$\preccurlyeq_{\mathsf{B}}$ is a WQO,
$\Sigma^{*}\setminus(L\mathord{\downarrow_{\mathsf{B}}})$ has finitely many
minimal elements. It thus remains to show that for each word $w\in\Sigma^{*}$,
the set of words $\preccurlyeq_{\mathsf{B}}$-larger than $w$ is regular, which
is a simple exercise. Details can be found in Appendix A.

#### Block order vs. priority order

We will later see (Theorem 4.5) that under mild conditions, computing priority
downward closures reduces to computing block downward closures. The following
Lemma is the main technical ingredient in this: It shows that the block order
refines the priority order on words that end in the same letter, assuming the
alphabet has a certain shape. A priority alphabet $(\Sigma,\mathcal{P})$ with
$\mathcal{P}=[1,d]$ is called _flat_ if $|\Sigma_{=i}|=1$ for each
$i\in[1,d]$.

######  Lemma 3.8.

If $\Sigma$ is flat and $u,v\in\Sigma^{*}a$ for some $a\in\Sigma$, then
$u\preccurlyeq_{\mathsf{B}}v$ implies $u\preccurlyeq_{\mathsf{P}}v$.

######  Proof 3.9.

Since $u\preccurlyeq_{\mathsf{B}}v$, there exists a witness position mapping
$\rho$ that maps the positions of the letters in $u$ to that of $v$, such that
it respects the block order, and it maps the last position of $u$ to the last
of $v$.

Let $u=u_{0}u_{1}\cdots u_{k}$. We say that a position mapping violates the
priority order at position $i$ (for $i\in[0,k-1]$), if
$v[\rho(i)+1,\rho(i+1)]$ has a letter of priority higher than that of
$u[i+1]$. Note that if $\rho$ does not violate the priority order at any
position, then $u\preccurlyeq_{\mathsf{P}}v$.

Let $i$ be the largest position at which $\rho$ violates the priority order,
i.e. $v[\rho(i)+1,\rho(i+1)]$ has a letter of priority higher than that of
$u[i+1]$. We show that if $\rho$ respects the block order till position $i$,
there exists another witness position mapping $\rho^{\prime}$ that respects
the block order till position $i-1$, and has one few position of violation
(i.e. no violation at position $i$).

We first observe that $u[i]>u[i+1]$, which holds since $\rho$ respects the
block order till position $i$, implying that $v[\rho(i)+1,\rho(i+1)]$ does not
have a letter of priority higher than $min\\{u[i],u[i+1]\\}$, and if $u[i]\leq
u[i+1]$, $\rho$ does not violate the priority order at $i$.

Then observe that $v[\rho(i)+1,\rho(i+1)]$ does not have a letter with
priority $p$, where $u[i]>p>u[i+1]$, otherwise the sub-$u[i]$ block of $u$
immediately after $u[i]$, can not be embedded to that of $v$ immediately after
$v[\rho(i)]$, since it would have to be split along $p$, and the first sub-$p$
block in $v$ will not be mapped to any in $u$. Then $v[\rho(i)+1,\rho(i+1)]$
has letter of priority $u[i]$ (for a violation at $i$). Then consider the
mapping $\rho^{\prime}$ that maps $i$ to the last $u[i]$ letter in
$v[\rho(i)+1,\rho(i+1)]$ (say at $v[j]$ for some $j$, $\rho(i)+1\leq
j\leq\rho(i+1)$).

This mapping respects the block order till position $i-1$, trivially, as we do
not change the mapping before $i$. We show that there is no priority order
violation at position $i$. This holds because the only larger priority letter
occurring in $v[\rho(i)+1,\rho(i+1)]$ was $u[i]$, and due to the definition of
$\rho^{\prime}$, $v[\rho^{\prime}(i)+1,\rho^{\prime}(i+1)]$ has no letter of
priority higher than $u[i+1]$. Since we do not change the mapping after
position $i$, $\rho^{\prime}$ does not introduce a violation at any position
after $i$. Hence we have a new position mapping that has one few position of
priority order violation.

######  Remark 3.10.

We want to stress that the flatness assumption in Lemma 3.8 is crucial:
Consider the alphabet $\Sigma$ from the Example 3.1. Then
$1^{a}0^{a}\preccurlyeq_{\mathsf{B}}1^{a}1^{b}0^{a}$, but
$1^{a}0^{a}\not\preccurlyeq_{\mathsf{P}}1^{a}1^{b}0^{a}$. Here only one
position mapping exists, and it is not possible to remap $1^{a}$ to $1^{b}$
since they are two distinct letters of same priority. Hence, we need to assume
that each priority greater than zero has at most one letter.

##  4 Regular Languages

In this section, we show how to construct an NFA for the block downward
closure of a regular language. To this end, we show that both orders are
rational transductions.

#### Rational transductions

A _finite state transducer_ is a tuple ${\rm NewA}=(Q,X,Y,E,q_{0},F)$, where
$Q$ is a finite set of states, $X$ and $Y$ are _input_ and _output alphabets_
, respectively, $E$ is the set of _edges_ i.e. finite subset of $Q\times
X^{*}\times Y^{*}\times Q$, $q_{0}\in Q$ is the _initial state_ , and
$F\subseteq Q$ is the set of _final states_. A _configuration_ of ${\rm NewA}$
is a triple $(q,u,v)\in Q\times X^{*}\times Y^{*}$. We write
$(q,u,v)\rightarrow_{{\rm NewA}}(q^{\prime},u^{\prime},v^{\prime})$, if there
is an edge $(q,x,y,q^{\prime})$ with $u^{\prime}=ux$ and $v^{\prime}=vy$. If
there is an edge $(q,x,y,q^{\prime})$, we sometimes denote this fact by
$q\xrightarrow{(x,y)}_{{\rm NewA}}q^{\prime}$, and say “read $x$ at $q$,
output $y$, and goto $q^{\prime}$”. The _size of a transducer_ , denoted by
$|{\rm NewA}|$, is the number of its states.

A _transduction_ is a subset of $X^{*}\times Y^{*}$ for some finite alphabets
$X,Y$. The _transduction defined by ${\rm NewA}$_ is $\mathcal{T}({\rm
NewA})=\\{(u,v)\in X^{*}\times Y^{*}\ |\
(q_{0},\epsilon,\epsilon)\rightarrow_{{\rm NewA}}^{*}(f,u,v)\text{ for some
}f\in F\\}.$ A transduction is called _rational_ if it is defined by some
finite-state transducer. Sometimes we abuse the notation and output a regular
language $R\subseteq Y^{*}$ on an edge, instead of a letter. It should be
noted that this abuse is equivalent to original definition of finite state
transducers.

We say that a language class $\mathcal{C}$ is _closed under rational
transductions_ if for each language $L\in\mathcal{C}$, and each rational
transduction $R\subseteq X^{*}\times Y^{*}$, _the language obtained by
applying the transduction_ $R$ to $L$, $RL\stackrel{{\scriptstyle
def}}{{=}}\\{v\in Y^{*}\ |\ (u,v)\in R\text{ for some }u\in L\\}$ also belongs
to $\mathcal{C}$. We call such language classes _full trio_. Regular
languages, context-free languages, recursively enumerable languages are some
examples of full trios [9].

#### Transducers for orders

It is well-known that the subword order is a rational transduction, i.e. the
relation $T=\\{(u,v)\in X^{*}\times X^{*}\ |\ v\preccurlyeq u\\}$ is defined
by a finite-state transducer. For example, it can be defined by a one-state
transducer that can non-deterministically decide to output or drop each
letter. Note that on applying the transduction to any language, it gives the
subword downward closure of the language. This means, for every $L\subseteq
X^{*}$, we have $TL=L\mathord{\downarrow}$. We will now describe analogous
transducers for the priority and block order.

######  Theorem 4.1.

Given a priority alphabet with priorities $[0,k]$, one can construct in
polynomial time a transducer for $\preccurlyeq_{\mathsf{B}}$ and a transducer
for $\preccurlyeq_{\mathsf{P}}$, each of size $\mathcal{O}(k)$.

######  Proof 4.2.

The transducers for the block and priority order are similar. Intuitively,
both remember the maximum of the priorities dropped or to be dropped, and keep
or drop the coming letters accordingly. We show the transducer for the
priority order here since it is applied in Theorem 4.5. The transducer for the
block order is detailed in Appendix B.

Let $\Sigma$ be a finite alphabet, with priorities $\mathcal{P}=[0,k]$.
Consider the transducer that has one state for every priority, a non-final
sink state, and a distinguished final state. If the transducer is in the state
for priority $r$ and reads a letter $a$ of priority $s$, then

  * •

if $s<r$, then it outputs nothing and stays in state $r$,

  * •

if $s\geq r$, then it can output nothing, and go to state $s$,

  * •

if $s\geq r$, it can also output $a$, and go to state $0$, or the accepting
state non-deterministically,

  * •

for any other scenario, goes to the sink state.

The priority $0$ state is the initial state. Intuitively, the transducer
remembers the largest priority letter that has been dropped, and keeps only a
letter of higher priority later. To be accepting, it has to read the last
letter to go to the accepting final state.

The following theorem states that the class of regular languages form a full
trio.

######  Theorem 4.3 ([27, Corollary 3.5.5]).

Given an NFA ${\rm NewA}$ and a transducer $\mathcal{B}$, we can construct in
polynomial time an NFA of size $|{\rm NewA}|\cdot|\mathcal{B}|$ for
$\mathcal{T}(\mathcal{B})(\mathcal{L}({\rm NewA}))$.

Theorems 4.3 and 4.1 give us a polynomial size NFA recognizing the priority
and block downward closure of a regular language, which is computable in
polynomial time as well.

######  Theorem 4.4.

Priority and block downward closures for regular languages are effectively
computable in time polynomial in the number of states in the NFA recognizing
the language.

Theorems 4.4 and 3.8 now allow us to reduce the priority downward closure
computability to computability for block order.

######  Theorem 4.5.

If $\mathcal{C}$ is a full trio and we can effectively compute block downward
closures for $\mathcal{C}$, then we can effectively compute priority downward
closures.

######  Proof 4.6.

The key idea is to reduce priority downward closure computation to the setting
where (i) all words end in the same letter and (ii) the alphabet is flat.
Since by Lemma 3.8, on those languages, the block order is finer than the
priority order, computing the block order will essentially be sufficient.

Let us first establish (i). Let $L\in\mathcal{C}$. Then for each $a\in\Sigma$,
the language $L_{a}=L\cap\Sigma^{*}a$ belongs to $\mathcal{C}$. Since
$L=\bigcup_{a\in\Sigma}L_{a}\cup E$ and thus
$L\mathord{\downarrow_{\mathsf{P}}}=\bigcup_{a\in\Sigma}L_{a}\mathord{\downarrow_{\mathsf{P}}}\cup
E$, it suffices to compute priority downward closures for each $L_{a}$, where
$E=\\{\epsilon\\}$ if $\epsilon\in L$, else $\emptyset$. This means, it
suffices to compute priority downward closures for languages where all words
end in the same letter.

To achieve (ii), we make the alphabet flat. We say that
$(\Sigma,\mathcal{P}^{\prime})$ is the _flattening_ of
$(\Sigma,\mathcal{P}=[0,d])$, if $\mathcal{P}^{\prime}$ is obtained by
choosing a total order to $\Sigma$ such that if $a$ has smaller priority than
$b$ in $(\Sigma,\mathcal{P})$, then $a$ has smaller priority than $b$ in
$(\Sigma,\mathcal{P}^{\prime})$. (In other words, we pick an arbitrary
linearization of the quasi-order on $\Sigma$ that expresses “has smaller
priority than”). Then, we assign priorities based on this total ordering. Let
$\preccurlyeq_{\mathsf{B}}^{\mathsf{flat}}$ and
$\preccurlyeq_{\mathsf{P}}^{\mathsf{flat}}$ denote the block order and
priority order, resp., based on the flat priority assignment. It is a simple
observation that for $u,v\in\Sigma^{*}$, we have that
$u\preccurlyeq_{\mathsf{P}}^{\mathsf{flat}}v$ implies
$u\preccurlyeq_{\mathsf{P}}v$.

Now observe that for $u,v\in L_{a}$, Lemma 3.8 tells us that
$u\preccurlyeq_{\mathsf{B}}^{\mathsf{flat}}v$ implies
$u\preccurlyeq_{\mathsf{P}}^{\mathsf{flat}}v$ and therefore also
$u\preccurlyeq_{\mathsf{P}}v$. This implies that
$(L_{a}\mathord{\downarrow_{\mathsf{B}}^{\mathsf{flat}}})\mathord{\downarrow_{\mathsf{P}}}=L_{a}\mathord{\downarrow_{\mathsf{P}}}$.
By assumption, we can compute a finite automaton ${\rm NewA}$ with
$\mathcal{L}({\rm
NewA})=L_{a}\mathord{\downarrow_{\mathsf{B}}^{\mathsf{flat}}}$. Since then
$\mathcal{L}({\rm
NewA})\mathord{\downarrow_{\mathsf{P}}}=(L_{a}\mathord{\downarrow_{\mathsf{B}}^{\mathsf{flat}}})\mathord{\downarrow_{\mathsf{P}}}=L_{a}\mathord{\downarrow_{\mathsf{P}}}$,
we can compute $L_{a}\mathord{\downarrow_{\mathsf{P}}}$ by applying Theorem
4.4 to ${\rm NewA}$ to compute $\mathcal{L}({\rm
NewA})\mathord{\downarrow_{\mathsf{P}}}=L_{a}\mathord{\downarrow_{\mathsf{P}}}$.

##  5 One-counter Languages

In this section, we show that for the class of languages accepted by one-
counter automata, which form a full-trio [9, Theorem 4.4], the block and
priority downward closures can be computed in polynomial time. We prove the
following theorem.

######  Theorem 5.1.

Given an OCA ${\rm NewA}$, $\mathcal{L}({\rm
NewA})\mathord{\downarrow_{\mathsf{B}}}$ and $\mathcal{L}({\rm
NewA})\mathord{\downarrow_{\mathsf{P}}}$ are computable in polynomial time.

Here, the difficulty is that existing downward closure constructions exploit
that inserting any letters in a word yields a super-word. However, for the
block order, this might not be true: Introducing high-priority letters might
split a block unintentionally. However, we observe that the subword closure
construction from [3] can be modified so that when constructing larger runs
(to show that our NFA only accepts words in the downward closure), we only
repeat existing factors. Lemma 3.5 then yields that the resulting word is
block-larger.

According to Theorem 4.5, it suffices to show that block downward closures are
computable in polynomial time (an inspection of the proof of Theorem 4.5 shows
that computing the priority downward closure only incurs a polynomial
overhead).

#### One-counter automata.

One-counter automata are finite state automata with a counter that can be
incremented, decremented, or tested for zero. Formally, a _one-counter
automaton (OCA)_ ${\rm NewA}$ is a $5$-tuple $(Q,\Sigma,\delta,q_{0},F)$ where
$Q$ is a finite set of states, $q_{0}\in Q$ is an initial state, $F\subseteq
Q$ is a set of final states, $\Sigma$ is a finite alphabet and
$\delta\subseteq Q\times(\Sigma\cup\\{\epsilon\\})\times\\{-1,0,+1,z\\}\times
Q$ is a set of transitions. Transitions $(p_{1},a,s,p_{2})\in\delta$ are
classified as _incrementing_ $(s=+1)$, _decrementing_ $(s=-1)$, _internal_
$(s=0)$, or _test for zero_ $(s=z)$.

A _configuration_ of an $OCA$ is a pair that consists of a state and a (non-
negative) counter value, i.e., $(q,n)\in Q\times\mathbb{N}$. A sequence
$\pi=(p_{0},c_{0}),t_{1},(p_{1},c_{1}),t_{2},\cdots,t_{m},(p_{m},c_{m})$ where
$(p_{i},c_{i})\in Q\times\mathbb{Z}$, $t_{i}\in\delta$ and
$(p_{i-1},c_{i-1})\xrightarrow{t_{i}}(p_{i},c_{i})$ is called:

  * •

a _quasi-run_ , denoted $\pi=(p_{0},c_{0})\xRightarrow{w}_{\rm
NewA}(p_{m},c_{m})$, if none of $t_{i}$ is a test for zero;

  * •

a _run_ , denoted $\pi=(p_{0},c_{0})\xrightarrow{w}_{\rm NewA}(p_{m},c_{m})$,
if all $(p_{i},c_{i})\in Q\times\mathbb{N}$.

For any quasi-run $\pi$ as above, the sequence of transitions
$t_{1},\cdots,t_{m}$ is called a _walk_ from the state $p_{0}$ to the state
$p_{m}$. A run $(p_{0},c_{0})\xrightarrow{w}(p_{m},c_{m})$ is called
_accepting_ in ${\rm NewA}$ if $(p_{0},c_{0})=(q_{0},0)$ where $q_{0}$ is the
initial state of ${\rm NewA}$ and $p_{m}$ is a final state of ${\rm NewA}$,
i.e. $p_{m}\in F$. In such a case, the word $w$ is _accepted_ by ${\rm NewA}$.

#### Simple one-counter automata

As we will show later, computing block downward closures of OCA easily reduces
to the case of simple OCA. A _simple OCA (SOCA)_ is defined analogously to
OCA, with the differences that (i) there are no zero tests, (ii) there is only
one final state, (iii) for acceptance, the final counter value must be zero.

We first show that the block downward closures can be effectively computed for
the simple one-counter automata languages.

######  Proposition 5.2.

Given a simple OCA ${\rm NewA}$, we can compute $\mathcal{L}({\rm
NewA})\mathord{\downarrow_{\mathsf{B}}}$ in polynomial time.

We present a rough sketch of the construction, full details can be found in
Appendix C. The starting point of the construction is the one for subwords in
[3], but the latter needs to be modified in a non-obvious way using Lemma 3.5.

Let ${\rm NewA}=(Q,\Sigma,\delta,q_{0},q_{f})$ be a simple OCA, with $|Q|=K$.
We construct an NFA $\mathcal{B}$ that can simulate ${\rm NewA}$ in three
different modes. In the first mode, it simulates ${\rm NewA}$ until the
counter value reaches $K$, and when the value reaches $K+1$, it switches to
the second mode. The second mode simulates ${\rm NewA}$ while the counter
value stays below $K^{2}+K+1$. Moreover, and this is where our construction
differs from [3]: if $\mathcal{B}$ is in the second mode simulating ${\rm
NewA}$ in some state $q$, then $\mathcal{B}$ can spontaneously execute a loop
from $q$ to $q$ of ${\rm NewA}$ while ignoring its counter updates. When the
counter value in the second mode drops to $K$ again, $\mathcal{B}$ non-
deterministically switches to the third mode to simulate ${\rm NewA}$ while
the counter value stays below $K$. Thus, $\mathcal{B}$ only needs to track
counter values in $[0,K^{2}+K+1]$, meaning they can be stored in its state. We
claim that then $\mathcal{L}({\rm
NewA})\subseteq\mathcal{L}(\mathcal{B})\subseteq\mathcal{L}({\rm
NewA})\mathord{\downarrow_{\mathsf{B}}}$.

######  Lemma 5.3.

$\mathcal{L}({\rm NewA})\subseteq\mathcal{L}(\mathcal{B})$.

If a word in $\mathcal{L}({\rm NewA})$ has a run with counters bounded by
$K^{2}+K+1$, then it trivially belongs to $\mathcal{L}(\mathcal{B})$. If the
counters go beyond $K^{2}+K+1$, then with the classical “unpumping” argument,
one can extract two loops, one increasing the counter, one decreasing it.
These loops can then be simulated by the spontaneous loops in the second mode
of $\mathcal{B}$.

The more interesting inclusion is the following:

######  Lemma 5.4.

$\mathcal{L}(\mathcal{B})\subseteq\mathcal{L}({\rm
NewA})\mathord{\downarrow_{\mathsf{B}}}$.

We have to show that each spontaneous loop in $\mathcal{B}$ can be justified
by padding the run with further loop executions so as to obtain a run of ${\rm
NewA}$. This is possible because to execute such a spontaneous loop, we must
have gone beyond $K$ and later go to zero again. Thus, there exists a “pumping
up” loop adding, say $k\geq 0$ to the counter, and a “pumping down” loop,
subtracting, say $\ell\geq 0$ from the counter. We can therefore repeat all
spontaneous loops so often that their effect — when seen as transitions in
${\rm NewA}$ — is a (positive or negative) multiple $M$ of $k\cdot\ell$. Then,
we execute the $k$\- and the $\ell$-loop so often so as to get the counter
values so high that (i) our repeated spontaneous loops never cross zero and
(ii) the effect difference of the new loops is exactly $M$. Since in our
construction (in contrast to [3]), the padding only _repeated words that
already exist_ in the run of $\mathcal{B}$, Lemma 3.5 implies that the word of
$\mathcal{B}$ embeds via the block order.

#### General OCA

Let us now show how to construct the block downward closure of general OCAs.
Suppose we are given an OCA ${\rm NewA}$. For any two states $p,q$, consider
the simple OCA ${\rm NewA}_{p,q}$ obtained from ${\rm NewA}$ by removing all
zero tests, making $p$ initial, and $q$ final. Then $\mathcal{L}({\rm NewA})$
is the set of words read from $(p,0)$ to $(q,0)$ without using zero tests. We
now compute for each $p,q$ a finite automaton $\mathcal{B}_{p,q}$ for the
block downward closure of ${\rm NewA}_{p,q}$. Clearly, we may assume that
$\mathcal{B}_{p,q}$ has exactly one initial state and one final state.
Finally, we obtain the finite automaton $\mathcal{B}$ from ${\rm NewA}$ as
follows: We remove all transitions _except_ the zero tests. Each zero test
from $p$ to $q$ is replaced with an edge $p\xrightarrow{\varepsilon}q$.
Moreover, for any states $p$ and $q$ coming from ${\rm NewA}$, we glue in the
automaton $\mathcal{B}_{p,q}$ (by connecting $p$ with $\mathcal{B}_{p,q}$’s
initial state and connecting $\mathcal{B}_{p,q}$’s final state with $q$).
Then, since the block order is multiplicative, we have that $L(\mathcal{B})$
accepts exactly the block downward closure of ${\rm NewA}$.

Futhermore, note that since our construction for simple OCA is polynomial, the
general case is as well: The latter employs the former to $|Q|^{2}$ simple
OCAs.

##  6 Context-free Languages

The key trick in our construction for OCA was that we could modify the subword
construction so that the overapproximating NFA $\mathcal{B}$ has the property
that in any word from $\mathcal{L}(\mathcal{B})$, we can repeat factors to
obtain a word from ${\rm NewA}$. This was possible because in an OCA,
essentially any pair of loops—one incrementing, one decrementing—could be
repeated to pad a run.

However, in context-free languages, the situation is more complicated. With a
stack, any pumping must always ensure that stack contents match: It is not
possible to compensate stack effects with just two loops. In terms of
grammars, the core idea for subword closures of context-free languages $L$ is
usually to overapproximate “pump-like” derivations $X\xRightarrow{*}uXv$ by
observing that—up to subwords—they can generate any $u^{\prime}Xv^{\prime}$
where the letters of $u^{\prime}$ can occur on the left and the letters of
$v^{\prime}$ can occur on the right in derivations $X\xRightarrow{*}\cdot
X\cdot$. Showing that all such words belong to the downward closure leads to
derivations $X\xRightarrow{*}u^{\prime\prime}\bar{v}Xv^{\prime\prime}\bar{u}$,
where $u^{\prime\prime},v^{\prime\prime}$ are super-words of
$u^{\prime},v^{\prime}$ such that $X\xRightarrow{*}u^{\prime\prime}X\bar{u}$
and $X\xRightarrow{*}\bar{v}Xv^{\prime\prime}$ can be derived. The additional
infixes could introduce high priority letters and thus split blocks
unintentionally.

Therefore, we provide a novel recursive approach to compute the block downward
closure by decomposing derivations at high-priority letters. This is non-
trivial as this decomposition might not match the decomposition given by
derivation trees. Formally, we show:

######  Theorem 6.1.

Given a context-free language $L\subseteq\Sigma_{\leq n}^{*}$, one can
construct a doubly-exponential-sized automaton for
$L\mathord{\downarrow_{\mathsf{B}}}$, and thus also for
$L\mathord{\downarrow_{\mathsf{P}}}$.

We do not know if this doubly exponential upper bound is optimal. A singly-
exponential lower bound follows from the subword case: It is known that
subword downward closures of context-free languages can require exponentially
many states [5]. However, it is not clear whether for priority or block
downward closures, there is a singly-exponential construction.

We again note that Theorem 4.5 (and its proof) imply that for Theorem 6.1, it
suffices to compute a finite automaton for the block downward closure of the
context-free language: Computing the priority downward closure then only
increases the size polynomially.

#### Grammars

We present the construction using _context-free grammars_ , which are tuples
$\mathcal{G}=(N,T,P,S)$, where $N$ is a finite set of _non-terminal letters_ ,
$T$ is a finite set of _terminal letters_ , $P$ is a finite set of
_productions_ of the form $X\to w$ with $X\in N$ and $w\in(N\cup T)^{*}$, and
$S$ is the _start symbol_. For $u,v\in(N\cup T)^{*}$, we have $u\Rightarrow v$
if there is a production $X\to w$ in $P$ and $x,y\in(N\cup T)^{*}$ with
$u=xXy$ and $v=xwy$. The _language generated by $\mathcal{G}$_, is then
$\mathcal{L}(\mathcal{G}):=\\{w\in T^{*}\mid S\xRightarrow{*}w\\}$, where
$\xRightarrow{*}$ is the reflexive, transitive closure of $\Rightarrow$.

#### Assumption on the alphabet

In order to compute block downward closures, it suffices to do this for flat
alphabets (see Section 3). The argument is essentially the same as in Theorem
4.5: By flattening the alphabet as in the proof of Theorem 4.5, we obtain a
finer block order, so that first computing an automaton for the flat alphabet
and then applying Theorem 4.4 to the resulting finite automaton will yield a
finite automaton for the original (non-flat) alphabet. In the following, we
will assume that the input grammar $\mathcal{G}$ is in Chomsky normal form,
meaning every production is of the form $X\to YZ$ for non-terminals $X,Y,Z$,
or of the form $X\to a$ for a non-terminal $X$ and a terminal $a$.

#### Kleene grammars

Suppose we are given a context-free grammar $\mathcal{G}=(N,\Sigma,P,S)$.
Roughly speaking, the idea is to construct another grammar
$\mathcal{G}^{\prime}$ whose language has the same block downward closure as
$\mathcal{L}(\mathcal{G})$, but with the additional property that every word
can be generated using a derivation tree that is _acyclic_ , meaning that each
path contains every non-terminal at most once. Of course, if this were
literally true, $\mathcal{G}^{\prime}$ would generate a finite language.
Therefore, we allow a slightly expanded syntax: We allow Kleene stars in
context-free productions.

This means, we allow right-hand sides to contain occurrences of $B^{*}$, where
$B$ is a non-terminal. The semantics is the obvious one: When applying such a
rule, then instead of inserting $B^{*}$, we can generate any $B^{k}$ with
$k\geq 0$. We call grammars with such productions _Kleene grammar_. A
_derivation tree_ in a Kleene grammar is defined as for context-free grammars,
aside from the expected modification: If some $B^{*}$ occurs on a right-hand
side, then we allow any (finite) number of $B$-labeled children in the
respective place. Then indeed, a Kleene grammar can generate infinite sets
using acyclic derivation trees. Given a Kleene grammar $\mathcal{H}$, let
$\mathsf{acyclic}(\mathcal{H})$ be the set of words generated by $\mathcal{H}$
using acyclic derivation trees.

######  Lemma 6.2.

Given a Kleene grammar $\mathcal{H}$, one can construct an exponential-sized
finite automaton accepting $\mathsf{acyclic}(\mathcal{H})$.

######  Proof 6.3 (Proof sketch).

The automaton simulates a (say, preorder) traversal of an acyclic derivation
tree of $\mathcal{H}$. This means, its state holds the path to the currently
visited node in the derivation tree. Since every path has length at most
$|N|$, where $N$ is the set of non-terminals of $\mathcal{H}$, the automaton
has at most exponentially many states.

Given Lemma 6.2, for Theorem 6.1, it suffices to construct a Kleene grammar
$\mathcal{G}^{\prime}$ of exponential size such that
$\mathsf{acyclic}(\mathcal{G}^{\prime})\mathord{\downarrow_{\mathsf{B}}}=\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$.

#### Normal form and grammar size

We will ensure that in the constructed grammars, the productions are of the
form (i) $X\to w$, where $w$ is a word of length $\leq 3$ and consisting of
non-terminals $Y$ or Kleene stars $Y^{*}$ or (ii) $X\to a$ where $a$ is a
terminal. This means, the total size of the grammar is always polynomial in
the number of non-terminals. Therefore, to analyze the complexity, it will
suffice to measure the number of non-terminals.

#### Highest occurring priorities

Similar to classical downward closure constructions for context-free
languages, we want to overapproximate the set of words generated by “pump
derivations” of the form $X\xRightarrow{*}uXv$. Since we are dealing with
priorities, we first partition the set of such derivations according to the
highest occurring priorities, on the left and on the right. Thus, for
$r,s\in[0,p]$, we will consider all derivations $X\xRightarrow{*}uXv$ where
$r$ is the highest occurring priority in $u$ and $s$ is the highest occurring
priority in $v$. To ease notation, we define $\Sigma_{\max r}$ to be the set
of words in $\Sigma_{\leq r}^{*}$ in which $r$ is the highest occurring
priority. Since $\Sigma_{\max r}=\Sigma_{\max r}^{+}$, we will write
$\Sigma_{\max r}^{+}$ to remind us that this is not an alphabet. Notice that
for $r\in[1,p]$, we have $\Sigma_{\max r}^{+}=\Sigma_{\leq r}^{*}r\Sigma_{\leq
r}^{*}$ and $\Sigma_{\max 0}^{+}=\Sigma_{\leq 0}^{*}$.

#### Language of ends

In order to perform an inductive construction, we need a way to transform
pairs $(u,v)\in\Sigma_{\max r}^{+}\times\Sigma_{\max s}^{+}$ into words over
an alphabet with fewer priorities. Part of this will be achieved by the _end
maps_ $\overleftarrow{\tau}_{r}(\cdot)$ and $\overrightarrow{\tau}_{s}(\cdot)$
as follows. Let $\hat{\Sigma}$ be the priority alphabet obtained from $\Sigma$
by adding the letters $\\#$, $\overleftarrow{\\#}$, and $\overrightarrow{\\#}$
as letters with priority zero. Now for $r\in[1,p]$, the function
$\overleftarrow{\tau}_{r}\colon\Sigma_{\max r}^{+}\to\hat{\Sigma}_{\leq
r-1}^{*}$ is defined as:

$\overleftarrow{\tau}_{r}(w)=u\overleftarrow{\\#}v,\leavevmode\nobreak\
\text{where $w=urx_{1}r\cdots x_{n}rv$ for some $n\geq 0$,
$u,v,x_{1},\ldots,x_{n}\in\Sigma_{\leq r-1}^{*}$}.$

Thus, $\overleftarrow{\tau}_{r}(w)$ is obtained from $w$ by replacing the
largest possible infix surrounded by $r$ with $\overleftarrow{\\#}$. For
$r=0$, it will be convenient to have the constant function
$\overleftarrow{\tau}_{0}\colon\Sigma_{\max
0}^{+}\to\\{\overleftarrow{\\#}\\}$. Analogously, we define for $s\in[1,p]$
the function $\overrightarrow{\tau}_{s}\colon\Sigma_{\max
s}^{+}\to\hat{\Sigma}_{\leq s-1}^{*}$ by

$\overrightarrow{\tau}_{s}(w)=u\overrightarrow{\\#}v,\leavevmode\nobreak\
\text{where $w=usx_{1}s\cdots x_{n}sv$ for some $n\geq 0$,
$u,v,x_{1},\ldots,x_{n}\in\Sigma_{\leq s-1}^{*}$}.$

Moreover, we also set $\overrightarrow{\tau}_{0}\colon\Sigma_{\max
0}^{+}\to\\{\overrightarrow{\\#}\\}$ to be the constant function yielding
$\overrightarrow{\\#}$.

In particular, for $r,s\in[1,p]$, we have
$\overleftarrow{\tau}_{r}(w),\overrightarrow{\tau}_{s}(w)\in\hat{\Sigma}_{\leq
p-1}$ and thus we have reduced the number of priorities. Now consider for
$r,s\in[0,p]$ the language

$\displaystyle
E_{X,r,s}=\\{\overleftarrow{\tau}_{r}(u)\\#\overrightarrow{\tau}_{s}(v)\mid
X\xRightarrow{*}uXv,\leavevmode\nobreak\ u\in\Sigma_{\leq r}^{*}r\Sigma_{\leq
r}^{*},\leavevmode\nobreak\ v\in\Sigma_{\leq s}^{*}s\Sigma_{\leq s}^{*}\\}.$

For the language $E_{X,r,s}$, it is easy to construct a context-free grammar:

######  Lemma 6.4.

Given $\mathcal{G}$, a non-terminal $X$, and $r,s\in[0,p]$, one can construct
a grammar $\mathcal{E}_{X,r,s}$ for $E_{X,r,s}$ of linear size.

Defining the sets $E_{X,r,s}$ with fresh zero-priority letters $\\#$,
$\overleftarrow{\\#}$, $\overrightarrow{\\#}$ is a key trick in our
construction: Note that each word in $E_{X,r,s}$ is of the form
$u\overleftarrow{\\#}v\\#w\overrightarrow{\\#}x$ for $u,v,w,x\in\Sigma_{\leq
p-1}^{*}$. The segments $u,v,w,x$ come from different blocks of the entire
generated word, so applying the block downward closure construction
recursively to $E_{X,r,s}$ must guarantee that these segments embed as if they
were blocks. However, there are only a bounded number of segments. Thus, we
can reduce the number of priorities while retaining the block behavior by
using fresh zero-priority letters. This is formalized in the following Lemma:

######  Lemma 6.5.

For $u,u^{\prime},v,v^{\prime}\in\Sigma_{\leq p}^{*}$, we have
$u\\#v\preccurlyeq_{\mathsf{B}}u^{\prime}\\#v^{\prime}$ iff both (i)
$u\preccurlyeq_{\mathsf{B}}u^{\prime}$ and (ii)
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$.

#### Language of repeated words

Roughly speaking, the language $E_{X,r,s}$ captures the “ends” of words
derived in derivations $X\xRightarrow{*}uXv$ with $u\in\Sigma_{\max r}^{+}$
and $v\in\Sigma_{\max s}^{+}$: On the left, it keeps everything that is not
between two occurrences of $r$ and on the right, it keeps everything not
between two occurrences of $s$. We now need languages that capture the infixes
that can occur between $r$’s and $s$’s, respectively. Intuitively, these are
the words that can occur again and again in words derived from $X$. There is a
“left version” and a “right version”. We set for $r,s\in[1,p]$:

$\displaystyle\overleftarrow{R}_{X,r,s}$ $\displaystyle=\\{yr\mid
y\in\Sigma_{\leq r-1}^{*},\leavevmode\nobreak\ \exists x,z\in\Sigma_{\leq
r}^{*},\leavevmode\nobreak\ v\in\Sigma_{\max s}^{+}\colon
X\xRightarrow{*}xryrzXv\\}$ $\displaystyle\overrightarrow{R}_{X,r,s}$
$\displaystyle=\\{ys\mid y\in\Sigma_{\leq s-1}^{*},\leavevmode\nobreak\
\exists u\in\Sigma_{\max r}^{+},\leavevmode\nobreak\ x,z\in\Sigma_{\leq
r}^{*}\colon X\xRightarrow{*}uXxsysz\\}.$

The case where one side has highest priority zero must be treated slightly
differently: There are no enveloping occurrences of some $r,s\in[1,p]$.
However, we can overapproximate those words by the set of all words over a
particular alphabet. Specifically, for $r,s\in[0,p]$, we set

$\displaystyle\overrightarrow{R}_{X,0,s}$ $\displaystyle=\\{a\in\Sigma_{\leq
0}\mid\exists u\in\Sigma_{\max 0}^{+},\leavevmode\nobreak\ v\in\Sigma_{\max
s}^{+}\colon X\xRightarrow{*}uXv,\leavevmode\nobreak\ \text{$a$ occurs in
$u$}\\}$ $\displaystyle\overleftarrow{R}_{X,r,0}$
$\displaystyle=\\{a\in\Sigma_{\leq 0}\mid\exists u\in\Sigma_{\max
r}^{+},\leavevmode\nobreak\ v\in\Sigma_{\max 0}^{+}\colon
X\xRightarrow{*}uXv,\leavevmode\nobreak\ \text{$a$ occurs in $v$}\\}$

######  Lemma 6.6.

Given $\mathcal{G}$, a non-terminal $X$, and $r,s\in[0,p]$, one can construct
grammars $\overleftarrow{\mathcal{R}}_{X,r,s}$,
$\overrightarrow{\mathcal{R}}_{X,r,s}$ for
$\overleftarrow{R}_{X,r,s}$,$\overrightarrow{R}_{X,r,s}$, respectively, of
linear size.

#### Overapproximating derivable words

The languages $E_{X,r,s}$ and $\overleftarrow{R}_{X,r,s}$ and
$\overrightarrow{R}_{X,r,s}$ now serve to define overapproximations of the set
of $(u,v)\in\Sigma_{\max r}^{+}\times\Sigma_{\max s}^{+}$ with
$X\xRightarrow{*}uXv$: One can obtain each such pair by taking a word from
$E_{X,r,s}$, replacing $\overleftarrow{\\#}$ and $\overrightarrow{\\#}$,
resp., by words in $r\overleftarrow{R}_{X,r,s}^{*}$
($\overleftarrow{R}_{X,0,s}^{*}$ if $r=0$) and
$s\overrightarrow{R}_{X,r,s}^{*}$ ($\overrightarrow{R}_{X,r,0}^{*}$ if $s=0$),
respectively. By choosing the right words from $E_{X,r,s}$,
$\overleftarrow{R}_{X,r,s}$, and $\overrightarrow{R}_{X,r,s}$, we can thus
obtain $u\\#v$. However, this process will also yield other words that cannot
be derived. However, the key idea in our construction is that every word
obtainable in this way from $E_{X,r,s}$, $\overleftarrow{R}_{X,r,s}$, and
$\overrightarrow{R}_{X,r,s}$ will be in the block downward closure of a pair
of words derivable using $X\xRightarrow{*}\cdot X\cdot$.

Let us make this precise. To describe the set of words obtained from
$E_{X,r,s}$, $\overleftarrow{R}_{X,r,s}$, and $\overrightarrow{R}_{X,r,s}$, we
need the notion of a substitution. For alphabets $\Gamma_{1},\Gamma_{2}$, a
_substitution_ is a map $\sigma\colon\Gamma_{1}\to 2^{\Gamma_{2}^{*}}$ that
yields a language in $\Gamma_{2}$ for each letter in $\Gamma_{1}$. Given a
word $w=w_{1}\cdots w_{n}$ with $w_{1},\ldots w_{n}\in\Gamma_{1}$, we define
$\sigma(w):=\sigma(w_{1})\cdots\sigma(w_{n})$. Then for
$K\subseteq\Gamma_{1}^{*}$, we set $\sigma(K)=\bigcup_{w\in K}\sigma(w)$. Now
let $\Sigma_{X,r,s}\colon\hat{\Sigma}_{\leq p}\to 2^{\hat{\Sigma}_{\leq
p}^{*}}$ be the substitution that maps every letter in $\Sigma_{\leq
p}\cup\\{\\#\\}$ to itself (as a singleton) and maps $\overleftarrow{\\#}$ to
$r\overleftarrow{R}_{X,r,s}^{*}$ and $\overrightarrow{\\#}$ to
$s\overrightarrow{R}_{X,r,s}^{*}$. Now our observation from the previous
paragraph can be phrased as:

######  Lemma 6.7.

For every $u\\#v\in\Sigma_{X,r,s}(E_{X,r,s})$, there are
$u^{\prime}\in\Sigma_{\max r}^{+}$ and $v^{\prime}\in\Sigma_{\max s}^{+}$ with
$u\preccurlyeq_{\mathsf{B}}u^{\prime}$,
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$, and
$X\xRightarrow{*}u^{\prime}Xv^{\prime}$.

#### Constructing the Kleene grammar

We now construct the Kleene grammar for
$\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$ by first computing
the grammars $\mathcal{E}_{X,r,s}$, $\overleftarrow{\mathcal{R}}_{X,r,s}$, and
$\overrightarrow{\mathcal{R}}_{X,r,s}$ for each non-terminal $X$ and each
$r,s\in[1,p]$. Then, since $\mathcal{E}_{X,r,s}$,
$\overleftarrow{\mathcal{R}}_{X,r,s}$, and
$\overrightarrow{\mathcal{R}}_{X,r,s}$ generate languages with at most $p-1$
priorities, we can call our construction recursively to obtain grammars
$\mathcal{E}^{\prime}_{X,r,s}$,
$\overleftarrow{\mathcal{R}}^{\prime}_{X,r,s}$, and
$\overrightarrow{\mathcal{R}}^{\prime}_{X,r,s}$, respectively. Then, we add
all productions of the grammars $\mathcal{E}^{\prime}_{X,r,s}$,
$\overleftarrow{\mathcal{R}}^{\prime}_{X,r,s}$, and
$\overrightarrow{\mathcal{R}}^{\prime}_{X,r,s}$ to $\mathcal{G}^{\prime}$.
Moreover, we make the following modifications: Each production of the form
$Y\to\overleftarrow{\\#}$ (resp. $Y\to\overrightarrow{\\#}$) in
$\mathcal{E}_{X,r,s}$ is replaced with $Y\to
Z_{r}\overleftarrow{S}_{X,r,s}^{*}$ (resp. $Y\to
Z_{s}\overrightarrow{S}_{X,r,s}^{*}$), where $\overleftarrow{S}_{X,r,s}$
(resp. $\overrightarrow{S}_{X,r,s}$) is the start symbol of
$\overleftarrow{\mathcal{R}}^{\prime}_{X,r,s}$ (resp.
$\overrightarrow{\mathcal{R}}^{\prime}_{X,r,s}$), and $Z_{r}$ is a fresh non-
terminal used to derive $r$ or $\varepsilon$: We also have $Z_{r}\to r$ for
each $r\in[1,p]$ and $Z_{0}\to\varepsilon$. Moreover, each production
$Y\to\\#$ in $\mathcal{E}^{\prime}_{X}$ is removed and replaced with a
production $Y\to w$ for each production $X\to w$ in $\mathcal{G}$. We call the
resulting grammar $\mathcal{G}^{\prime}$.

#### Correctness

Let us now observe that the grammar $\mathcal{G}^{\prime}$ does indeed satisfy
$\mathcal{L}(\mathcal{G}^{\prime})\mathord{\downarrow_{\mathsf{B}}}=\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$.
The inclusion “$\supseteq$” is trivial as $\mathcal{G}^{\prime}$ is obtained
by adding productions. For the converse, we need some terminology. We say that
a derivation tree $t_{1}$ in $\mathcal{G}^{\prime}$ is obtained using an
_expansion step_ from $t_{0}$ if we take an $X$-labeled node $x$ in $t_{0}$,
where $X$ is a non-terminal from $\mathcal{G}$, and replace this node by a
derivation $X\xRightarrow{*}uwv$ using newly added productions (i.e. using
$\mathcal{E}_{X,r,s}$, $\overleftarrow{\mathcal{R}}_{X,r,s}$, and
$\overrightarrow{\mathcal{R}}_{X,r,s}$ and some $Y\to w$ where $X\to w$ was
the production applied to $x$ in $t_{0}$). Then by construction of
$\mathcal{G}^{\prime}$, any derivation in $\mathcal{G}^{\prime}$ can be
obtained from a derivation in $\mathcal{G}$ by finitely many expansion steps.
An induction on the number of expansion steps shows:

######  Lemma 6.8.

We have
$\mathcal{L}(\mathcal{G}^{\prime})\mathord{\downarrow_{\mathsf{B}}}=\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$.

#### Acyclic derivations suffice

Now that we have the grammar $\mathcal{G}^{\prime}$ with
$\mathcal{L}(\mathcal{G}^{\prime})\mathord{\downarrow_{\mathsf{B}}}=\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$,
it remains to show that every word in $\mathcal{G}^{\prime}$ can be derived
using an acyclic derivation:

######  Lemma 6.9.

$\mathsf{acyclic}(\mathcal{G}^{\prime})\mathord{\downarrow_{\mathsf{B}}}=\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$.

Essentially, this is due to the fact that any repetition of a non-terminal $X$
on some path means that we can replace a corresponding derivation
$X\xRightarrow{*}uXv$ by using new productions from
$\mathcal{E}^{\prime}_{X,r,s}$,
$\overleftarrow{\mathcal{R}}^{\prime}_{X,r,s}$, and
$\overrightarrow{\mathcal{R}}^{\prime}_{X,r,s}$. Since these also have the
property that every derivation can be made acyclic, the lemma follows. See
Appendix D for details.

#### Complexity analysis

To estimate the size of the constructed grammar, let $f_{p}(n)$ be the maximal
number of non-terminals of a constructed Kleene grammar for an input grammar
with $n$ non-terminals over $p$ priorities. By Lemmas 6.4 and 6.6, there is a
constant $c$ such that each grammar $\mathcal{E}_{X}$,
$\overleftarrow{\mathcal{R}}_{X}$, and $\overrightarrow{\mathcal{R}}_{X}$ has
at most $cn$ non-terminals. Furthermore, $\mathcal{G}^{\prime}$ is obtained by
applying our construction to $3n(p+1)^{2}$ grammars with $p-1$ priorities of
size $cn$, and adding $Z_{p}$. Thus $f_{p}(n)\leq n+3n(p+1)^{2}f_{p-1}(cn)+1$.
Since $f_{p-1}(n)\geq 1$, we can simplify to $f_{p}(n)\leq
4n(p+1)^{2}f_{p-1}(cn)$. It is easy to check that $f_{0}(n)\leq 4n+1\leq 5n$,
because $\mathcal{E}_{X,0,0}$ and $\overleftarrow{\mathcal{R}}_{X,0,0}$ and
$\overrightarrow{\mathcal{R}}_{X,0,0}$ each only have one non-terminal. Hence
$f_{p}(n)\leq(4n(p+1)^{2})^{p}f_{0}(c^{p}n)\leq(4n(p+1)^{2})\cdot 4(c^{p}n)$,
which is exponential in the size of $\mathcal{G}$.

##  7 Conclusion

We have initiated the study of computing priority and block downward closures
for infinite-state systems. We have shown that for OCA, both closures can be
computed in polynomial time. For CFL, we have provided a doubly exponential
construction.

Many questions remain. First, we leave open whether the doubly exponential
bound for context-free languages can be improved to exponential. An
exponential lower bound is easily inherited from the exponential lower bound
for subwords [5]. Moreover, it is an intriguing question whether computability
of subword downward closures for vector addition systems [18], higher-order
pushdown automata [19], and higher-order recursion schemes [11] can be
strengthend to block and priority downward closures.

## References

  * [1] Parosh Aziz Abdulla, Luc Boasson, and Ahmed Bouajjani.  Effective lossy queue languages.  In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 639–651. Springer, 2001.  doi:10.1007/3-540-48224-5\\_53.
  * [2] Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer.  Context-bounded analysis for concurrent programs with dynamic creation of threads.  Log. Methods Comput. Sci., 7(4), 2011.  doi:10.2168/LMCS-7(4:4)2011.
  * [3] Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, and Georg Zetzsche.  The complexity of regular abstractions of one-counter languages.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, page 207–216, New York, NY, USA, 2016. Association for Computing Machinery.  doi:10.1145/2933575.2934561.
  * [4] Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan.  On the upward/downward closures of Petri nets.  In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 49:1–49:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.  doi:10.4230/LIPIcs.MFCS.2017.49.
  * [5] Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund.  Finite automata for the sub- and superword closure of cfls: Descriptional and computational complexity.  In Adrian-Horia Dediu, Enrico Formenti, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 9th International Conference, LATA 2015, Nice, France, March 2-6, 2015, Proceedings, volume 8977 of Lecture Notes in Computer Science, pages 473–485. Springer, 2015.  doi:10.1007/978-3-319-15579-1\\_37.
  * [6] Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche.  Context-bounded analysis of concurrent programs (invited talk).  In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany, volume 261 of LIPIcs, pages 3:1–3:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  doi:10.4230/LIPIcs.ICALP.2023.3.
  * [7] Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche.  Context-bounded verification of context-free specifications.  Proc. ACM Program. Lang., 7(POPL):2141–2170, 2023.  doi:10.1145/3571266.
  * [8] Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche.  Context-bounded verification of thread pools.  Proc. ACM Program. Lang., 6(POPL):1–28, 2022.  doi:10.1145/3498678.
  * [9] J. Berstel.  Transductions and Context-Free Languages.  Vieweg+Teubner Verlag, 1979.
  * [10] S. Blake, D. Black, M. Carlson, Elwyn B. Davies, Zheng Wang, and Walter Weiss.  An architecture for differentiated services.  RFC, 2475:1–36, 1998.
  * [11] Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz.  The diagonal problem for higher-order recursion schemes is decidable.  In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 96–105. ACM, 2016.  doi:10.1145/2933575.2934527.
  * [12] Bruno Courcelle.  On constructing obstruction sets of words.  Bulletin of the EATCS, 44:178–186, 01 1991.
  * [13] Leonard Eugene Dickson.  Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors.  American Journal of Mathematics, 35(4):413–422, 1913.  URL: http://www.jstor.org/stable/2370405.
  * [14] A. Ehrenfeucht, D. Haussler, and G. Rozenberg.  On regularity of context-free languages.  Theoretical Computer Science, 27(3):311–332, 1983.  Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982.  doi:10.1016/0304-3975(82)90124-4.
  * [15] Jean Goubault-Larrecq, Simon Halfon, Prateek Karandikar, K. Narayan Kumar, and Philippe Schnoebelen.  The ideal approach to computing closed subsets in well-quasi-ordering.  CoRR, abs/1904.10703, 2019.  arXiv:1904.10703.
  * [16] Hermann Gruber, Markus Holzer, and Martin Kutrib.  The size of higman–haines sets.  Theoretical Computer Science, 387(2):167–176, 2007.  Descriptional Complexity of Formal Systems.  doi:10.1016/j.tcs.2007.07.036.
  * [17] Christoph Haase, Sylvain Schmitz, and Philippe Schnoebelen.  The Power of Priority Channel Systems.  Logical Methods in Computer Science, Volume 10, Issue 4, December 2014.  doi:10.2168/LMCS-10(4:4)2014.
  * [18] Peter Habermehl, Roland Meyer, and Harro Wimmel.  The downward-closure of Petri net languages.  In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 466–477. Springer, 2010.  doi:10.1007/978-3-642-14162-1\\_39.
  * [19] Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong.  Unboundedness and downward closures of higher-order pushdown automata.  In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 151–163. ACM, 2016.  doi:10.1145/2837614.2837627.
  * [20] Leonard H. Haines.  On free monoids partially ordered by embedding.  Journal of Combinatorial Theory, 6(1):94–98, 1969.  doi:10.1016/S0021-9800(69)80111-0.
  * [21] Simon Halfon.  On Effective Representations of Well Quasi-Orderings.  Theses, Université Paris-Saclay, June 2018.  URL: https://tel.archives-ouvertes.fr/tel-01945232.
  * [22] Graham Higman.  Ordering by Divisibility in Abstract Algebras.  Proceedings of the London Mathematical Society, s3-2(1):326–336, 01 1952.  doi:10.1112/plms/s3-2.1.326.
  * [23] J. Kruskal.  Well-quasi-ordering, the tree theorem, and vazsonyi’s conjecture.  Transactions of the American Mathematical Society, 95:210–225, 1960\.
  * [24] Jean-Yves Le Boudec.  The asynchronous transfer mode: a tutorial.  Computer Networks and ISDN Systems, 24(4):279–309, 1992.  The ATM-Asynchronous Transfer Mode.  doi:10.1016/0169-7552(92)90114-6.
  * [25] Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche.  General decidability results for asynchronous shared-memory programs: Higher-order and beyond.  Log. Methods Comput. Sci., 18(4), 2022.  doi:10.46298/lmcs-18(4:2)2022.
  * [26] Richard Mayr.  Undecidable problems in unreliable computations.  In Gaston H. Gonnet and Alfredo Viola, editors, LATIN 2000: Theoretical Informatics, pages 377–386, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg.
  * [27] Jeffrey Shallit.  A Second Course in Formal Languages and Automata Theory.  Cambridge University Press, 2008.  doi:10.1017/CBO9780511808876.
  * [28] Salvatore La Torre, Anca Muscholl, and Igor Walukiewicz.  Safety of parametrized asynchronous shared-memory systems is almost always decidable.  In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 72–84. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.  doi:10.4230/LIPIcs.CONCUR.2015.72.
  * [29] Jan van Leeuwen.  Effective constructions in well-partially-ordered free monoids.  Discrete Mathematics, 21(3):237–252, 1978.
  * [30] Georg Zetzsche.  An approach to computing downward closures.  In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 440–451. Springer, 2015.  doi:10.1007/978-3-662-47666-6\\_35.
  * [31] Georg Zetzsche.  Computing downward closures for stacked counter automata.  In Ernst W. Mayr and Nicolas Ollinger, editors, 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, volume 30 of LIPIcs, pages 743–756. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.  doi:10.4230/LIPIcs.STACS.2015.743.
  * [32] Georg Zetzsche.  The complexity of downward closure comparisons.  In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 123:1–123:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.  doi:10.4230/LIPIcs.ICALP.2016.123.
  * [33] Georg Zetzsche.  Monoids as Storage Mechanisms.  PhD thesis, Technische Universität Kaiserslautern, 2016.
  * [34] Georg Zetzsche.  Separability by piecewise testable languages and downward closures beyond subwords.  In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 929–938. ACM, 2018.  doi:10.1145/3209108.3209201.

##  Appendix A Missing proofs from Section 3

Before we prove Theorem 3.2, we recall some well-known facts that are used in
the proof. WQOs are preserved under many operations on quasi-ordered sets. We
mention some of these operations below, which will be used later in the paper
to show the WQO property. The reader is referred to Halfon’s thesis [21] for a
well informed survey of such results. We mention some of these results below.

######  Lemma A.1 (Dickson’s Lemma, [13] ).

Given two WQOs $(A,\leq_{1})$ and $(B,\leq_{2})$, its product $(A\times
B,\leq_{1}\times\leq_{2})$ is also a WQO. Here,
$(a_{1},b_{1})\leq_{1}\times\leq_{2}(a_{2},b_{2})$ if $a_{1}\leq_{1}a_{2}$ and
$b_{1}\leq_{2}b_{2}$.

######  Lemma A.2 (Higman’s Lemma, [22]).

$(X^{*},\leq_{*})$ is a WQO $\iff$ $(X,\leq)$ is a WQO. We say
$a_{1}a_{2}\cdots a_{k}\leq_{*}b_{1}b_{2}\cdots b_{l}$ if there is a strictly
monotonically increasing map $\phi:[1,k]\rightarrow[1,l]$ such that $\forall\
i\in[1,k],a_{i}\leq b_{\phi(i)}$.

######  Lemma A.3 (Monomorphism Lemma, [23]).

Let $(X,\leq_{1})$ and $(Y,\leq_{2})$ be two quasi orders, and $h:X\rightarrow
Y$ be a monomorphism. If $(Y,\leq_{2})$ is a WQO then $(X,\leq_{1})$ is a WQO.

We prove that the block order is a WQO. We restate Theorem 3.2 for convenience
of the reader. See 3.2

######  Proof A.4.

We will prove the lemma by induction on the size of $\mathcal{P}$. Firstly, we
note that generalized block order and subword order coincide for singleton
priority set i.e. $u\preccurlyeq_{\mathsf{B}}v\iff u\preccurlyeq v$, by
definition. Since $(\Sigma^{*},\preccurlyeq)$ is a WQO, this gives us the base
case, i.e. if $\mathcal{P}$ is singleton, then
$(\Sigma^{*},\preccurlyeq_{\mathsf{B}})$ is a WQO.

Now, for the induction hypothesis, assume that the lemma is true for
$\mathcal{P}=[0,p-1]$. We show that the lemma holds for $\mathcal{P}=[0,p]$.

Since $(A,=)$ is a WQO for any finite $A$, by Dickson’s lemma,
$(\Sigma_{p-1}^{*}\times A_{p},\leavevmode\nobreak\
\preccurlyeq_{\mathsf{B}}\times=)$ is a WQO. Then, by Higman’s lemma,
$((\Sigma_{p-1}^{*}\times A_{p})^{*},\
(\preccurlyeq_{\mathsf{B}}\times=)_{*})$ is a WQO. Again, by Dickson’s lemma,
$((\Sigma_{p-1}^{*}\times A_{p})\times(\Sigma_{p-1}^{*}\times
A_{p})^{*}\times\Sigma_{p-1}^{*},\
(\preccurlyeq_{\mathsf{B}}\times=)\times(\preccurlyeq_{\mathsf{B}}\times=)_{*}\times\preccurlyeq_{\mathsf{B}})$
is a WQO.

Now, consider the function

$h:(\Sigma_{p}^{*},\preccurlyeq_{\mathsf{B}})\rightarrow((\Sigma_{p-1}^{*}\times
A_{p})\times(\Sigma_{p-1}^{*}\times A_{p})^{*}\times\Sigma_{p-1}^{*},\
(\preccurlyeq_{\mathsf{B}}\times=)\times(\preccurlyeq_{\mathsf{B}}\times=)_{*}\times\preccurlyeq_{\mathsf{B}})$

defined as,

$u_{0}y_{0}u_{1}y_{1}u_{2}y_{2}\cdots
y_{k-1}u_{k}\mapsto((u_{0},y_{0}),(u_{1},y_{1}),(u_{2},y_{2}),\ldots,(u_{k-1},y_{k-1}),u_{k}),$

where $u_{i}$s are sub-$p$ blocks.

It is easy to see that $h$ is a monomorphism. Then, by the monomorphism lemma,
we get that $(\Sigma_{p}^{*},\preccurlyeq_{\mathsf{B}})$ is a WQO.

We now introduce the notion of upward closed sets, which allows us to prove
the Lemma 3.7.

Upward closure. Upward closure is the dual of downward closure. Given a set
$S$ with a partial order $\triangleleft$, the $\triangleleft$-upward closure
of $L\subseteq S$, denoted by $L\uparrow_{\triangleleft}$, is the set of
elements of $S$ which are larger w.r.t. $\triangleleft$ than some element in
$L$, i.e.

$L\uparrow_{\triangleleft}=\\{u\in S\,|\ \exists\ v\text{ such that }v\
\triangleleft\ u\\}$

A subset $L$ of $S$ is called $\triangleleft$-upward closed if
$L=L\uparrow_{\triangleleft}$.

The subword upward closure and block upward closure are defined by taking the
set of finite words $\Sigma^{*}$ with the partial orders $\preccurlyeq$ and
$\preccurlyeq_{\mathsf{B}}$, respectively. For $L\subseteq\Sigma^{*}$,

$\displaystyle L\uparrow$ $\displaystyle=$ $\displaystyle\\{u\in S\,|\
\exists\ v\text{ such that }v\ \preccurlyeq\ u\\}$ $\displaystyle L\Uparrow$
$\displaystyle=$ $\displaystyle\\{u\in S\,|\ \exists\ v\text{ such that }v\
\preccurlyeq_{\mathsf{B}}\ u\\}$

It is easy to see that the complement of a downward closed set is an upward
closed set and vice versa, hence they are dual of each other. The following
theorem characterizes regular sets using upward closure.

######  Theorem A.5 ([14]).

A set $S$ is regular iff it is the upward closure of some multiplicative WQO.

We restate the Lemma 2.2 and Lemma 3.7 below.

See 2.2 The proof for priority downward closure is analogous for that of block
order, as shown below. See 3.7

######  Proof A.6.

Since the complement of the downward closed set is an upward closed set,
regular languages are closed under complementation, and block order is a
multiplicative WQO (Lemma 3.3), the proof of the lemma is a simple corollary
of Theorem A.5.

##  Appendix B Missing proofs from Section 4

See 4.1

######  Proof B.1.

For the block order consider the transducer that has one state for every
priority and a sink state, and for every state it reads a letter, and

  * •

if the letter has lower or equal priority as the state, does not output it,
and stays there,

  * •

if the letter has equal priority, outputs it, and goes to state $0$, and

  * •

for other scenarios, goes to the sink state.

At state $0$, if the letter is output, then it stays at $0$, else goes to the
state with priority of the letter. This intuitively allows dropping whole
sub-$i$ blocks until priority $i$ is output again. The construction exploits
the fact that between two consecutive letters which are not dropped, no bigger
priority letter is dropped.

Similarly, for priority order, we have the same state space, along with
another accepting state.

  * •

if the letter has strictly lower priority than the state, then does not output
it, and stays there,

  * •

if the letter has same or higher priority, does not output it, and goes to the
state with priority of the letter,

  * •

if the letter has same or higher priority, outputs it, and goes to the state
with priority 0, or the accepting state non-deterministically.

The priority $0$ state is the initial state, and the new accepting state is
the final state. Intuitively, the transducer remembers the largest priority
letter that has been dropped, and keeps only a letter of higher priority
later. To be accepting, it has to read the last letter to go to the accepting
final state.

##  Appendix C Missing proofs from Section 5

We restate the Proposition 5.2 below and prove it formally.

See 5.2

######  Proof C.1.

In this proof we use the shorthand $[n]$ for $[0,n]=\\{0,\ldots,n\\}$, and
$(n)$ for $[1,n]=\\{1,\ldots,n\\}$. We describe the construction of the
intermediate NFA $\mathcal{B}$ formally. Let $U\geq K^{2}+K+1$.

$\mathcal{B}=(Q_{1}\cup Q_{2}\cup
Q_{3},\Sigma,\Delta,q_{0}^{\prime},F^{\prime})$

where
$Q_{1}=Q\times[K]\times\\{1\\},Q_{2}=(Q\times[U]\times\\{2\\})\cup(Q\times Q)$
and $Q_{3}=Q\times[K]\times\\{3\\}$. We let $q_{0}^{\prime}=(q_{0},0,1)$ and
$F^{\prime}=\\{(q_{f},0,1),(q_{f},0,3)\\}$. The transition relation is the
union of the relations $\Delta_{1},\Delta_{2}$ and $\Delta_{3}$ defined as
follows:

Transitions in $\Delta_{1}$:

  1. 1.

$(q,n,1)\xrightarrow{a}(q^{\prime},n,1)$ for all $n\in[K]$ whenever
$(q,a,i,q^{\prime})\in\delta$. Simulate an internal move.

  2. 2.

$(q,n,1)\xrightarrow{a}(q^{\prime},n-1,1)$ for all $n\in(K)$ whenever
$(q,a,-1,q^{\prime})\in\delta$. Simulate a decrement.

  3. 3.

$(q,n,1)\xrightarrow{a}(q^{\prime},n+1,1)$ for all $n\in[K-1]$ whenever
$(q,a,+1,q^{\prime})\in\delta$. Simulate an increment.

  4. 4.

$(q,K,1)\xrightarrow{a}(q^{\prime},K+1,2)$ whenever
$(q,a,+1,q^{\prime})\in\delta$. Simulate an increment and shift to second
phase.

Transitions in $\Delta_{2}$:

  1. 1.

$(q,n,2)\xrightarrow{a}(q^{\prime},n,2)$ for all $n\in[U]$ whenever
$(q,a,i,q^{\prime})\in\delta$. Simulate an internal move.

  2. 2.

$(q,n,2)\xrightarrow{a}(q^{\prime},n-1,2)$ for all $n\in(U)$ whenever
$(q,a,-1,q^{\prime})\in\delta$. Simulate a decrement.

  3. 3.

$(q,n,2)\xrightarrow{a}(q^{\prime},n+1,2)$ for all $n\in[U-1]$ whenever
$(q,a,+1,q^{\prime})\in\delta$. Simulate an increment.

  4. 4.

$(q,K+1,1)\xrightarrow{a}(q^{\prime},K,3)$ whenever
$(q,a,+1,q^{\prime})\in\delta$. Simulate an decrement and shift to third
phase.

  5. 5.

$(q,n,2)\xrightarrow{\epsilon}(q,q)$. Start simulating OCA as an NFA.

  6. 6.

$(q,q)\xrightarrow{\epsilon}(q,n,2)$. Stop simulating OCA as an NFA.

  7. 7.

$(q_{1},q_{2})\xrightarrow{a}(q_{1}^{\prime},q_{2})$ for all $a\in\Sigma$ and
$q_{2}\in Q$ whenever $(q_{1},a,x,q_{1}^{\prime})\in\delta$ for some
$x\in\\{+1,-1,0,z\\}$. Simulate OCA as an NFA starting from $q_{2}$.

Transitions in $\Delta_{3}$:

  1. 1.

$(q,n,3)\xrightarrow{a}(q^{\prime},n,3)$ for all $n\in[K]$ whenever
$(q,a,i,q^{\prime})\in\delta$. Simulate an internal move.

  2. 2.

$(q,n,3)\xrightarrow{a}(q^{\prime},n-1,3)$ for all $n\in(K)$ whenever
$(q,a,-1,q^{\prime})\in\delta$. Simulate a decrement.

  3. 3.

$(q,n,3)\xrightarrow{a}(q^{\prime},n+1,3)$ for all $n\in[K-1]$ whenever
$(q,a,+1,q^{\prime})\in\delta$. Simulate an increment.

See 5.3 Let $w\in\mathcal{L}({\rm NewA})$. Then there is a run $\rho$ in
$\mathcal{L}({\rm NewA})$ on $w$, which can be partitioned as follows,

$\rho=(q_{0},0)\xrightarrow{x}(q_{1},s)\xrightarrow{y}(q_{2},t)\xrightarrow{z}(f,0)$

where $\rho_{1}=(q_{0},0)\xrightarrow{x}(q_{1},s)$ is the longest prefix such
that the counter value stays below $K$, and
$\rho_{3}=(q_{2},t)\xrightarrow{z}(f,0)$ is the longest suffix disjoint from
$\rho_{1}$ such that the counter value stays below $K$, and
$\rho_{2}=(q_{1},s)\xrightarrow{y}(q_{2},t)$. Since $Q_{1}$ and $Q_{2}$ can
simulate ${\rm NewA}$ by keeping track of counter values below $K$, we know
that there are runs $\rho^{\prime}_{1}=(q_{0},0,1)\xrightarrow{x}(q_{1},s,1)$
and $\rho^{\prime}_{3}=(q_{2},t,1)\xrightarrow{z}(q_{3},0,1)$ in
$\mathcal{B}$. We also observe that if the counter value does not go above $K$
in $\rho$, then $\rho_{2}$ and $\rho_{3}$ are empty, and
$\rho=(q_{0},0)\xrightarrow{w}(f,0)$. So $(q_{0},0,1)\xrightarrow{w}(f,0,1)$
is a valid and accepting run in $\mathcal{B}$.

So now suppose $\rho$ exceeds $K$ in the counter. Now if the counter value
stays below $U$, then $\rho_{2}$ can be simulated by $Q_{2}$ and it’s
transitions, and

$\rho^{\prime}=(q_{0},0,1)\xrightarrow{x}(q_{1},K,1)\xrightarrow{y}(q_{2},K,1)\xrightarrow{z}(f,0,1)$

is a valid run in $\mathcal{B}$.

Let the maximum counter value reached in the run $\rho$ be $m$. If $m\geq U$,
then we show that the run can be shortened to keep the counter value below
$U$, and the new run along with the trimmed part can be simulated by
$\mathcal{B}$.

Let $\rho_{m}$ be the shortest prefix of $\rho_{2}$ such that at the end of
$\rho_{m}$ the counter value is $m$. For each $K\leq i\leq m$, consider the
pair of states $(p_{l}^{i},p_{r}^{i})$, such that $(p_{l}^{i},i)$ be the last
configuration in $\rho_{m}$ with the counter value $i$, and $(p_{r}^{i},i)$ be
the first configuration in $\rho_{2}$ after $\rho_{m}$ such that the counter
value is $i$. Since we have only $K$ many vertices, we have $K^{2}$ such
pairs. But $i$ ranges from $K+1$ to $K^{2}+K+1$, by PHP, we have that for some
$K\leq i<j\leq m$, $(p_{l}^{i},p_{r}^{i})=(p_{l}^{j},p_{r}^{j})$. Then the
runs $(p_{l}^{i},i)\xrightarrow{y_{(i,j)}}(p_{l}^{j},j)$
$(p_{r}^{j},j)\xrightarrow{y_{(j,i)}}(p_{r}^{i},i)$ can be removed from
$\rho_{2}$ to reduce the counter value, and can be simulated in $\mathcal{B}$
by edges of type 5, 6, and 7 in $\Delta_{2}$. We do this repeatedly to get a
shorter run in ${\rm NewA}$ which does not exceed $U$, and simulate the
trimmed parts by edges of type $5,6,$ and $7$. And this shorter run can be
trivially simulated by edges of type $1-4$ in $\Delta_{2}$. Hence, we can
simulate $\rho$ in $\mathcal{B}$, and $w\in\mathcal{L}(\mathcal{B})$.

See 5.4 Let $w\in\mathcal{L}(\mathcal{B})$, and let $\rho$ be the witnessing
run. Let the minimum value of the counter in $\rho$ be $m$. If $m\geq 0$, then
it is a run in ${\rm NewA}$, and there is nothing to show. Now suppose $m$ is
negative. Then let

$\rho=(q_{0},0,1)\xrightarrow{x}(q_{1},K,1)\xrightarrow{a}(q_{2},K+1,2)\xrightarrow{y}(q_{3},K+1,2)\xrightarrow{b}(q_{4},K,1)\xrightarrow{z}(f,0,1).$

For $0\leq i\leq K$, consider the state $p_{i}$ such that $(p_{i},i,1)$ is the
first configuration along $(q_{0},0,1)\xrightarrow{x}(q_{1},K,1)$ with the
counter value $i$. Then by PHP, there exist $0\leq i<j\leq K$, such that
$p_{i}=p_{j}$. Let the run between $(p_{i},i)$ to $(p_{j},j)$ be $\rho_{l}$,
and the counter difference $k_{1}=j-i$. Similarly, there exist a similar run
$\rho_{r}$ with counter difference $k_{2}$ in
$(q_{4},K,3)\xrightarrow{z}(f,0,3)$. Notice that $\rho_{l}$ can be pumped to
make the counter value arbitrary high, and similarly, $\rho_{r}$ can be pumped
to bring down the counter value from arbitrary high value. Moreover, observe
that since $m$ is negative, there must exist

$\rho_{c}=(q,n,2)\xrightarrow{\epsilon}(q,q)\xrightarrow{u}(q,q)\xrightarrow{\epsilon}(q,n,2),$

such that the counter value reduces by $m^{\prime}>0$ after this execution.

Now consider a $N$ such that $k_{1}N+m>0$. Then on pumping $\rho_{l}$
$k_{2}Nm^{\prime}$ times, the counter value before $\rho_{c}$ becomes
$n+k_{1}k_{2}Nm^{\prime}$. And executing $u$ $k_{2}m$ times makes the counter
value
$n+k_{1}k_{2}Nm^{\prime}+k_{2}mm^{\prime}=n+(k_{1}N+m)k_{2}m^{\prime}>0$. Then
pumping $\rho_{r}$ $(k_{1}N+m)m^{\prime}$ times brings the counter value to 0
in the end.

However, this will give a run on word of the form
$w^{\prime}=x_{1}x_{2}^{K_{1}}x_{3}ay_{1}u^{K_{2}}y_{2}bz_{1}z_{2}^{K^{3}}z_{3}$
where $K_{1}=k_{2}Nm^{\prime}$, $K_{2}=k_{2}m$ and
$K_{3}=(k_{1}N+m)m^{\prime}$, such that $x_{1}x_{2}x_{3}=x$, $y_{1}uy_{2}=y$
and $z_{1}z_{2}z_{3}=z$. But from lemma 3.5, we know that
$w\preccurlyeq_{\mathsf{B}}w^{\prime}$. Since $w^{\prime}\in\mathcal{L}({\rm
NewA})$, $w\in\mathcal{L}({\rm NewA})\mathord{\downarrow_{\mathsf{B}}}$. With
this we have shown that $\mathcal{B}$ has the same downward closure as ${\rm
NewA}$. And observe that the $\mathcal{B}$ is a NFA with polynomially many
states, $K^{3}+3K^{2}+K$, where $K=|Q|$.

##  Appendix D Missing proofs from Section 6

######  Lemma D.1.

Given a non-terminal $X$ in a context-free grammar, one can construct a
linear-size grammar for the language $\\{u\\#v\mid X\xRightarrow{*}uXv\\}$.

######  Lemma D.2.

Given a non-terminal $X$, one can compute in polynomial time the alphabets
$\overleftarrow{\Gamma}_{X}$ and $\overrightarrow{\Gamma}_{X}$.

######  Proof D.3.

First, apply Lemma D.1 to construct a grammar for $K=\\{u\\#v\mid
X\xRightarrow{*}uXv\\}$. Then, we can decide whether
$a\in\overleftarrow{\Gamma}_{X}$ by checking whether $K$ intersects the
regular language $R_{a}=\\{xay\\#v\mid x,y,v\in\Sigma_{0}^{*}\\}$, for which
one can construct a three-state automaton. Since intersection emptiness
between a context-free language and a given regular language is decidable in
polynomial time, the set $\overleftarrow{\Gamma}_{X}$ can be computed in
polynomial time. An analogous argument holds for
$\overrightarrow{\Gamma}_{X}$.

Since the context-free languages are closed under rational transduction, we
use the standard triple construction (see e.g., [33, Prop. 2.6.1]) to obtain
new grammars after applying transductions. The technique allows construction
of new grammar of size linear in the original grammar and polynomial in the
size of the transducer.

######  Lemma D.4.

Given a CFG $\mathcal{G}$ recognizing a language $L$, and a transducer
$\mathcal{B}$ defining a transduction $T$, the language $TL$ is recognized by
a CFG of size $|\mathcal{G}|\cdot|Q|^{2}$, where $Q$ is the number of states
in $\mathcal{B}$.

###  D.1 Proof of Lemma 6.4

See 6.4

######  Proof D.5.

We first apply Lemma D.1 to construct a grammar $\mathcal{G}^{\prime}$ for
$K=\\{u\\#v\mid X\xRightarrow{*}uXv\\}$. Then consider the following
transducer $T$, that first reads and outputs all the letters until an $r$ is
seen. Once an $r$ is read, it outputs $\overleftarrow{\\#}$ and keeps dropping
subsequent letters until on reading another $r$ it non-deterministically
decides that $r$ will not be seen before $\\#$. Then if another $r$ is read
before the $\\#$, it rejects the run by going to a non-final sink state.
Otherwise, it outputs the letters that are seen until it encounters a $\\#$,
and outputs it. Then it reads and outputs all the letters until a $s$ is read,
in which case it outputs $\overrightarrow{\\#}$, and continues dropping the
letters until another $s$ is read, and it non-deterministically decides to not
read a $s$. It output all the letters after this $s$. Moreover, it goes to the
sink state if it reads a letter with priority greater than $r$ (and, priority
greater than $s$) before the $\\#$ (after the $\\#$).

Note that the transducer only needs $7$ states; one reject state, 3 states for
the right part of $\\#$, and 3 for the left part. We apply the transducer $T$
to the grammar $\mathcal{G}^{\prime}$ to obtain a grammar of size
$49|\mathcal{G}^{\prime}|$, which is linear in the original grammar, due to
Lemma D.1.

Although we show the transducer for $r,s>0$, for the case of $r=0$ or $s=0$,
the transducer just outputs $\overleftarrow{\\#}$ or $\overrightarrow{\\#}$
accordingly.

###  D.2 Proof of Lemma 6.5

See 6.5

######  Proof D.6.

For the forward direction, let us assume that
$u\\#v\preccurlyeq_{\mathsf{B}}u^{\prime}\\#v^{\prime}$. Then suppose the
largest priority occurring in $u\\#v$ and $u^{\prime}\\#v^{\prime}$ be $p$.
Then there exists a witness block map $\rho$ for
$u\\#v\preccurlyeq_{\mathsf{B}}u^{\prime}\\#v^{\prime}$.

Now let $\\#$ belongs to the $m^{th}$ and $n^{th}$ sub-$p$ blocks of $u\\#v$
and $u^{\prime}\\#v^{\prime}$ respectively. We then show that
$u\preccurlyeq_{\mathsf{B}}u^{\prime}$. Consider the block map $\rho_{u}$ that
maps $i^{th}$ sub-$p$ block of $u$ to the $\rho(i)^{th}$ sub-$p$ block of
$u^{\prime}$ for all $i\in[0,m]$. By definition of $\rho$,
$u_{i}\preccurlyeq_{\mathsf{B}}u^{\prime}_{\rho_{u}(i)}$, where $w_{i}$
denotes the $i^{th}$ sub-$p$ block of $w$ for all $i\in[0,n-1]$. Moreover,
$\rho_{u}(0)=0$, and $\rho_{u}(m)=n$. It only remains to show that
$u_{m}\preccurlyeq_{\mathsf{B}}u^{\prime}_{n}$. But this holds recursively,
since the $0$-block that $\\#$ of $u$ belongs to is subword smaller than the
$0$-block that $\\#$ of $u^{\prime}$ belongs to.

A similar argument shows that the block map $\rho_{v}$ that maps $i^{th}$
sub-$p$ block of $v$ to $(\rho(i+m)-n)^{th}$ sub-$p$ block of $v^{\prime}$ is
the required witness block map.

Now, for the other direction, let $\rho_{u}$ and $\rho_{v}$ be the witness
block maps for $u\preccurlyeq_{\mathsf{B}}u^{\prime}$ and
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$. Then consider the block map $\rho$
such that

$i\mapsto\begin{cases}\rho_{u}(i),\text{ if }i\geq n\\\ \rho_{v}(i-m)+n,\text{
otherwise}.\end{cases}$

Again it suffices to show that the $m^{th}$ sub-$p$ block of $u\\#v$ is block
smaller than the $n^{th}$ sub-$p$ block of $u^{\prime}\\#v^{\prime}$. But this
again recursively holds since the $0$-block that $\\#$ of $u\\#v$ belongs to
is subword smaller than the $0$-block that $\\#$ of $u^{\prime}\\#v^{\prime}$
belongs to.

###  D.3 Proof of Lemma 6.6

See 6.6

######  Proof D.7.

Due to Lemma D.4, we again only construct a transducer of constant size that
results in $\overleftarrow{R}_{X,r,s}$ when applied to $\mathcal{G}^{\prime}$
where $\mathcal{G}^{\prime}$ is the grammar for the language $K=\\{u\\#v\mid
X\xRightarrow{*}uXv\\}$ obtained via Lemma D.1. The case of
$\overrightarrow{R}_{X,r,s}$ is analogous.

Consider the following transducer $T$. The transducer has a non-final sink
state, which we call the rejecting state. The transducer reads the letters
(with equal or less priority than r) and does not output anything (i.e.
outputs $\epsilon$), until it reads an $r$ and decides to output the next
sub-$r$ block non-deterministically. It then outputs all the letters read till
the next $r$, and then does not output the subsequent letters. On reading
$\\#$, it outputs nothing, but verifies if the highest occurring letter in the
right of $\\#$ is $s$. If that is the case, it accepts, otherwise rejects. It
is clear from the construction that $T\mathcal{L}(\mathcal{G}^{\prime})$ is
the language $\overleftarrow{R}_{X,r,s}$.

Note that the transducer has 5 states: one rejecting state, 3 to output
sub-$r$ block on the left of $\\#$, and one to verify if the word on the right
of $\\#$ is in $\Sigma_{\max s}^{+}$.

The cases when $r=0$ or $s=0$ are rather straightforward, as the transducer
just non-deterministically outputs one arbitrary letter from the corresponding
side of $\\#$.

###  D.4 Proof of Lemma 6.7

See 6.7

######  Proof D.8.

For every $u\\#v\in\sigma_{X,r,s}(E_{X,r,s})$, there are
$u^{\prime}\in\Sigma_{\max r}^{+}$ and $v^{\prime}\in\Sigma_{\max s}^{+}$ with
$u\preccurlyeq_{\mathsf{B}}u^{\prime}$,
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$, and
$X\xRightarrow{*}u^{\prime}Xv^{\prime}$.

Let $u\\#v\in\sigma_{X,r,s}(E_{X,r,s})$. Then let $u=u_{0}ru_{1}ru_{2}r\cdots
ru_{k}$, for $u_{1}r\cdots u_{k-1}r\in\overleftarrow{R}_{X,r,s}^{*}$, and
$v=v_{0}sv_{1}sv_{2}s\cdots sv_{l}$, for $v_{1}sv_{2}s\cdots
v_{l-1}s\in\overrightarrow{R}_{X,r,s}^{*}$. That is,
$u_{0}\overleftarrow{\\#}u_{k}\\#v_{0}\overrightarrow{\\#}v_{k}\in E_{X,r,s}$.
This implies that there exists $\overleftarrow{w}$ (and $\overrightarrow{w}$),
such that $u_{0}$ ($v_{0}$) and $u_{k}$ ($v_{l}$) are respectively the first
and the last sub-$r$ (sub-$s$) blocks of $\overleftarrow{w}$
($\overrightarrow{w}$). Let the production rule sequence
$X\xRightarrow{*}\overleftarrow{w}X\overrightarrow{w}$ be denoted by
$\rho_{0}$.

Then by the definition of $\overleftarrow{R}_{X,r,s}$, we have production rule
sequences $\overleftarrow{\rho}_{i}\coloneqq X\xRightarrow{*}e_{i}Xf_{i}$,
such that $u_{i}$ is a sub-$r$ block of $e_{i}$, and $f_{i}\in\Sigma_{\max
s}^{+}$. Similarly, there are production rule sequences
$\overrightarrow{\rho}_{j}\coloneqq X\xRightarrow{*}g_{j}Xh_{i}$ such that
$v_{j}$ is a sub-$s$ block of $h_{j}$, and $g_{j}\in\Sigma_{\max r}^{+}$.

Then the derivation sequence
$\rho_{0}\overleftarrow{\rho}_{1}\cdots\overleftarrow{\rho}_{k}\overrightarrow{\rho}_{1}\cdots\overrightarrow{\rho}_{l}\rho_{0}$
gives $X\xRightarrow{*}u^{\prime}Xv^{\prime}$, where
$u^{\prime}=\overleftarrow{w}e_{1}e_{2}\cdots e_{k}g_{1}\cdots
g_{l}\overleftarrow{w}$ and $v^{\prime}=\overrightarrow{w}f_{1}f_{2}\cdots
f_{k}h_{1}\cdots h_{l}\overrightarrow{w}$. It is easy to see that
$u\preccurlyeq_{\mathsf{B}}u^{\prime}$ and
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$.

###  D.5 Proof of Lemma 6.8

See 6.8

######  Proof D.9.

Of course, for zero expansions, there is nothing to prove, so suppose we have
a derivation in $\mathcal{G}^{\prime}$ with $k$ expansions and let $t$ be a
derivation tree obtained by an expansion step from $t_{0}$ by replacing the
$X$-labeled node $x$. Moreover, let $X\xRightarrow{*}uwv$ be the derivation
using new productions inserted at $x$. Then by construction, we know that
$u\\#v\in\sigma_{X}(E_{X})\mathord{\downarrow_{\mathsf{B}}}$. By Lemma 6.5,
this implies that there is a word
$u^{\prime}\\#v^{\prime}\in\sigma_{X}(E_{X})$ with
$u^{\prime},v^{\prime}\in\Sigma_{p}^{*}$,
$u\preccurlyeq_{\mathsf{B}}u^{\prime}$, and
$v\preccurlyeq_{\mathsf{B}}v^{\prime}$ Therefore, by Lemma 6.7, there exist
$u^{\prime\prime},v^{\prime\prime}\in\Sigma_{p}^{*}$ with
$u^{\prime}\preccurlyeq_{\mathsf{B}}u^{\prime\prime}$ and
$v^{\prime}\preccurlyeq_{\mathsf{B}}v^{\prime\prime}$ and a derivation
$X\xRightarrow{*}u^{\prime\prime}Xv^{\prime\prime}$ in $\mathcal{G}$. In
particular, there is a derivation
$X\xRightarrow{*}u^{\prime\prime}wv^{\prime\prime}$ in $\mathcal{G}$. Now
consider the derivation $t_{1}$ obtained from $t_{0}$ by replacing $x$ with
the derivation $X\xRightarrow{*}u^{\prime\prime}wv^{\prime\prime}$. Then
$t_{1}$ derives a new word of the form $\alpha u^{\prime\prime}\beta
v^{\prime\prime}\gamma$, where $\alpha\beta\gamma$ is the word derived by
$t_{0}$. Since $t_{1}$ only uses productions from $\mathcal{G}$ in addition to
those in $t_{0}$, we know that $t_{1}$ needs just $k-1$ expansions. Hence, we
know by induction that $\alpha u^{\prime\prime}\beta
v^{\prime\prime}\gamma\in\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$.
Since $\preccurlyeq_{\mathsf{B}}$ is multiplicative, we have $\alpha u\beta
v\gamma\preccurlyeq_{\mathsf{B}}\alpha u^{\prime}\beta
v^{\prime}\gamma\preccurlyeq_{\mathsf{B}}\alpha u^{\prime\prime}\beta
v^{\prime\prime}\gamma\in\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$.
Since $\alpha u\beta v\gamma$ is the word generated by $t$ and belongs to
$\mathcal{L}(\mathcal{G})\mathord{\downarrow_{\mathsf{B}}}$, this completes
the proof.

###  D.6 Proof of Lemma 6.9

See 6.9

######  Proof D.10.

Consider a derivation tree $t$ in $\mathcal{G}^{\prime}$. We pick $t$ so that
it minimizes the number of nodes whose label repeats below them. Note that
each path in $t$ alternates between productions from $\mathcal{G}$ and
segments using newly introduced productions. By induction, we may assume that
within each segment, no non-terminal repeats. Now observe that if any new non-
terminal that occurs in two segments, then these two segments must come from
the same grammar $\mathcal{E}^{\prime}_{X}$ and thus $X$ must repeat on that
path. Therefore, if there is any repetition, there is also a repetition of
some non-terminal $X$ of $\mathcal{G}$. On the path where $X$ repeats, pick
the top-most and the lowest occurrence of $X$. Between these two, we have a
derivation $X\xRightarrow{*}_{\mathcal{G}^{\prime}}uXv$. This derivation can
be replaced by a single derivation using new productions. Moreover, by our
choice of occurrences of $X$, this replacement will not introduce cross-
segment repetitions. Thus, we obtain a new derivation with (at least) one
fewer repetition. By applying this argument again and again, we arrive at a
derivation with no repetitions. We have thus shown: For every derivation tree
$t$ in $\mathcal{G}^{\prime}$ with repetition of non-terminals, there exists
an equivalent acyclic tree in $\mathcal{G}^{\prime}$. This, with Lemma 6.8,
gives the desired result.