# Parikh’s theorem for infinite alphabets††thanks: This work was partially
supported by NCN grants 2016/21/D/ST6/01368, 2017/27/B/ST6/02093 and
2019/35/B/ST6/02322.

Piotr Hofman  University of Warsaw  Marta Juzepczuk  University of Warsaw
Sławomir Lasota  University of Warsaw  Mohnish Pattathurajan  University of
Warsaw

###### Abstract

We investigate commutative images of languages recognised by register automata
and grammars. Semi-linear and rational sets can be naturally extended to this
setting by allowing for orbit-finite unions instead of only finite ones. We
prove that commutative images of languages of one-register automata are not
always semi-linear, but they are always rational. We also lift the latter
result to grammars: commutative images of one-register context-free languages
are rational, and in consequence commutatively equivalent to register
automata. We conjecture analogous results for automata and grammars with
arbitrarily many registers.

††publicationid: pubid: 978-1-6654-4895-6/21/$31.00 ©2021 IEEE

##  I Introduction

_Register automata_ , introduced over 25 year ago by Francez and Kaminski [1],
are nondeterministic finite-state devices equipped with a finite number of
registers that can store data values from an infinite data domain. A register
automaton inputs a string of data values (a data word) and compares each
consecutive input data value to its registers; based on this comparison and on
the current control state, it chooses a next control state and possibly stores
the input value in one of its registers. The only allowed comparisons of data
values considered in this paper are equality tests. An automaton can also
guess a fresh data value not previously seen in the input, and store it in a
register (we thus consider nondeterministic register automata _with guessing_
[2]). Likewise one defines register context-free grammars [3], [4, Sect.5].

Register automata lack most of the good properties known from the classical
theory of finite automata, like determinisation or closure properties. In
particular, no satisfactory characterisation in terms of rational (regular)
expressions is known. Indeed, all known generalisations of Kleene’s theorem
for register automata either apply to a restricted subclass of the model, or
introduce an involved syntax significantly extending the concept of rational
expressions [5, 6, 7].

Register automata are expressively equivalent to _orbit-finite automata_ [8,
3], a natural extension of finite automata where one allows for input
alphabets and state spaces which are infinite, but finite up to permutation of
the data domain (= orbit-finite). Along the same lines, in this paper we focus
on a natural extension of rational expressions, which differ from the
classical ones just by allowing for _orbit-finite unions_. In other words, we
consider the class of _rational languages_ , defined as the smallest class of
languages closed under concatenation, star, and orbit-finite unions. In
particular, the class contains the empty language, all finite and all orbit-
finite languages.

Languages of register automata are not rational in general, even in case of
deterministic one-register automata. Kleene theorem may be however recovered
when commutative images (Parikh images) are considered: we prove that the
language of every one-register automaton is Parikh-equivalent to (i.e., has
the same Parikh image as) a rational language.

######  Example 1.

Fix the data domain $\text{\sc Atoms}=\\{0,1,2,\ldots\\}$ and consider the
language $L_{1}$ consisting of all nonempty words over Atoms where every two
consecutive letters are different:

$L_{1}\ =\ \\{a_{1}a_{2}\ldots a_{n}\in\text{\sc Atoms}^{*}\,:\,a_{1}\neq
a_{2}\neq\ldots\neq a_{n}\\}.$

The language is recognised by a deterministic one-register automaton but it is
not rational (cf. Section III). It is however Parikh-equivalent to a larger
language $L_{2}$, where the non-equality constraint is imposed at every second
position only:

$L_{2}\ =\ \\{a_{1}a_{2}\ldots a_{n}\in\text{\sc Atoms}^{*}\,:\,a_{1}\neq
a_{2},\ a_{3}\neq a_{4},\ \ldots\\},$

which is defined by the rational (regular) expression

$\displaystyle L_{2}\ =\ \Big{(}\bigcup_{a,b\in\text{\sc Atoms},a\neq
b}ab\Big{)}^{*}\,\big{(}\varepsilon\,\,\cup\,\bigcup_{a\in\text{\sc
Atoms}}a\big{)}$ (1)

and is thus rational (the formal definition of rational languages will be
given in Section III). Indeed, every $w\in L_{2}$ can be transformed, by
swapping letters, to a word in $L_{1}$. Let $w=a_{1}a_{2}\ldots a_{n}$. If
$a_{2}=a_{3}$ we swap non-equal letters $a_{3}$ and $a_{4}$ thus achieving
$a_{1}\neq a_{2}\neq a_{3}\neq a_{4}$. Next, if $a_{4}=a_{5}$ we swap
analogously $a_{5}$ and $a_{6}$, and so on. Continuing in this way we finally
arrive at a word in $L_{1}$. ∎

#### Contribution

We contribute to understanding commutative images of languages of one-register
automata and grammars, by investigating sets of _data vectors_ obtainable as
Parikh images of these languages. Parikh images of rational languages we call
rational as well. Here are our contributions:

  * (1)

We show that Parikh images of languages of one-register automata are not
_semilinear sets_ of data vectors in general. By seminilinear sets we
naturally mean orbit-finite unions of linear sets, which in turn are
determined by a base and an orbit-finite set of periods, like classically.

  * (2)

We prove that languages of one-register automata have rational Parikh images.
The crucial part of the proof resorts to a graph-theoretical characterisation
of these Parikh images, and uses a necessary condition for a Hamiltonian cycle
in directed graphs ([9, 10]).

  * (3)

Finally, we extend (2) to context-free grammars by showing that one-register
context-free languages have rational Parikh images. The result is obtained by
a novel type of transformations of derivation trees.

We conjecture that the restriction on the number of registers in (2) and (3)
can be dropped; the combinatoric complexity we have encountered already in
one-register case makes it however difficult to envisage a generalisation of
our approach to the general case. According to (1), one-register automata and
grammars fail to have semilinear Parikh images in general. However, as a
direct corollary of (3) we recover an analog of the Parikh’s classical theorem
[11]: one-register context-free grammars are Parikh-equivalent to register
automata (but not to one-register automata).

#### Related research

Register automata have been intensively studied with respect to their
foundational properties [1, 12, 5, 13]. Following the seminal paper of Francez
and Kaminski [1], subsequent extensions of the model allow for comparing data
values with respect to some fixed relations such as a total order, or
introduce alternation, variations on the allowed form of nondeterminism, etc.
The model is well known to satisfy almost no semantic equivalences that hold
for classical finite automata. Here are few positive results: simulation of
two-way nondeterministic automata by one-way alternating automata with
guessing [4]; Myhill-Nerode-style characterisation of languages of
deterministic automata [14, 8, 3]; and the well-behaved class of languages
definable by orbit-finite monoids [15], characterised in terms of logic [16]
and a syntactic subclass of deterministic automata [17]. Register automata
have been also intensively studied with respect to their applications to XML
databases and logics [18, 13, 19] (see [2] for a survey). Register context-
free grammars are equivalent to register pushdown automata [4, 20].

Other extensions of finite-state machines to infinite alphabets include:
abstract reformulation or register automata, known as orbit-finite automata,
or nominal automata, or automata over atoms) [8, 3, 4]; symbolic automata
[21]; pebble automata [22]; and data automata [23, 24].

##  II Preliminaries

#### Sets with atoms

Our definitions rely on basic notions and results of the theory of _sets with
atoms_ [4], also known as nominal sets [25]. This paper is a part of a uniform
abstract approach to register automata in the realm of orbit-finite sets with
atoms, developed in [8, 3, 4].

Fix a countably infinite set Atoms, whose elements we call _atoms_. We reserve
initial alphabet letters $a,b,\ldots$ to range over atoms. Informally
speaking, a set with atoms is a set that can have atoms, or other sets with
atoms, as elements. Formally, we define the universe of sets with atoms by a
suitably adapted cumulative hierarchy of sets, by transfinite induction: the
only set of _rank_ 0 is the empty set; and for a cardinal $\gamma$, a set of
rank $\gamma$ may contain, as elements, sets of rank smaller than $\gamma$ as
well as atoms. In particular, nonempty subsets $X\subseteq\text{\sc Atoms}$
have rank 1.

Denote by Perm the group of all permutations of Atoms. Atom permutations
$\pi:\text{\sc Atoms}\to\text{\sc Atoms}$ act on sets with atoms by
consistently renaming all atoms in a given set. Formally, by another
transfinite induction we define $\pi(X)=\\{\pi(x)\,:\,x\in X\\}$. Via standard
set-theoretic encodings of pairs or finite sequences we obtain, in particular,
the pointwise action on pairs $\pi(x,y)=(\pi(x),\pi(y))$, and likewise on
finite sequences. Relations and functions from $X$ to $Y$ are considered as
subsets of $X\times Y$; for instance, in case of $f:\text{\sc
Atoms}\to\text{\sc Atoms}$, we have $\pi(f)(a)=\pi(f(\pi^{-1}(a)))$.

We restrict to sets with atoms that only depend on finitely many atoms, in the
following sense. A _support_ of $x$ is any set $S\subseteq\text{\sc Atoms}$
such that the following implication holds for all $\pi\in\text{\sc Perm}$: if
$\pi(s)=s$ for all $s\in S$, then $\pi(x)=x$. An element (or set) $x$ is
_finitely supported_ if it has some finite support; in this case $x$ has the
least support, denoted $\text{\sc supp}(x)$, called _the support_ of $x$ (cf.
[4, Sect. 6]). Sets supported by $\emptyset$ we call _equivariant_. For
instance, given $a,b\in\text{\sc Atoms}$, the support of the set

$L_{ab}\ =\ \\{a_{1}a_{2}\ldots a_{n}\in\text{\sc Atoms}^{*}\,:\,n\geq 2,\
a_{1}\neq a,\ a_{n}=b\\}$

is $\\{a,b\\}$; the projection function $\pi_{1}:\text{\sc
Atoms}^{2}\to\text{\sc Atoms}:\langle a,b\rangle\mapsto a$ is equivariant; the
support of a sequence $\langle a_{1}\ldots a_{n}\rangle\in\text{\sc
Atoms}^{*}$, encoded as a set in a standard way, is the set of atoms
$\\{a_{1},\ldots,a_{n}\\}$ appearing in it; and the support of a function
$f:\text{\sc Atoms}\to\mathbb{N}$ such that $\text{\sc
dom}(f)=\\{a\in\text{\sc Atoms}\,:\,f(a)>0\\}$ is finite, is exactly
$\text{\sc dom}(f)$.

From now on, we shall only consider sets with atoms that are hereditarily
finitely supported (called briefly _legal_), i.e., ones that have a finite
support, whose every element has some finite support, and so on.

#### Orbit-finite sets

Two (elements of) sets with atoms $x,y$ are _in the same orbit_ if $\pi(x)=y$
for some $\pi\in\text{\sc Perm}$. This equivalence relation splits every set
with atoms $X$ into equivalence classes, which we call _orbits in_ $X$. A
(legal) set is _orbit-finite_ if it splits into finitely many orbits. Examples
of orbit-finite sets are: Atoms (1 orbit); $\text{\sc Atoms}-\\{a\\}$ for some
$a\in\text{\sc Atoms}$ (1 orbit); $\text{\sc Atoms}^{2}$ (2 orbits: diagonal
and non-diagonal); $\text{\sc Atoms}^{3}$ (5 orbits, corresponding to equality
types of triples); $\\{1,\ldots,n\\}\times\text{\sc Atoms}$ ($n$ orbits, as
$\pi(i)=i$ for every $i\in\mathbb{N}$ and $\pi\in\text{\sc Perm}$, according
to the standard set-theoretic definition of natural numbers); the set of
$n$-element subsets of atoms $\mathcal{P}_{n}(\text{\sc
Atoms})=\\{X\subseteq\text{\sc Atoms}\,:\,|X|=n\\}$ (1 orbit).

Given a family $(X_{i})_{i\in I}$ of sets indexed by an orbit-finite set $I$,
the union $\bigcup_{i\in I}X_{i}$ we call _orbit-finite union_ of sets
$X_{i}$. (Formally, not only each set $X_{i}$ is assumed to be legal, but also
the indexing function $i\mapsto X_{i}$.) As an example, consider
$(L_{ab})_{b\in\text{\sc Atoms}}$. The indexing function $b\mapsto L_{ab}$ is
supported by $\\{a\\}$, and so is the union:

$\bigcup_{b\in\text{\sc Atoms}}L_{ab}\ =\ \\{a_{1}a_{2}\ldots
a_{n}\in\text{\sc Atoms}^{*}\,:\,n\geq 2,\ a_{1}\neq a\\}.$

Orbit-finite sets are closed under Cartesian products, subsets, and orbit-
finite unions: if each of $X_{i}$ is orbit-finite, their union $\bigcup_{i\in
I}X_{i}$ is orbit-finite too [4, Sect. 3].

#### Data words and vectors

By a finite multiset over a set $\Sigma$ we mean any function
$v:\Sigma\to\mathbb{N}$ such that $v(\alpha)=0$ for all $\alpha\in\Sigma$
except finitely many. We define the _domain_ of $v$ as $\text{\sc
dom}(v)=\\{\alpha\in\Sigma\,:\,v(\alpha)>0\\}$, and its _size_ as
$|v|=\sum_{\alpha\in\text{\sc dom}(v)}v(\alpha)$ (the same notation is used
for the size of a set). The _Parikh image_ (commutative image) of a word
$w\in\Sigma^{*}$ is the multiset $\text{\sc Par}(w):\Sigma\to\mathbb{N}$,
where $\text{\sc Par}(w)(\alpha)$ is the number of appearances of a letter
$\alpha\in\Sigma$ in $w$. For a language $L\subseteq\Sigma^{*}$, its Parikh
image is $\text{\sc Par}(L)=\\{\text{\sc Par}(w)\,:\,w\in L\\}$. Two languages
$L,L^{\prime}\subseteq\Sigma^{*}$ are _Parikh-equivalent_ if they have the
same Parikh images: $\text{\sc Par}(L)=\text{\sc Par}(L^{\prime})$. We write
$|w|$ for the _length_ of $w$, hence $|v|=|w|$ if $v=\text{\sc Par}(w)$. We
order multisets pointwise: $v\sqsubseteq v^{\prime}$ if $v(\alpha)\leq
v^{\prime}(\alpha)$ for all $\alpha\in\Sigma$. The zero (empty) multiset
$\mathbf{0}$ satisfies $\mathbf{0}(\alpha)=0$ for every $\alpha\in\Sigma$. A
singleton, written $\\{\alpha\\}$, maps $\alpha$ to $1$ and all other letters
to $0$. Addition of multisets is pointwise:
$(v+v^{\prime})(\alpha)=v(\alpha)+v^{\prime}(\alpha)$ for every
$\alpha\in\Sigma$; likewise subtraction $v-v^{\prime}$, for
$v^{\prime}\sqsubseteq v$.

When $\Sigma$ is an orbit-finite alphabet, words $w\in\Sigma^{*}$ we
traditionally call _data words_ , languages $L\subseteq\Sigma^{*}$ we call
_data languages_ , and finite multisets $v:\Sigma\to\mathbb{N}$ we call _data
vectors_. Orbit-finiteness of a set of data words (or data vectors) is
equivalent to bounded length (or size) of its elements:

######  Lemma 1.

A set $X$ of data words or data vectors over an orbit-finite alphabet $\Sigma$
is orbit-finite if, and only if, $\\{|v|\,:\,v\in X\\}\subseteq\mathbb{N}$ is
bounded.

#### One-register automata

For defining register automata we consider input alphabets of the form
$\Sigma=H\times\text{\sc Atoms}$, where $H$ is a finite set. We use three
fixed variables $x,y,x^{\prime}$ to represent register values and input atoms.
A _nondeterministic register automaton_ with one register ($1\textsf{-\sc
NRA}$) $\mathcal{A}$ consists of: a finite set $H$ (finite component of the
alphabet), a finite set of control locations $Q$, subsets $I,F\subseteq Q$ of
initial resp. accepting locations, and a finite set $\Delta$ of transition
rules of the form

$\displaystyle({q}(x),\langle h,y\rangle,\varphi,{q^{\prime}}(x^{\prime}))$
(2)

where $q,q^{\prime}\in Q$, $h\in H$, and $\varphi(x,y,x^{\prime})$ is a
Boolean combination of equalities involving the variables $x,y,x^{\prime}$,
specifying relation between current register value ($x$), input atom ($y$),
and next register value ($x^{\prime}$) resulting from a transition.

A configuration $\langle q,a\rangle\in Q\times\text{\sc Atoms}$ of
$\mathcal{A}$, written ${q}(a)$, consists of a control location $q\in Q$ and a
register value $a\in\text{\sc Atoms}$. For all atoms $a,b,a^{\prime}$ such
that $(a,b,a^{\prime})\models\varphi$, a rule (2) induces a transition

${{q}(a)}\xrightarrow{\langle h,b\rangle}{{q^{\prime}}(a^{\prime})}$

from a configuration ${q}(a)$ to a configuration ${q^{\prime}}(a^{\prime})$.
The semantics of $1\textsf{-\sc NRA}$ is defined as in case of classical NFA,
with configurations considered as states and $\Sigma=H\times\text{\sc Atoms}$
as an alphabet. A _run_ of $\mathcal{A}$ over a data word $w=\langle
h_{1},b_{1}\rangle\langle h_{2},b_{2}\rangle\ldots\langle
h_{n},b_{n}\rangle\in\Sigma^{*}$ is any sequence

$\displaystyle{{q_{0}}(a_{0})}\xrightarrow{\langle
h_{1},b_{1}\rangle}{{q_{1}}(a_{1})}\xrightarrow{\langle
h_{2},b_{2}\rangle}\ldots\xrightarrow{\langle
h_{n},b_{n}\rangle}{q_{n}}(a_{n}).$ (3)

Let $L_{{q}(a)\,{q^{\prime}}(a^{\prime})}(\mathcal{A})$ be the set of data
words admitting a run starting in ${q_{0}}(a_{0})={q}(a)$ and ending in
${q_{n}}(a_{n})={q^{\prime}}(a^{\prime})$. The _language_ recognised by
$\mathcal{A}$, denoted $L(\mathcal{A})$, is defined as:

$\displaystyle L(\mathcal{A})\ =\ \bigcup_{q\in I,q^{\prime}\in
F,a,a^{\prime}\in\text{\sc
Atoms}}L_{{q}(a)\,{q^{\prime}}(a^{\prime})}(\mathcal{A}).$ (4)

######  Remark 2.

The definition allows for _guessing_ , i.e., an automaton may
nondeterministically guess, and store in its register, an atom not yet seen in
the input (cf. [2]). In particular, the initial register value is guessed
nondeterministically.

######  Example 2.

Let $H$ be a singleton, omitted below; we thus consider Atoms as an alphabet.
The $1\textsf{-\sc NRA}$ consisting of $Q=F=\\{q,p\\}$, $I=\\{q\\}$, and two
transition rules:

$\displaystyle({q}(x),y,y=x^{\prime},{p}(x^{\prime}))\qquad({p}(x),y,x\neq
y=x^{\prime},{p}(x^{\prime}))$

recognises $L_{1}$ from Example 1, and can be drawn as:

#### One-register context-free grammars

For technical convenience we restrict to production rules of arity at most 2
(higher arities can be treated similarly, but inessentially increase the
combinatorial complexity of Section VII, see the comment in Section VIII).
Unary production rules are easily simulated using binary and nullary ones.

A _context-free grammar_ with one register ($1\textsf{-\sc CFG}$)
$\mathcal{G}$ consists of: two finite sets $H$ and $Q$ of terminals and
nonterminals, an initial nonterminal $q_{0}\in Q$, and two finite sets
$\Delta_{2}$ and $\Delta_{0}$ of binary and nullary _production rules_ , of
the forms

$\displaystyle{q}(x)\xrightarrow{\varphi}{p}(y)\,\,{p^{\prime}}(y^{\prime})\
\in\ \Delta_{2},\qquad{q}(x)\xrightarrow{}\varepsilon\ \in\ \Delta_{0},$ (5)

where $q\in Q$, $p,p^{\prime}\in Q\cup H$, and $\varphi(x,y,y^{\prime})$ is a
Boolean combination of equalities involving the three (still fixed) variables.
Similarly as before, a configuration ${q}(a)\in Q\times\text{\sc Atoms}$ of
$\mathcal{A}$ consists of a nonterminal $q\in Q$ and a register value
$a\in\text{\sc Atoms}$. Elements of $\Sigma=H\times\text{\sc Atoms}$ we denote
either as ${h}(a)$ or as $\langle h,a\rangle$. Production rules (5) induce
_productions_

$\displaystyle{{q}(a)}\xrightarrow{}{{p}(b)}\,\,{{p^{\prime}}(b^{\prime})},\qquad{{q}(a)}\xrightarrow{}{\varepsilon},$
(6)

the former one under the condition $(a,b,b^{\prime})\models\varphi$. We denote
by $\Pi_{2}$ and $\Pi_{0}$, respectively, the (infinite) sets of productions
induced by rules from $\Delta_{2}$ and $\Delta_{0}$.

The semantics of $1\textsf{-\sc CFG}$ is defined as for classical CFG, with
configurations considered as nonterminals, alphabet $\Sigma=H\times\text{\sc
Atoms}$, and productions $\Pi_{2}\cup\Pi_{0}$. Derivation trees $\mathcal{T}$
of $\mathcal{G}$ are labeled by configurations, alphabet letters $\langle
h,a\rangle={h}(a)\in\Sigma$, or the empty word $\varepsilon$, in a way
consistent with productions (6):

_Complete_ derivation trees have all leaves labeled by elements of
$\Sigma\cup\\{\varepsilon\\}$. We write
$L_{{q}(a)}(\mathcal{G})\subseteq\Sigma^{*}$ for the language of yields of all
complete derivation trees $\mathcal{T}$ with root labeled by ${q}(a)$, as
usual, where $\text{\sc yield}(\mathcal{T})\in\Sigma^{*}$ is obtained as
concatenation of labels of the leaves of $\mathcal{T}$. The language
$L(\mathcal{G})\subseteq\Sigma^{*}$ generated by $\mathcal{G}$ is defined as
the union (as in case of $1\textsf{-\sc NRA}$, the initial register value is
guessed nondeterministically):

$L(\mathcal{G})\ =\ \bigcup_{a\in\text{\sc
Atoms}}L_{{q_{0}}(a)}(\mathcal{G}).$

######  Example 3.

The $1\textsf{-\sc CFG}$ consisting of nonterminals $Q=\\{q,p\\}$, terminals
$H=\\{l,r\\}$, initial nonterminal $q$, and rules

$\displaystyle{q}(x)\xrightarrow{x\neq y=y^{\prime}}\langle
l,y\rangle{p}(y^{\prime})\ \ {p}(x)\xrightarrow{x=y=y^{\prime}}{q}(y)\langle
r,y^{\prime}\rangle\ \ {q}(x)\xrightarrow{}\varepsilon$

generates palindrome-like words of the form

$\langle l,a_{1}\rangle\langle l,a_{2}\rangle\ldots\langle
l,a_{n}\rangle\,\langle r,a_{n}\rangle\ldots\langle r,a_{2}\rangle\langle
r,a_{1}\rangle$

where $n\geq 0$ and $a_{1}\neq a_{2}\neq\ldots\neq a_{n}$.

######  Remark 3.

An alphabet $H\times\text{\sc Atoms}$ and configurations $Q\times\text{\sc
Atoms}$ are orbit-finite. $1\textsf{-\sc NRA}$ and $1\textsf{-\sc CFG}$ are
thus special cases of the abstract notions of orbit-finite automata and
context-free grammars (cf. [4, Sect. 5]), where alphabets, state spaces and
nonterminals may be arbitrary orbit-finite sets.

#### Normal forms

In the sequel we assume, w.l.o.g., that each constraint $\varphi$ appearing in
a transition rule (2) defines a single orbit of $\text{\sc Atoms}^{3}$. In
other terms, $\varphi$ contains either equality or disequality of every pair
of variables. This can be easily achieved by splitting every constraint into a
number of single-orbit ones. For the automaton from Example 2 we get:

There are thus just five possible constraints $\varphi$ and, correspondingly,
five _types_ of transition rules. The first two types preserve register value
($x=x^{\prime}$):

  1. $\langle 1\rangle$

$\varphi_{1}\equiv x=x^{\prime}=y$ (register value equal to input atom);

  2. $\langle 2\rangle$

$\varphi_{2}\equiv x=x^{\prime}\neq y$ (register value different from input).

The remaining types describe an update of register value:

  1. $\langle 3\rangle$

$\varphi_{3}\equiv x\neq y=x^{\prime}$ (register updated with input atom);

  2. $\langle 4\rangle$

$\varphi_{4}\equiv x=y\neq x^{\prime}$ (register updated freshly);

  3. $\langle 5\rangle$

$\varphi_{5}\equiv x\neq y\neq x^{\prime}\neq x$ (register updated freshly).

In the sequel we distinguish between _register-preserving_ (types $\langle
1\rangle$, $\langle 2\rangle$) and _register-updating_ (types $\langle
3\rangle$–$\langle 5\rangle$) constraints $\varphi$, transition rules, and
transitions.

Likewise we assume, w.l.o.g., that each constraint $\varphi$ appearing in a
production rule of a $1\textsf{-\sc CFG}$ defines a single orbit of $\text{\sc
Atoms}^{3}$. The grammar in Example 3 is in normal form.

##  III Rational sets

In this section we define rational sets of data words and data vectors, prove
their closure under substitutions, and formulate our main results.

#### Orbit-finite unions

Consider a family of sets $\mathcal{X}$. We say that $\mathcal{X}$ is _closed
under orbit-finite unions_ if for every orbit-finite family $(X_{i})_{i\in I}$
of sets $X_{i}\in\mathcal{X}$, the union $\bigcup_{i\in I}X_{i}$ belongs to
$\mathcal{X}$. We instantiate below this abstract definition to families
$\mathcal{X}$ of sets of data words and data vectors.

#### Rational data languages

We consider data languages over a fixed orbit-finite alphabet $\Sigma$.

As usual, we define concatenation of two data languages
$LL^{\prime}=\\{ww^{\prime}\,:\,w\in L,w^{\prime}\in L^{\prime}\\},$ and the
Kleene star (iteration): $L^{*}=\\{w_{1}\ldots w_{n}\,:\,n\geq
0,w_{1},\ldots,w_{n}\in L\\}.$ Let _rational data languages_ be the smallest
class of data languages that contains all singleton languages $\\{w\\}$, for
$w\in\Sigma^{*}$, and is closed under concatenation, iteration, and orbit-
finite unions. In particular the empty language, all finite languages and all
orbit-finite ones are rational. For finite $\Sigma$ we obtain the classical
rational (regular) sets. As expected, without the Kleene star we obtain
exactly sets of words of bounded length, or equivalently, due to Lemma 1,
orbit-finite languages.

When convenient, we may speak of _rational expressions_ , by which we mean
formal derivations of rational languages according to the closure rules listed
above.

######  Example 4.

Continuing Example 1, the language $L_{2}$ is rational, as it can be presented
by a rational expression:

$L_{2}\ =\ \Big{(}\bigcup_{a,b\in\text{\sc Atoms},a\neq
b}\\{ab\\}\Big{)}^{*}\,\big{(}\\{\varepsilon\\}\,\cup\bigcup_{a\in\text{\sc
Atoms}}\\{a\\}\big{)}.$

For readability we omit brackets $\\{\\}$ in the sequel, as in (1). On the
other hand, one easy shows that the language $L_{1}$ is not rational. ∎

#### Rational sets of data vectors

We consider sets of data vectors over a fixed orbit-finite alphabet $\Sigma$.
Let addition of two sets $X,Y$ of data vectors be defined by Minkowski sum

$X+Y=\\{x+y\,:\,x\in X,y\in Y\\},$

and let $X^{*}$ contain all finite sums of elements of $X$:

$X^{*}=\\{x_{1}+\ldots+x_{n}\,:\,n\geq 0,x_{1},\ldots,x_{n}\in X\\}.$

We define _rational sets_ of data vectors as the smallest class of sets of
data vectors that contains all singletons $\\{x\\}$ and is closed under
addition, star, and orbit-finite unions. In particular, the empty set, all
finite sets and all orbit-finite sets of data vectors are rational.

######  Example 5.

Continuing Example 4, the Parikh image of $L_{1}$ (and $L_{2}$) is rational
(for readability we keep omitting brackets $\\{\\}$):

$\displaystyle\text{\sc Par}(L_{1})\ =\ \Big{(}\bigcup_{a,b\in\text{\sc
Atoms},a\neq
b}a+b\Big{)}^{*}\,+\,\big{(}\mathbf{0}\,\,\cup\bigcup_{a\in\text{\sc
Atoms}}a\big{)}.$

######  Claim 1.

(1) Rational sets of data vectors are exactly Parikh images of rational data
languages. (2) $\text{\sc Par}(L)$ is rational if, and only if, $L$ is Parikh-
equivalent to a rational data language.

######  Remark 4.

The classical notion of rational sets in an arbitrary monoid ([26, Chapter
VII]) can be generalised along the same lines as above to sets with atoms, by
considering orbit-finite unions instead of finite ones. In this paper we stick
to monoids of data words and data vectors, over an orbit-finite alphabet.

#### Substitutions

Consider a language $L$ over an orbit-finite alphabet $\Sigma$ and a (legal)
family of languages $K=(K_{\sigma})_{\sigma\in\Sigma}$ over an alphabet
$\Gamma$, indexed by $\Sigma$. We typically use the anonymous function
notation

$\sigma\quad\mapsto\quad K_{\sigma}.$

The _substitution_ $L(K)$ is the language over $\Gamma$ containing all words
obtained from some word $\sigma_{1}\sigma_{2}\ldots\sigma_{n}\in L$, by
replacing every letter $\sigma_{i}$ by some word from $K_{\sigma_{i}}$:

$L(K)\ =\ \bigcup_{\sigma_{1}\sigma_{2}\ldots\sigma_{n}\in
L}K_{\sigma_{1}}K_{\sigma_{2}}\ldots K_{\sigma_{n}}.$

######  Example 6.

As usual we use the shorthand $L^{+}=L^{*}L$. Consider the language $L_{1}$
from Example 1 and $\Sigma=\Gamma=\text{\sc Atoms}$. By the equivariant
substitution $K_{a}=(aa)^{+}$, or $a\ \mapsto\ (aa)^{+},$ we obtain the
language $L_{1}(K)=\big{(}\bigcup_{a\in\text{\sc Atoms}}aa\big{)}^{+}$
containing words, where all maximal constant infixes have even length.

######  Lemma 5.

If $L$ and all languages $K_{\sigma}$ have rational Parikh images (resp. are
rational) then the substitution $L(K)$ has also rational Parikh image (resp.
is rational).

###### Proof.

Intuitively speaking, it is enough to replace syntactically, in the rational
expression defining $\text{\sc Par}(L)$, every appearance of a letter $\sigma$
by an expression defining $\text{\sc Par}(K_{\sigma})$.

Formally, we proceed by induction on a derivation of $L$. By Claim 1(2) we
assume, w.l.o.g., that languages $L$ and $K_{\sigma}$ are rational. If
$L=\\{\sigma\\}$ is a singleton, $\sigma\in\Sigma$, then $L(K)=K_{\sigma}$ and
hence is rational. The cases of $L=L_{1}L_{2}$, or $L=(L^{\prime})^{*}$, are
both immediate, as both the operations preserve rationality, and $L_{1},L_{2}$
and $L^{\prime}$ are rational by induction assumption. Finally, when
$L=\bigcup_{x\in X}L_{x}$, by induction assumption we know rationality of the
languages $L_{x}(K)$ for $x\in X$. As

$L(K)\ =\ \bigcup_{x\in X}L_{x}(K)$

and the mapping $x\mapsto L_{x}(K)$ is supported by the union of the supports
of $x\mapsto L_{x}$ and $\sigma\mapsto K_{\sigma}$, we deduce that $L(K)$ is
an orbit-finite union of rational sets and hence rational. ∎

#### Main results

As our main contribution, we prove rationality of Parikh images of
$1\textsf{-\sc NRA}$ and $1\textsf{-\sc CFG}$:

######  Theorem 6.

Parikh images of $1\textsf{-\sc NRA}$ languages are rational.

######  Theorem 7.

Parikh images of $1\textsf{-\sc CFG}$ languages are rational.

We actually prove a refined version of Theorem 6 (needed also for proving
Theorem 7) which, due to (4), implies Theorem 6:

######  Lemma 8.

For every $1\textsf{-\sc NRA}$ $\mathcal{A}$, the languages
$L_{{q}(a)\,{q^{\prime}}(a^{\prime})}(\mathcal{A})$ have rational Parikh
images.

Before proving Theorem 7 and Lemma 8 in Sections V–VII, we first demonstrate
that semi-linear sets are not sufficient to capture Parikh images of
$1\textsf{-\sc CFG}$, or even $1\textsf{-\sc NRA}$.

##  IV Semi-linear sets

Analogously to rational sets, we lift semi-linear sets to orbit-finite
alphabets. Consider data vectors over a fixed orbit-finite alphabet $\Sigma$.
A _linear set_ is then any set of the form

$N\ =\ g+P^{*}$

for a data vector $g$ and an orbit-finite set $P$ of data vectors, and a semi-
linear set is any orbit-finite union of linear sets:

$\displaystyle\bigcup_{i\in I}\,N_{i}\quad=\quad\bigcup_{i\in
I}\,g_{i}+{P_{i}}^{*}.$ (7)

In particular, $I$ is orbit-finite, and the function $i\mapsto(g_{i},P_{i})$
mapping $i\in I$ to a data vector $g_{i}$ (base) and an orbit-finite set
$P_{i}$ of data vectors (periods) is legal. By definition, semi-linear sets
are a subset of rational sets of _star-height 1_ (star-height is defined as
usual, as the maximal nesting depth of stars).

######  Example 7.

Parikh image of $L_{1}$ (cf. Example 5, $\Sigma=\text{\sc Atoms}$) is semi-
linear: (with all sets $P_{i}$ equal):

$I\ =\ \big{(}\mathbf{0}\,\,\cup\bigcup_{a\in\text{\sc
Atoms}}\\!a\big{)}\qquad g_{i}\ =\ i\qquad P_{i}\ =\\!\bigcup_{a,b\in\text{\sc
Atoms},a\neq b}\\!\\!\\!a+b.$

######  Proposition 9.

Semi-linear sets of data vectors are exactly rational sets of star-height at
most $1$.

#### Semi-linear sets are not sufficient

We demonstrate that Parikh images of $1\textsf{-\sc NRA}$ languages are not
semi-linear in general. As a counterexample we take the following language
$L_{3}\subseteq\text{\sc Atoms}$. For $a\in\text{\sc Atoms}$, let

$\displaystyle K_{a}\ =\ \bigcup_{b\in\text{\sc Atoms}-\\{a\\}}b;\qquad L_{a}\
=\ aa\,\big{(}a\,K_{a}\big{)}^{*}.$ (8)

Let $L_{3}$ be the language obtained from $L_{1}$ by the substitution: $a\
\mapsto\ L_{a}.$ The language is clearly rational, and recognised by a
(deterministic) one-register automaton ($H$ is omitted):

As we show, its Parikh image is not semi-linear, which motivates consideration
of rational sets in forthcoming sections.

######  Lemma 10.

$\text{\sc Par}(L_{3})$ is not semi-linear.

Let $\text{\sc Sing}(v)=|\\{a\in\text{\sc Atoms}\,:\,v(a)=1\\}|$ denote the
number of atoms appearing exactly once in $v$. The argument relies on a
careful analysis of the limit value of the _singularity ratio_
$\frac{\text{\sc Sing}(v)}{|v|}$ for $v\in\text{\sc Par}(L_{3})$, when $|v|$
tends to infinity.

##  V Proof of Theorem 7

Consider a fixed $1\textsf{-\sc CFG}$
$\mathcal{G}=(H,Q,q_{0},\Delta_{2},\Delta_{0})$.

#### Proof strategy

We proceed in three steps. First, by a Ramsey’s argument, we prove that a
sufficiently large set of productions contains a _compatible_ pair (Lemma 11).
Then we define _width_ of derivation trees and show that for a sufficiently
large $n\in\mathbb{N}$, every derivation tree can be transformed into a tree
of width at most $n$ while preserving the Parikh image of its yield (Lemma
13). The cut-and-paste transformation relies on compatibility of productions
in a tree. Finally, we argue that Parikh image of the set of words generated
by derivation trees of width bounded by $n$ is rational, for every fixed
$n\in\mathbb{N}$ (Lemma 15). Lemmas 13 and 15 imply Theorem 7.

#### Compatibility

The equality type of a tuple $\langle a_{1},\ldots,a_{k}\rangle\in\text{\sc
Atoms}^{k}$ is defined as the set $\\{\langle i,j\rangle\,:\,1\leq i<j\leq k,\
a_{i}=a_{j}\\}$. Intuitively speaking, tuples of the same equality type admit
the same equalities between their coordinates. Two tuples $\alpha=\langle
a_{1},\ldots,a_{k}\rangle$ and $\beta=\langle b_{1},\ldots,b_{k}\rangle$ we
call _compatible_ if they have the same equality type, and for every
coordinate $i\in\\{1,\ldots,k\\}$ one of two conditions holds: either (1)
$a_{i}=b_{i}$; or (2) $a_{i}\neq b_{i}$ and both $a_{i}$ and $b_{i}$ do not
appear in the other tuple: $a_{i}\notin\\{b_{1},\ldots,b_{k}\\}$,
$b_{i}\notin\\{a_{1},\ldots,a_{k}\\}$. In particular, two equal $k$-tuples are
always compatible.

######  Lemma 11.

For every $k\in\mathbb{N}$ there is some $l=f(k)\in\mathbb{N}$ such that every
finite multiset of $k$-tuples of atoms $A:\text{\sc Atoms}^{k}\to\mathbb{N}$
of size at least $l$ contains two compatible $k$-tuples.

###### Proof.

Let $k\in\mathbb{N}$ be fixed. If $A$ contains two equal tuples, they are
compatible. Thus we can assume $A$ to be a set. We take $l=f(k)$ large enough
to satisfy the constraint (9) below.

The number of different equality types $E_{k}$ is finite and equal to the
number of partitions of the coordinates set $\\{1,\ldots,k\\}$ (the $k$th Bell
number). By the pigeonhole principle, for $l=|A|$ large enough, there is a
subset $A^{\prime}\subseteq A$ of size
$l^{\prime}=|A^{\prime}|=\frac{l}{E_{k}}$ whose elements have all the same
equality type.

We now consider an undirected clique of size $l^{\prime}$ with vertices
$A^{\prime}$, where the edge between vertices $\alpha=\langle
a_{1},\ldots,a_{k}\rangle$ and $\beta=\langle b_{1},\ldots,b_{k}\rangle$ is
labeled (coloured) by the set
$D_{\alpha\beta}=\\{i\in\\{1,\ldots,k\\}\,:\,a_{i}\neq b_{i}\\}$. Intuitively,
the colour describes the coordinates on which $\alpha$ and $\beta$ disagree.
The number of colours is at most $C=2^{k}$. By Ramsey’s theorem, for
$l^{\prime}$ large enough the graph contains a monochromatic clique
$A^{\prime\prime}$ of size $l^{\prime\prime}=k^{2}+1$; indeed, it suffices to
take

$\displaystyle l^{\prime}\ \geq\
R(\underbrace{l^{\prime\prime},l^{\prime\prime},\ldots,l^{\prime\prime}}_{C}).$
(9)

Thus every two elements of $A^{\prime\prime}$ disagree on the same coordinates
$D\subseteq\\{1,\ldots,k\\}$, and hence also agree on the same coordinates
$\\{1,\ldots,k\\}-D$.

Take any $\alpha=\langle a_{1},\ldots,a_{k}\rangle\in A^{\prime\prime}$. For
every coordinate $i\in D$, all tuples $\beta\in A^{\prime\prime}$ are pairwise
different on that coordinate. Therefore, at most $k$ tuples $\beta=\langle
b_{1},\ldots,b_{k}\rangle\in A^{\prime\prime}$ may satisfy

$\displaystyle b_{i}\in\\{a_{1},\ldots,a_{k}\\},$ (10)

i.e., $b_{i}$ appears in $\alpha$. As $|D|\leq k$, at most $k^{2}$ tuples
(including $\alpha$ itself) may satisfy the condition (10) for some coordinate
$i\in D$. Therefore taking any of the remaining tuples, say $\beta$, we obtain
a compatible pair $\alpha,\beta$. ∎

#### Traversals and side-effects

The number of children of a node $x$ in a derivation tree $\mathcal{T}$ we
call _arity_ of $x$ (leaves are nodes of arity 0). Let $\preceq$ denote the
tree order ($x\preceq y$ if $x$ is an ancestor of $y$). A path from a node $x$
to a node $y$, assuming $x\preceq y$, is the set
$\\{z\in\mathcal{T}\,:\,x\preceq z\preceq y\\}$ of all nodes $z$ appearing
between the nodes $x$ and $y$, including $x$ and $y$.

Consider an arbitrary derivation tree $\mathcal{T}$ of $\mathcal{G}$. We
distinguish two ways of traversing a production
${{q}(a)}\xrightarrow{}{{p}(b)}\,\,{{p^{\prime}}(b^{\prime})}\in\Pi_{2}$
appearing in $\mathcal{T}$ by a path, namely left and right traversal:

Once left or right traversal is chosen, say the right one, a production
${{q}(a)}\xrightarrow{}{{p}(b)}\,\,{{p^{\prime}}(b^{\prime})}\in\Pi_{2}$
resembles a transition of $1\textsf{-\sc NRA}$ (over the extended input
alphabet $\Gamma=(Q\cup H)\times\text{\sc Atoms}$) from ${q}(a)$ to
${p^{\prime}}(b^{\prime})$ which inputs the label of the remaining node,
namely ${p}(b)$. We call the pair ${p}(b)\in\Gamma$ the _side-effect_ of the
right traversal; symmetrically we call ${p^{\prime}}(b^{\prime})$ the side-
effect of the left traversal. For two configurations ${q}(a)$ and ${p}(b)$ of
$\mathcal{G}$, we denote by $S_{{q}(a)\,{p}(b)}\subseteq\Gamma^{*}$ the set of
all sequences of side-effects that may appear along a path from a node labeled
by ${q}(a)$ to a node labeled by ${p}(b)$ in a derivation tree of
$\mathcal{G}$. As a corollary of Lemma 8 we get:

######  Lemma 12.

Languages $S_{{q}(a)\,{p}(b)}$ have rational Parikh images.

###### Proof.

Indeed, the claim follows immediately by Lemma 8, if production traversals are
considered as transitions of a $1\textsf{-\sc NRA}$ over the input alphabet
$\Gamma$, and the side-effect of a traversal is considered as input of a
transition. ∎

#### Height, width, and rank

Recall the normal form of constraints $\langle 1\rangle$–$\langle 5\rangle$ as
defined in Section II. Similarly as in case of $1\textsf{-\sc NRA}$, the right
traversal of a production
${{q}(a)}\xrightarrow{}{{p}(b)}\,\,{{p^{\prime}}(b^{\prime})}\in\Pi_{2}$ is
called _register-preserving_ if $a=b^{\prime}$, and _register-updating_ if
$a\neq b^{\prime}$; likewise for the left traversal.

We define the _length_ of a path in a derivation tree $\mathcal{T}$ as the
number of register-updating production traversals along the path, and the
_height_ of a node $x$ in $\mathcal{T}$ as the maximal length of a path from
$x$ to a leaf. A _cut_ in $\mathcal{T}$ is a set of nodes which are pairwise
incomparable with respect to the tree ordering. A cut is called _$n$ -cut_ if
its size is at least $n$ and the height of every node in the cut is at least
$n$. The _width_ of a derivation tree $\mathcal{T}$ is the maximal $n$ for
which $\mathcal{T}$ contains some $n$-cut.

The _rank_ of a derivation tree is defined as the multiset of lengths of all
paths from the root to some leaf. For a finite multiset
$r:\mathbb{N}\to\mathbb{N}$ of natural numbers, let the _diagram of_ $r$ be
the unique non-increasing sequence $w\in\mathbb{N}^{*}$ such that $\text{\sc
Par}(w)=r$. We define the order on ranks as follows: $r\leq r^{\prime}$ if the
diagram of $r$ is lexicographically smaller than the diagram of $r^{\prime}$.
For instance, $\\{7,5,2,2\\}<\\{7,7,3\\}$.

We call two derivation trees $\mathcal{T},\mathcal{T}^{\prime}$ Parikh-
equivalent if $\text{\sc Par}(\text{\sc yield}(\mathcal{T}))=\text{\sc
Par}(\text{\sc yield}(\mathcal{T}^{\prime}))$.

######  Lemma 13.

For a sufficiently large $n$, every derivation tree is Parikh-equivalent to a
derivation tree of width at most $n$.

###### Proof.

Let $m=|\Delta_{2}|$. Fix an arbitrary $n\geq f(6)\cdot 2m$, for $f$ given by
Lemma 11. We show:

######  Claim 2.

Every derivation tree $\mathcal{T}$ of $\mathcal{G}$ of width $\geq n$ can be
transformed, by cutting and pasting of some parts, into a Parikh-equivalent
derivation tree $\mathcal{T}^{\prime}$ of rank strictly larger than
$\mathcal{T}$, but of the same size (= the number of nodes) as $\mathcal{T}$.

The claim is sufficient for proving Lemma 13. Indeed, as the transformation
preserves the size, the rank can increase only finitely many times. Therefore,
by iterating the transformation we ultimately arrive at a derivation tree
$\mathcal{T}^{\prime}$ whose rank can not be further increased. By Claim 2,
the width of $\mathcal{T}^{\prime}$ is forcedly at most $n-1$, as required.

From now on we concentrate on proving Claim 2. Let $\mathcal{T}$ be a
derivation tree of width $\geq n$. Consider some fixed $n$-cut
$\\{x_{1},\ldots,x_{n}\\}$ and disjoint paths $\pi_{1},\ldots,\pi_{n}$ in
$\mathcal{T}$ of length $\geq n$, each path $\pi_{i}$ going from $x_{i}$ to
some leaf.

Consider a fixed path $\pi_{i}$. It contains $\geq n$ register-updating
production traversals, and therefore by the pigeonhole principle the same
production rule $q\xrightarrow{\varphi}p\,\,p^{\prime}\ \in\ \Delta_{2}$ and
the same (say left) register-updating traversal repeats at least
$n^{\prime}=\frac{n}{2m}$ times along $\pi_{i}$. We apply Lemma 11 for $k=3$
to deduce that, as $n^{\prime}\geq f(6)\geq f(3)$, some two of these
traversals

are compatible, by which we mean that their underlying $3$-tuples $\langle
a,b,b^{\prime}\rangle$ and $\langle c,d,d^{\prime}\rangle$ are so. Thus each
path $\pi_{i}$ traverses a pair of compatible productions $\delta_{i}$,
$\sigma_{i}$ which agree on the production rule and (left or right) traversal.

We now repeat a similar argument for paths. As before, by the pigeonhole
principle in at least $n^{\prime}$ paths $\pi_{i}$, the same production rule
and the same traversal was used in productions $\delta_{i}$ and $\sigma_{i}$
derived in the above reasoning. We now apply Lemma 11 for $k=6$ to deal with
pairs $\langle\delta_{i},\sigma_{i}\rangle$ of productions, where a pair
$\langle\delta_{i},\sigma_{i}\rangle$ induces a 6-tuple obtained by
concatenating two underlying 3-tuples of $\delta_{i}$ and $\sigma_{i}$. Since
$n^{\prime}\geq f(6)$, according to the lemma some two of these pairs, say
$\langle\delta_{i},\sigma_{i}\rangle$ and
$\langle\delta_{j},\sigma_{j}\rangle$, are compatible (by which we mean that
the two induced $6$-tuples are so).

We have thus four productions $\delta,\sigma,\bar{\delta},\bar{\sigma}$,
traversed by two disjoint paths in $\mathcal{T}$ (we do not depict
nonterminals as all the four productions are induced by the same rule):

######  Claim 3.

The four underlying triples $\langle a,b,b^{\prime}\rangle$, $\langle
c,d,d^{\prime}\rangle$, $\langle\bar{a},\bar{b},\bar{b}^{\prime}\rangle$ and
$\langle\bar{c},\bar{d},\bar{d}^{\prime}\rangle$ are pairwise compatible.

###### Proof of Claim 3.

By the construction we have compatibility of triples $\langle
a,b,b^{\prime}\rangle$ and $\langle c,d,d^{\prime}\rangle$, and of triples
$\langle\bar{a},\bar{b},\bar{b}^{\prime}\rangle$ and
$\langle\bar{c},\bar{d},\bar{d}^{\prime}\rangle$. Furthermore, we have also
compatibility of 6-tuples $\langle a,b,b^{\prime},c,d,d^{\prime}\rangle$ and
$\langle\bar{a},\bar{b},\bar{b}^{\prime},\bar{c},\bar{d},\bar{d}^{\prime}\rangle$,
which implies compatibility of triples $\langle a,b,b^{\prime}\rangle$ and
$\langle\bar{a},\bar{b},\bar{b}^{\prime}\rangle$, and of $\langle
c,d,d^{\prime}\rangle$ and $\langle\bar{c},\bar{d},\bar{d}^{\prime}\rangle$.
Therefore, it only remains to prove compatibility of $\langle
a,b,b^{\prime}\rangle$ and $\langle\bar{c},\bar{d},\bar{d}^{\prime}\rangle$,
and of $\langle c,d,d^{\prime}\rangle$ and
$\langle\bar{a},\bar{b},\bar{b}^{\prime}\rangle$. We concentrate of the former
pair, as the other one is dealt with similarly.

The equality types of triples $\langle a,b,b^{\prime}\rangle$ and
$\langle\bar{c},\bar{d},\bar{d}^{\prime}\rangle$ are the same, since so are
the equality types of $\langle a,b,b^{\prime}\rangle$ and $\langle
c,d,d^{\prime}\rangle$, and of $\langle c,d,d^{\prime}\rangle$ and
$\langle\bar{c},\bar{d},\bar{d}^{\prime}\rangle$. We concern the first
coordinate of the triples. Supposing $a\neq\bar{c}$, we derive
$a\notin\\{\bar{c},\bar{d},\bar{d}^{\prime}\\}$: if $a\neq\bar{a}$ then this
follows due to compatibility of the two 6-tuples, and if $a=\bar{a}$ then this
follows due to compatibility of
$\langle\bar{a},\bar{b},\bar{b}^{\prime}\rangle$ and
$\langle\bar{c},\bar{d},\bar{d}^{\prime}\rangle$; symmetrically we derive
$\bar{c}\notin\\{a,b,b^{\prime}\\}$. The two remaining coordinates are dealt
with similarly. ∎

We are now prepared to cutting and pasting in $\mathcal{T}$. For convenience
we use below atoms $a,b$, etc. to identify respective nodes (keeping in mind
potential equalities between these atoms). Recall that all the four traversals
are register-updating, and hence $a\neq b$, and likewise for other tuples. We
distinguish three cases, depending on the relation of $b^{\prime}$ to $a$ and
$b$:

#### Case 1 $b^{\prime}=a$

Define the _relevance_ of a node $x$ in $\mathcal{T}$ as the maximal length of
a path from the root of $\mathcal{T}$ to a leaf that traverses $x$. By
symmetry assume, w.l.o.g., that the relevance $\bar{r}$ of the node $\bar{b}$
is larger or equal to the relevance $r$ of the node $b$. We cut the segment of
$\mathcal{T}$ starting from the edge $a\xrightarrow{}b$ and ending with the
edge $c\xrightarrow{}d$, and paste this segment between the nodes $\bar{a}$
and $\bar{b}$ as depicted in the figure:

By Claim 3 the tree $\mathcal{T}^{\prime}$ so obtained is still a derivation
tree:

Indeed, $d\neq a$ (because either $d=b$ or $d$ does not appear elsewhere) and
hence ${{q}(a)}\xrightarrow{}{{p}(d)}\,\,{{p^{\prime}}(b^{\prime})}\in\Pi_{2}$
is a production; likewise for the two remaining productions above.

Furthermore, we claim that rank of $\mathcal{T}^{\prime}$ is strictly larger
than rank of $\mathcal{T}$. To this aim we analyse the effect of cut and paste
on the lengths of the paths from the root to a leaf in $\mathcal{T}$. First,
all paths not traversing $b$ or $\bar{b}$ remain untouched. Furthermore, the
lengths of all paths traversing $\bar{b}$ strictly increase. Thus some path of
length $\bar{r}$ in $\mathcal{T}$ gets strictly prolonged, and all other
affected paths in $\mathcal{T}$ have lengths at most $r\leq\bar{r}$. These two
properties ensure that the rank of $\mathcal{T}^{\prime}$ is strictly larger
than the rank of $\mathcal{T}$.

#### Case 2 $b^{\prime}=b$

By symmetry assume, w.l.o.g., that the relevance $\bar{r}$ of the node
$\bar{a}$ is larger or equal to the relevance $r$ of the node $a$. We cut the
segment of $\mathcal{T}$ starting from the edge $a\xrightarrow{}b$ and ending
with edges $c\xrightarrow{}d$ and $c\xrightarrow{}d^{\prime}$, and paste this
segment between the node $\bar{a}$ and the nodes $\bar{b},\bar{b}^{\prime}$,
and moreover cut the subtree rooted in $b^{\prime}$ and paste it in place of
the subtree rooted in $\bar{b}^{\prime}$, as depicted in the figure:

By Claim 3 the tree $\mathcal{T}^{\prime}$ obtained is a derivation tree, as
before:

Similarly as before, we claim that the rank of $\mathcal{T}^{\prime}$ is
strictly larger than the rank of $\mathcal{T}$. First, all paths from the root
to a leaf in $\mathcal{T}$ not traversing $a$ or $\bar{a}$ remain untouched.
Furthermore, the lengths of all paths from the root to a leaf that traverse
$\bar{a}$ strictly increase. Thus some path of length $\bar{r}$ in
$\mathcal{T}$ gets strictly prolonged, and all other affected paths in
$\mathcal{T}$ have lengths at most $r\leq\bar{r}$. As before, these two
properties ensure that the rank of $\mathcal{T}^{\prime}$ is strictly larger
than the rank of $\mathcal{T}$.

#### Case 3 $b^{\prime}\notin\\{a,b\\}$

In this case one can use any of the two cut-and-paste schemes described above.

The proof of Claim 2 is thus completed, and hence so is the proof of Lemma 13.
∎

We denote by $H_{{q}(a),n}\subseteq L_{{q}(a)}(\mathcal{G})$ the subset of
words generated by a derivation tree of height at most $n$, and by $W_{n}$ the
subset of $L(\mathcal{G})$ of words generated by a derivation tree of width at
most $n$. We now prove, for every $n\in\mathbb{N}$, rationality of the
languages $H_{{q}(a),n}$, and then use it to derive rationality of the Parikh
image of the language $W_{n}$.

######  Lemma 14.

For every $n\in\mathbb{N}$, the languages $H_{{q}(a),n}$ have rational Parikh
images.

######  Lemma 15.

For every $n\in\mathbb{N}$, the language $W_{n}$ has rational Parikh image.

###### Proof.

For a fixed $n\in\mathbb{N}$, consider an arbitrary derivation tree
$\mathcal{T}$ of width at most $n$, and the subset
$\mathcal{H}\subseteq\mathcal{T}$ of those nodes which have height at least
$n+1$. The set $\mathcal{H}$ is closed under ancestors and is thus itself a
tree; contrarily to $\mathcal{T}$ whose non-leaf nodes have arity 2, the tree
$\mathcal{H}$ may contain nodes of arity 1. Notably, as a special case
$\mathcal{H}$ may be empty.

By assumption, width of $\mathcal{T}$ is at most $n$, and hence it may contain
$n$-cuts but no $(n+1)$-cuts. This implies that the largest cut in
$\mathcal{H}$ has size $n$. In consequence:

######  Claim 4.

$\mathcal{H}$ has at most $n$ leaves, and hence at most $n-1$ nodes of arity
2.

Let $\cal L$ denote the finite multiset (of size at most $n$) of
configurations ${q}(a)$ labelling leaves of $\mathcal{H}$.

Any maximal path consisting of nodes of arity 1 we call a _segment_. Thus
$\mathcal{H}$ decomposes uniquely into leaves, nodes of arity 2, and segments.
An example tree on the right has $n=4$ leaves, 3 nodes of arity 2 and 4
segments (depicted by blue areas) of size 3, 2, 2 and 1, respectively. Using
Claim 4 we deduce:

######  Claim 5.

$\mathcal{H}$ contains at most $2n-1$ segments.

Let $\cal S$ denote the finite multiset (of size at most $2n-1$) of pairs of
configurations $\langle{q}(a),{p}(b)\rangle$ labelling ends of segments. Let
$\widetilde{S}_{{q}(a)\,{p}(b)}$ be obtained from the side-effect language
$S_{{q}(a)\,{p}(b)}$ by the equivariant substitution (for $q^{\prime}\in Q$):

${q^{\prime}}(c)\quad\mapsto\quad H_{{q^{\prime}}(c),n-1};$

by Lemmas 14 and 12 languages $\widetilde{S}_{{q}(a)\,{p}(b)}$ have thus
rational Parikh images. Let’s define ($\prod$ denotes concatenation)

$L_{\cal L,\cal S}\quad=\quad\Big{(}\prod_{{q}(a)\in\cal
L}H_{{q}(a),n}\Big{)}\quad\Big{(}\prod_{\langle{q}(a),{p}(b)\rangle\in\cal
S}\widetilde{S}_{{q}(a)\,{p}(b)}\Big{)}$

as the concatenation of two concatenations, one of them ranging over $\cal L$
and the other one over $\cal S$. By the very definition of the language
$L_{\cal L,\cal S}$ we have

######  Claim 6.

$\text{\sc Par}(\text{\sc yield}(\mathcal{T}))\in\text{\sc Par}(L_{\cal L,\cal
S})$.

######  Claim 7.

The languages $W_{n}$ and $K\ =\ \bigcup_{\cal L,\cal S}L_{\cal L,\cal S}$ are
Parikh-equivalent, where $\cal L,\cal S$ range over all possible sets arising
from all derivation trees $\mathcal{T}$ of $\mathcal{G}$ of width at most $n$.

###### Proof.

The inclusion $\text{\sc Par}(W_{n})\subseteq\text{\sc Par}(K)$ we deduce by
Claim 6. For the converse inclusion $\text{\sc Par}(K)\subseteq\text{\sc
Par}(W_{n})$ we should prove: for every $\cal L,\cal S$ arising from some
derivation tree $\mathcal{T}$ of width at most $n$, the language $L_{\cal
L,\cal S}$ is included in $W_{n}$. Indeed, given $\mathcal{T}$ and
$\mathcal{H}$ used to derive sets $\cal L,\cal S$, we observe that every word
$w\in L_{\cal L,\cal S}$ is Parikh-equivalent to the yield of a derivation
tree $\mathcal{T}^{\prime}$ of width at most $n$, obtained from $\mathcal{H}$
by replacing each leaf labelled by ${q}(a)$ with a tree of height $\leq n$
with root labeled by ${q}(a)$, and replacing each segment with a sequence of
productions, where every side-effect ${q}(a)$ is replaced by a tree of height
at most $n-1$ with root labeled by ${q}(a)$. Thus $\text{\sc
Par}(w)\in\text{\sc Par}(W_{n})$. ∎

Finally, we derive rationality of $\text{\sc Par}(K)$. By Lemmas 14 and 12 the
languages $L_{\cal L,\cal S}$ have rational Parikh images. Due to the bounds
on the size of $\cal L$ and $\cal S$ (cf. Claims 4 and 5), by Lemma 1 the set
of all possible pairs $\cal L,\cal S$ is orbit-finite. Therefore $K$, as an
orbit-finite union of languages with rational Parikh images, has a rational
Parikh image too. ∎

##  VI Proof of Lemma 8

Consider a fixed $1\textsf{-\sc NRA}$ $\mathcal{A}=\langle
H,Q,I,F,\Delta\rangle$.

#### Proof strategy

The proof proceeds by a sequence of simplifying steps, as stated in
consecutive Lemmas 17–18 in this section and in Lemmas 19–23 in the next one.
Instead of only considering Parikh images of input words, in the proof we
investigate Parikh images of _runs_ , mostly concentrating on _alterings_ of
register value along a run. This leads us to consider, besides languages over
the alphabet $H\times\text{\sc Atoms}$ of a $1\textsf{-\sc NRA}$, also
languages over richer alphabets:

  * •

languages of _altering paths_ over the alphabet $(Q\times\text{\sc
Atoms}\times Q)\ \cup\ (H\times\text{\sc Atoms})$ in Lemma 17;

  * •

languages of _altering loops_ over the alphabet $\text{\sc
Atoms}^{2}\times\text{\sc Atoms}$ in Lemma 18;

  * •

languages of _anti-paths_ and _anti-cycles_ over $\text{\sc
Atoms}\times\mathcal{P}_{2}(\text{\sc Atoms})$ in Lemmas 19–23.

The intuitive idea underlying the final, most technical steps (Lemmas 19–23)
is, roughly speaking, that the set of words

$\langle a_{1},b_{1}\rangle\,\langle a_{2},b_{2}\rangle\,\ldots\,\langle
a_{n},b_{n}\rangle$

over $\text{\sc Atoms}^{2}$, satisfying $b_{i}\neq a_{i+1}$ for all
$i=1,\ldots,n-1$, has rational Parikh image. Notably, this is not true for
_paths_ , where one requires $b_{i}=a_{i+1}$ instead.

###  VI-A Proof of Lemma 8

For locations $q,p\in Q$ of $\mathcal{A}$ and $a\in\text{\sc Atoms}$, let
$L_{qap}$ be the language of all data words read by a run from configuration
${q}(a)$ to ${p}(a)$ that use register-preserving transitions only (thus the
register stores $a$ along the whole run).

######  Lemma 16.

The languages $L_{qap}$ are rational.

###### Proof.

We only need to consider register-preserving transitions. Define the finite
alphabet $\Delta=H\times\\{\varphi_{1},\varphi_{2}\\}$ and consider every
transition rule $({q}(x),\langle h,y\rangle,\varphi,{q^{\prime}}(x^{\prime}))$
to be _labeled_ by $\langle h,\varphi\rangle\in\Delta$.

Fix $q,a$ and $p$ and let $E_{qp}$ be the classical regular expression over
$\Delta$ defining the labels of all those runs from $q$ to $p$ that only use
transitions of types $\langle 1\rangle$ and $\langle 2\rangle$. Then the
language $L_{qap}$ is defined by the expression $E_{qap}$ obtained from
$E_{qp}$ by replacing $(h,\varphi_{1})$ with $\langle h,a\rangle$ and
replacing $\langle h,\varphi_{2}\rangle$ with

$L_{e,\neq a}\quad=\quad\bigcup_{b\in\text{\sc Atoms}-\\{a\\}}\langle
h,b\rangle.$

Thus $L_{qap}$ is a rational data language. ∎

We now state the central lemma that generalises Example 1. Define the language
$P$ over the alphabet $(Q\times\text{\sc Atoms}\times Q)\ \cup\
(H\times\text{\sc Atoms})$ containing words of the form ($n\geq 1$):

$\displaystyle\begin{aligned} \langle q_{1},a_{1},p_{1}\rangle\langle
h_{1},b_{1}\rangle\langle q_{2},a_{2},p_{2}\rangle\langle
h_{2},b_{2}\rangle\ldots\langle q_{n},a_{n},p_{n}\rangle\end{aligned}$ (11)

such that ${p_{i}}(a_{i})\xrightarrow{\langle
h_{i},b_{i}\rangle}{q_{i+1}}(a_{i+1})$ is a register-updating transition for
$i=1,\ldots,n-1$ (in particular $a_{i}\neq a_{i+1}$ for $i=1,\ldots,n-1$).
Words in $P$ we call _altering paths_. Furthermore, define the subsets
$P_{{q}(a)\,{q^{\prime}}(a^{\prime})}\subseteq P$ of those altering paths as
in (11) where ${q}(a)={q_{1}}(a_{1})$ and
${q^{\prime}}(a^{\prime})={p_{n}}(a_{n})$.

######  Lemma 17.

Altering path languages $P_{{q}(a)\,{q^{\prime}}(a^{\prime})}$ have rational
Parikh images.

Before proving the lemma we use it to complete the proof of Lemma 8. Indeed,
$L_{{q}(a)\,{q^{\prime}}(a^{\prime})}(\mathcal{A})$ is obtained from the
altering path language $P_{{q}(a)\,{q^{\prime}}(a^{\prime})}$ using the
equivariant substitution ($q,p$ range over locations and $a,b$ over Atoms):

$\langle q,a,p\rangle\quad\mapsto\quad L_{qap}\qquad\qquad\langle
h,b\rangle\quad\mapsto\quad\langle h,b\rangle.$

As a substitution by languages with rational Parikh images preserves
rationality of Parikh image (cf. Lemma 5), by Lemmas 16 and 17 we deduce that
the languages $L_{{q}(a)\,{q^{\prime}}(a^{\prime})}(\mathcal{A})$ have
rational Parikh images, as required.

###  VI-B Proof of Lemma 17

We define, for a register-updating transition constraint
$\varphi\in\\{\varphi_{4},\varphi_{5}\\}$ and (not necessariy distinct) atoms
$a^{\prime},b,a\in\text{\sc Atoms}$, the language $L_{(a^{\prime},b)\varphi
a}$ over the alphabet $\text{\sc Atoms}^{2}\times\text{\sc Atoms}$ as follows:
let $L_{(a^{\prime}_{0},b_{0})\varphi a_{n+1}}$ contain all (possibly empty)
words of the form

$\displaystyle\langle\langle
a_{1},a^{\prime}_{1}\rangle,\,b_{1}\rangle\,\,\langle\langle
a_{2},a^{\prime}_{2}\rangle,\,b_{2}\rangle\,\,\ldots\,\,\langle\langle
a_{n},a^{\prime}_{n}\rangle,\,b_{n}\rangle$ (12)

such that $(a^{\prime}_{i},b_{i},a_{i+1})\models\varphi$ for $i=0,\ldots,n$.
We omit the case $\varphi=\varphi_{3}$ as it is can be treated symmetrically
to the case $\varphi=\varphi_{4}$. Words in $L_{(a^{\prime}_{0},b_{0})\varphi
a_{n+1}}$ we call _altering loops_. Intuitively, a letter $\langle\langle
d,d^{\prime}\rangle,e\rangle\in\text{\sc Atoms}^{2}\times\text{\sc Atoms}$
represents (cf. the substitution (13) below), for some locations
$p^{\prime},p$ and $h\in H$, an altering path from ${p}(d)$ to
${p^{\prime}}(d^{\prime})$ followed by a register-updating transition that
inputs $\langle h,e\rangle$. We derive Lemma 17 from the following one (proved
itself in Section VI-C below):

######  Lemma 18.

Altering loop languages $L_{(a^{\prime},b)\varphi a}$ have rational Parikh
images.

We mimic the standard proof of Kleene theorem, exploiting altering loops to
capture all iterations along loops in $\mathcal{A}$. We proceed by induction
on the number of register-updating transition rules in $\mathcal{A}$. If there
is no such transition rules, we have trivial (and obviously rational) altering
path languages

$P_{{q}(a)\,{q^{\prime}}(a^{\prime})}=\begin{cases}\\{\langle
q,a,q^{\prime}\rangle\\}&\text{ if }a=a^{\prime},\\\ \emptyset&\text{
otherwise.}\end{cases}$

Otherwise, remove an arbitrary register-updating transition rule
$t=({q}(x),\langle h,y\rangle,\varphi,{q^{\prime}}(x^{\prime}))$ from
$\mathcal{A}$ (if $\varphi=\varphi_{3}$ consider the inverse of $\mathcal{A}$
and $\varphi=\varphi_{4}$ instead), and use the induction assumption for the
so obtained automaton $\mathcal{A}^{\prime}$ to get altering path languages
$K_{{q}(a)\,{q^{\prime}}(a^{\prime})}$ for every locations $q,q^{\prime}$ and
atoms $a,a^{\prime}$, with rational Parikh images. Let
$L_{(c^{\prime},b)h\varphi c}$ be the language obtained from the altering
loops $L_{(c^{\prime},b)\varphi c}$ by the equivariant substitution
($d,d^{\prime},e$ range over Atoms)

$\displaystyle\langle\langle d,d^{\prime}\rangle,e\rangle\quad\mapsto\
K_{{p}(d)\,{p^{\prime}}(d^{\prime})}\ \langle h,e\rangle.$ (13)

Rationality of the Parikh images of the altering path languages
$P_{{q}(a)\,{q^{\prime}}(a^{\prime})}$ of $\mathcal{A}$ follows by the fact
that $P_{{q}(a)\,{q^{\prime}}(a^{\prime})}$ is equal to the union of
$K_{{q}(a)\,{q^{\prime}}(a^{\prime})}$ and the following set

$\displaystyle\\!\\!\bigcup_{c^{\prime},b,c\in\text{\sc
Atoms}}K_{{q}(a)\,{p^{\prime}}(c^{\prime})}\,\langle
h,b\rangle\,L_{(c^{\prime},b)h\varphi
c}\,K_{{p}(c)\,{q^{\prime}}(a^{\prime})}.$ (14)

To show the equality, we observe that $K_{{q}(a)\,{a^{\prime}}(q^{\prime})}$
contains all altering paths in $\mathcal{A}$ that do not use $t$, and claim
that the set (14) contains those altering paths in $\mathcal{A}$ that do use
$t$. Specifically, as $\varepsilon\in L_{(c^{\prime},b)h\varphi c}$, we obtain
altering paths using $t$ exactly once (dotted arrow depict altering paths in
$\mathcal{A}^{\prime}$):

or more than once (for instance twice, as shown in the figure):

In general, a word in (14) factorises into a prefix before the first use of
$t$ (an altering path from ${q}(a)$ to ${p^{\prime}}(c^{\prime})$), the suffix
after the last use of $t$ (an altering path from ${p}(c)$ to
${q^{\prime}}(a^{\prime})$), and the infix leading from
${p^{\prime}}(c^{\prime})$ to ${p}(c)$. The infix starts with the letter
$\langle h,b\rangle$ input by the first traversal of $t$, and then contains
alternately altering paths that do not use $t$ (from ${p}(d)$ to
${p^{\prime}}(d^{\prime})$, for some $d,d^{\prime}\in\text{\sc Atoms}$) and
traversals of $t$ (a letter $\langle h,e\rangle$ for some $e\in\text{\sc
Atoms}$), cf. the substitution (13). Therefore, by the definition (12) of
altering loops $L_{(a^{\prime},b)\varphi a}$, the set (14) contains exactly
those altering paths in $\mathcal{A}$ that do use $t$, as claimed.

###  VI-C Proof of Lemma 18

We concentrate on the hardest case $\varphi=\varphi_{5}$ (all the three atoms
involved in $\varphi$ are pairwise distinct). The remaining case
$\varphi=\varphi_{4}$ is obtained then using the substitution

$\langle\langle a,a^{\prime}\rangle,b\rangle\quad\mapsto\quad\langle\langle
a,a^{\prime}\rangle,a^{\prime}\rangle.$

We need to show that the altering loop languages $L_{(c,b){\varphi_{5}}a}$
have rational Parikh images. Recall that
$L_{(c_{0},b_{0}){\varphi_{5}}a_{n+1}}$ contains all words over $\text{\sc
Atoms}^{2}\times\text{\sc Atoms}$ of the form

$\displaystyle\langle\langle
a_{1},c_{1}\rangle,\,b_{1}\rangle\,\,\langle\langle
a_{2},c_{2}\rangle,\,b_{2}\rangle\,\,\ldots\,\,\langle\langle
a_{n},c_{n}\rangle,\,b_{n}\rangle$ (15)

such that $c_{i},b_{i},a_{i+1}$ are pairwise different for $i=0,\ldots,n$.

We reduce Lemma 18 to Lemma 19 (which constitutes the technical core of the
proof of Lemma 8). Relying on the observation that $b_{i}$ and $c_{i}$ play
entirely symmetric roles in (15) and are forcedly distinct, we rearrange words
(15) into words over the alphabet $\Gamma=\text{\sc
Atoms}\times\mathcal{P}_{2}(\text{\sc Atoms})$ as follows:

$\displaystyle\langle a_{1},\\{b_{1},c_{1}\\}\rangle\,\,\langle
a_{2},\\{b_{2},c_{2}\\}\rangle\,\,\ldots\,\,\langle
a_{n},\\{b_{n},c_{n}\\}\rangle.$ (16)

Let $\mathbf{P}_{\\{b_{0},c_{0}\\}a_{n+1}}\subseteq\Gamma^{*}$ denote the
language of all _nonempty_ words of the form (16) subject to the same
constraints as in (15), namely $a_{i+1}\notin\\{b_{i},c_{i}\\}$ for
$i=0,\ldots,n$; these words we call _anti-paths_ in the sequel. Note that
$a_{i}\in\\{b_{i},c_{i}\\}$ is allowed. We observe that
$L_{(c,b){\varphi_{5}}a}$ is obtained from $\mathbf{P}_{\\{b,c\\}a}$ using the
equivariant substitution

$\langle d,\\{e,f\\}\rangle\mapsto\langle d,e\rangle\,f\ \ \cup\ \ \langle
d,f\rangle\,e,$

and adding the empty word. Therefore the language $L_{(c,b){\varphi_{5}}a}$
has rational Parikh image assuming $\mathbf{P}_{\\{b,c\\}a}$ has so, and Lemma
18 is implied by the following core technical result:

######  Lemma 19.

The anti-path languages $\mathbf{P}_{\\{b,c\\}a}\subseteq\Gamma^{*}$ have
rational Parikh images.

The proof of Theorem 6 is thus completed once we prove Lemma 19. The whole
next section is devoted to this task.

##  VII Anti-paths: Proof of Lemma 19

For a letter $\alpha=\langle a,\\{b,c\\}\rangle\in\Gamma$ we call the atom $a$
its _source_ , and the two-element set $\\{b,c\\}$ its _target_ , denoted
$a=\text{\sc src}(\alpha)$ and $\\{b,c\\}=\text{\sc trg}(\alpha)$,
respectively. For a word $w=\alpha_{1}\ldots\alpha_{n}\in\Gamma^{*}$ we denote
by $\text{\sc src}(w)=\text{\sc src}(\alpha_{1})$ the first source, and by
$\text{\sc trg}(w)=\text{\sc trg}(\alpha_{n})$ the last target.

#### Anti-cycles

An anti-path $w$ is called an _anti-cycle_ if $\text{\sc
src}(w)\notin\text{\sc trg}(w)$ (the first source does not belong to the last
target). Anti-cycles are closed under cyclic shifts, and hence we use the
cyclic order when speaking about precedence of letters in anti-cycles. Denote
the set of all anti-cycles by $\mathbf{C}$. We build on a simple but crucial
observation: anti-paths $\mathbf{P}_{\\{b,c\\}a}$ are exactly those words
$w\in\Gamma^{*}$ which, prolonged with a single letter $w\,\langle
a,\\{b,c\\}\rangle\in\Gamma$, form an anti-cycle:

######  Claim 8.

$\mathbf{P}_{\\{b,c\\}a}=\\{w\in\Gamma^{*}\,:\,w\,\langle
a,\\{b,c\\}\rangle\in\mathbf{C}\\}$.

######  Lemma 20.

If $L\subseteq\Gamma^{*}$ is rational and $\alpha\in\Gamma$ then the language
$L\triangleleft\alpha=\\{w\in\Gamma^{*}\,:\,w\,\alpha\in L\\}$ is rational
too.

Claim 8 and Lemma 20 prove Lemma 19, once we have:

######  Lemma 21.

$\mathbf{C}$ has rational Parikh image.

Indeed, let $L\subseteq\Gamma^{*}$ be rational and Parikh-equivalent to
$\mathbf{C}$. By Claim 8, $\mathbf{P}_{\\{b,c\\}a}$ is Parikh-equivalent to
$L\triangleleft\langle a,\\{b,c\\}\rangle$, which is rational by Lemma 20.
Thus it suffices to prove Lemma 21.

We mostly focus on a special but central case of Lemma 21, namely we restrict
to the sub-alphabet

$\Sigma\ =\ \\{\alpha\in\Gamma\,:\,\text{\sc src}(\alpha)\notin\\{b,c\\}\\}\
\subseteq\ \Gamma.$

######  Lemma 22.

If the language $\mathbf{D}=\mathbf{C}\cap\Sigma^{*}$ has rational Parikh
image then $\mathbf{C}$ has rational Parikh image too.

######  Lemma 23.

The language $\mathbf{D}$ has rational Parikh image.

###  VII-A Proof of Lemma 23

The number of different sources of letters appearing in a data vector
$v:\Sigma\to\mathbb{N}$, i.e., the size of the set

$\displaystyle V_{v}\ =\ \\{\text{\sc src}(\alpha)\,:\,\alpha\in\text{\sc
dom}(v)\\},$ (17)

we denote by $\text{\sc ord}(v)$ and call _the order_ of $v$ (clearly, an atom
can be the source of more than one letter in $\text{\sc dom}(v)$). The order
of a data word $w\in\Sigma^{*}$ is defined naturally as $\text{\sc
ord}(w)=\text{\sc ord}(\text{\sc Par}(w))$. We write $\mathbf{D}^{<n}$ (resp.
$\mathbf{D}^{\geq n}$) for the subsets of $\mathbf{D}$ containing anti-cycles
of order smaller than $n$ (resp. at least $n$). Anti-cycles of bounded order
can be easily dealt with separately:

######  Lemma 24.

For every $n\in\mathbb{N}$, the language $\mathbf{D}^{<n}$ is rational.

Therefore, in the rest of the proof we concentrate on anti-cycles or order at
laest $n$, for a sufficiently large $n\in\mathbb{N}$.

#### Source graphs

In the sequel we consider directed graphs without self-loops or parallel
edges, but possibly containing tight two-vertex cycles.

Let $v:\Sigma\to\mathbb{N}$ be a fixed data vector. Guided by the crucial
property of anti-paths that the source of every letter does not belong to the
target of the preceding letter, we define the directed graph
$\mathcal{G}_{v}=(V_{v},E_{v})$, called _source graph_ induced by $v$: let the
vertices $V_{v}$ of $\mathcal{G}_{v}$ be the sources of all letters appearing
in $v$, as defined in (17), and let $(d,e)\in E_{v}$ be an edge if, and only
if

$\exists\alpha\in\text{\sc dom}(v)\colon d=\text{\sc
src}(\alpha),e\notin\text{\sc trg}(\alpha).$

Whenever $(d,e)\notin E_{v}$, for distinct atoms $d\neq e$, we say that $d$
_excludes_ $e$ (or call $(d,e)$ an _excluded_ edge); equivalently, $e$ belongs
to the target of every letter in $\text{\sc dom}(v)$ with source $d$:

$\forall\alpha\in\text{\sc dom}(v)\colon\,d=\text{\sc src}(\alpha)\implies
e\in\text{\sc trg}(\alpha).$

Note that an atom never excludes itself, due to restriction to $\Sigma$, and
that $\mathcal{G}_{v}$ depends only on the set $\text{\sc
dom}(v)\subseteq\Sigma$ of letters appearing in $v$, and not on cardinalities
of letters in $v$.

Let $\text{\sc in}(e)=\\{d\in V_{v}\,:\,(d,e)\in E_{v}\\}$ denote the set of
in-neighbours of a vertex $e$, and let $\text{\sc in-deg}(e)=|\text{\sc
in}(e)|$ denote the _in-degree_ of $e$. Symmetrically we define out-neighbours
$\text{\sc out}(e)$ and _out-degree_ $\text{\sc out-deg}(e)$. Clearly, an atom
may exclude at most two other atoms, and hence (let $n=\text{\sc ord}(v)$):

######  Claim 9.

$\text{\sc out-deg}(d)\geq n-3$ for every vertex $d\in V_{v}$.

######  Corollary 25.

There are at most $2n$ excluded edges.

In the sequel we rely on Claim 9 and Corollary 25 according to which
$\mathcal{G}_{v}$ is not much different from the full directed clique.

For $A\subseteq\text{\sc dom}(v)$, let ${v}_{|A}$ denote the restriction of
$v$ to $A$: ${v}_{|A}(\alpha)\ =\ v(\alpha)$ if $\alpha\in A$, and
${v}_{|A}(\alpha)=0$ otherwise. In the proof of Lemma 29 we transform cycles
in $\mathcal{G}_{v}$ into anti-cycles, using the following lemma:

######  Lemma 26.

For every simple cycle $\pi=a_{1}a_{2}\ldots a_{n}$ in $\mathcal{G}_{v}$ there
exists an anti-cycle $w$ with $\text{\sc Par}(w)={v}_{|A}$ where
$A=\\{\alpha\in\text{\sc dom}(v)\,:\,\text{\sc
src}(\alpha)\in\\{a_{1},a_{2},\ldots,a_{n}\\}\\}$.

###### Proof.

We arrange the letters into an anti-path $w$ by taking first all
$a_{1}$-sourced letters in a consecutive block, then all $a_{2}$-sourced ones
in a consecutive block, etc. The order of $a_{i}$-sourced letters inside a
block (including repetitions of equal letters) is irrelevant as long as the
last one, say $\alpha$, satisfies $a_{i+1}\notin\text{\sc trg}(\alpha)$ (where
$n+1$ is identified cyclicly with $1$). ∎

In the proof of Lemma 29 we also use a sufficient condition for a directed
graph to admit a Hamiltonian cycle:

######  Theorem 27 ([9], cf. also Thm. 1 in [10]).

Let $\mathcal{G}$ be a strongly connected directed graph with $n$ vertices
such that for every two vertices $d,d^{\prime}$, $\text{\sc in-
deg}(d)+\text{\sc out-deg}(d^{\prime})\geq n$. Then $\mathcal{G}$ contains a
Hamiltonian cycle.

The tool will be applicable due to the following observation:

######  Lemma 28.

For sufficiently large $n$, a directed graph with $n$ vertices such that
$\text{\sc in-deg}(d)\geq 3$ and $\text{\sc out-deg}(d)\geq n-3$ for every
vertex $d$, is necessarily strongly connected.

###### Proof.

Consider the decomposition of the graph into strongly connected components. As
the first step we observe that there may be no singleton components $\\{d\\}$.
Indeed, by the assumption we have $\text{\sc in-deg}(d)+\text{\sc out-
deg}(d)\geq n$, and hence $d$ forms a tight 2-vertex cycle with some other
vertex $d^{\prime}$.

In the sequel we use Corollary 25. As the second step we argue that for
sufficiently large $n$, a component $\\{d,e\\}$ of size $2$ is impossible
(and, in consequence, a component of size $n-2$ is impossible too). Towards
contradiction, suppose $\\{d,e\\}$ is a strongly connected component (hence
the two vertices form a tight cycle). In consequence, (a) the sets
$V_{d}=\text{\sc out}(d)-\\{e\\}$ and $V_{e}=\text{\sc in}(e)-\\{d\\}$ are
disjoint, and (b) there is no edge from $V_{d}$ to $V_{e}\cup\\{d,e\\}$. As
$\text{\sc out-deg}(d)\geq 3$ and $\text{\sc in-deg}(e)\geq 3$, we have
$|V_{d}|\geq n-4$ and $|V_{e}|\geq 2$. By (a) we deduce $|V_{d}|=n-4$ and
$|V_{e}|=2$. By (b), all $4(n-4)$ edges from $V_{d}$ to $V_{e}\cup\\{d,e\\}$
are excluded. This is impossible as long as $4(n-4)>2n$.

Likewise one argues that there may be no component of size strictly between
$2$ and $n-2$. Indeed, supposing there is a component $C$ of size $k$, for
$2<k<n-2$, no vertex in $C$ may form a tight cycle with other vertex outside
of $C$, and hence at least $k(n-k)$ edges are excluded. This is impossible as
long as $k(n-k)>2n$. As $k(n-k)$ reaches its minimum for $k=3$ or $k=n-3$,
there may be no component of size strictly between $2$ and $n-2$ as long as
$3(n-3)>2n.$ ∎

#### Non-degeneracy

Let $\text{\sc pre}(d)=\\{\alpha\in\text{\sc dom}(v)\,:\,d\neq\text{\sc
src}(\alpha),d\notin\text{\sc trg}(\alpha)\\}$ denote the set of letters that
can precede a $d$-sourced letter and have themselves source different than
$d$. A data vector $v:\Sigma\to\mathbb{N}$ is called _non-degenerate_ if the
following conditions holds:

  * (1)

$\text{\sc in}(d)\neq\emptyset$ for every $d\in V_{v}$,

  * (2)

$\text{\sc in}(d)\cup\text{\sc in}(e)\not\subseteq\\{d,e\\}$ for every non-
equal $d,e\in V_{v}$,

  * (3)

$|{v}_{|\text{\sc pre}(d)\cup\text{\sc pre}(e)}|\geq 2$ for every non-equal
$d,e\in V_{v}$.

(1) excludes vertices of in-degree $0$. (2) excludes pairs of vertices $d,e$
with $\text{\sc in}(d)=\\{e\\}$ and $\text{\sc in}(e)=\\{d\\}$. (3) excludes
the case when there is only one letter $\alpha\in\text{\sc dom}(v)$ that can
precede $d$\- or $e$-sourced letters, and moreover $v(\alpha)=1$.

######  Lemma 29.

For data vectors $v:\Sigma\to\mathbb{N}$ of sufficiently large order,
$v\in\text{\sc Par}(\mathbf{D})$ if, and only if $v$ is non-degenerate.

###### Proof.

Let $\mathcal{G}_{v}=(V_{v},E_{v})$ be the source graph and $n=\text{\sc
ord}(v)$.

The ’only if’ implication is immediate for data vectors of order at least $3$.
Indeed, suppose $v=\text{\sc Par}(w)$ for an anti-cycle $w\in\mathbf{D}$. By
the definition of anti-cycles, $\text{\sc in}(d)\neq\emptyset$ for every $d\in
V_{v}$ and hence (1) forcedly holds. The other two conditions are easily shown
by contradiction. Indeed, if (2) fails for some $d,e\in V_{v}$ then every
$d$\- or $e$-sourced letter would be preceded in $w$ by a $d$\- or $e$-sourced
one, which is impossible as long as $\text{\sc ord}(v)\geq 3$. Finally, if (3)
fails then the same letter $\alpha$ would have to precede two different
letters in $w$.

For the ’if’ implication, we assume that $v$ is non-degenerate ((1)–(3) hold)
and prove that $v=\text{\sc Par}(w)$ for some $w\in\mathbf{D}$.

Let $k=9$. Due to Corollary 25 we can assume $n$ to be large enough so that:

######  Claim 10.

At most two atoms in $V_{v}$ have in-degree $<k$.

In other words, this means that there are no $3$ atoms excluded by at least
$n-k$ vertices. Therefore, relying on Corollary 25 it is enough to assume
$3(n-k)\ >\ 2n,$ i.e., $n>3k$.

Let $a_{1},a_{2}\in V$ be the vertices with the smallest in-degrees. By
assumption, $\text{\sc in-deg}(a_{1})\geq 1,\text{\sc in-deg}(a_{2})\geq 1$,
and by Claim 10 we have:

######  Claim 11.

Every $d\in V_{v}-\\{a_{1},a_{2}\\}$ satisfies $\text{\sc in-deg}(d)\geq k$.

We construct a cycle $\pi$ in $\mathcal{G}_{v}$ such that ($\circ$) its first
vertex $d$, as well as vertices $d$ not contained in $\pi$, satisfy $\text{\sc
in-deg}(d)\geq k$. Due to (1), it suffices to consider the following cases:

#### _Case 1. $|\text{\sc in}(a_{1})\cup\text{\sc in}(a_{2})|\geq 2$_

Relying on (1), choose in $V_{v}-\\{a_{1},a_{2}\\}$ two distinct atoms $d\neq
d^{\prime}$ with $d\in\text{\sc in}(a_{1})$ and $d^{\prime}\in\text{\sc
in}(a_{2})$. Due to (2) the atoms can be chosen so that $d\neq a_{2}$ or
$d^{\prime}\neq a_{1}$. By symmetry we assume w.l.o.g. that $d\neq a_{2}$. If
$d^{\prime}=a_{1}$ we take the following simple path $\pi$ in
$\mathcal{G}_{v}$ satisfying ($\circ$):

Otherwise, suppose $d^{\prime}\neq a_{1}$ either. By Claim 11, $\text{\sc in-
deg}(d)\geq k$ and $\text{\sc in-deg}(d^{\prime})\geq k$. Choose in
$V-\\{d,a_{1},d^{\prime},a_{2}\\}$ any atom $e$ with $e\in\text{\sc
in}(d^{\prime})\cap\text{\sc out}(a_{1})$ (since $\text{\sc in-
deg}(d^{\prime})\geq k$, such $e$ exists as $a_{1}$ excludes at most two
atoms, as long as $k\geq 7$). This yields the following simple path $\pi$ in
$\mathcal{G}_{v}$ satisfying ($\circ$):

#### _Case 2. $\text{\sc in}(a_{1})=\text{\sc in}(a_{2})=\\{d\\}$ for some
$d\in V_{v}{-}\\{a_{1},a_{2}\\}$_

Take some two letters $\alpha_{1},\alpha_{2}$ appearing in $v$ such that
$a_{1}\notin\text{\sc trg}(\alpha_{1})$ and $a_{2}\notin\text{\sc
trg}(\alpha_{2})$. Due to (3) we can assume that either
$\alpha_{1}\neq\alpha_{2}$, or $\alpha_{1}=\alpha_{2}$ but $v(\alpha_{1})\geq
2$ (their cardinality in $v$ is at least $2$). Note that $\text{\sc
src}(\alpha_{1})=\text{\sc src}(\alpha_{2})=d$, and by Claim 11, $\text{\sc
in-deg}(d)\geq k$. Choose in $V-\\{d,a_{1},a_{2}\\}$ any atom $e$ with
$e\in\text{\sc in}(d)\cap\text{\sc out}(a_{1})$ (similarly as before, such $e$
exists as long as $k\geq 6$). This yields the non-simple path $\pi$ in
$\mathcal{G}_{v}$ satisfying ($\circ$):

We have thus constructed a path $\pi$ from $d$ to $a_{2}$. If
$a_{2}\notin\text{\sc in}(d)$, append at the end of $\pi$ any vertex $c$ such
that $c\in\text{\sc out}(a_{2})\cap\text{\sc in}(d)$. As before, such a vertex
exists since $a_{2}$ excludes at most $2$ atoms and $\text{\sc in-deg}(d)\geq
k$, as long as $k\geq 8$. Therefore the last vertex $c$ of $\pi$ satisfies
$c\in\text{\sc in}(d)$, which means that $\pi$ is a cycle as required.

In Case 1 we transform $\pi$, using Lemma 26, into an anti-cycle $\bar{w}$. In
Case 2 we proceed similarly, except that the vertex $d$ appears twice in
$\pi$; this exception is treated by splitting all $d$-sourced letters into two
disjoint blocks (cf. the proof of Lemma 26), containing $\alpha_{1}$ and
$\alpha_{2}$, respectively.

We now remove, intuitively speaking, the anti-cycle $\bar{w}$ from $v$ thus
obtaining a smaller data vector $v^{\prime}$ to which we apply Theorem 27 and
Lemma 26. We remove from $v$ all letters appearing in $\bar{w}$, and add a
single letter $\beta=\langle\text{\sc src}(\bar{w}),\text{\sc
trg}(\bar{w})\rangle\in\Sigma$. This yields a data vector $v^{\prime}$. As the
length of $\pi$ is at most $6$, the in-degree of a node $e$ in the graph
$\mathcal{G}_{v^{\prime}}$ may be smaller by at most $6$ than in the graph
$\mathcal{G}_{v}$. Thus $\text{\sc in-deg}(e)\geq 3$ in
$\mathcal{G}_{v^{\prime}}$ as $k\geq 9$. Moreover $\text{\sc out-deg}(e)\geq
n^{\prime}-3$ in $\mathcal{G}_{v^{\prime}}$, where $n^{\prime}$ is the number
of nodes of $\mathcal{G}_{v^{\prime}}$, by Corollary 25. Therefore the graph
$\mathcal{G}_{v^{\prime}}$, assuming $n$ to be sufficiently large, satisfies
assumptions of Lemma 28, by which $\mathcal{G}_{v^{\prime}}$ is strongly
connected. In consequence, $\mathcal{G}_{v^{\prime}}$ satisfies assumptions of
Theorem 27, by which we derive a Hamiltonian cycle $\mathcal{C}$ in
$\mathcal{G}$. The Hamiltonian cycle is turned, using Lemma 26, into an anti-
cycle in $w^{\prime}$ with $\text{\sc Par}(w^{\prime})=v^{\prime}$. Finally,
replacing the letter $\beta$ in $w^{\prime}$ by $\bar{w}$, yields an anti-
cycle $w$ with $\text{\sc Par}(w)=v$, as required. ∎

Let $\mathbf{N}$ denote the set of all non-degenerate data vectors, and
$\mathbf{N}^{{\geq}n}=\\{v\in\mathbf{N}\,:\,\text{\sc ord}(v)\geq n\\}$. In
these terms, Lemma 29 claims $\mathbf{N}^{{\geq}n}=\text{\sc
Par}(\mathbf{D}^{\geq n})$ for sufficiently large $n$.

######  Lemma 30.

$\mathbf{N}^{{\geq}n}$ is rational, for sufficiently large $n\in\mathbb{N}$.

For $n\in\mathbb{N}$ sufficiently large for Lemmas 29 and 30 to hold, we
decompose the Parikh image of anti-cycles into

$\text{\sc Par}(\mathbf{D})\ =\ \text{\sc Par}(\mathbf{D}^{<n})\ \cup\
\mathbf{N}^{{\geq}n},$

both of them rational by Lemmas 24 and Lemma 30, respectively. Lemma 23 is
thus proved.

##  VIII Final remarks

We have shown that Parikh images of languages of one-register automata are not
semi-linear in general, but are rational; and likewise for one-register
context-free languages. As a corollary of Theorem 7 we obtain an analog of
Parikh’s theorem mentioned in the introduction: one-register context-free
grammars are Parikh-equivalent to register automata (but not to one-register
ones). Indeed, every rational set of data vectors is the Parikh image of some
register automaton.

We conjecture that the restriction to one register can be dropped, and that
general register context-free grammars have rational Parikh images and are
Parikh-equivalent to register automata; our present proof techniques do not
allow however to tackle the general case. On the other hand our proof method
routinely (but tediously) adapts to $1\textsf{-\sc CFG}$ of any arity, but at
the price of considering anti-paths over a larger alphabet $\text{\sc
Atoms}\times\mathcal{P}_{n}(\text{\sc Atoms})$, where $n$ is the largest arity
of a $1\textsf{-\sc CFG}$.

Besides dropping one-register restriction, we envisage several potential
directions of generalisation: richer input alphabets, more structured atoms,
etc. As future work we leave also investigation of algorithmic problems on
rational sets, like testing equality of such sets. Finally, we hope to develop
a general theory of rational sets of data vectors, e.g., study closure
properties, strictness of the star-height hierarchy, or logical
characterisations.

## Acknowledgment

The authors would like to thank the anonymous reviewers for helpful remarks
and suggestions.

## References

  * [1] N. Francez and M. Kaminski, “Finite-memory automata,” _Theor. Comput. Sci._ , vol. 134, no. 2, pp. 329–363, 1994.
  * [2] L. Segoufin, “Automata and logics for words and trees over an infinite alphabet,” in _Proc. CSL 2006_ , ser. Lecture Notes in Computer Science, vol. 4207. Springer, 2006, pp. 41–57.
  * [3] M. Bojańczyk, B. Klin, and S. Lasota, “Automata theory in nominal sets,” _Log. Methods Comput. Sci._ , vol. 10, no. 3, 2014.
  * [4] M. Bojańczyk, “Slightly infinite sets,” a draft of a book. [Online]. Available: https://www.mimuw.edu.pl/ bojan/paper/atom-book
  * [5] M. Kaminski and T. Tan, “Regular expressions for languages over infinite alphabets,” _Fundam. Informaticae_ , vol. 69, no. 3, pp. 301–318, 2006.
  * [6] L. Libkin, T. Tan, and D. Vrgoc, “Regular expressions for data words,” _J. Comput. Syst. Sci._ , vol. 81, no. 7, pp. 1278–1297, 2015.
  * [7] A. Kurz, T. Suzuki, and E. Tuosto, “On nominal regular languages with binders,” in _Proc. FOSSACS 2012_ , ser. Lecture Notes in Computer Science, L. Birkedal, Ed., vol. 7213. Springer, 2012, pp. 255–269.
  * [8] M. Bojańczyk, B. Klin, and S. Lasota, “Automata with group actions,” in _Proc. LICS 2011_ , 2011, pp. 355–364.
  * [9] A. Ghouila-Houri, “Une condition suffisante d’existence d’un circuit hamiltonien,” _C. R. Acad. Sci. Paris_ , vol. 25, pp. 495–497, 1960.
  * [10] D. Kühn and D. Osthus, “A survey on hamilton cycles in directed graphs,” _European Journal of Combinatorics_ , vol. 33, no. 5, pp. 750 – 766, 2012\.
  * [11] R. Parikh, “On context-free languages,” _J. ACM_ , vol. 13, no. 4, pp. 570–581, 1966.
  * [12] H. Sakamoto and D. Ikeda, “Intractability of decision problems for finite-memory automata,” _Theor. Comput. Sci._ , vol. 231, no. 2, pp. 297–308, 2000.
  * [13] F. Neven, T. Schwentick, and V. Vianu, “Finite state machines for strings over infinite alphabets,” _ACM Trans. Comput. Log._ , vol. 5, no. 3, pp. 403–435, 2004.
  * [14] N. Francez and M. Kaminski, “An algebraic characterization of deterministic regular languages over infinite alphabets,” _Theor. Comput. Sci._ , vol. 306, no. 1-3, pp. 155–175, 2003.
  * [15] M. Bojańczyk, “Data monoids,” in _Proc. STACS 2011_ , ser. LIPIcs, vol. 9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011, pp. 105–116.
  * [16] T. Colcombet, C. Ley, and G. Puppis, “Logics with rigidly guarded data tests,” _Log. Methods Comput. Sci._ , vol. 11, no. 3, 2015. [Online]. Available: https://doi.org/10.2168/LMCS-11(3:10)2015
  * [17] M. Bojańczyk and R. Stefański, “Single-use automata and transducers for infinite alphabets,” in _Proc. ICALP 2020_ , ser. LIPIcs, vol. 168\. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, pp. 113:1–113:14.
  * [18] S. Demri and R. Lazic, “LTL with the freeze quantifier and register automata,” _ACM Trans. Comput. Log._ , vol. 10, no. 3, pp. 16:1–16:30, 2009.
  * [19] T. Colcombet and A. Manuel, “Generalized data automata and fixpoint logic,” in _Proc. FSTTCS 2014_ , ser. LIPIcs, vol. 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 267–278.
  * [20] L. Clemente and S. Lasota, “Reachability analysis of first-order definable pushdown systems,” in _Proc. CSL 2015_ , ser. LIPIcs, S. Kreutzer, Ed., vol. 41. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 244–259.
  * [21] L. D’Antoni and M. Veanes, “Minimization of symbolic automata,” in _Proc. POPL ’14_. ACM, 2014, pp. 541–554.
  * [22] T. Milo, D. Suciu, and V. Vianu, “Typechecking for XML transformers,” _J. Comput. Syst. Sci._ , vol. 66, no. 1, pp. 66–97, 2003.
  * [23] M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin, “Two-variable logic on data words,” _ACM Trans. Comput. Log._ , vol. 12, no. 4, pp. 27:1–27:26, 2011.
  * [24] M. Bojańczyk and S. Lasota, “An extension of data automata that captures XPath,” _Log. Methods Comput. Sci._ , vol. 8, no. 1, 2012.
  * [25] A. M. Pitts, _Nominal Sets: Names and Symmetry in Computer Science_ , ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013, vol. 57.
  * [26] S. Eilenberg, _Automata, languages, and machines. A_ , ser. Pure and applied mathematics. Academic Press, 1974\. [Online]. Available: https://www.worldcat.org/oclc/310535248
  * [27] M. Juzepczuk, “Zbiory semiliniowe nad nieskończonym alfabetem (in Polish),” Master’s thesis, University of Warsaw, 2013.

###  -A Missing items in Section II

###### Proof of Lemma 1.

Fix an orbit-finite set $\Sigma$. The ’only if’ implication is immediate, as
the length (or size) is invariant inside an orbit. Towards the ’if’
implication for data languages, we observe that the set $\Sigma^{n}$ of words
of length $n$ is orbit-finite, for every $n\in\mathbb{N}$, as Cartesian
products preserve orbit-finiteness. Therefore a language
$X\subseteq\Sigma^{*}$ satisfying $|v|\leq n$ for $v\in X$, is a subset of a
finite union of orbit-finite sets and hence orbit-finite itself. In
consequence, $\text{\sc Par}(X)$ is is also orbit-finite, as the image of $X$
under an equivariant function, which proves the claim for sets of data
vectors. ∎

###  -B Missing items in Section III

######  Lemma 31.

The language $L_{1}$ from Example 1 is not rational.

###### Proof.

Indeed, towards contradiction suppose $L_{1}$ is rational, and hence generated
by a rational expression $R$. Consider the sublanguage $L\subset L_{1}$
containing words in which all atoms are different. The language $L$ is orbit-
infinite and hence it cannot be generated without star; indeed, concatenation
and orbit-finite sums preserve orbit-finiteness of languages. Therefore, there
must be a star subexpression $R^{\prime}$ of $R$ such that the number of
iterations of $R^{\prime}$ is unbounded in generation of words in $L$. In
other words, for every $n\in\mathbb{N}$ there is a word $w\in L$ whose some
infix $u$ is generated by at least $n$ iterations of $R^{\prime}$. Thus
$w=w^{\prime}uw^{\prime\prime}$, the infix $u$ splits into $u=u_{1}\ldots
u_{n}$, and each of factors $u_{i}$ is generated by $R^{\prime}$. Choose $n$
sufficiently large, namely $n>2\cdot|\text{\sc supp}(R^{\prime})|$
(considering union operations as atom-binding constructs, the support of a
rational expression $R^{\prime}$ consists of those atoms appearing in
$R^{\prime}$ which are not bounded by any union). As no atom repeats twice in
words in $L$, some of words $u_{i}$ is fresh for $R^{\prime}$, i.e.,
$\text{\sc supp}(u)\cap\text{\sc supp}(R^{\prime})=\emptyset$, and $u_{i}$ is
either preceded or succeeded in $w$ by an atom $a\notin\text{\sc
supp}(R^{\prime})$. Consider w.l.o.g. the first case, and let $a^{\prime}$ be
the first atom in $u_{i}$. Necessarily $a\neq a^{\prime}$. As $R^{\prime}$ is
invariant under the swap $a^{\prime}\leftrightarrow a$, applying this swap to
$u_{i}$ yields a word $u^{\prime}$ still generated by $R^{\prime}$. Replacing
$u_{i}$ by $u^{\prime}$ in $w$ yields a word $w^{\prime}$ still generated by
$R$, but $w^{\prime}\notin L_{1}$ as it contains two consecutive atoms $a$.
The contradiction completes the proof. ∎

###  -C Missing items in Section IV

###### Proof of Proposition 9.

Every semilinear set is, by definition, a rational set of star-heigth at most
$1$. For the converse inclusion we use a distributive law of addition over
orbit finite unions:

$\bigcup_{i\in I}L_{i}\quad+\quad\bigcup_{j\in
J}K_{i}\quad=\quad\bigcup_{\langle i,j\rangle\in I\times J}L_{i}+K_{j}.$

Note that the Cartesian product $I\times J$ of orbit-finite sets $I$ and $J$
is necessarily orbit-finite (cf. [4, Sect. 3]).

Consider a rational set $X$ of data vectors of star-height $h\leq 1$. If
$h=0$, by the distributive law the set $X$ is orbit-finite and hence vacuously
semi-linear. If $h=1$, by the distributive law we similarly deduce that, for
every star subexpression $Y^{*}$, the set $Y$ is orbit-finite; and moreover,
the set $X$ is an orbit-finite union

$\displaystyle X\quad=\quad\bigcup_{i\in I}X_{i},$ (18)

where each $X_{i}$ is a sum of star subexpressions $Y^{*}$ and orbit-finite
sets. As addition is commutative, preserves orbit-finiteness, and admits
merging of stars:

$Y^{*}\ +\ Z^{*}\quad=\quad\big{(}Y\cup Z\big{)}^{*},$

each of sets $X_{i}$ is of the form

$Z+Y^{*}$

where $Y$ and $Z$ are both obit-finite. Therefore each $X_{i}$ is semi-linear,
and hence the orbit-finite (18) union is semi-linear too. ∎

###### Proof of Lemma 10.

The proof is an adaptation of the argument from [27]. Towards contradiction,
suppose $\text{\sc Par}(L_{3})$ is semilinear:

$\displaystyle\text{\sc Par}(L_{3})\quad=\quad\bigcup_{i\in
I}\,g_{i}+{P_{i}}^{*}.$

For a data vector $p:\text{\sc Atoms}\to\mathbb{N}$, let $\text{\sc
Sing}(p)=|\\{a\in\text{\sc Atoms}\,:\,p(a)=1\\}|$ denote the number of atoms
appearing exactly once in $p$. Our argument relies on a careful analysis of
the limit value of the _singularity ratio_ $\frac{\text{\sc Sing}(p)}{|p|}$,
for $p\in\text{\sc Par}(L_{3})$, when $|p|$ tends to infinity.

By induction on the length of $w\in L_{3}$ one easily proves:

######  Claim 12.

Every $p\in\text{\sc Par}(L_{3})$ satisfies $\text{\sc
Sing}(p)<\frac{1}{2}|p|$.

######  Claim 13.

Every $p\in\text{\sc Par}(L_{3})$ satisfies $\text{\sc
dom}(p)\leq\frac{1}{2}|p|$.

For a data vector $p:\text{\sc Atoms}\to\mathbb{N}$ and $S\subseteq\text{\sc
Atoms}$, we denote by $p-S$ the data vector obtained from $p$ by removing all
occurences of atoms from $S$:

$(p-S)(a)=\begin{cases}p(a)&\text{ if }a\notin S\\\ 0&\text{
otherwise.}\end{cases}$

Let $S_{i}=\text{\sc supp}(P_{i})$. As a consequence of Claim 12, we get:

######  Claim 14.

Every $p\in P_{i}$ ($i\in I$) satisfies $\text{\sc
Sing}(p-S_{i})\leq\frac{1}{2}|p|$.

###### Proof.

Towards contradiction, suppose $\text{\sc Sing}(p-S_{i})>\frac{1}{2}|p|$ for
some $p\in P_{i}$. Let $S^{\prime}=\text{\sc dom}(p-S_{i})$. For an arbitrary
permutation of atoms $\pi\in\text{\sc Perm}$ such that $\pi(a)=a$ for all
$a\in S_{i}$, we have $\pi(p)\in P_{i}$. Consider such permutations
$\pi_{1},\ldots,\pi_{n}\in\text{\sc Perm}$, such that $\pi_{k}(S^{\prime})$
and $\pi_{l}(S^{\prime})$ are disjoint for $k\neq l$. As $|g_{i}|$ is fixed,
for sufficiently large $n$ the vector

$g_{i}+\pi_{1}(p)+\ldots+\pi_{n}(p)\ \in\ \text{\sc Par}(L_{3})$

contradicts Claim 12. This completes the proof. ∎

We call a data vector $p:\text{\sc Atoms}\to\mathbb{N}$ _non-singular_ if
$p(a)>1$ for some $a\in\text{\sc Atoms}$. Claim 14 can be strengthened as long
as non-singular data vectors are considered:

######  Claim 15.

Every $p\in P_{i}$ ($i\in I$) such that $p-S_{i}$ is non-singular, satisfies
$\text{\sc Sing}(p-S_{i})<\frac{1}{2}|p|$.

###### Proof.

Indeed, suppose $\text{\sc Sing}(p-S_{i})\geq\frac{1}{2}|p|$ for some $p\in
P_{i}$, and hence $\text{\sc dom}(p-S_{i})>\frac{1}{2}|p|$ due to non-
singularity of $p-S_{i}$. Considering similar permutations of $p$ as in the
argument for Claim 14, we contradict Claim 13. ∎

Let $k=\max\\{|S_{i}|\,:\,i\in I\\}$ be the maximal size of the support of
$P_{i}$; note that $k$ is well defined as the family of sets
$\\{P_{i}\\}_{i\in I}$ is orbit-finite, and the size of the support is
invariant inside an orbit. Likewise, let $t=\max\\{|g_{i}|\,:\,i\in I\\}$ be
the maximal size of a base and let $s=\max\\{|p|\,:\,p\in\bigcup_{i}P_{i}\\}$
be the maximal size of a period.

Let $Z=\\{a_{0},\ldots,a_{k}\\}\subseteq\text{\sc Atoms}$ be some fixed $k+1$
atoms. A word $v\in L_{a}$ (cf. (8)) we call _varied_ if all atoms different
than $a$ appear at most once in $v$. For every $m\in\mathbb{N}$ choose some
arbitrary but fixed word $w_{m}\in L_{3}$ of the form:

$\displaystyle w_{m}\ =\ v_{0}\,v_{1}\,\ldots\,v_{k}\ \in\
L_{a_{0}}\,L_{a_{1}}\,\ldots\,L_{a_{k}},$ (19)

where each $v_{i}\in L_{a_{i}}$ is a varied word of length $2m$ and no atom
appears in two distinct words $v_{a_{i}}$, $v_{a_{j}}$, for $i\neq j$. Let
$q_{m}=\text{\sc Par}(w_{m})$. Hence $|w_{m}|=|q_{m}|=2m(k+1)$. As $\text{\sc
Sing}(q_{m})=(m-1)(k+1)$, in the limit we have:

$\displaystyle\lim_{m\to\infty}\frac{\text{\sc Sing}(q_{m})}{|q_{m}|}\ =\
\lim_{m\to\infty}\frac{(m-1)(k+1)}{2m(k+1)}\ =\ \frac{1}{2},$ (20)

irrespectively of the choice of the words $w_{m}$. Let
$g_{i_{m}}+{P_{i_{m}}}^{\\!\\!*}$ ($i_{m}\in I$) be a linear set to which
$q_{m}$ belongs. Thus $q_{m}=g_{i_{m}}+p_{m}$, for
$p_{m}\in{P_{i_{m}}}^{\\!\\!*}$. Recalling (19), choose $a_{i_{m}}\in Z$ so
that $a_{i_{m}}\notin S_{i_{m}}$ (such $a_{i_{m}}$ exists as $|S_{i_{m}}|\leq
k$). We split $p_{m}$:

$\displaystyle q_{m}\ =\ \,(g_{i_{m}}+p_{m,0})\,+\,p_{m,1}\,+\,p_{m,>1},$ (21)

where $p_{m,1}$ is a sum of vectors from $P_{i_{m}}$ that contain exactly one
appearance of $a_{i_{m}}$; $p_{m,>1}$ is a sum of vectors from $P_{i_{m}}$
that contain more than one appearance of $a_{i_{m}}$; and $p_{m,0}$ is a sum
of vectors from $P_{i_{m}}$ that contain no appearance of $a_{i_{m}}$ at all.
Applying Claim 12 to $g_{i_{m}}+p_{m,0}\in\text{\sc Par}(L_{3})$, we obtain:

$\displaystyle\limsup_{m\to\infty}\frac{\text{\sc
Sing}(g_{i_{m}}+p_{m,0})}{|g_{i_{m}}+p_{m,0}|}\leq\frac{1}{2}.$ (22)

Observe that the size of the sum of the last two data vectors in (21)
constitutes, up to a constant $t$, at least $\frac{1}{2(k+1)}$ fraction of the
whole size $|p_{m}|$ (recall that $|g_{i}|$ is bounded by $t$):

$\displaystyle\frac{1}{2(k+1)}|p_{m}|-|g_{i}|\ <\ |p_{m,1}+p_{m,>1}|$ (23)

as it includes all $\frac{1}{2(k+1)}|p_{m}|+1$ appearances of $a_{i_{m}}$ in
$q_{m}$, except for at most $|g_{i}|$ many of them, possibly appearing in
$g_{i}$. We are going to prove the following strict inequality

$\displaystyle\limsup_{m\to\infty}\frac{\text{\sc
Sing}(p_{m,1}+p_{m,>1})}{|p_{m,1}+p_{m,>1}|}<\frac{1}{2}$ (24)

which, together with inequalities (22) and (23), implies

$\limsup_{m\to\infty}\frac{\text{\sc Sing}(q_{m})}{|q_{m}|}<\frac{1}{2}$

and thus contradicts the equality (20). Call $p_{m,1}$ _non-trivial_ if it is
a sum of at least two vectors from $P_{m}$. When $p_{m,1}$ is trivial,
$|p_{m,1}|\leq s$ is bounded and hence $p_{m,1}$ can be ignored in (24). We
split the inequality (24) into two separate ones

$\displaystyle\limsup_{m\to\infty}\frac{\text{\sc
Sing}(p_{m,1})}{|p_{m,1}|}<\frac{1}{2},\ \limsup_{m\to\infty}\frac{\text{\sc
Sing}(p_{m,>1})}{|p_{m,>1}|}<\frac{1}{2}$ (25)

and prove the first one assuming that $p_{m,1}$ is non-trivial, and the second
one unconditionally. This is enough to derive (24).

Concerning the first inequality, we observe that the atom $a_{i_{m}}\notin
S_{i_{m}}$ is counted in $\text{\sc Sing}(v-S_{i_{m}})$ for every data vector
$v$ contributing to the sum $p_{m,1}$, but if there are more than one of these
vectors $v$, then the atom $a_{i_{m}}$ is no more counted in $\text{\sc
Sing}(p_{m,1}-S_{i_{m}})$. Thus $\text{\sc Sing}(p_{m,1}-S_{i_{m}})$ loses,
intuitively speaking, at least the $\frac{1}{s}$ fraction of the maximal
possible value $\frac{1}{2}|p_{m,1}|$ according to Claim 14. This allows us to
deduce:

$\frac{\text{\sc
Sing}(p_{m,1}-S_{i_{m}})}{|p_{m,1}|}\leq\frac{1}{2}\cdot\Big{(}1-\frac{1}{s}\Big{)}<\frac{1}{2}$

which implies, in the limit, the first inequality in (25), as $|S_{i_{m}}|$ is
bounded (by $k$).

Concerning the second inequality, let’s put

$r=\max\\{\frac{\text{\sc Sing}(v-S_{i})}{|v|}\,:\,v\in P_{i},\ v-S_{i}\text{
is non-singular}\\}.$

As before, $r$ is well defined due to orbit-finiteness of all $P_{i}$ and
$(P_{i})_{i\in I}$, and moreover $r<\frac{1}{2}$ by Claim 15. A crucial
observation is that

$\frac{\text{\sc Sing}(p_{m,>1}-S_{i_{m}})}{|p_{m,>1}|}\leq\frac{\text{\sc
Sing}(v-S_{i_{m}})}{|v|}$

for some $v\in P_{m}$ that contributes to the sum $p_{m,>1}$, and hence

$\frac{\text{\sc Sing}(p_{m,>1}-S_{i_{m}})}{|p_{m,>1}|}\leq r<\frac{1}{2}$

which implies, in the limit, the second inequality in (25), as $|S_{i_{m}}|$
is bounded. The inequalities (25) are thus proved. ∎

###  -D Missing items in Section V

###### Proof of Lemma 14.

For a nonterminal $q\in Q$ and an atom $a\in\text{\sc Atoms}$, consider the
set of derivation trees of $\mathcal{G}$ with root labeled by ${q}(a)$, which
use only productions with the left-hand side in $Q\times\\{a\\}$ (thus every
non-leaf in such a tree belongs to $Q\times\\{a\\}$), and where every leaf
belongs either to $H\times\text{\sc Atoms}$ or to $Q\times(\text{\sc
Atoms}-\\{a\\})$. Intuitively, we stop derivation at a terminal, or at a
configuration with register value different than $a$ (i.e., at first register
update along every path). The language $L_{{q}(a)}$ generated by such trees is
obtained by applying a substitution to a classical context-free language (with
the finite set $Q\times\\{a\\}$ of nonterminals), and thus has rational Parikh
image.

The proof is by induction on $n$. In case $n=0$, we observe that
$H_{{q}(a),0}$ is the restriction of $L_{{q}(a)}$ to terminals
$H\times\\{a\\}$:

$H_{{q}(a),0}\quad=\quad L_{{q}(a)}\ \cap\ (H\times\\{a\\})^{*}$

and thus is itself a classical context-free language (with the finite set
$Q\times\\{a\\}$ of nonterminals and the finite set $H\times\\{a\\}$ of
terminals); in consequence, it has rational Parikh image.

For the induction step we assume rationality of languages $H_{{q}(a),n}$, and
observe that $H_{{q}(a),{n+1}}$ is obtained by applying to the language
$L_{{q}(a)}$ the substitution:

${p}(b)\quad\mapsto\quad H_{{p}(b),n}\qquad\langle
h,b\rangle\quad\mapsto\quad\langle h,b\rangle,$

where $p\in Q$, $h\in H$, and $b\in\text{\sc Atoms}$. Indeed, intuitively
speaking, $L_{{q}(a)}$ allows for exactly one register update, while
$H_{{p}(b),n}$ allows for ${\leq}n$ additional register updates along every
path. Therefore $H_{{q}(a),{n+1}}$ has rational Parikh image, as required. ∎

###  -E Missing items in Section VII

###### Proof of Lemma 20.

We transform a rational expression $E$ defining a language
$L\subseteq\Gamma^{*}$ into a rational expression $\widetilde{E}$ defining
$L\triangleleft\alpha$. We proceed by structural induction on $E$. In case of
orbit-finite union the transformation is distributive:

$\widetilde{\bigcup_{i\in I}E_{i}}\quad:=\quad\bigcup_{i\in
I}\widetilde{E_{i}}.$

In case of sum, the transformation is applied to one of summands:

$\widetilde{\ \ E_{1}\ +\ E_{2}\ \ }\ :=\quad(\widetilde{E_{1}}\ +\
E_{2})\quad\cup\quad(E_{1}\ +\ \widetilde{E_{2}}).$

In case of iteration, the transformation is applied to a single iteration
(which forces at least one iteration and hence rules out the vacuous
generation of the zero vector $\mathbf{0}$ due to $0$ iterations):

$\widetilde{\ E^{*}\ }\quad:=\quad\widetilde{E\ }E^{*}.$

Finally, the induction base, for a singleton $\\{\beta\\}$, is given by:

$\widetilde{\\{\beta\\}}\quad:=\quad\begin{cases}\mathbf{0}&\text{ if }\
\beta=\alpha\\\ \emptyset&\text{ otherwise}.\end{cases}$

∎

For a word $w=\alpha_{1}\ldots\alpha_{n}\in\Gamma^{*}$ we denote by $\text{\sc
srces}(w)$ the sequence $\text{\sc src}(\alpha_{1})\ldots\text{\sc
src}(\alpha_{n})$ of sources. For a finite subset $X\subset\text{\sc Atoms}$
and a regular language $K\subseteq X^{*}$ we define:

$\mathbf{C}^{K}_{a}\ =\ \\{w\in\Gamma^{*}\,:\,\text{\sc srces}(w)\in
K,a\notin\text{\sc trg}(w)\\}.$

######  Lemma 32.

For every finite set $X\subset\text{\sc Atoms}$ and regular language
$K\subseteq X^{*}$, the languages $\mathbf{C}^{K}_{a}$ are rational.

###### Proof.

Consider the finite set $\Delta=(X\cup\\{a\\})^{2}$ as an alphabet, and the
regular language $P\subseteq\Delta^{*}$ of all _$K,a$ -paths_, i.e., all
nonempty sequences

$\langle d_{1},d_{2}\rangle\,\langle d_{2},d_{3}\rangle\,\ldots\,\langle
d_{n},d_{n+1}\rangle\ \in\ \Delta^{*}$

such that $d_{1}d_{2}\ldots d_{n}\in K$ and $d_{n+1}=a$. The language
$\mathbf{C}^{X}_{a}$ is obtained from $P$ by the substitution

$\langle
d,e\rangle\quad\mapsto\quad\bigcup_{\\{e^{\prime},e^{\prime\prime}\\}\in\mathcal{P}_{2}(\text{\sc
Atoms}-\\{e\\})}\langle d,\\{e^{\prime},e^{\prime\prime}\\}\rangle$

and is thus rational. ∎

###### Proof of Lemma 22.

We show that rationality of $\text{\sc Par}(\mathbf{D})$ implies rationality
of $\text{\sc Par}(\mathbf{C})$. To this aim we define, for distinct atoms
$b,c\in\text{\sc Atoms}$, the language

$\displaystyle K_{bc}\ :=\ $ $\displaystyle\
\mathbf{C}^{b\\{b,c\\}^{*}}_{b}\,\,\langle
b,\\{b,c\\}\rangle\quad\cup\quad\mathbf{C}^{b\\{b,c\\}^{*}}_{c}\,\,\langle
c,\\{b,c\\}\rangle$

of all anti-paths where the last target is $\\{b,c\\}$, all sources are in
$\\{b,c\\}$, and the first one is $b$. Languages $K_{bc}$ are rational, due to
Lemma 32. Further, for pairwise distinct atoms $a,b,c$ we define the following
rational language

$\displaystyle K_{a\\{b,c\\}}\ :=\ $ $\displaystyle\ \langle
a,\\{b,c\\}\rangle\ \ \cup\ \bigcup_{b^{\prime},c^{\prime}\in\text{\sc
Atoms}{-}\\{b\\}}\langle a,\\{b^{\prime},c^{\prime}\\}\rangle\,K_{bc}.$

Note that the source of the first letter in every word in $K_{a\\{b,c\\}}$ is
$a$, and the target of the last letter is $\\{b,c\\}$. Lemma 22 follows once
we show the following claim:

######  Claim 16.

$\text{\sc Par}(\mathbf{C})$ is obtained from $\text{\sc Par}(\mathbf{D})$ by
applying _twice_ the substitution

$\langle d,\\{e,f\\}\rangle\quad\mapsto\quad K_{d\\{e,f\\}}.$

(We consider Parikh images of $\mathbf{C}$ and $\mathbf{D}$, instead of the
languages themselves, only because we reason below up to cyclic shifts.) From
now on we concentrate on the proof of the claim. Let $\widetilde{\mathbf{D}}$
denote the set of data vectors obtained from $\text{\sc Par}(\mathbf{D})$ by
applying twice the above-defined substitution. By the very definition,
$\widetilde{\mathbf{D}}\subseteq\text{\sc Par}(\mathbf{C})$. For the converse
inclusion, we prove that every data vector $v\in\text{\sc Par}(\mathbf{C})$
belongs to $\widetilde{\mathbf{D}}$.

If $v$ contains no unwanted letters from $\Gamma-\Sigma$ then $v\in\text{\sc
Par}(\mathbf{D})$, and the claim follows due to $\text{\sc
Par}(\mathbf{D})\subseteq\widetilde{\mathbf{D}}$.

Otherwise, choose an anti-cycle $w\in\mathbf{C}$ with $v=\text{\sc Par}(w)$
and consider the last appearance of an unwanted letter
$(b,\\{b,c\\})\in\Gamma-\Sigma$ in $w$. Applying a cyclic shift
($\rightarrow$) we can assume, w.l.o.g., that the letter is the last one in
$w$. Let $u$ be the maximal suffix of $w$ that belongs to $K_{bc}$ (or,
symmetrically, to $K_{cb}$):

$w\quad=\quad w^{\prime}\,u.$

We observe that $w^{\prime}\neq\varepsilon$; indeed, as $\text{\sc
src}(u)=b\in\text{\sc trg}(u)=\\{b,c\\}$, the word $u$ itself is not an anti-
cycle.

Let $w^{\prime}=w^{\prime\prime}\langle a,\\{b^{\prime},c^{\prime}\\}\rangle$;
since $w$ is an anti-chain we have $b\notin\\{b^{\prime},c^{\prime}\\}$, and
by maximality of $u$ we have $a\notin\\{b,c\\}$. Then $u^{\prime}=\langle
a,\\{b^{\prime},c^{\prime}\\}\rangle\,u\in K_{a,\\{b,c\\}}$. Replace the
suffix $u^{\prime}$ by $\langle a,\\{b,c\\}\rangle$, thus obtaining a data
word $\widetilde{w}=w^{\prime\prime}\langle a,\\{b,c\\}\rangle$ with smaller
number of occurrences of unwanted letters. We continue in the same way with
$\widetilde{w}$ untill all occurences of letters from $\Gamma-\Sigma$ are
eliminated. A crucial observation is that during elimination of all letters,
except for possibly the very last one, the total sum of cyclic shifts
($\rightarrow$) performed does not exceed the full cyclic shift of $w$.
Therefore, Parikh image of the word obtained by elimination of all unwanted
letters except for the last one, belongs to the result of application the
substitution once to $\mathbf{D}$. In consequence, the final word belongs to
the result of applying the substitution twice, as required. ∎

###### Proof of Lemma 24.

For a finite subset $X\subseteq\text{\sc Atoms}$ the language

$\mathbf{C}_{X}\ =\ \mathbf{C}\ \cap\ \\{\alpha\in\Gamma\,:\,\text{\sc
src}(\alpha)\in X\\}^{*}.$

is rational, due to Lemma 32, as it equals

$\bigcup_{a\in X}\mathbf{C}^{aX^{*}}_{a},$

and hence so is its restriction $\mathbf{D}_{X}=\mathbf{C}_{X}\cap\Sigma^{*}$.
The language $\mathbf{D}^{<n}$, being the union of all the rational languages
$\mathbf{D}_{X}$ for subsets $X\subseteq\text{\sc Atoms}$ of cardinality $<n$,
is thus rational as well. ∎

###### Proof of Lemma 30.

Fix $n\geq 6$. We define _the kernel_ of a data vector $v:\Sigma\to\mathbb{N}$
as the intersection of all targets in $v$:

$\text{\sc ker}(v)\ =\ \bigcap_{\alpha\in\text{\sc dom}(v)}\text{\sc
trg}(\alpha).$

The size of the kernel is $0,1$ or $2$. For $X\subseteq\text{\sc Atoms}$ of
size at most $2$, let

$\mathbf{N}^{X,{\geq}n}\ =\ \\{v\in\mathbf{N}^{{\geq}n}\,:\,\text{\sc
ker}(v)=X\\}.$

As $\mathbf{N}^{{\geq}n}=\bigcup_{X}\mathbf{N}^{X,{\geq}n}$, it is enough to
show that the sets $\mathbf{N}^{X,{\geq}n}$ are rational. This, in turn, is
implied by the following decomposition property of sets
$\mathbf{N}^{X,{\geq}n}$:

$\displaystyle\mathbf{N}^{X,{\geq}n}\ =\ \mathbf{N}^{X,{}n}\ +\ \text{\sc
Par}({\Sigma_{X}}^{*}),$ (26)

where $\mathbf{N}^{X,{}n}=\\{v\in\mathbf{N}^{X,{\geq}n}\,:\,\text{\sc
ord}(v)=n\\}$ and $\Sigma_{X}=\\{\alpha\in\Sigma\,:\,X\subseteq\text{\sc
trg}(\alpha)\\}$. Towards showing the decomposition (26) we prove that kernel-
preserving extensions by one letter $\alpha\in\Sigma$ preserve membership in
$\mathbf{N}$:

$v\in\mathbf{N},\ \text{\sc ker}(v)=\text{\sc ker}(v+\alpha)\implies
v+\alpha\in\mathbf{N};$

and also that there always exists a letter $\alpha$ that one can remove from a
vector in $\mathbf{N}^{{\geq}n+1}$, preserving kernel and membership in
$\mathbf{N}$:

$\displaystyle v\in\mathbf{N}^{{\geq}n+1}\implies\exists\alpha\in\text{\sc
dom}(v)\ \colon\ $ $\displaystyle\text{\sc ker}(v)=\text{\sc ker}(v-\alpha),$
$\displaystyle v-\alpha\in\mathbf{N}.$

Concerning the first property, suppose $v\in\mathbf{N}$ and $\text{\sc
ker}(v)=\text{\sc ker}(v+\alpha)$. We thus know that $v$ satisfies conditions
(1)–(3) and that $d=\text{\sc src}(\alpha)\notin\text{\sc ker}(v)$ since
$d\notin\text{\sc trg}(\alpha)$. This implies that $v+\alpha$ satisfies (1).
For conditions (2)–(3) we consider two separate cases. If $d\in V_{v}$ then
adding $\alpha$ may only increase in-neighbour sets $\text{\sc in}(\\_)$ and
preceeding-letter sets $\text{\sc pre}(\\_)$, and hence $v+\alpha$ satisfies
(2)–(3). Otherwise, suppose $d\notin V_{v}$ is a fresh source. We reason by
contradiction. If $v+\alpha$ violates (2) for $d$ and some $e\in V_{v}$, then
$v$ necessarily violates (1) due to $\text{\sc in}(e)=\emptyset$. If
$v+\alpha$ violates (3) for $d$ and some $e\in V_{v}$, then all
$\beta\in\text{\sc dom}(v)$, except for exactly one, satisfy $\text{\sc
trg}(\beta)=\\{d,e\\}$ and hence forcedly $\text{\sc src}(\beta)\neq e$.
Therefore there is exactly one $e$-sourced letter in $v$ and $\text{\sc
in}(e)=\emptyset$, and hence $v$ violates (1) again.

We now concentrate on the second property. Removal of a letter from $v$ may
only increase (inclusion-wise) the kernel, say from $X$ to $X^{\prime}$, but
this only happens if $v(\alpha)=1$, $X^{\prime}\not\subseteq\text{\sc
trg}(\alpha)$, and $X^{\prime}\subseteq\text{\sc trg}(\beta)$ for all
$\beta\in\text{\sc dom}(v)-\\{\alpha\\}$. By inspection of possible sizes 1, 2
of $X^{\prime}$, one deduces that $v$ may contain at most two such kernel-
increasing letters. This eliminates at most $2$ potential sources $\text{\sc
src}(\alpha)$.

Non-degeneracy can be only violated by vertices in the source graph of in-
degree below $2$. Therefore non-degeneracy of $v-\alpha$ is guaranteed if
removal of $\alpha$ does not decrease in-degree of any vertex below $2$, i.e.,
$\text{\sc src}(\alpha)$ does not belong to $\text{\sc in}(d)$ for $d\in
V_{v}$ of in-degree $\text{\sc in-deg}(d)\leq 2$. For sufficiently large $n$,
similarly as in Claim 11, there are at most $2$ such vertices $d$ in $V_{v}$.
This eliminates at most $4$ potential sources $\text{\sc src}(\alpha)$.

In total, at most $6$ potential sources $\text{\sc src}(\alpha)$ are
eliminated. Therefore, as long as $\text{\sc ord}(v)>6$, there is
$\alpha\in\text{\sc dom}(v)$ such that $\text{\sc ker}(v)=\text{\sc
ker}(v-\alpha)$ and $v-\alpha\in\mathbf{N}$. ∎