One-way definability of two-way word transducers
*The results presented here were published
in [4] and [6]. The work was partially supported by the projects ExStream  (ANR-13-JS02-0010)
and DeLTA (ANR-16-CE40-0007).
F. Baschenis]Félix Baschenis1
1Department of Mathematics and Informatics, University Bremen

O. Gauwin]Olivier Gauwin2
2LaBRI, University of Bordeaux, CNRS

A. Muscholl]Anca Muscholl2

G. Puppis]Gabriele Puppis3
3CNRS, LaBRI

Functional transductions realized by two-way transducers
(or, equally, by streaming transducers or MSO transductions)
are the natural and standard notion of “regular” mappings from words to words.
It was shown in 2013 that it is decidable if such a
transduction can be implemented by some one-way transducer,
but the given algorithm has non-elementary complexity.
We provide an algorithm of different flavor solving the
above question, that has doubly exponential space complexity. In the
special case of sweeping transducers the complexity is one exponential
less.  We also show how to
construct an equivalent one-way transducer, whenever
it exists, in doubly or triply exponential time, again depending on
whether the input transducer is sweeping or two-way. In the sweeping
case our construction is shown to be optimal.

[inline]One can deplore that said figures are not always present to help understand some notation heavy proofs, but as it stands, the paper is nicely illustrated.

[inline]The fact that some long, intricate proofs do not benefit the same degree of structure and illustrations is the only blemish.

[inline]It is announced that those results are already published in two other papers [3,4]. If some results are new to this version, it should be made explicit. If not, disregard this comment.
[inline]done, added paragraph in intro

§ INTRODUCTION

Since the early times of computer science, transducers have been
identified as a fundamental computational model. Numerous
fields of computer science are ultimately concerned with
transformations, ranging from databases to image
processing, and an important challenge is to perform transformations with
low costs, whenever possible.

The most basic form of transformations is obtained using devices that
process an input with finite memory
and produce outputs during the processing. Such
devices are called finite-state transducers. Word-to-word finite-state
transducers were considered in very early work in formal language
theory [29, 1, 16], and it was soon clear that they are much more
challenging than finite-state word acceptors (classical finite-state
automata). One essential difference between transducers and automata
over words is that the capability to process the
input in both directions strictly increases the expressive power in the case
of transducers, whereas this does not for
automata [28, 30]. In other words, two-way word transducers
are strictly more expressive than one-way word transducers.

We consider in this paper  functional transducers, that compute
functions from words to words. Two-way word transducers capture very
nicely the notion of regularity in this setting. Regular word
functions, in other words,  functions computed by functional two-way transducers
[We know from [17, 15] that deterministic
and non-deterministic functional two-way transducers have the
same expressive power, though the non-deterministic variants are
usually more succinct.],
inherit many of the characterizations and algorithmic properties of the robust
class of regular languages. Engelfriet and Hoogeboom [17]
showed that monadic second-order definable graph transductions,
restricted to words, are equivalent to two-way transducers — this
justifies the
notation “regular” word functions, in the spirit of classical
results in automata theory and logic by Büchi, Elgot, Rabin and
others. Recently, Alur and Cerný [2] proposed an enhanced
version of one-way transducers called streaming transducers, and
showed that they are equivalent to the two previous models. A streaming
transducer processes the input word from left to right, and stores
(partial) output words in some given write-only registers, that are
updated through concatenation and constant updates.

[inline]Few reasons are given for a specific focus towards two-way transducers as opposed to equivalent models.
[inline]I answered to the editor that the main reason is that we are more familiar with it, so it seems natural. But we shouldn't mention it here.

[inline]I agree not to say it here, but I would not say this
is the real reason - and I changed the answer. The real reason (for
me) is that pumping SST is much less intuitive.

Two-way transducers raise challenging questions about resource
requirements. One crucial resource is the number of times the
transducer needs to re-process the input word. In particular, the case
where the input can be processed in a single pass, from left to right,
is very attractive as it corresponds to the setting of streaming,
where the (possibly very large) inputs do not need to be stored in order
to be processed. The one-way definability of a functional
two-way transducer, that is, the question
whether the transducer is equivalent to some one-way transducer, was
considered quite recently: [19] shows that one-way
definability of string transducers is a decidable property. However, the decision procedure
of [19] has non-elementary complexity, which raises the
question about the intrinsic complexity of this problem.

In this paper we provide an algorithm of elementary complexity solving
the one-way definability problem.
Our decision algorithm has single or doubly exponential space complexity,
depending on whether the input transducer is sweeping (namely, it performs reversals
only at the extremities of the input word) or genuinely two-way.

We also describe an algorithm that constructs an equivalent one-way
transducer, whenever it exists, in doubly or triply exponential time,
again depending on whether the input transducer is sweeping or
two-way.   For the
construction of an equivalent one-way transducer we obtain a doubly
exponential lower bound, which is tight for sweeping transducers. Note that for the decision problem,
the best lower bound known is only polynomial space [19].
[inline]The subclass of sweeping transducers is central to
the paper: not only is the algorithm of better complexity in this
particular case, it is also used as an easy case to prepare for the
general proof. However, beyond this property, it is unclear whether
this class has other interesting properties, or has garnered
interest in the part. This information should, ideally, be made
available in the introduction.  [inline]added a paragraph

[inline]Were deterministic two-way word transducers
considered at all (Introduction)? If not, do you plan to consider
them (Conclusion)?  [inline]added the footnote in intro,
and a paragraph in conclusion
[inline]I think the question is "do you have a better
complexity if the given transducer is deterministic?" like
usually. We maybe also need to add something like : One can notice
that if we want to decide definability by deterministic
one-way transducers, an efficient procedure is known since
Choffrut78 [inline]you can complete the conclusion if you
want. To me it is sufficient.

added this paragraph
Changed a bit (without the reviewer comment the paragraph was a bit isolated)
changed a bit more
Our initial interest in sweeping transducers was the fact that they
provide a simpler setting for characterizing one-way
definability. Later it turned out that sweeping transducers enjoy interesting and
useful connections with streaming transducers: they have the same
expressiveness as streaming transducers where concatenation of
registers is disallowed. The connection goes even further, since the number of
sweeps corresponds exactly to the number of
registers [5]. The results of this paper were refined
in [5], and used to determine the minimal number of
registers required by functional streaming transducers without
register concatenation.

§.§ Related work.

Besides the papers mentioned above, there are
several recent results around the expressivity and the resources of
two-way transducers, or
equivalently, streaming transducers.
First-order definable transductions were shown to be equivalent to
transductions defined by aperiodic
streaming transducers [20] and to aperiodic two-way
transducers [10]. An effective characterization of
aperiodicity for one-way transducers was obtained in [18].

Register minimization for right-appending deterministic streaming

was shown to be
decidable in [14]. An algebraic characterization of (not necessarily
functional) two-way transducers over unary alphabets was
provided in [12]. It was shown that in this case
sweeping transducers have the same expressivity.
The expressivity of non-deterministic input-unary
or output-unary two-way
transducers was investigated in [22].

In [32] a pumping lemma for two-way transducers is proposed,
and used to investigate properties of the output languages of  two-way
transducers. In this paper we also rely on pumping arguments over runs
of two-way transducers, but we require loops of a particular form,
that allows to identify periodicities in the output.

TODO ref Ismael to be improved before resubmission

The present paper unifies results on one-way definability obtained
in [4] and [6].

Compared to the conference versions, some combinatorial proofs have
I have removed the reference to Saarela
been simplified,

and the complexity of the procedure presented in [4] has been
improved by one exponential.
please check. I deleted the sentence on the
under-approximation, because I don't find it understandable at this point.
added this paragraph

§.§ Overview.

Section <ref> introduces basic
notations for two-way and sweeping transducers, and Section <ref>
states the main result and provides a roadmap of the proofs. For
better readability our paper
is divided in two parts: in the first part we consider the easier case of
sweeping transducers, and in the second part the general case. The two
proofs are similar, but the general case is more involved since we
need to deal with special loops (see
Section <ref>).  Since the high-level ideas of the
proofs are the same and the sweeping case illustrates them in a
simpler way, the proof in that setting is a preparation for the
general case.  Both proofs have
the same structure: first we introduce some combinatorial arguments
(see Section <ref> for the sweeping case
and Section <ref> for the general case), then we provide the
characterization of one-way definability (see
Section <ref> for the sweeping case and
Section <ref> for the general
case). Finally, Section <ref> establishes the complexity
of our algorithms.

§ PRELIMINARIES

We start with some basic notations and definitions for two-way
automata and transducers. We assume that every input word $w=a_1\cdots a_n$
has two special delimiting symbols $a_1 = \vdash$
and $a_n = \dashv$ that do not occur elsewhere: $a_i \notin \{\vdash,\dashv\}$
for all $i=2,\dots,n-1$.

A two-way automaton is a tuple
$\cA=(Q,\Sigma,\vdash,\dashv,\Delta,I,F)$, where

* $Q$ is a finite set of states,

* $\Sigma$ is a finite alphabet (including $\vdash, \dashv$),

* $\Delta \subseteq Q \times \Sigma \times Q \times \set{\Left,\Right}$
is a transition relation,

* $I,F\subseteq Q$ are sets of initial and final states, respectively.

By convention, left transitions on $\vdash$ are not
allowed; on the other hand, right transitions on $\dashv$ are allowed, but, as we will see,
they will necessarily appear as last transitions of successful runs.
A configuration of $\cA$ has the form $u\,q\,v$,
with $uv \in \vdash\,  \S^* \, \dashv$
and $q \in Q$. A configuration $u\,q\,v$ represents the
situation where the current state of $\cA$ is $q$ and its head reads the first
symbol of $v$ (on input $uv$). If $(q,a,q',\Right) \in \Delta$,

then there is a transition from any configuration of the form
$u\,q\,av$ to the configuration $ua\,q'\,v$; we denote such a transition
by $u\,q\,av \trans{a,\Right} ua\,q'\,v$.
Similarly, if $(q,a,q',\Left) \in \Delta$,
then there is a transition from any configuration of the form
$ub\,q\,av$ to the configuration $u\,q'\,bav$,
denoted as $ub\,q\,av \trans{a,\Left} u\,q'\,bav$.

A run on $w$
is a sequence of transitions.

It is successful if it starts in an initial configuration
$q\, w$, with $q\in I$, and ends in a final configuration $w\,q'$,
with $q' \in F$ — note that this latter configuration does not allow
additional transitions. The language of $\cA$ is the set of words
that admit a successful run of $\cA$.

The definition of two-way transducers is similar to that of two-way automata,
with the only difference that now there is an additional output alphabet $\Gamma$ and the transition
relation is a finite subset of $Q \times \Sigma \times \Gamma^* \times  Q \times \{\Left,\Right\}$,
which associates an output over $\Gamma$ with each transition of the underlying two-way automaton.
For a two-way transducer $\cT=(Q,\Sigma,\vdash,\dashv,\Gamma,\Delta,I,F)$,
we have a transition of the form $ub\,q\,av \trans{a,d \, \mid w} u'\,q'\,v'$, outputting $w$,
whenever $(q,a,w,q',d)\in\Delta$ and either $u'=uba ~\wedge~ v'=v$ or
$u'=u ~\wedge~ v'=bav$, depending on whether $d=\Right$ or $d=\Left$.
The output associated with a  run
$\rho = u_1\,q_1\,v_1 \trans{a_1,d_1 \mid w_1}<\qquad> \dots
\trans{a_n,d_n \mid w_n}<\qquad> u_{n+1}\,q_{n+1}\,v_{n+1}$
of $\cT$ is the word $\out{\rho} = w_1\cdots w_n$. A transducer $\cT$
defines a relation $\sL(\cT)$
I was wondering if we ever use this notation, but
I found it on page 10... Maybe it is the only place...
consisting of all pairs $(u,w)$ such that
$w=\out{\rho}$, for some successful run $\rho$ on $u$.
The domain of $\cT$, denoted $\dom(\cT)$,
is the set of input words that have a successful run.
For transducers $\cT,\cT'$, we write $\cT' \subseteq \cT$
to mean that $\dom(\cT') \subseteq \dom(\cT)$ and the transductions
computed by $\cT,\cT'$ coincide on $\dom(\cT)$.

A transducer is called one-way if it does not contain transition
rules of the form $(q,a,w,q',\Left)$. It is called sweeping if
it can perform reversals only at the borders of the input word.
A transducer that is equivalent to some one-way
(resp. sweeping) transducer is called one-way definable
(resp. sweeping definable).

The size of a transducer takes into
account both the state space and the transition relation, and thus
includes the length of the output of each transition.

§.§ Crossing sequences.

The first notion that we use throughout the paper is that of crossing sequence.
We follow the convenient presentation from [24], which appeals to a
graphical representation of runs of a two-way transducer, where each configuration
is seen as a point (location) in a two-dimensional space.
Let $u=a_1\cdots a_n$ be an input word (recall that $a_1=\vdash$ and $a_n=\dashv$)
and let $\rho$ be a run of a two-way automaton (or transducer) on $u$.
The positions of $\rho$ are the numbers from $0$ to $n$, corresponding
to “cuts” between two consecutive letters of the input. For example,
position $0$ is just before the first letter $a_1$,
position $n$ is just after the last letter $a_n$,
and any other position $x$, with $1\le x<n$, is between
the letters $a_x$ and $a_{x+1}$.
We will denote by $u[x_1,x_2]$ the factor of $u$ between
the positions $x_1$ and $x_2$ (both included).

Please check this reformulation in terms of configurations
Each configuration $u\,q\,v$ of a two-way run $\r$
has a specific position associated with it. For technical reasons
%(i.e.~to correctly define crossing sequences later),
we need to distinguish leftward and rightward transitions. If the configuration $u q v$
is the target of a rightward transition %  , namely, if $\rho$
% contains a transition of the form $u'\,q'\,v' \trans{a,\Right} u\,q\,v$,
then the position associated with $u q v$ is  $x=|u|$.
The same definition also applies when $u q v$ is the initial configuration,
for which we have $u=$ and $x=|u|=0$.
Otherwise, if $u q v$ is the target of a leftward transition
% $u'\,q'\,v' \trans{a,\Left} u\,q\,v$ of $\rho$,
then the position associated with $u q v$ is $x=|u|+1$. Note that in
both cases, the letter read by the transition leading to $u q v$ is
\anca{rewritten a bit}%
%We say that a transition $u\,q\,v \trans{a,d} u'\,q'\,v'$ of $\rho$ \emph{crosses position $x$}
%if either $d=\Right$ and $|u'|=x$, or $d=\Left$ and $|u|=x$.
%\olivier{I swapped $|u|$ and $|u'|$ here, see review 2 below. Please check!}%
%\felix{it's fine, but maybe we can gain some place by dealing with these issues in the paragraph where we define configurations (where the same distinctions happen)?}%
A \emph{location} of $ρ$ is any pair $(x,y)$,
where $x$ is the position of some configuration of $ρ$ and
$y$ is any non-negative integer for which there are at least
$y+1$ configurations in $ρ$ with the same position $x$.
The second component $y$ of a location is called \emph{level}.
For example, in Figure \ref{fig:run} we represent a possible
run of a two-way automaton together with its locations $(0,0)$,
$(1,0)$, $(2,0)$, $(2,1)$, etc.
Each location is naturally associated with a configuration, and thus a state.
Formally, we say that $q$ is the \emph{state at location $\ell=(x,y)$} in $ρ$,
and we denote this by writing $ρ(ℓ)=q$,
if the $(y+1)$-th configuration of $ρ$ with position $x$ has state $q$.
%For the location $(0,0)$, the state is the source state of the first transition
%in $\rho$.
%\olivier{added, see review 2 below}
Finally, we define the \emph{crossing sequence} of $ρ$ at position $x$
as the tuple $ρ|x=(q_0,…,q_h)$, where the $q_y$'s are all the states
at locations of the form $(x,y)$, for $y=0,…,h$.

\input{run}

As shown in Figure~\ref{fig:run}, a two-way run can be represented
as an path between locations annotated by the associated states.
We observe in particular that if a location $(x,y)$ is the target
of a rightward transition, then this transition has read the symbol $a_x$;
similarly, if $(x,y)$ is the target of a leftward transition, then
the transition has read the symbol $a_x+1$.
We also observe that, in any successful run $ρ$, every crossing
sequence has odd length and every rightward (resp.~leftward) transition
reaches a location with even (resp.~odd) level.
In particular, we can identify four types of transitions between locations,
depending on the parities of the levels (the reader may refer again to
\begin{center}
\begin{tikzpicture}[baseline=0,scale=0.9]
\draw (-1,1.75) node (node1) {$\phantom{\!+\!1}~(x,2y)$};
\draw (3,1.75) node (node2) {$(x\!+\!1,2y')~\phantom{\!+\!1}$};
\draw (-1,0) node (node3) {$(x,2y\!+\!1)$};
\draw (3,0) node (node4) {$(x\!+\!1,2y'\!+\!1)$};
\draw (9,1.75) node (node5) {$\phantom{\!+\!1}~(x,2y)$};
\draw (9,2.5) node (node6) {$(x,2y\!+\!1)$};
\draw (9,0) node (node7) {$(x,2y\!+\!1)$};
\draw (9,0.75) node (node8) {$(x,2y\!+\!2)$};
\draw (node1) edge [->] node [above=-0.05, scale=0.9] {\small $a_{x+1},\Right$} (node2);
\draw (node4) edge [->] node [above=-0.05, scale=0.9] {\small $a_{x+1},\Left$} (node3);
\draw (node5.east) edge [->, out=0, in=0, looseness=2]
node [right=0, scale=0.9] {\small $a_{x+1},\Left$} (node6.east);
\draw (node7.west) edge [->, out=180, in=180, looseness=2]
node [left=0, scale=0.9] {\small $a_x,\Right$} (node8.west);
\end{tikzpicture}
\vspace{1mm}
\end{center}
Hereafter, we will identify runs with the corresponding annotated paths between locations.

It is also convenient to define a total order $$ on the locations of a run $ρ$
by letting $ℓ_1 ℓ_2$ if $ℓ_2$ is reachable from $ℓ_1$ by following the
path described by $ρ$ --- the order $$ on locations is called
\emph{run order}.
Given two locations $ℓ_1 ℓ_2$ of a run $ρ$, we write $ρ[ℓ_1,ℓ_2]$
for the factor of the run that starts in $ℓ_1$ and ends in $ℓ_2$. Note that the latter
is also a run and hence the notation $ρ[ℓ_1,ℓ_2]$ is permitted.
\gabriele{Parity of levels needs to be preserved}%
We will often reason with factors of runs up to isomorphism, that is, modulo
shifting the coordinates of their locations while preserving the parity of the levels.
Of course, when the last location of (a factor of) a run $ρ_1$
coincides with the first location of (another factor of) a run $ρ_2$,
then $ρ_1$ and $ρ_2$ can be concatenated to form a longer run,
denoted by $ρ_1 ρ_2$.
\olivier{added, see review 2 below}%
\gabriele{rephrased a bit, and I think corrected a problem with negative numbers.
But do we really need to say this?}%
This operation can be performed even if the two locations,
say $(x_1,y_1)$ and $(x_2,y_2)$, are different, provided that
$y_1=y_22$: in this case it suffices to shift the positions
(resp.~levels) of the locations of the first run $ρ_1$ by $x_2$ (resp.~$y_2$)
and, similarly, the positions (resp.~levels) of the locations of the second
run $ρ_2$ by $x_1$ (resp.~$y_1$).
\felix{it's not really enough, with our current definition the first location of $\rho_2$ is $(x,0)$ is $x$ is the position of the cut. So we cannot even concatenate $\rho_1$ and $\rho_2$. I have an alternate paragraph where the locations of the subruns use the levels of the original run.}%
\gabriele{I don't understand your comment Felix. Does it still apply?}%
%, provided that $\rho_1$ ends in location $(x,y)$,
%$\rho_2$ starts in location $(x,y')$, such that $y'=y \pmod{2}$ and $(x,y)$, $(x,y')$ are
%labelled by the same state.
%\anca{shouldn't we simply ask that the last location of the first run
%      equals the first location of the second run, as it is written
%      the line after}
%\gabriele{That would be correct, but I think not complete: when reasoning with flows, we need
%          to be able to concatenate "abstract" runs, no matter what are their locations.
%          Alternatively, we could take the definition you suggest, but then say that
%          runs are treated essentially up to isomorphism or, equally, up to translations
%          of their locations. Would this be better?}
%\anca{I prefer your second suggestion (up to isomorphism).}
%We denote by $\r_1 \r_2$ the run resulting from concatenating
%$\r_1$ with $\r_2$.
%Clearly, we have $\rho[\ell_1,\ell_2] ~ \rho[\ell_2,\ell_3] = \rho[\ell_1,\ell_3]$
%for all locations $\ell_1 \leqtime \ell_2 \leqtime \ell_3$.

\reviewTwo[inline]{
There seems to be some problems in you definition of crossing sequences.

First, according to your definition, the state at location $(x,y)$ is the state reached by the $(y+1)$-th transition that crosses x. In order for this to be consistent with Figure 1, you should swap u and u' in your definition of a position crossed by a transition.
\olivier[inline]{Correct, there was a mistake there! Check my fix above.}%

Second, since, following your definition, the state at a given location always is the target of a transition, the first state of the run has no location (it should be added explicitly).
\olivier[inline]{Correct, also fixed}%

Third, not allowing more freedom in the second components of the locations seems to cause some problems while considering subruns.
Let me explain what I mean with an example.
Let us suppose that we split the run $\rho$ of your Figure 1 into two runs $\rho_1$ and $\rho_2$, where $\rho_2$ is composed of the last three transitions.
Then the locations of the states of the run $\rho_1$ (considered as a whole run) are equal to the locations of the same states considered as part of $\rho$.
However, the locations of the states of the run $\rho_2$ (considered as a whole run) are (1,0), (2,0), (3,0), (4,0), whereas in $\rho$, the locations of the corresponding states are  (1,2), (2,2), (3,0), (4,0).
As a consequence, $\rho_1$ and $\rho_2$ can not be concatenated to reform $\rho$, since to do so we need that “the last location of [\dots] $\rho_1$ coincides with the first location of [\dots] $\rho_2$” (p.5 l.15).
\olivier[inline]{Added a sentence to explicit}%

Finally (and this one is not a real problem), you introduce precise notions, but sometimes do not use them in the following parts of the paper: for example, p.4, “never uses a left transition from position x” corresponds to “no transition crosses position x”. Why not use the latter ?
\olivier[inline]{``no left transition on $\vdash$'' comes before the definition of ``crosses'' and is more explicit, so I would not change.}%
\anca{there is no ``crosses'' anymore, right?}%

\begin{wrapfigure}{r}{5.1cm}
\input{intercepted-factors}
\end{wrapfigure}
%  \input{intercepted-factors}
\medskip
\subsection*{Intercepted factors.}
%\gabriele{Be careful if you move text before this point: every time we need to
%  adjust the layout}
%\olivier{Indeed. So I moved it to a usual figure env.}
For simplicity, we will denote by $ω$
the maximal position of the input word.
We will consider \emph{intervals of positions} of
the form $I=[x_1,x_2]$, with $0 ≤x_1<x_2 ≤ω$.
The \emph{containment} relation $⊆$ on intervals is
defined expected, as $[x_3,x_4] ⊆[x_1,x_2]$ if $x_1≤x_3 < x_4≤x_2$.
%Throughout the paper, an \emph{interval} $I=[x_1,x_2]$ is a contiguous
%set of positions of a run $\rho$. So, if $\r$ is a run over a word of
%length $n$, then $0 \le x_1 \le x_2 \le n$.
A \emph{factor} of a run $ρ$ is a contiguous subsequence of $ρ$.
A factor of $ρ$ \emph{intercepted} by an interval
$I=[x_1,x_2]$ is a maximal factor  that visits only
positions $x∈I$, and never uses a left transition from
position $x_1$ or a right transition from position $x_2$.
%It is easy to see that distinct factors intercepted by $I$
%visit disjoint sets of locations.
Figure~\ref{fig:intercepted-factors} on the right shows
the factors $α,β,γ,δ,ζ$ intercepted
by an interval $I$.
The numbers that annotate the endpoints of the factors
represent their levels.

\medskip
\subsection*{Functionality.}
We say that a transducer is \emph{functional}  (equivalently, one-valued, or single-valued)
if for each input $u$, at most one output $w$ can be
produced by any possible successful run on $u$.
Of course, every deterministic transducer is functional, while the opposite
implication fails in general.
To the best of our knowledge determining the precise complexity of the determinization
of a two-way transducer (whenever an equivalent deterministic one-way transducer exists)
is still open. From classical bounds on determinization of finite automata, we only know
that the size of a determinized transducer may be exponential in the worst-case.
One solution to this question, which is probably
not the most efficient one,  is to
check one-way definability: if an equivalent one-way transducer is
constructed, one can check in $$ if it can be
determinized~[11, 33, 7].

The following result,  proven in Section \ref{sec:complexity},
is the  reason to consider only functional transducers:

\renewcommand{\thethm}{\ref{prop:undecidability}}
\begin{prop}[]%\label{prop:undecidability}
The one-way definability problem for \emph{non-functional}
sweeping transducers is undecidable.
\end{prop}

Unless otherwise stated, hereafter we tacitly assume that all transducers
are functional. Note that functionality is a decidable property, as shown below.
The proof of this result is similar to the decidability proof for the equivalence problem
of deterministic two-way transducers~[23], as it reduces the functionality
problem to the reachability problem of a $1$-counter automaton of exponential size.
A matching $$ lower bound follows by a reduction of the emptiness problem
for the intersection of finite-state automata [26].

\begin{prop}\label{prop:functionality-pspace}
Functionality of two-way transducers can be decided in polynomial
space. This problem is $\pspace$-hard already for sweeping transducers.
\end{prop}

A (successful) run of a two-way transducer is called \emph{normalized}
if it never visits two locations with the same position, the same
state, and both either at even or at odd level. It is easy to see that
if a successful run $ρ$ of a \emph{functional} transducer visits two locations
$ℓ_1=(x,y)$ and $ℓ_2=(x,y')$ with the same state
$ρ(ℓ_1)=ρ(ℓ_2)$ and with $y=y' 2$,  then the output
produced by $ρ$ between $ℓ_1$ and $ℓ_2$ is empty:
otherwise, by repeating the non-empty factor $ρ[ℓ_1,ℓ_2]$, we would
contradict functionality.  So, by deleting the factor
$ρ[ℓ_1,ℓ_2]$ we obtain a successful run that produces the
same output. Iterating this operation leads to an equivalent,
normalized run.

Normalized runs are interesting because their crossing sequences have
bounded length (at most $= 2|Q|-1$). Throughout the paper we
will implicitly assume that successful runs are normalized. The
latter property can be easily checked on crossing sequences.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\section{One-way definability: overview}\label{sec:overview}

In this section we state our main result, which is the existence of an
elementary algorithm for checking whether a two-way transducer is
equivalent to some one-way transducer. We call such transducers
\emph{one-way definable}. Before stating our result, we
start with  a few examples illustrating the reasons that may prevent a
transducer to be one-way definable.

\begin{exa}\label{ex:one-way-definability}
We consider two-way transducers that accept any input $u$
from a given regular language $R$ and produce as output the word $u\,u$.
We will argue how, depending on $R$, these transducers may or may not be one-way definable.
\begin{enumerate}
\item If $R=(a+b)^*$, then there is no equivalent one-way transducer,
as the output language is not regular.
If $R$ is finite, however, then the transduction mapping $u\in R$ to $u\,u$
can be implemented by a one-way transducer that stores the input $u$
(this requires at least as many states as the cardinality of $R$),
and outputs $u\,u$ at the end of the computation.
\item A special case of transduction with finite domain is obtained from the language
$R_n = \{ a_0 \, w_0 \, \cdots a_{2^n-1} \, w_{2^n-1} \::\: a_i\in\{a,b\} \}$,
where $n$ is a fixed natural number, the input alphabet is $\{a,b,0,1\}$,
and each $w_i$ is the binary encoding of the index $i=0,\dots,2^n-1$
(hence $w_i\in\{0,1\}^n$).
According to Proposition~\ref{prop:lower-bound} below, the transduction
mapping $u\in R_n$ to $u\,u$ can be implemented by a two-way transducer
of size $\cO(n^2)$, but every equivalent one-way transducer
%      requires a number of states
has size (at least) doubly exponential in $n$.
\item Consider now the periodic language $R=(abc)^*$.
The function that maps $u\in R$ to $u\,u$ can be easily implemented by a
one-way transducer: it suffices to output alternatively $ab$, $ca$, $bc$
for each input letter, while checking that the input is in $R$.
\end{enumerate}
\end{exa}

\begin{exa}\label{ex:running}
We consider now a slightly more complicated transduction
that is defined on input words of the form $u_1 \:\#\: \cdots \:\#\: u_n$,
where each factor $u_i$ is over the alphabet $\Sigma=\{a,b,c\}$.
The associated output has the form
$w_1 \:\#\: \cdots \:\#\: w_n$, where each $w_i$
is either $u_i \: u_i$ or just $u_i$, depending on whether or not
$u_i\in (abc)^*$ and $u_{i+1}$ has even length, with $u_{n+1}=\emptystr$
by convention.

\noindent
The natural way to implement this transduction is by means
of a two-way transducer that performs multiple passes
on the factors of the input:
a first left-to-right pass is performed on
$u_i \,\#\, u_{i+1}$ to produce the first copy of $u_i$
and to check whether $u_i\in (abc)^*$ and $|u_{i+1}|$ is even; if so,
a second pass on $u_i$ is performed to produce
another copy of $u_i$.

\noindent
Observe however that the above transduction can also be implemented by a one-way
transducer, using non-determinism: when entering a factor $u_i$, the transducer
guesses whether or not $u_i\in (abc)^*$ and $|u_{i+1}|$ is even;
depending on this it outputs either $(abc\,abc)^{\frac{|u_i|}{3}}$
or $u_i$, and checks that the guess is correct while proceeding to
read the input.
\end{exa}

\noindent
% We can already state our effective characterization without
% appealing to technical definitions.

\medskip

The  main result of our paper is an elementary algorithm that decides
whether a functional transducer is one-way definable:

\begin{thm}\label{thm:main}
There is an algorithm that takes as input a functional two-way
transducer $\cT$ and outputs in $3\exptime$ a \emph{one-way} transducer
$\cT'$ satisfying the following properties:
\begin{enumerate}
\item $\cT'\subseteq\cT$,
\item $\dom(\cT')=\dom(\cT)$ if and only if $\cT$ is one-way definable.
\item $\dom(\cT')=\dom(\cT)$ can be checked in $2\expspace$.
\end{enumerate}
Moreover, if $\cT$ is a sweeping transducer, then $\cT'$ can be
constructed in $2\exptime$
and $\dom(\cT')=\dom(\cT)$ is decidable in $\expspace$.
\end{thm}

\begin{rem}
The transducer $\cT'$ constructed in the above theorem is
in a certain sense maximal: for every
$v \in \dom(\cT) ~\setminus~ \dom(\cT')$
and every one-way transducer $\cT''$ with
$\dom(\cT') \subseteq \dom(\cT'') \subseteq \dom(\cT)$ there exists
some witness input $v'$ obtained from $v$ such that
$v' \in \dom(\cT) ~\setminus~ \dom(\cT'')$. We will make this more
precise at the end of Section~\ref{sec:characterization-twoway}.
\end{rem}

We also provide a two-exponential lower bound for the size of the equivalent transducer.
As the lower bound is achieved by a sweeping transduction (even a deterministic one),
this gives a tight lower bound on the size of any one-way transducer equivalent to
some sweeping transducer.

\begin{prop}\label{prop:lower-bound}
\gabriele{I have added the fact that the sweeping transducers are even deterministic}%
There is a family $(f_n)_{n\in\bbN}$ of transductions such that
\begin{enumerate}
\item $f_n$ can be implemented by a deterministic sweeping transducer of size $\cO(n^2)$,
\item $f_n$ can be implemented by a one-way transducer,
\item every one-way transducer that implements $f_n$
has size $\Omega(2^{2^n})$.
\end{enumerate}
\end{prop}

\begin{proof}
The family of transformations is precisely the one described in
Example~\ref{ex:one-way-definability}~(2), where $f_n$ maps inputs of the form
$u = a_0 \, w_0 \, \cdots \, a_{2^n-1} ~ w_{2^n-1}$ to outputs of the form $u\,u$,
where $a_i\in\{a,b\}$ and $w_i\in\{0,1\}^n$ is the binary encoding of $i$.
A deterministic sweeping transducer implementing $f_n$ first checks that the
binary encodings $w_i$, for $i=0,\dots,2^n-1$, are correct.
This can be done with $n$ passes:
the $j$-th pass uses $\cO(n)$ states to check the correctness of
the $j$-th bits of the binary encodings.
Then, the sweeping transducer performs two additional passes to
copy the input twice. Overall, the sweeping transducer has size $\cO(n^2)$.

As already mentioned, every one-way transducer that implements $f_n$ needs
to remember input words $u$ of exponential length in order to output $u\,u$, which
roughly requires doubly exponentially many states.
A more formal argument providing a lower bound for the size of a one-way
transducer implementing $f_n$ goes as follows.

First of all, one observes that given a one-way transducer $\cT$,
the language of its outputs,
i.e., $L^{\text{out}}_\cT = \{ w \::\: (u,w)\in\sL(\cT) \text{ for
some } u\}$
is regular. More precisely, if $\cT$ has size $N$, then the language
$L^{\text{out}}_\cT$ is recognized by an automaton of size linear in $N$.
%, where $\cmax$ is the maximal length of an output produced by a single transition.
Indeed, while parsing $w$, the automaton can guess an input word $u$
and a run on $u$,
together with a factorization of $w$ in which the $i$-th
factor corresponds to the output of the transition
on the $i$-th letter of $u$. Basically, this requires
storing as control states the transition rules of $\cT$ and the
suffixes of outputs.

Now, suppose that the function $f_n$ is implemented by a one-way
transducer $\cT$ of size $N$. The language
$L^{\text{out}}_\cT = \{ u\,u \::\: u\in\dom(f_n) \}$ is then
recognized by an automaton of size $\cO(N)$.
Finally, we recall a result from [21], which shows that,
given a sequence of pairs of words $(u_i,v_i)$, for $i=1,\dots,M$,
every non-deterministic automaton that separates the language
$\{u_i\,v_i \::\: 1\le i\le M\}$ from the language
$\{u_i\,u_j \::\: 1\le i\neq j\le M\}$ must have at least $M$ states.
%and hence at least size $M$.
By applying this result to our language $L^{\text{out}}_\cT$, where
$u_i=v_i$ for all $i=1,\dots,M=2^{2^n}$, we get that $N$ must be at
least linear in $M$, and hence $N \in \Omega(2^{2^n})$.
\end{proof}

\bigskip
\gabriele{improved a bit, but we may do better}%
The proof of Theorem~\ref{thm:main} will be developed in the next sections.
The main idea is to decompose a run of the two-way transducer $$
into factors that can be easily simulated in a one-way manner. We defer the
formal definition of such a decomposition to Section \ref{sec:characterization-sweeping},
while here we refer to it simply as a ``$$-decomposition'', where
$$ is a suitable number computed from $$.
The reader can refer to Figure~\ref{fig:decomposition-sweeping} on page
\pageref{fig:decomposition-sweeping}, which provides some intuitive
account of a $$-decomposition for a sweeping run.
Roughly speaking, % the reason why such a characterization is possible is that
each factor
of a $$-decomposition either already looks like a run of a
one-way transducer (e.g.~the factors $D_1$ and $D_2$ of Figure~\ref{fig:decomposition-sweeping}),
or it produces a periodic output, where the period is bounded by $$
(e.g.~the factor between $ℓ_1$ and $ℓ_2$).
Identifying factors that look like runs of one-way transducers is rather easy.
On the other hand, to identify factors with periodic outputs we rely on
a notion of ``inversion'' of a run. Again, we defer the formal definition
and the important combinatorial properties of inversions
to Section \ref{sec:combinatorics-sweeping}.
The reader can refer to Figure \ref{fig:inversion-sweeping}
on page \pageref{fig:inversion-sweeping}
for an example of an inversion of a run of a sweeping transducer.
Intuitively, this is a portion of run that is potentially difficult to simulate
in a one-way manner, due to existence of long factors of the output that are
generated following the opposite order of the input.
Finally, the complexity of the decision procedure in Theorem~\ref{thm:main}
is analyzed in Section~\ref{sec:complexity}.

\reviewOne[inline]{As neither inversions nor blocks are defined by Page 8, the presence of Theorem 3.6 is not as enlightening as one might hope. If the notion of inversion and their relevance is made quite clear at a glance of Page 11, the definition of run decomposition is not as intuitive. Hence, Theorem 3.6 cannot be appreciated before Page 17. It might be a good idea to give an intuition about inversion and diagonal/blocks before 3.6 (this solution being preferable, but made challenging by how involved the notion of decomposition seems to be in a first read).
\felix[inline]{added the references to the corresponding figures}%
\olivier[inline]{and Gabriele added some intuitions on decompositions}%

\subsection*{Roadmap.}
In order to provide a roadmap of our proofs, we state below the equivalence
between the key properties related to one-way definability, inversions of runs,
and existence of decompositions:

\begin{thm}\label{thm:main2}
Given a functional two-way transducer $\cT$,
an integer $\bound$ can be computed such that the following are equivalent:
\begin{itemize}
\item[\PR1)] $\cT$ is one-way definable,
\item[\PR2)] for every successful run of $\cT$ and every inversion in it,
the output produced amid
the inversion has period at most $\bound$,
\item[\PR3)] every input has a successful run of $\cT$ that admits a $\bound$-decomposition.
\end{itemize}
\end{thm}

%implications, and defer the definitions of $\bound$-decomposition  (Definitions~\ref{def:factors-sweeping},
%and inversions to the subsequent sections. Property \PR2 is stated in
%Propositions~\ref{prop:periodicity-sweeping} and \ref{prop:periodicity-twoway}. The reader can note that in
%the following theorem, the number $\bound$ is  doubly exponential
%in the size of $\cT$ in the general case, and simply exponential when $\cT$ is

As the notions of inversion and $$-decomposition are simpler to formalize
for sweeping transducers, we will first prove the theorem assuming that $T$ is
a sweeping transducer; we will focus later on unrestricted two-way transducers.
Specifically, in Section~\ref{sec:combinatorics-sweeping} we introduce the basic combinatorics
on words and the key notion of inversion for a run of a sweeping transducer, and we prove the
implication \PR1 $⇒$ \PR2.
In Section~\ref{sec:characterization-sweeping} we define $$-decompositions of runs of
sweeping transducers, prove the implication \PR2 $⇒$ \PR3, and sketch a proof of
\PR3 $⇒$ \PR1 (as a matter of fact, this latter implication can be proved in a way
that is independent of whether $$ is sweeping or not, which explains why we
only sketch the proof in the sweeping case).
Section~\ref{sec:loops-twoway} lays down the appropriate definitions
concerning loops of  two-way transducers, and analyzes in detail the effect of
pumping special idempotent loops.
In Section~\ref{sec:combinatorics-twoway} we further develop the combinatorial arguments
that are used to prove the implication \PR1 $⇒$ \PR2 in the general case.
Finally, in Section~\ref{sec:characterization-twoway} we prove the implications
\PR2 $⇒$ \PR3 $⇒$ \PR1 in the general setting,
and show how to decide the condition $(')=()$ of Theorem \ref{thm:main}.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\section{Basic combinatorics for sweeping transducers}\label{sec:combinatorics-sweeping}

We fix for the rest of the section a functional \emph{sweeping transducer} $$,
an input word $u$, and a (normalized) successful run $ρ$ of $$ on $u$.

\medskip
\subsection*{Pumping loops.}
Loops turn out to be a basic concept for characterizing one-way definability.
Formally, a \emph{loop} of $ρ$ is an interval $L=[x_1,x_2]$ such that $ρ|x_1=ρ|x_2$,
namely, with the same crossing sequences at the extremities.
The run $ρ$ can be pumped at any loop $L=[x_1,x_2]$, and this gives rise
to new runs with iterated factors. Below we study precisely the shape of
these pumped runs.

\begin{defi}[anchor point, trace]
Given a loop $L$ and a location $\ell$ of $\rho$, we say that $\ell$ is an
\emph{anchor point in $L$} if $\ell$ is the first location of some factor
of $\rho$ that is intercepted by $L$;
this factor is then denoted%
\footnote{This is a slight abuse of notation, since the factor $\tr{\ell}$
is not determined by $\ell$ alone, but requires also the knowledge of the loop $L$,
which is usually clear from the context.}
as $\tr{\ell}$ and called the \emph{trace of $\ell$}.
\end{defi}

Observe that a loop can have at most $= 2|Q|-1$ anchor points, since
we consider only normalized runs.

Given a loop $L$ of $ρ$ and a number $n∈$, we can replicate $n$ times
the factor $u[x_1,x_2]$ of the input, obtaining a new input of the form
\begin{equation}\label{eq:pumped-word}
\pump_L^{n+1}(u) ~=~ u[1,x_1]\cdot \big(u[x_1+1,x_2]\big)^{n+1} \cdot u[x_2+1,|u|].
\end{equation}
\reviewTwo[inline]{The notation $u[x_1,x_2]$ is not defined.\olivier[inline]{fixed}}
Similarly, we can replicate $n$ times the intercepted factors $ℓ$ of $ρ$,
for all anchor points $ℓ$ of $L$. In this way we obtain a successful run on $_L^n+1(u)$
that is of the form
\begin{equation}\label{eq:pumped-run}
\pump_L^{n+1}(\rho) ~=~ \rho_0 ~ \tr{\ell_1}^n ~ \rho_1 ~ \dots ~ \rho_{k-1} ~ \tr{\ell_k}^n ~ \rho_k
\end{equation}
where $ℓ_1…ℓ_k$ are all the anchor points in $L$
(listed according to the run order $$), $ρ_0$ is the prefix of $ρ$
%before $\tr{\ell_1}$,
ending at $ℓ_1$,
$ρ_k$ is the suffix of $ρ$
%after $\tr{\ell_k}$,
starting at $ℓ_k$, and for all $i=1,…,k-1$,
$ρ_i$ is the factor of $ρ$ between
%$\tr{\ell_i}$ and $\tr{\ell_{i+1}}$.
$ℓ_i$ and $ℓ_i+1$.
Note that $_L^1(ρ)$ coincides with the original run $ρ$. As a matter of fact,
one could define in a similar way the run $_L^0(ρ)$ obtained from removing the loop
$L$ from $ρ$. However, we do not need this, and we will always parametrize the operation
$_L$ by a positive number $n+1$.

An example of a pumped run $_L_1^3(ρ)$ is given in Figure \ref{fig:pumping-sweeping},
together with the indication of the anchor points $ℓ_i$ and the intercepted factors $ℓ_i$.

\input{pumping-sweeping}

\medskip
\subsection*{Output minimality.}
We are interested into factors of the run $ρ$ that lie on a single level
and that contribute to the final output, but in a minimal way, in the sense
that is formalized by the following definition:

\begin{defi}\label{def:output-minimal-sweeping}
Consider a factor $\a=\rho[\ell,\ell']$ of $\rho$.
We say that $\a$ is \emph{output-minimal} if
$\ell=(x,y)$ and $\ell'=(x',y)$, and all loops $L \subsetneq
[x,x']$ %  strictly
% between positions $x,x'$
produce empty output at level $y$.
% with $\min(x,x') < \min(L) \le \max(L) < \max(x,x')$,
% the unique sub-factor of $\rho[\ell,\ell']$ that is intercepted by $L$
% produces empty output.
\end{defi}

From now on, we set the constant $= |Q|^+1$,
where $$ is the capacity of the transducer, that is, the
maximal length of an output produced on a single transition (recall
that  $|Q|^$ is the maximal number of crossing sequences).
As shown below, $$ bounds the length of
the output produced by an output-minimal factor:

\begin{lem}\label{lem:output-minimal-sweeping}
For all output-minimal factors $\alpha$, % intercepted by some interval $I$,
$|\out{\alpha}| \le \bound$.
\end{lem}

\begin{proof}
% Let $\rho[\ell,\ell']$ be a factor of $\rho$ that lies on the same level,
% namely, with $\ell=(x,y)$ and $\ell=(x',y)$,
%Clearly, $\alpha$ starts at a location $(x,y)$ and ends at a location $(x',y)$ on the same level,
%with $x,x'$ endpoints of $I$ (either $x<x'$ or $x'<x$ depending on whether $y$ is even or odd).
Suppose by contradiction that $|\out{\alpha}| > \bound$, with
$\a=\rho[\ell,\ell']$, $\ell=(x,y)$ and $\ell=(x',y)$.
%\olivier{$|\out{\rho[\ell,\ell']}| > \bound$ (or set $\alpha=\rho[\ell,\ell']$)}
%  We head towards proving
%  that $\alpha$ is not
%  output-minimal.

Let $X$ be the set of all positions $x''$, with $\min(x,x') < x'' < \max(x,x')$,
%between $x$ and $x'$ (with $x$ included and $x'$ excluded)
that are sources of transitions of $\alpha$ that produce non-empty output.
Clearly, the total number of letters produced by the transitions that depart
from locations in $X\times\{y\}$ is strictly larger than $\bound-1$.
Moreover, since each transition emits at most $\cmax$ symbols, we have $|X| > \frac{\bound-1}{\cmax} = |Q|^\hmax$.
Now, recall that crossing sequences are sequences of states of length at most $\hmax$.
Since $|X|$ is larger than the number of crossing sequences, $X$ contains two positions
$x_1<x_2$ such that $\rho|x_1=\rho|x_2$. In particular, $L=[x_1,x_2]$
is a loop strictly between  $x,x'$
%  such
% that $\min(x,x') < x_1 = \min(L) \le \max(L) = x_2 < \max(x,x')$
%strictly contained in $I$ and that
%and that intercepts a sub-factor of $\alpha$ that produces
with non-empty output on level $y$.
This shows that $\rho[\ell,\ell']$ is not output-minimal.
\end{proof}

\medskip
\subsection*{Inversions and periodicity.}
Next, we define the crucial notion of inversion. Intuitively, an inversion
in a run identifies a part of the run that is potentially difficult to
simulate in a one-way manner because the order of generating the
output is reversed w.r.t.~the input. Inversions arise naturally in transducers
that reverse arbitrarily long portions of the input, as well as in transducers
that produce copies of arbitrarily long portions of the input.

\label{page-def-inversion}

\begin{defi}\label{def:inversion-sweeping}
An \emph{inversion} of the run $\rho$ is a tuple $(L_1,\ell_1,L_2,\ell_2)$ such that
\begin{enumerate}
\item $L_1,L_2$ are loops of $\r$,
\item $\ell_1=(x_1,y_1)$ and $\ell_2=(x_2,y_2)$
are anchor points of $L_1$ and $L_2$, respectively,
\item $\ell_1 \lesstime \ell_2$ and $x_1 > x_2$
\par\noindent
(namely, $\ell_2$ follows $\ell_1$ in the run,
but the position of $\ell_2$ precedes the position of $\ell_1$),
\item for both $i=1$ and $i=2$, $\out{\tr{\ell_i}}\neq\emptystr$ and $\tr{\ell_i}$ is output-minimal.
\end{enumerate}
\end{defi}

\noindent
The left hand-side of Figure~\ref{fig:inversion-sweeping} gives an example of an inversion,
assuming that the outputs $v_1=\tr{\ell_1}$ and $v_2=\tr{\ell_2}$ are non-empty
and the intercepted factors are output-minimal.

\input{inversion-sweeping}

The rest of the section is devoted to prove the implication \PR1 $\Rightarrow$ \PR2
of Theorem \ref{thm:main2}.
We recall that a word $w=a_1 \cdots a_n$ has \emph{period} $p$ if for every $1\le i\le |w|-p$,
we have $a_i = a_{i+p}$. For example, the word $abc \, abc \, ab$ has period $3$.

We remark that, thanks to Lemma \ref{lem:output-minimal-sweeping},
for every inversion $(L_1,\ell_1,L_2,\ell_2)$, the outputs
$\out{\tr{\ell_1}}$ and $\out{\tr{\ell_2}}$ have length at most $\bound$.
By pairing this with the assumption that the transducer $\cT$ is one-way definable,
and by using some classical word combinatorics, we show that the output
produced between the anchor points of every inversion has period that divides
the lengths of $\out{\tr{\ell_1}}$ and $\out{\tr{\ell_2}}$. In particular, this
period is at most $\bound$.
The proposition below shows a slightly stronger periodicity property,
which refers to the output produced between the anchor points $\ell_1,\ell_2$
of an inversion, but extended on both sides with the words $\out{\tr{\ell_1}}$ and $\out{\tr{\ell_2}}$.
We will exploit this stronger periodicity property later, when dealing with
overlapping portions of the run delimited by different inversions
(cf.~Lemma \ref{lem:overlapping}).

\begin{prop}\label{prop:periodicity-sweeping}
If $\cT$ is one-way definable, then the following property \PR2 holds:
\begin{quote}
For all inversions
$(L_1,\ell_1,L_2,\ell_2)$ of $\rho$, the period $p$ of the word
\[
\out{\tr{\ell_1}} ~ \out{\rho[\ell_1,\ell_2]} ~ \out{\tr{\ell_2}}
\]
divides both $|\out{\tr{\ell_1}}|$ and
$|\out{\tr{\ell_2}}|$. Moreover, $p \le \bound$.
\end{quote}
\end{prop}

The above proposition %, together with Lemma \ref{lem:output-minimal-sweeping},
thus formalizes the implication \PR1 $\Rightarrow$ \PR2 of
Theorem \ref{thm:main2}.
Its proof relies on a few combinatorial results.
The first one is Fine and Wilf's theorem~[27].
In short, this theorem says that, whenever two periodic
words $w_1,w_2$ share a sufficiently long factor, then they
have the same period.
Here we use a slightly stronger variant of Fine and Wilf's theorem,
which additionally shows how to align a common factor of the two words $w_1,w_2$
so as to form a third word containing a prefix of $w_1$ and a suffix of $w_2$.
This variant of Fine-Wilf's theorem will be particularly useful in the proof of Lemma~\ref{lem:overlapping}, while for all other applications the classical
statement suffices.
\olivier{This last sentence is outdated, right?}%
\gabriele{This refers to the variant of Fine-Wilf, which still used in the referenced lemma.
But I rephrased so as to make it clear. Let me know if it makes more sense now.}%

\begin{thm}[Fine-Wilf's theorem]\label{thm:fine-wilf}
If $w_1 = w'_1\,w\:w''_1$ has period $p_1$,
$w_2 = w'_2\,w\,w''_2$ has  period $p_2$, and
the common factor $w$ has length at least $p_1+p_2-\gcd(p_1,p_2)$,
then $w_1$, $w_2$, and $w_3 = w'_1\,w\,w''_2$ have period $\gcd(p_1,p_2)$.
\end{thm}

%A second combinatorial result required in our proof
%was shown by Kortelainen~\cite{kortelainen98}, and later improved
%by Saarela \cite{saarela15}. The result is related to word equations
%with iterated factors, like those that arise from considering outputs of pumped runs.
The second combinatorial result required in our proof concerns periods of words
with iterated factors, like those that arise from considering outputs of pumped runs,
and it is formalized precisely by the lemma below.
To improve readability, we often highlight the
%important iterations of factors inside the considered equation.
important iterations of factors inside a word.

%\begin{thm}[Theorem 4.3 in \cite{saarela15}]\label{thm:saarela}
%Consider a word equation %of the form
%  v_0 \: \pmb{v_1^n} \: v_2 \: \cdots \: v_{k-1} \: \pmb{v_k^n} \: v_{k+1}
%  ~=~
%  w_0 \: \pmb{w_1^n} \: w_2 \: \cdots \: w_{k'-1} \: \pmb{w_{k'}^n} \: w_{k'+1}
%where $n$ is the unknown and $v_i,w_j$ are words.
%%and $v_0,\dots,v_{k+1},w_0,\dots,w_{k'+1}$ do not depend on $m$.
%Then the set of solutions of the equation is either finite or $\bbN$.
%We will use the above result mainly to reason about periodicities of words
%with iterated factors:

\begin{lem}\label{lem:periods}
Assume that $v_0 \: \pmb{v_1^n} \: v_2 \: \cdots \: v_{k-1} \: \pmb{v_k^n} \: v_{k+1}$
has period $p$ for some $n >p$.
Then  $v_0 \: \pmb{{v_1}^{n_1}} \: v_2 \: \cdots \: v_{k-1} \: \pmb{{v_k}^{n_k}} \: v_{k+1}$
has period $p$ for all $n_1,\ldots,n_k \in \Nat$.
\end{lem}

\begin{proof}
Assume that
$w=v_0 \: \pmb{v_1^n} \: v_2 \: \cdots \: v_{k-1} \: \pmb{v_k^n} \: v_{k+1}$
has period $p$, and that $n >p$.
Consider an arbitrary factor $v_i^p$ of $w$. Since $v_i^p$ has periods $p$ and $|v_i|$,
it has also period $r=\gcd(p,|v_i|)$.
By Fine-Wilf (Theorem \ref{thm:fine-wilf}), % elementary word combinatorics,
we know that $w$ has period $r$ as well.
Moreover, since the length of $v_i$ is multiple of $r$,
changing the number of repetitions of $v_i$ inside $w$ does
not affect the period $r$ of $w$.
Since $v_i$ was chosen arbitrarily, this means that, for all $n_1,\dots,n_k\in\bbN$,
$v_0 \: \pmb{{v_1}^{n_1}} \: v_2 \: \cdots \: v_{k-1} \: \pmb{{v_k}^{n_k}} \: v_{k+1}$
has period $r$, and hence period $p$ as well.
\end{proof}

%If $v_0 \: \pmb{v_1^n} \: v_2 \: \cdots \: v_{k-1} \: \pmb{v_k^n} \: v_{k+1}$
%has period $p$ for infinitely many $n$, then it has period $p$ for all $n$.
%\anca{proof rewritten, now it should be ok, but please check}%
%\gabriele{Simplified and corrected further}
%Assume that there is an infinite set $N$ of numbers such that
%$v_0 \: \pmb{v_1^n} \: v_2 \: \cdots \: v_{k-1} \: \pmb{v_k^n} \: v_{k+1}$
%has period $p$ for all $n\in N$.
%Without loss of generality (namely, by restricting $N$ to an infinite subset),
%we can write
%$v_0 \: \pmb{v_1^n} \: v_2 \: \cdots \: v_{k-1} \: \pmb{v_k^n} \: v_{k+1}
% = \pmb{w^{m_n}} \: w'$ for infinitely many $n$,
%where $m_n\in\bbN$, $w$ is some fixed word of length $p$,
%and $w'$ is some fixed prefix of $w$.
%Let $\ell,\ell',\ell''$ denote the lengths of $v_0v_2 \cdots
%v_{k+1}$, $v_1 \cdots v_k$, and $w'$, respectively.
%The equation yields $\ell+\ell'\cdot n = p \cdot m_n + \ell''$,
%and hence $m_n=\frac{\ell'}{p}\cdot n + \frac{\ell-\ell''}{p}$.
%By further restricting the range of the parameter $n$,
%we can enforce that $n \bmod p$ is a constant $c$.
%Now, by letting $\tilde n = \frac{n - c}{p}$ (this is an integer
%for infinitely many $n$), we can rewrite the previous equation as
%  v_0 \: \pmb{\big(v_1^p\big)^{\tilde n}} \: \big(v_1^c\big) \: v_2 \: \cdots \:
%  v_{k-1} \: \pmb{\big(v_k^p\big)^{\tilde n}} \: \big(v_k^c\big) \: v_{k+1}
%  ~=~
%  \pmb{\big(w^{\ell'}\big)^{\tilde n}} \: \big(w^{\frac{\ell+\ell'\cdot c-\ell''}{p}}\big) \: w'.
%%We can even suppose that $n \pmod p=r$, for some $0 \le r <p$ and
%%infinitely many $n$. Pick one such value of $n$ and write
%%$n=pm+r$, so $N(n)=b \cdot m + (br+a-c)/p$.
%%$v_0 \: \pmb{(v_1^p)^m} \: v'_2 \: \cdots \: v'_{k-1} \: \pmb{(v_k^p)^m} \: v'_{k+1}
%% = \pmb{(w^b)^m} \: w''$
%%for suitable words $v'_2,\ldots,
%% v'_{k+1},w''$,  that are all independent of $m$.
%As the equation holds for infinitely many $\tilde n$,
%Theorem \ref{thm:saarela} implies that it also holds for all $\tilde n\in\bbN$,
%and thus for all $n = \tilde n \cdot p + c$. This means that the left handside
%of the equation is a word period $p$ ($=|w|$).
%To establish the periodicity for all $n\in\bbN$, it suffices to observe the following:
%  \item every repetition $(v_i^p)$ has length multiple of $p$ and has period $p$,
%        so, by Fine-Wilf (Theorem \ref{thm:fine-wilf}), it has also period $p'=\gcd(p,|v_i|)$;
%  \item again by Fine-Wilf, the entire word on the left handside has period $p'$;
%  \item the period of a word is preserved when removing or repeating factors
%        of length multiple of that period; in particular,
%        modifying the number of repetitions of each $v_i$
%        in the above left handside preserves the period $p'$,
%        and hence also the period $p$.
%%First, as there is only a finite number of words of length smaller than $C$, we know that there exists a word $z$ such that $|z|\leq C$ and there is an infinite number of integers $n,n'$ such that $z^{(n)}= z^{k(n)} z'$ where $z'$ is a prefix of $z$. Moreover, by analysing the lenght of the words on each side of the equation, one can describe $k(n)$ as a linear function $k(n)=kn + k'$. First as the lenghts of words at the power $n$ on each side of the equation is $|z^k|$ and $\sum |x_i|$, we have $k= \frac{\sum |x_i|}{|z|}$. Then, as the lenghts of words that are not at the power $n$ is $|z^{k'}|+|z'|$and $\sum |y_i|$, we have $k'= \frac{\sum |y_i| -|z'|}{|z|}$.
%%Thus, we can write the equation in the following way : $ y_0 x_0^{n} y_1 x_1^{n} \cdots x_k^{n} y_k= z^{k'}(z^k)^n z' $, where $z^{k'}$, $z^k$, and $z'$ are independent of $n$. This allows us to apply Theorem \ref{thm:saarela} and conclude that $z^{(0)} = z^{k'} z'$, and thus that it has a period $p = |z| \leq C$.

Recall that our goal is to show that the output produced amid every
inversion has period bounded by $\bound$.
The general idea is to pump the loops of the inversion and compare the outputs
of the two-way transducer $\cT$ with those of an equivalent one-way
transducer $\cT'$.
The comparison leads to an equation between words with
iterated factors, where the iterations are parametrized by two unknowns
$n_1,n_2$ that occur in opposite order in the left, respectively right
hand-side of the equation.
Our third and last combinatorial result considers a word equation of
this precise form, and derives from it a periodicity property.
\reviewOne[inline]{In Corollary 4.8, the definition of $v^{(n_1,n_2)}$ is hard to process, especially when introduced in the middle of a proof. The notion is used later in the part: it warrants a proper definition and/or clear example either in the preliminaries or at the beginning of Part 4.
\felix[inline]{I don't understand this remark}
\olivier[inline]{answered in review1-answers.txt: the best place is here.}
\gabriele[inline]{This reviewer commend has led to a number of corrections, and the removal of Saarela tool}
For the sake of brevity, we use the notation $v^{(n_1,n_2)}$
to represent words with factors iterated $n_1$ or $n_2$ times,
namely, words of the form
$v_0 \: v_1^{n_{i_1}} \: v_2 \: \cdots \: v_{k-1} \: v_k^{n_{i_k}} \: v_{k+1}$,
where the $v_0,v_1,v_2,\dots,v_{k-1},v_k,v_{k+1}$ are fixed words (possibly empty)
and each index among $i_1,\dots,i_k$ is either $1$ or $2$.

\begin{lem}\label{lem:oneway-vs-twoway}
Consider a word equation of the form
\[
v_0^{(n_1,n_2)} \: \pmb{v_1^{n_1}} \: v_2^{(n_1,n_2)} \: \pmb{v_3^{n_2}} \: v_4^{(n_1,n_2)}
w_0 \: \pmb{w_1^{n_2}} \: w_2 \: \pmb{w_3^{n_1}} \: w_4
\]
where $n_1,n_2$ are the unknowns and $v_1,v_3$ are non-empty words.
%and $v_0^{(n_1,n_2)},v_2^{(n_1,n_2)},v_4^{(n_1,n_2)}$ are words
%with iterated factors of the form $v^{n_1}$ or $v^{n_2}$,
%for generic words $v$.
If the above equation holds for all $n_1,n_2\in\bbN$,
\[
\pmb{v_1} ~ \pmb{v_1^{n_1}} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3^{n_2}} ~ \pmb{v_3}
\]
has period $\gcd(|v_1|,|v_3|)$ for all $n_1,n_2\in\bbN$.
\end{lem}

\begin{proof}
The idea of the proof is to let the parameters $n_1,n_2$ of the equation
grow independently, and apply Fine and Wilf's theorem (Theorem \ref{thm:fine-wilf})
a certain number of times to establish periodicities in overlapping factors of the
considered words.

We begin by fixing $n_1$ large enough so that the factor
$\pmb{v_1^{n_1}}$ of the left hand-side of the equation becomes
longer than $|w_0|+|w_1|$ (this is possible because $v_1$ is non-empty).
Now, if we let $n_2$ grow arbitrarily large, we see that the length of
the periodic word $\pmb{w_1^{n_2}}$ is almost equal to the length of
the left hand-side term
$v_0^{(n_1,n_2)} ~ \pmb{v_1^{n_1}} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3^{n_2}} ~ v_4^{(n_1,n_2)}$:
indeed, the difference in length is given by the constant
$|w_0| + |w_2| + n_1\cdot |w_3| + |w_4|$.
In particular, this implies that $\pmb{w_1^{n_2}}$
covers arbitrarily long prefixes of
$\pmb{v_1} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3^{n_2+1}}$,
which in its turn contains long repetitions of the word $v_3$.
Hence, by Theorem \ref{thm:fine-wilf},
the word
$\pmb{v_1} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3^{n_2+1}}$
has period $|v_3|$.

We remark that the periodicity shown so far holds for a large enough
$n_1$ and for all but finitely many $n_2$, where the threshold for
$n_2$ depends on $n_1$: once $n_1$ is fixed, $n_2$ needs to be larger
than $f(n_1)$, for a suitable function $f$.
In fact, by using
\gabriele{Saarela has been replaced by the new lemma here}
Lemma \ref{lem:periods},
with $n_1$ fixed and $n=n_2$ large enough,
we deduce that the periodicity holds for large enough $n_1\in\bbN$ and
for all $n_2\in\bbN$.

We could also apply a symmetric reasoning: we choose
$n_2$ large enough and let $n_1$ grow arbitrarily large. Doing so, we
prove that for a large enough $n_2$ and for all but finitely many $n_1$,
the word $\pmb{v_1^{n_1+1}} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3}$ is periodic
with period $|v_1|$. As before, with the help of
%Corollary \ref{cor:saarela},
\gabriele{same here for Saarela...}
Lemma \ref{lem:periods},
this can be strengthened to hold for large enough $n_2\in\bbN$ and for all $n_1\in\bbN$.

Putting together the results proven so far, we get that for all but finitely many $n_1,n_2$,
\[
\rightward{ \underbracket[0.5pt]{ \phantom{ \pmb{v_1^{n_1}} \cdot \pmb{v_1} ~\cdot~
v_2^{(n_1,n_2)} ~\cdot~ \pmb{v_3} } }%
_{\text{period } |v_1|} }
\pmb{v_1^{n_1}} \cdot
\overbracket[0.5pt]{ \pmb{v_1} ~\cdot~ v_2^{(n_1,n_2)} ~\cdot~
\pmb{v_3} \cdot \pmb{v_3^{n_2}} }%
^{\text{period } |v_3|}
\]
Finally, we observe that the prefix
$\pmb{v_1^{n_1+1}}\cdot v_2^{(n_1,n_2)}\cdot \pmb{v_3}$
and the suffix
$\pmb{v_1}\cdot v_2^{(n_1,n_2)}\cdot\pmb{v_3^{n_2+1}}$
share a common factor of length at least $|v_1|+|v_3|$.
By Theorem~\ref{thm:fine-wilf},
we derive that $\pmb{v_1^{n_1+1}}\cdot v_2^{(n_1,n_2)}\cdot
\pmb{v_3^{n_2+1}}$ has period $\gcd(|v_1|,|v_3|)$ for all but finitely
many $n_1,n_2$.
Finally, by using again
%Corollary \ref{cor:saarela},
\gabriele{...and here}
Lemma \ref{lem:periods},
we conclude that the periodicity holds for all $n_1,n_2\in\bbN$.
\end{proof}

\medskip
We are now ready to prove the implication \PR1 $\Rightarrow$ \PR2:

\begin{proof}[Proof of Proposition~\ref{prop:periodicity-sweeping}]
Let $\cT'$ be a one-way transducer equivalent to $\cT$, and consider
an inversion $(L_1,\ell_1,L_2,\ell_2)$ of the successful run $\rho$ of $\cT$
on input $u$.
%, and let $y_i$ be the level of location $\ell_i$, for $i=1,2$.
The reader may refer to Figure \ref{fig:inversion-sweeping}
to get basic intuition about the proof technique.
For simplicity, we assume that the loops $L_1$ and $L_2$ are disjoint,
as shown in the figure. If this were not the case, we would have
at least $\max(L_1) > \min(L_2)$, since the anchor point $\ell_1$
is strictly to the right of the anchor point $\ell_2$.
We could then consider the pumped run $\pump_{L_1}^k(\rho)$ for a
large enough $k>1$ in such a way that the rightmost copy of $L_1$
turns out to be disjoint from and strictly to the right of $L_2$.
We could thus reason as we do below, by replacing everywhere
(except in the final part of the proof, cf.~{\em Transferring periodicity to the original run})
the run $\rho$ with the pumped run $\pump_{L_1}^k(\rho)$, and the formal
parameter $m_1$ with $m_1+k$.

\smallskip\noindent
{\em Inducing loops in $T'$.}~
We begin by pumping the run $\rho$ and the underlying input $u$,
on the loops $L_1$ and $L_2$, in order to induce new loops $L'_1$
and $L'_2$ that are also loops in a successful run of $\cT'$.
Assuming that $L_1$ is strictly to the right of $L_2$, we define for all numbers $m_1,m_2\in\bbN$:
\[
\begin{array}{rcl}
u^{(m_1,m_2)}    &=& \pump_{L_1}^{m_1+1}(\pump_{L_2}^{m_2+1}(u))  \\[1ex]
\rho^{(m_1,m_2)} &=& \pump_{L_1}^{m_1+1}(\pump_{L_2}^{m_2+1}(\rho)).
\end{array}
\]
In the pumped run $\rho^{(m_1,m_2)}$, we identify the positions that mark the
endpoints of the occurrences of $L_1,L_2$. More precisely, if $L_1=[x_1,x_2]$
and $L_2=[x_3,x_4]$, with $x_1>x_4$, then the sets of these positions are
\[
\begin{array}{rcl}
X_2^{(m_1,m_2)} &=& \big\{ x_3 + i(x_4-x_3) ~:~ 0\le i\le m_2+1 \big\} \\[1ex]
X_1^{(m_1,m_2)} &=& \big\{ x_1 + j(x_2-x_1) + m_2(x_4-x_3) ~:~ 0\le j\le m_1+1 \big\}.
\end{array}
\]

\smallskip\noindent
{\em Periodicity of outputs of pumped runs.}~
We use now the fact that $\cT'$ is a one-way transducer equivalent to $\cT$.
\reviewTwo[inline]{you fix $\lambda^{m_1,m_2}$ to be a particular run of T’ on the input $u^{m_1,m_2}$, and then, on line 10, you state that for some particular $m_1$ and $m_2$, this run can be obtained by pumping $\lambda^{k_0,k_0}$. This does not seem true in general: since $T$ is not deterministic, we might just have chosen a different run.}%
\gabriele[inline]{Corrected}%
We first recall (see, for instance, [16, 8])
that every functional one-way transducer can be made unambiguous, namely,
can be transformed into an equivalent one-way transducer that admits at
most one successful run on each input.
This means that, without loss of generality, we can assume that $\cT'$ too
is unambiguous, and hence it admits exactly one successful run, say
$\lambda^{(m_1,m_2)}$, on each input $u^{(m_1,m_2)}$.
%Let $\lambda^{(m_1,m_2)}$ be a successful run of $\cT'$ on the input $u^{(m_1,m_2)}$.

Since $\cT'$ has finitely many states, we can find, for a large enough number $k_0$
%a run $\lambda^{(k_0,k_0)}$,
two positions $x'_1<x'_2$, both in $X_1^{(k_0,k_0)}$, such that $L'_1=[x'_1,x'_2]$
is a loop of $\lambda^{(k_0,k_0)}$. Similarly, we can find two positions
$x'_3<x'_4$, both in $X_2^{(k_0,k_0)}$, such that $L'_2=[x'_3,x'_4]$ is a
loop of $\lambda^{(k_0,k_0)}$.
By construction $L'_1$ (resp.~$L'_2$) consists of $k_1\leq k_0$
(resp.~$k_2\leq k_0$) copies of $L_1$ (resp.~$L_2$), and
hence $L'_1,L'_2$ are also loops of $\rho^{(k_0,k_0)}$.
In particular, this implies that for all $n_1,n_2\in\bbN$:
\[
\begin{array}{rcl}
\pump_{L'_1}^{n_1+1}(\pump_{L'_2}^{n_2+1}(u^{(k_0,k_0)}))
&=& u^{(f(n_1),g(n_2))} \\[1ex]
\pump_{L'_1}^{n_1+1}(\pump_{L'_2}^{n_2+1}(\rho^{(k_0,k_0)}))
&=& \rho^{(f(n_1),g(n_2))} \\[1ex]
\pump_{L'_1}^{n_1+1}(\pump_{L'_2}^{n_2+1}(\lambda^{(k_0,k_0)}))
&=& \lambda^{(f(n_1),g(n_2))}.
\end{array}
\]
where $f(n_1)=k_1 n_1+k_0$ and $g(n_2)=k_2 n_2+k_0$.

Now recall that $\rho^{(f(n_1),g(n_2))}$ and $\lambda^{(f(n_1),g(n_2))}$ are
runs of $\cT$ and $\cT'$ on the same word $u^{(f(n_1),g(n_2))}$, and they
produce the same output. Let us denote this output by $w^{(f(n_1),g(n_2))}$.
Below, we show two possible factorizations of $w^{(f(n_1),g(n_2))}$
based on the shapes of the pumped runs $\lambda^{(f(n_1),g(n_2))}$
and $\rho^{(f(n_1),g(n_2))}$.
For the first factorization, we recall that $L'_2$ precedes $L'_1$,
according to the ordering of positions, and that the run
$\lambda^{(f(n_1),g(n_2))}$ is one-way (in particular loops have only one anchor point and one trace). We thus obtain:
\reviewTwo[inline]{eq. 4.3 The exponents should be $n_2 + 1$ and $n_1 + 1$. (same for eq. 4.4)}
\felix[inline]{Yes but not sure it makes sense to keep the +1 everywhere then}
\gabriele[inline]{We agreed to change the two itemized lists below and replace `right border'
by `left border' everywhere. I have implemented this...}
\begin{equation}\label{eq:one-way}
w^{(f(n_1),g(n_2))} ~=~ w_0 ~ \pmb{w_1^{n_2}} ~ w_2 ~ \pmb{w_3^{n_1}} ~ w_4
\end{equation}
\begin{itemize}
\item $w_0$ is the output produced by the prefix of $\lambda^{(k_0,k_0)}$
ending at the only anchor point of $L'_2$,
\item $\pmb{w_1}$ is the trace of $L'_2$,
\item $w_2$ is the output produced by the factor of $\lambda^{(k_0,k_0)}$
between the anchor points of $L'_2$ and $L'_1$,
\item $\pmb{w_3}$ is the trace of $L'_1$,
\item $w_4$ is the output produced by the suffix of
$\lambda^{(k_0,k_0)}$ starting at the anchor point of $L'_1$. Hence, $w_0 ~ w_2 ~ w_4$ is the output of $\lambda^{(k_0,k_0)}$.
\end{itemize}
\felix{added the last sentence to avoid the $+1$ or not confusion. In addition to the anchor point/trace usage that we talked about}
For the second factorization, we consider $L'_1$ and $L'_2$ as loops of $\rho^{(k_0,k_0)}$.
We recall that $\ell_1,\ell_2$ are anchor points of the loops $L_1,L_2$ of $\rho$, and that
there are corresponding copies of these anchor points in the pumped
run $\rho^{(f(n_1),g(n_2))}$.
We define $\ell'_1$ (resp.~$\ell'_2$) to be the first (resp.~last)
location in $\rho^{(f(n_1),g(n_2))}$ %$\rho^{(k_0,k_0)}$
that corresponds to $\ell_1$ (resp.~$\ell_2$) and that is an anchor point of a copy of $L'_1$ (resp.~$L'_2$).
For example, if $\ell_1=(x_1,y_1)$, with $y_1$ even, then $\ell'_1=\big(x_1+f(n_2)(x_4-x_3),y_1\big)$.
Thanks to Equation \ref{eq:pumped-run} we know that the output produced by
$\rho^{(f(n_1),g(n_2))}$ is of the form
\begin{equation}\label{eq:two-way}
w^{(f(n_1),g(n_2))} ~=~
v_0^{(n_1,n_2)} ~ \pmb{v_1^{n_1}} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3^{n_2}} ~ v_4^{(n_1,n_2)}
\end{equation}
\begin{itemize}
\item $\pmb{v_1}=\out{\tr{\ell'_1}}$, where $\ell'_1$ is seen as an anchor point in a copy of $L'_1$,
%is the trace output of $C_1$ inside $L'_1$
\item $\pmb{v_3}=\out{\tr{\ell'_2}}$, where $\ell'_2$ is seen as an anchor point in a copy of $L'_2$
% is the trace output of $C_2$ inside $L'_2$,
\par\noindent
(note that the words $v_1,v_3$ depend on $k_0$, but not on $n_1,n_2$),
\item $v_0^{(n_1,n_2)}$ is the output produced by the prefix of $\rho^{(f(n_1),g(n_2))}$
that ends at $\ell_1'$ %before the first repetition of $\tr{\ell'_1}$
(this word may depend on the parameters $n_1,n_2$ since the loops
$L'_1,L'_2$ may be traversed several times before reaching the first occurrence of $\tr{\ell'_1}$),
\item $v_2^{(n_1,n_2)}$ is the output produced by the factor of $\rho^{(f(n_1),g(n_2))}$
% betwee the first repetition ... and the last repetition ...
that starts at $\ell'_1$ %the first repetition of $\tr{\ell'_1}$
and ends at $\ell'_2$, % the last repetition of $\tr{\ell'_2}$,
\item $v_4^{(n_1,n_2)}$ is the output produced by the suffix of $\rho^{(f(n_1),g(n_2))}$
%after the last repetition ...
that starts at $\ell'_2$. %the last repetition of $\tr{\ell'_2}$.
\end{itemize}

Putting together Equations~(\ref{eq:one-way}) and (\ref{eq:two-way}), we get
\begin{equation}\label{eq:one-way-vs-two-way}
v_0^{(n_1,n_2)} ~ \pmb{v_1^{n_1}} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3^{n_2}} ~ v_4^{(n_1,n_2)}
w_0 ~ \pmb{w_1^{n_2}} ~ w_2 ~ \pmb{w_3^{n_1}} ~ w_4 .
\end{equation}
%\felix{instead of saying (resp.~$L_2$) everywhere, wouldn't it be clearer is we say
%what we mean for $L_i$, $v_i$, etc... ?}
%\gabriele{I think no. I would like to avoid as much as possible the heavy notations...}
Recall that the  definition of inversions (Definition
\ref{def:inversion-sweeping}) states
that the words $v_1,v_3$ are non-empty.
This allows us to apply Lemma \ref{lem:oneway-vs-twoway}, which shows that the word
$\pmb{v_1} ~ \pmb{v_1^{n_1}} ~ v_2^{(n_1,n_2)} ~ \pmb{v_3^{n_2}} ~ \pmb{v_3}$
has period $p=\gcd(|v_1|,|v_3|)$, for all $n_1,n_2\in\bbN$.
%In particular, this holds for $n_1=n(k_2+1)$ and $n_2=n(k_1+1)$, when
%$n$ ranges over all natural numbers
%--- basically we performed a renaming of variables that satisfies $f(n_1)=g(n_2)$.

Note that the latter period $p$ still depends on $\cT'$, since
the words $v_1,v_3$ were obtained from loops
$L'_1,L'_2$ on the run $\lambda^{(k_0,k_0)}$ of $\cT'$.
However, because each loop $L'_i$ consists of $k_i$ copies of the original loop $L_i$,
we also know that $v_1=(\out{\tr{\ell_1}})^{k_1}$ and $v_3=(\out{\tr{\ell_2}})^{k_2}$.
By Theorem \ref{thm:fine-wilf}, this implies that for all $n_1,n_2\in\bbN$, the word
%This shows that, for all $n\in\bbN$, the word
\[
\big(\out{\tr{\ell_1}}\big) ~
\big(\out{\tr{\ell_1}}\big)^{k_1 n_1} ~
v_2^{(n_1,n_2)} ~
\big(\out{\tr{\ell_2}}\big)^{k_2 n_2} ~
\big(\out{\tr{\ell_2}}\big)
\]
has a period that divides $|\out{\tr{\ell_1}}|$ and $|\out{\tr{\ell_2}}|$.

\smallskip\noindent
{\em Transferring periodicity to the original run.}~
The last part of the proof amounts at showing a similar periodicity property
for the output produced by the original run $\rho$.
By construction, the iterated factors inside $v_2^{(n_1,n_2)}$ in the previous
word are all of the form $v^{k_1 n_1 + k_0}$ or $v^{k_2 n_2 + k_0}$,
for some words $v$. By taking out the constant factors $v^{k_0}$ from the
latter repetitions, we can write $v_2^{(n_1,n_2)}$ as a word with iterated
factors of the form $v^{k_1 n_1}$ or $v^{k_2 n_2}$, namely, as ${v'_2}^{(k_1 n_1, k_2 n_2)}$.
So the word
\[
\big(\out{\tr{\ell_1}}\big) ~
\big(\out{\tr{\ell_1}}\big)^{k'_1} ~
{v'_2}^{(k'_1, k'_2)} ~
\big(\out{\tr{\ell_2}}\big)^{k'_2} ~
\big(\out{\tr{\ell_2}}\big)
\]
is periodic, with period that divides $|\out{\tr{\ell_1}}|$ and $|\out{\tr{\ell_2}}|$,
for all $k'_1 \in \{k_1 n \::\: n\in\bbN\}$ and all $k'_2 \in \{k_2 n \::\: n\in\bbN\}$.
We now apply
%Corollary \ref{cor:saarela},
\gabriele{Also here Saarela has been replaced by the new lemma}
Lemma \ref{lem:periods},
once with $n=k'_1$ and once with $n=k'_2$,
to conclude that the latter periodicity property holds also for $k'_1=1$ and $k'_2=1$.
This shows that the word
\[
\out{\tr{\ell_1}} ~ \out{\rho[\ell_1,\ell_2]} ~ \out{\tr{\ell_2}}
\]
is periodic, with period that divides $|\out{\tr{\ell_1}}|$ and $|\out{\tr{\ell_2}}|$.
\end{proof}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:

\section{One-way definability in the sweeping case}%
\label{sec:characterization-sweeping}

\reviewOne[inline]{From Part 5 onwards, a major point is that an output you can bound is an output you can guess, and a periodic output is an output you don't have to guess, as you can produce it "out of order". On your Figures (and any you might care to add during potential revisions), having a specific visual representation (if possible coherent throughout the paper) to differentiate path sections with empty, bounded, or periodic output will make your point way more intelligible.
\felix[inline]{so this is just about uniformizing the figure for sweeping and for two way ?}%

In the previous section we have shown the implication \PR1 $\Rightarrow$ \PR2 for a functional sweeping
transducer $\cT$. Here we close the cycle by proving the implications \PR2 $\Rightarrow$ \PR3 and \PR3 $\Rightarrow$ \PR1.
In particular, we show how to derive the existence of successful runs admitting a $\bound$-decomposition
and construct a one-way transducer $\cT'$ that simulates $\cT$ on those runs.
This will basically prove Theorem~\ref{thm:main2} in the sweeping case.

\medskip
\subsection*{Run decomposition.}
We begin by giving the definition of $\bound$-decomposition for a run $\rho$ of $\cT$.
Intuitively,  a $\bound$-decomposition of $\rho$ identifies factors of $\rho$ that can be easily simulated
in a one-way manner. The definition below describes precisely the shape of these factors.

First we need to  recall the notion of almost periodicity:
a word $w$ is \emph{almost periodic with bound $p$} if $w=w_0~w_1~w_2$
for some words $w_0,w_2$ of length at most $p$ and some word $w_1$
of period at most $p$.

We need to work with subsequences of the run $\rho$ that are induced by
particular sets of locations, not necessarily consecutive.
Recall that $\rho[\ell,\ell']$ denotes the factor of $\rho$
delimited by two locations $\ell\leqtime\ell'$. Similarly, given any
set $Z$ of locations, we denote by $\rho|Z$ the subsequence of $\rho$
induced by $Z$. Note that, even though $\rho|Z$ might not be a valid
\label{rhoZ}
of the transducer, we can still refer to the number of transitions in it
and to the size of the produced output $\out{\rho|Z}$.
Formally, a transition in $\rho|Z$ is a transition from some $\ell$ to $\ell'$,
where both $\ell,\ell'$ belong to $Z$. The output $\out{\rho|Z}$ is the
concatenation of the outputs of the transitions of $\rho| Z$
(according to the order given by $\rho$).

\reviewOne[inline]{Fig. 5 is moderately informative... Figure 17 and 18 are a more inspiring illustration of the intuition behind diagonal and blocks. Their "restricted" counterpart could be simpler to represent.}%
\gabriele[inline]{done}%

\begin{defi}\label{def:factors-sweeping}
Consider a factor $\rho[\ell,\ell ']$ of a run $\rho$ of $\cT$,
where $\ell=(x,y)$, $\ell'=(x',y')$ are two locations with $x \le x'$.
We call $\rho[\ell,\ell']$
\begin{itemize}
\medskip
%HACKS TO MAKE WRAPFIG WORK IN ITEMIZED LISTS!
\item \parbox[t]{\dimexpr\textwidth-\leftmargin}{%
\vspace{-2.75mm}
\begin{wrapfigure}{r}{7.5cm}
\end{wrapfigure}
a \emph{floor} if $y=y'$ is even, namely, if $\rho[\ell,\ell']$
lies entirely on the same level and is rightward oriented; %$x < x'$ and $y=y'$ is even;
\bigskip
\bigskip
\item \parbox[t]{\dimexpr\textwidth-\leftmargin}{%
\vspace{-2.75mm}
\begin{wrapfigure}{r}{7.5cm}
\vspace{-22mm}
\input{diagonal-sweeping}
\vspace{-4mm}
\end{wrapfigure}
a \emph{$\bound$-diagonal} if %$x < x'$ $y$ and $y'$ are even, and
there is a sequence
$\ell = \ell_0 \leqtime \ell_1 \leqtime \dots \leqtime \ell_{2n+1} = \ell'$,
where each $\rho[\ell_{2i+1},\ell_{2i+2}]$ is a floor,
each $\rho[\ell_{2i}, \ell_{2i+1}]$ produces an output
of length at most $2\hmax\bound$,
and the position of each $\ell_{2i}$
is to the left of the position of $\ell_{2i+1}$;
\bigskip
\smallskip
\item \parbox[t]{\dimexpr\textwidth-\leftmargin}{%
\vspace{-2.75mm}
\begin{wrapfigure}{r}{7.5cm}
\vspace{-10mm}
\input{block-sweeping}
\vspace{-5mm}
\end{wrapfigure}
a \emph{$\bound$-block} if %$x < x'$, $y$ and $y'$ are even,
the output produced by $\rho[\ell,\ell']$ is almost periodic with bound $2\bound$,
and the output produced by the subsequence $\rho|Z$,
where $Z=[\ell,\ell'] ~\setminus~ \big([x,x']\times[y,y']\big)$,
has length at most $2\hmax\bound$.
\vspace{8mm}
\end{itemize}
\end{defi}

Before continuing we give some intuition on the above definitions.
The simplest concept is that of floor, which is a rightward oriented factor of a run.
Diagonals are sequences of consecutive floors interleaved by factors that
produce small (bounded) outputs. We see an example of a diagonal
in Figure \ref{fig:diagonal-sweeping}, where we marked the important
locations and highlighted with thick arrows the two floors that form
the diagonal. The factors of the diagonal that are not floors are
represented instead by dotted arrows.
The third notion is that of a block.
An important constraint in the definition of a block
is that the produce output must be almost periodic, with small enough bound.
In Figure \ref{fig:block-sweeping}, the periodic output is represented by the
thick arrows, either solid or dotted, that go from location $\ell$ to
location $\ell'$.
In addition, the block must satisfy a constraint on the length of
the output produced by the subsequence $\rho|Z$, where
$Z=[\ell,\ell'] ~\setminus~ \big([x,x']\times[y,y']\big)$.
The latter set $Z$ consists of location that are either to the left
of the position of $\ell$ or to the right of the position of $\ell'$.
For example, in Figure \ref{fig:block-sweeping} the set $Z$ coincides
with the area outside the hatched rectangle. Accordingly, the portion
of the subsequence $\rho|Z$ is represented by the dotted bold arrows.

Diagonals and blocks are used as key objects to derive a notion of
decomposition for a run of a sweeping transducer. We formalize this
notion below.
%The general idea for turning $\cT$ into an equivalent one-way transducer
%will be to guess (and check) a decomposition of the run of $\cT$ into factors
%that are diagonals or blocks.

\begin{defi}\label{def:decomposition-sweeping}
A \emph{$\bound$-decomposition} of a run $\rho$ of $\cT$ is a factorization
$\prod_i\,\rho[\ell_i,\ell_{i+1}]$ of $\rho$ into $\bound$-diagonals and $\bound$-blocks.
%where $\ell_i=(x_i,y_i)$, $x_i < x_{i+1}$, and $y_i\le y_{i+1}$ for all $i$.
\end{defi}

\reviewOne[inline]{Fig.6 does not look like a fully factorized run: what happens for example, between the end of $D_1$ and $l_1$? Can a concrete example be devised? This works rather well in Part 8.}%
\gabriele{Improved the figure and the explanation}%
Figure~\ref{fig:decomposition-sweeping} gives an example of such a
\anca{dans Fig 7, les aretes de $B_2$ vont dans la
mauvaise direction}%
\gabriele{I have corrected this. Now the figure is a bit more regular (perhaps too much),
but at least conveys the correct information!}%
Each factor is either a diagonal $D_i$ or a block $B_i$.
Inside each factor we highlight by thick arrows the portions
of the run that can be simulated by a one-way transducer,
either because they are produced from left to right (thus forming diagonals)
or because they are periodic (thus forming blocks).
%and each diagonal is built up of one or more floors.
%The hatched rectangles represent
%\anca{``bounding boxes'' removed, since the name ``block'' should auto-suffice}
%\gabriele{Here I meant to stress a slight difference between a block (an interval of a run) and
%          its bounding box, which might not be an interval of a run: it may consists of several
%          intercepted factors, not necessarily contiguous. But it is fine like this too
%          (nobody will see the difference at first glance!).}
%the bounding boxes of
%the blocks.
We also recall from Definition \ref{def:factors-sweeping}
that most of the output is produced inside the
hatched rectangles, since the output produced by a diagonal
or a block outside the corresponding blue or red hatched rectangle
has length at most $2\hmaxsq\bound$.
Finally, we observe that the locations delimiting the factors of the
decomposition are arranged following the natural order of positions and levels.
All together, this means that the output produced by a run that enjoys
a decomposition can be simulated in a one-way manner.

\input{decomposition-sweeping}

\medskip
\reviewOne[inline]{Part 5: In "From periodicity of inversions to existence of decompositions", the general proof structure in general and transition between lemmas in particular could be made more visually and conceptually explicit, as the global idea of the proof is difficult to grasp at first. A mini "road map" as made in Part 3 for the whole of Part 4 and 5 might be another way to help the reader through these rather intricate proofs.}%

\subsection*{From periodicity of inversions to existence of decompositions.}
Now that we set up the definition of $\bound$-decomposition, we turn
towards proving the implication \PR2 $\Rightarrow$ \PR3 of Theorem \ref{thm:main2}.
In fact, we will prove a slightly stronger result than \PR2 $\Rightarrow$ \PR3,
which is stated further below.
Formally, when we say that a run \emph{$\rho$ satisfies \PR2} we mean
that for every inversion $(L_1,\ell_1,L_2,\ell_2)$ of $\rho$, the word
$\out{\tr{\ell_1}} ~ \out{\rho[\ell_1,\ell_2]} ~ \out{\tr{\ell_2}}$
has period $\gcd(|\out{\tr{\ell_1}}|, |\out{\tr{\ell_2}}|) \le \bound$.
We aim at proving that every run that satisfies \PR2 enjoys a decomposition,
independently of whether other runs do or do not satisfy \PR2:

\begin{prop}\label{prop:decomposition-sweeping}
If $\rho$ is a run of $\cT$ that satisfies \PR2, then $\rho$ admits a $\bound$-decomposition.
\end{prop}

\felix{a few lines for the roadmap asked by the reviewer, but I don't think they're useful at all}%
\gabriele{I think it is good}%
Let us fix a run $\rho$ of $\cT$ and assume that it satisfies \PR2.
To show that $\rho$ admits a $\bound$-decomposition, we will identify
the blocks of the decomposition as equivalence classes of a suitable
relation based on inversions (cf.~Definition \ref{def:crossrel}).
Then, we will use combinatorial arguments (notably,
Lemmas \ref{lem:output-minimal-sweeping} and \ref{lem:overlapping})
to prove that the constructed blocks satisfy the desired properties.
Finally, we will show how the resulting equivalence classes form all
the necessary blocks of the decomposition, in the sense that the factors
in between those classes are diagonals.

We begin by introducing the equivalence relation by means of which we can
then identify the blocks of a decomposition of $\rho$.

\begin{defi}\label{def:crossrel}
Let $\crossrel$ be the relation that pairs every two locations $\ell,\ell'$ of $\rho$
whenever there is an inversion $(L_1,\ell_1,L_2,\ell_2)$ of $\rho$ such that
$\ell_1 \leqtime \ell,\ell' \leqtime \ell_2$, namely, whenever $\ell$ and $\ell'$
occur within the same inversion.
Let $\simeq$ be the reflexive and transitive closure of $\crossrel$.
\end{defi}

It is easy to see that every equivalence class of $\simeq$ is a convex
subset with respect to the run order on locations of $\rho$.
Moreover, every \emph{non-singleton} equivalence class of $\simeq$ is a
union of a series of inversions that are two-by-two overlapping.
One can refer to Figure~\ref{fig:overlapping}
% \anca{the last indices in the figure are strange: I would remove
%       $\ell_6$ and $\ell_{n-2}$, and replace $\ell_{n-3}$ by $\ell_{n-1}$}
% \gabriele{Agree! Even better: I replaced the $n$ with a $2k+1$, as it is used
%           in the proof of Lemma 5.5}
for an intuitive account of what we mean by two-by-two overlapping: the thick
arrows represent factors of the run that lie entire inside an $\simeq$-equivalence class,
each inversion is identified by a pair of consecutive anchor points with the same
color. According to the run order, between every pair of anchor points with the
same color, there is at least one anchor point of different color: this means that
the inversions corresponding to the two colors are overlapping.

\reviewOne[inline]{Fig.7 might benefit from some $L_1$, $L_2$ appearing, to illustrate the point made in Claim 5.6
\felix[inline]{I don't agree}%
\olivier[inline]{I also disagree. Argued in review1-answer.txt.}%
Formally, we say that an inversion $(L_1,\ell_1,L_2,\ell_2)$ \emph{covers}
a location $\ell$ when $\ell_1 \leqtime \ell \leqtime \ell_2$. We say that
two inversions $(L_1,\ell_1,L_2,\ell_2)$ and $(L_3,\ell_3,L_4,\ell_4)$
are \emph{overlapping} if $(L_1,\ell_1,L_2,\ell_2)$ covers $\ell_3$
and $(L_3,\ell_3,L_4,\ell_4)$ covers $\ell_2$ (or the other way around).

\input{overlapping}

The next lemma uses the fact that $\rho$ satisfies \PR2 to deduce that
the output produced inside every $\simeq$-equivalence class has
period at most $\bound$. Note that the proof below does not exploit
the fact that the transducer is sweeping.

\begin{lem}\label{lem:overlapping}
If $\rho$ satisfies \PR2 and $\ell\leqtime\ell'$ are two locations of $\rho$
such that $\ell \simeq \ell'$, then the output $\out{\rho[\ell,\ell']}$
produced between these locations has period at most $\bound$.
\end{lem}

\begin{proof}
The claim for $\ell=\ell'$ holds trivially, so we assume that $\ell\lesstime\ell'$.
Since the $\simeq$-equivalence class that contains $\ell,\ell'$ is non-singleton,
we know that there is a series of inversions
\[
(L_0,\ell_0,L_1,\ell_1) \quad
(L_2,\ell_2,L_3,\ell_3) \quad
\dots\dots \quad
\]
that are two-by-two overlapping and such that
Without loss of generality, we can assume that every
inversion $(L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$ is \emph{maximal}
in the following sense: there is no other inversion
$(\tilde L,\tilde\ell,\tilde L',\tilde\ell') \neq (L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$
such that $\tilde\ell \leqtime \ell_{2i} \leqtime \ell_{2i+1} \leqtime \tilde\ell'$.

For the sake of brevity, let $v_i = \out{\tr{\ell_i}}$ and $p_i = | v_i |$.
% By Definition~\ref{def:inversion-sweeping} and Lemma~\ref{lem:output-minimal-sweeping}, we have $p_i \le \bound$
% for all $i=0,\dots,2k+1$.
Since $\rho$ satisfies \PR2 (recall Proposition~\ref{prop:periodicity-sweeping}), we know that, for all $i=0,\dots,n$, the word
\[
v_{2i} ~ \out{\rho[\ell_{2i},\ell_{2i+1}]} ~ v_{2i+1}
\]
has period that divides both $p_{2i}$ and $p_{2i+1}$ and is at most $\bound$.
In order to show that the period of $\out{\rho[\ell,\ell']}$ is also bounded
by $\bound$, it suffices to prove the following claim by induction on $i$:

\reviewOne[inline]{Claim 5.6, end of page 18: making explicit what words you wish to use Fine-Wilf on might make for a more readable proof.
\olivier[inline]{answered in review1-answer.txt}%

\begin{clm}
For all $i=0,\dots,k$, the word
$\outb{\rho[\ell_0,\ell_{2i+1}]} \: v_{2i+1}$
has period at most $\bound$ that divides $p_{2i+1}$.
\end{clm}

The base case $i=0$ follows immediately from our hypothesis,
since $(L_0,\ell_0,L_1,\ell_1)$ is an inversion.
For the inductive step, we assume that the claim holds for $i<k$,
and we prove it for $i+1$. First of all, we factorize our word as follows:
\[
\outb{\rho[\ell_0,\ell_{2i+3}]} ~ v_{2i+3}
\rightward{ \underbracket[0.5pt]{ \phantom{ %\outb{\rho[\ell_0,\ell_{2i}]} ~
\outb{\rho[\ell_0,\ell_{2i+2}]} ~
\outb{\rho[\ell_{2i+2},\ell_{2i+1}]} ~ } }%
_{\text{period } p_{2i+1}} }
%  \outb{\rho[\ell_0,\ell_{2i}]} ~
\outb{\rho[\ell_0,\ell_{2i+2}]}
\overbracket[0.5pt]{ ~ \outb{\rho[\ell_{2i+2},\ell_{2i+1}]} ~
\outb{\rho[\ell_{2i+1},\ell_{2i+3}]} ~
v_{2i+3} }%
^{\text{periods } p_{2i+2} \text{ and } p_{2i+3}}
\]
By the inductive hypothesis, the output produced between $\ell_0$
and $\ell_{2i+1}$, extended to the right with $v_{2i+1}$,
has period that divides $p_{2i+1}$.
%Moreover, because $\rho$ satisfies \PR2 and
%$(L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$ is an inversion,
%the output produced between the locations
%$\ell_{2i}$ and $\ell_{2i+1}$,
%extended to the left with $v_{2i}$ and to the
%right with $v_{2i+1}$, has period that divides both $p_{2i}$ and $p_{2i+1}$.
%Note that this is not yet sufficient for applying Fine-Wilf's theorem,
%since the common factor $\outb{\rho[\ell_{2i+2},\ell_{2i+1}]}$
%might be too short.
Moreover, because $\rho$ satisfies \PR2 and
$(L_{2i+2},\ell_{2i+2},L_{2i+3},\ell_{2i+3})$ is an inversion,
the output produced between the locations
$\ell_{2i+2}$ and $\ell_{2i+3}$,
extended to the left with $v_{2i+2}$ and to the
right with $v_{2i+3}$, has period that divides both $p_{2i+2}$ and $p_{2i+3}$.
Note that this is not yet sufficient for applying Fine-Wilf's theorem,
since the common factor $\outb{\rho[\ell_{2i+2},\ell_{2i+1}]}$
might be too short (possibly just equal to $v_{2i+2}$).
The key argument here is to prove that the interval $[\ell_{2i+2},\ell_{2i+1}]$
is covered by an inversion
which is different from those that we considered above, namely,
i.e.~$(L_{2i+2},\ell_{2i+2},L_{2i+1},\ell_{2i+1})$. For example,
$[\ell_2,\ell_1]$ in
Figure~\ref{fig:overlapping}  is covered by the inversion

For this, we have to prove that the anchor points $\ell_{2i+2}$ and $\ell_{2i+1}$
are correctly ordered w.r.t.~$\leqtime$ and the ordering of positions
(recall Definition~\ref{def:inversion-sweeping}).
First, we observe that $\ell_{2i+2} \leqtime \ell_{2i+1}$, since
$(L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$ and $(L_{2i+2},\ell_{2i+2},L_{2i+3},\ell_{2i+3})$
are overlapping inversions.
Next, we prove that the position of $\ell_{2i+1}$ is strictly to the left of
the position of $\ell_{2i+2}$. By way of contradiction, suppose that this is
not the case, namely, $\ell_{2i+1}=(x_{2i+1},y_{2i+1})$, $\ell_{2i+2}=(x_{2i+2},y_{2i+2})$,
and $x_{2i+1} \ge x_{2i+2}$. Because $(L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$ and
$(L_{2i+2},\ell_{2i+2},L_{2i+3},\ell_{2i+3})$ are inversions,
we know that $\ell_{2i+3}$ is strictly to the left of $\ell_{2i+2}$
and $\ell_{2i+1}$ is strictly to the left of $\ell_{2i}$.
This implies that $\ell_{2i+3}$ is strictly to the left of $\ell_{2i}$,
and hence $(L_{2i},\ell_{2i},L_{2i+3},\ell_{2i+3})$ is also an inversion.
Moreover, recall that $\ell_{2i} \leqtime \ell_{2i+2} \leqtime \ell_{2i+1} \leqtime \ell_{2i+3}$.
This contradicts the maximality of $(L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$,
which we assumed at the beginning of the proof.
Therefore, we must conclude that $\ell_{2i+1}$ is strictly to the left of $\ell_{2i+2}$.
%Moreover, as $(L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$ is a maximal inversion, we have $x_{2i+2}>x_{2i}$.
%If that was not the case, as $(L_{2i+1},\ell_{2i+2},L_{2i+3},\ell_{2i+3})$ is an inversion, we would have
%$x_{2i+3}\leq x_{2i+2} \leq x_{2i}$, and as $\ell_{2i} \lesstime \ell_{2i+1} \lesstime \ell_{2i+3}$, $(L_{2i},\ell_{2i},L_{2i+3},\ell_{2i+3})$ would be an inversion covering $(L_{2i},\ell_{2i},L_{2i+1},\ell_{2i+1})$
%which is in contradiction with its maximality.

Now that we know that $\ell_{2i+2} \leqtime \ell_{2i+1}$ and that $\ell_{2i+1}$ is to the left of $\ell_{2i+2}$,
we derive the existence of the inversion $(L_{2i+2},\ell_{2i+2},L_{2i+1},\ell_{2i+1})$.
Again, because $\rho$ satisfies \PR2, we know that the word
$v_{2i+2} ~ \out{\rho[\ell_{2i+2},\ell_{2i+1}]} ~ v_{2i+1}$ has period at most $\bound$
that divides $p_{2i+2}$ and $p_{2i+1}$.
Summing up, we have:
\begin{enumerate}
\item $w_1 ~=~ \outb{\rho[\ell_0,\ell_{2i+1}]} ~ v_{2i+1}$ has period $p_{2i+1}$,
\item $w_2 ~=~ v_{2i+2} ~ \outb{\rho[\ell_{2i+2},\ell_{2i+1}]} ~ v_{2i+1}$
has period $p = \gcd(p_{2i+2},p_{2i+1})$,
\item $w_3 ~=~ v_{2i+2} ~ \outb{\rho[\ell_{2i+2},\ell_{2i+3}]} ~ v_{2i+3}$
has period $p' = \gcd(p_{2i+2},p_{2i+3})$.
\end{enumerate}
We are now ready to exploit our stronger variant of Fine-Wilf's theorem,
that is, Theorem~\ref{thm:fine-wilf}.

% \anca{I have rewritten the paragraph, the previous version had some
%   index problems and had to be more precise with the bounds.}
% \gabriele{Well done!}
We begin with  (1) and (2) above.
Let $w = \outb{\rho[\ell_{2i+2},\ell_{2i+1}]}~ v_{2i+1}$ be the common suffix of
$w_1$ and $w_2$. First note that since $p$ divides $p_{2i+2}$, the
word $w$ is also a prefix of $w_2$, thus we can write
$w_2=w\,w'_2$. Second, note that the length of $w$ is at least
$|v_{2i+1}| = p_{2i+1} = p_{2i+1} + p - \gcd(p_{2i+1},p)$. We can
apply now Theorem~\ref{thm:fine-wilf} to $w_1=w'_1\,w$ and
$w_2=w\,w'_2$ and obtain:
% Note that the length of $w$ is at least $|v_{2i+1}| = p_{2i+1} = p_{2i+1} + p - \gcd(p_{2i+1},p)$,
% as required by the hypothesis of Theorem~\ref{thm:fine-wilf}.
% This implies that the period of $w$ divides both
% $p_{2i+1}$ and $p$.
% Moreover, since $p$ divides $|w_2|-|w|$ ($=|v_{2i+2}|$),
% $w$ is also a prefix of $w_2$, and thus we can write $w_2=w\,w'_2$.
% Now, we can think of $w$ as a common factor of $w_1=w'_1\,w$ and $w_2=w\,w'_2$,
% which is sufficiently long to enable the application of Theorem~\ref{thm:fine-wilf}.
% From this we get
\begin{enumerate}
\setcounter{enumi}{3}
\item $w_4 ~=~ w'_1 \: w \: w'_2
~=~ \outb{\rho[\ell_0,\ell_{2i+2}]} ~ v_{2i+2} ~ \outb{\rho[\ell_{2i+2},\ell_{2i+1}]} ~ v_{2i+1}$
has period $p$.
\end{enumerate}

We apply next Theorem~\ref{thm:fine-wilf} to (2) and (3), namely, to
the words $w_2$ and $w_3$ with $v_{2i+2}$ as common factor. It is not
difficult to check that $|v_{2i+2}|=p_{2i+2} \ge p+p'-p''$ with
$p''=\gcd(p,p')$, using the definitions of $p$ and $p'$: we can
write $p_{2i+2}=p''rq=p''r'q'$ with $p=p''r$ and $p'=p''r'$. It suffices  to check
that $p''rq+p''r'q' \ge 2(p''r + p''r'-p'')$, hence that $rq+r'q' \ge 2r+2r'-2$. This
is clear if $\min(q,q')>1$. Otherwise the inequality $p_{2i+2} \ge
p+p'-p''$ follows easily because $p=p''$ or $p'=p''$ holds. Hence we obtain
that $w_2$ and $w_3$ have both period $p''$.
% and hence $|v_{2i+2}| \ge p+p'-\gcd(p,p')$ (this is folklore, and follows from basic
% facts in number theory, such as $q\cdot q' \ge q + q' - 1$ for all $q,q'\in\bbN$).
% By applying Theorem~\ref{thm:fine-wilf} we obtain:
% \begin{enumerate}
%   \setcounter{enumi}{4}
%   \item $w_5 ~=~ v_{2i+2} ~ \outb{\rho[\ell_{2i+2},\ell_{2i+3}]} ~ v_{2i+3}$
%         has period $p''$.
%% anca: $w_5=w_3$
% \end{enumerate}

Applying once more Theorem~\ref{thm:fine-wilf} to $w_3$ and $w_4$ with
$v_{2i+2}$ as common factor, yields period $p''$ for the word
\[
w_5 ~=~ \outb{\rho[\ell_0,\ell_{2i+2}]} ~ v_{2i+2} ~
\outb{\rho[\ell_{2i+2},\ell_{2i+3}]} ~ v_{2i+3}
\]
% In a similar way, from (4) and (5), using again $v_{2i+2}$ as common factor of $w_4$ and $w_5$,
% we derive
% \begin{enumerate}
%   \setcounter{enumi}{4}
%   \item $w_5 ~=~ \outb{\rho[\ell_0,\ell_{2i+2}]} ~ v_{2i+2} ~
%                  \outb{\rho[\ell_{2i+2},\ell_{2i+3}]} ~ v_{2i+3}$
%         has period $p''$.
% \end{enumerate}

Finally, the periodicity is not affected when we remove
factors of length multiple than the period. In particular,
by removing the factor $v_{2i+2}$ from $w_5$,
we obtain the desired word
$\outb{\rho[\ell_0,\ell_{2i+3}]} ~ v_{2i+3}$, whose period
$p''$ divides $p_{2i+3}$. This proves the claim for the inductive step,
and completes the proof of the proposition.
\end{proof}

\medskip
The $\simeq$-classes considered so far cannot be directly used to
define the blocks in  the desired decomposition of $\rho$, since the $x$-coordinates of their
endpoints might not be in the appropriate order. The next definition
takes care of this, by enlarging the $\simeq$-classes according to
$x$-coordinates of the anchor points in the equivalence class.

\bigskip\noindent
\begin{minipage}[l]{\textwidth-5.8cm}
\begin{defi}\label{def:bounding-box-sweeping}
Consider a non-singleton $\simeq$-equivalence class $K=[\ell,\ell']$.
Let $\an{K}$
be the restriction of $K$ to the anchor points occurring in some inversion,
and $X_{\an{K}} = \{x \::\: \exists y\: (x,y)\in \an{K}\}$
be the projection of $\an{K}$ on positions.
We define $\block{K}=[\tilde\ell,\tilde\ell']$, where
\begin{itemize}
\item $\tilde\ell$ is the latest location $(\tilde x,\tilde y) \leqtime \ell$
such that $\tilde x = \min(X_{\an{K}})$,
\item $\tilde\ell'$ is the earliest location $(\tilde x,\tilde y) \geqtime \ell'$
such that $\tilde x = \max(X_{\an{K}})$
\end{itemize}
(note that the locations $\tilde\ell,\tilde\ell'$ exist since $\ell,\ell'$
are anchor points in some inversion).
\end{defi}
\end{minipage}
\begin{minipage}[r]{5.7cm}
\input{block-construction-sweeping}
\end{minipage}

\smallskip

\begin{lem}\label{lem:bounding-box-sweeping}
If $K$ is a non-singleton $\simeq$-equivalence class,
then $\rho|\block{K}$ is a $\bound$-block.
\end{lem}

\begin{proof}
Consider a non-singleton $\simeq$-class $K=[\ell,\ell']$ and let $\an{K}$, $X_{\an{K}}$, and
be as in Definition \ref{def:bounding-box-sweeping}.
The reader can refer to Figure \ref{fig:block-construction-sweeping}
to quickly recall the notation.
We need to verify that $\rho[\tilde\ell,\tilde\ell']$ is a $\bound$-block
(cf.~Definition \ref{def:factors-sweeping}), namely, that:
\begin{itemize}
\item $\tilde\ell=(\tilde x,\tilde y)$, $\tilde\ell'=(\tilde x',\tilde y')$,
with $\tilde x \le \tilde x'$,
%  \item $y_1$ and $y_2$ are even,
\item the output produced by $\rho[\tilde\ell,\tilde\ell']$
is almost periodic with bound $2\bound$,
\item the output produced by the subsequence $\rho|Z$,
where $Z=[\tilde\ell,\tilde\ell'] ~\setminus~
\big([\tilde x,\tilde x']\times[\tilde y,\tilde y']\big)$,
has length at most $2\hmax\bound$.
\end{itemize}
The first condition $\tilde x \le \tilde x'$ follows immediately from
the definition of $\tilde x$ and $\tilde x'$ as $\min(X_{\an{K}})$
and $\max(X_{\an{K}})$, respectively.

Next, we prove that the output produced by the factor
$\rho[\tilde\ell,\tilde\ell']$ is almost periodic with bound $2\bound$.
By Definition \ref{def:bounding-box-sweeping}, we have
$\tilde\ell \leqtime \ell \lesstime \ell' \leqtime \tilde\ell'$,
and by Lemma \ref{lem:overlapping} we know that $\out{\rho[\ell,\ell']}$
is periodic with period at most $\bound$ ($\le 2\bound$). So it suffices to show that
the lengths of the words $\out{\rho[\tilde\ell,\ell]}$ and
$\out{\rho[\ell',\tilde\ell']}$ are at most $2\bound$.
We shall focus on the former word, as the arguments for
the latter are similar.

First, we note that the factor $\rho[\tilde\ell,\ell]$
lies entirely to the right of position $\tilde x$, and
in particular, it starts at an even level $\tilde y$. This follows
from the definition of $\tilde\ell$, and whether $\ell$ itself is at
an odd/even level. In particular, the location $\ell$ is either at the same level as $\tilde\ell$,
or just one level above.
% Indeed, if this were not the case, there would exist another location
% $\ell''=(\tilde x,\tilde y + 1)$, on the same position as $\tilde\ell$,
% but at a higher level, such that $\tilde\ell \lesstime \ell'' \leqtime \ell$.
% But this would contradict Definition \ref{def:bounding-box-sweeping}.

Now, suppose, by way of contradiction, that $|\out{\rho[\tilde\ell,\ell]}| > 2\bound$.
We head towards a contradiction by finding a location $\ell'' \lesstime \ell$
that is $\simeq$-equivalent to the first location $\ell$ of the $\simeq$-equivalence
class $K$. % Since the factor $\rho[\tilde\ell,\ell]$ lies entirely to the right of
% position $\tilde x$,
Since the location $\ell$ is either at the same level as $\tilde\ell$,
or just above it, %  (otherwise, since the transducer $\cT$ is sweeping, the factor
% $\rho[\tilde\ell,\ell]$ would visit a position to the left of $\tilde x$).
% This means that
the factor $\rho[\tilde\ell,\ell]$ is of the form $\alpha\,\beta$,
where $\alpha$ is rightward factor lying on the same level as $\tilde\ell$
and $\beta$ is either empty or a leftward factor on the next level.
Moreover, since $|\out{\rho[\tilde\ell,\ell]}| > 2\bound$, we know that
either $|\out{\alpha}| > \bound$ or $|\out{\beta}| > \bound$.
Thus,  Lemma \ref{lem:output-minimal-sweeping}
says that one of the two factors $\alpha,\beta$ is not output-minimal.
In particular, there is a loop $L_1$, strictly to the right of $\tilde x$,
that intercepts a subfactor $\gamma$ of $\rho[\tilde\ell,\ell]$,
with $\out{\gamma}$ non-empty and output-minimal.

Let $\ell''$ be the first location of the factor $\gamma$.
%\anca{tried to write it lighter...}
Clearly, $\ell''$ is an anchor point of $L$ and $\out{\tr{\ell''}}\neq\emptystr$.
Further recall that $\tilde x=\min(X_{\an{K}})$ is the leftmost position of
locations in the class $K=[\ell,\ell']$ that are also anchor points of inversions.
In particular, there is a loop $L_2$ with some anchor point
$\ell''_2=(\tilde x,y''_2)\in \an{K}$, and such that $\tr{\ell''}$ is
non-empty and output-minimal.
% an inversion $(L_1,\ell''_1,L_2,\ell''_2)$ such that
% and $\ell''_2=(\tilde x,y''_2)\in K$.
Since $\ell'' \lesstime \ell \leqtime \ell''_2$
and the position of $\ell''$ is to the right of the position of $\ell''_2$,
we know that $(L_1,\ell'',L_2,\ell''_2)$ is also an inversion,
and hence $\ell'' \simeq \ell''_2 \simeq \ell$.
But since $\ell'' \lesstime \ell$, we get a contradiction with the
assumption that $\ell$ is the first location of a $\simeq$-class.
In this way we have shown that $|\out{\rho[\ell_1,\ell]}| \le 2\bound$.

It remains to show that the output produced
by the subsequence $\rho|Z$, where
$Z=[\tilde\ell,\tilde\ell'] ~\setminus~ \big([\tilde x,\tilde x']\times[\tilde y,\tilde y']\big)$,
has length at most $2\hmax\bound$.
For this it suffices to prove that
$|\out{\alpha}| \le \bound$ for every factor $\alpha$ of
$\rho[\tilde\ell, \tilde\ell']$ that lies
at a single level and either to the left of $\tilde x$ or to the right of $\tilde x'$.
%intercepted by $[0,\tilde x]$ or by $[\tilde x',\omega]$.
By symmetry, we consider only one of the two types of factors.
Suppose, by way of contradiction, that there is a factor $\alpha$
at level $y''$, to the left of $\tilde x$,
%intercepted by $[0,\tilde x]$ and
and such that $|\out{\alpha}| > \bound$.
By Lemma \ref{lem:output-minimal-sweeping} we know that
$\alpha$ is not output-minimal, so there is some loop
$L_2$ strictly to the left of $\tilde x$ that intercepts an
output-minimal subfactor
$\beta$ of $\alpha$ with non-empty output.
Let $\ell''$ be the first location of $\beta$. We know that
$\tilde\ell \lesstime \ell'' \leqtime \tilde\ell'$. Since the level
$\tilde y$ is even, this means that the level of $\ell''$ is strictly
greater than $\tilde y$. Since we also know that $\ell$
is an anchor point of some inversion, we can take a suitable loop $L_1$
with anchor point $\ell$ and obtain that $(L_1,\ell,L_2,\ell'')$ is an
inversion, so $\ell'' \simeq \ell$. But
this contradicts the fact that $\tilde x$ is the leftmost position of
% \anca{I changed the last paragraph, because it did not make sense (to me). Please check.}
% \gabriele{It looks good now!}
% By following the same line of reasoning as before,
% %from the fact that $\ell$ is the first location of the non-singleton class $K$,
% we know that there exists a loop $L_2$ with some anchor point
% $\ell''_2=(\tilde x,y''_2) \in \an{K}$.
% % derive the existence of an inversion $(L_1,\ell''_1,L_2,\ell''_2)$,
% % with $\ell''_2=(\tilde x,y''_2) \in K$.
% This shows that $(L,\ell'',L_2,\ell''_2)$ is also an inversion.
% But since $\ell'' \neq \ell$, this contradicts the fact that $\ell$ is
% the first location of the class $K$.
We thus conclude that $|\out{\alpha}| \le \bound$, and this
completes the proof that $\rho|\block{K}$ is a $\bound$-block.
\begin{comment}
We now prove that the output produce by the subsequence $\rho\mid Z$, where
$Z=[\ell_1,\ell_2]\setminus[x_1,x_2]\times[y_1,y_2]$, has length at most
$2 (y_2 - y_1)\cdot \bound \leq \hmax \bound $.

Suppose, by way of contradiction, that this is not the case, and
that $\big|\out{\rho\mid Z}\big| > 2(y_2 - y_1) \cdot \bound$.
Since the set $Z$ spans across at most $y_2 - y_1$ levels and does not cover
the locations inside the ``bounding box'' $[x_1,x_2]\times[y_1,y_2]$,
we could find a factor $\alpha$ that produces an output longer than $\bound$,
that lies on a single level $y'$, and either to the left of $x_1$ or to the
right of $x_2$.

Suppose that this output is on the left (the right case is symmetric), and that $\alpha$ is a factor
on some level $y'\in\{y_1+1,\ldots,y_2\}$ that is intercepted by the interval
$I=[1,x_1]$ and that produces an output of length strictly greater than $\bound$.
By the contrapositive of Lemma \ref{lemma:simple-loop}, the factor $\alpha$
is captured by some loop $L'=[x'_1,x'_2]$ that is {\sl strongly contained} in
$I=[1,x_1]$, namely, such that $1\le x'_1<x'_2<x_1$, and such that the output of $L'$ at level $y'$ is non-empty.
Let $\ell'=(x',y')$ be the anchor point of $L'$, where $x'=x'_1$ or $x'=x'_2$
depending on whether $y'$ is odd or even. Recall that, by the definition of $[K]$,
there is also a location $\ell=(x,y)$ that strictly precedes $\ell'$ along the
run and that belongs to $H$. This implies that $\ell$ is an, anchor point of some loop $L$.
Moreover, recall that $x'_1\le x'\le x'_2 < x_1$ and $x_1\le x\le x_2$, namely,
$\ell'$ is {\sl strictly to the left} of $\ell$ according to the ordering of
the $x$-coordinates. This shows that $(L,\ell,L',\ell')$ is also an inversion, and
hence $\ell'$ also belongs to $H$.
However, this contradicts the definition of $x_1$ as the minimum of the
$x$-coordinates of the locations in $H$.
A similar contradiction can be obtained in the case where the factor that produces an
output of length strictly greater than $ \bound$ lies at the right of $x_2$.

By the above arguments, we know that $\big|\out{\rho\mid Z}| \le 2 (y_2 - y_1)\cdot \bound \leq \hmax \bound$,
where $Z=[\ell_1,\ell_2]\setminus[x_1,x_2]\times[y_1,y_2]$, namely, that the second
condition of the definition of block is satisfied.

It remains to verify the first condition, that the output produced by
$\rho[\ell_1,\ell_2]$ is almost periodic with bound $2 \cdot \bound$.
Let $\ell'_1$ and $\ell'_2$ be the first and the last locations of the
$\simeq$-equivalence class $K$ (note that $\ell_1\le \ell'_1\le \ell'_2\le\ell_2$).
Recall that Lemma \ref{lem:overlapping} already shows that the output produced between
$\ell'_1$ and $\ell'_2$ is periodic with period at most $\bound$.
Thus, we just need to show that the prefix $\out{\rho[\ell_1,\ell'_1]}$ and
the suffix $\out{\rho[\ell'_2,\ell_2]}$ have length at most $2 \cdot \bound$.

Suppose that the length of $\out{\rho[\ell_1,\ell'_1]}$ exceeds $ 2 \cdot \bound$.
By the definition of $[K]$, the two locations $\ell_1$ and $\ell'_1$ would be either
on the same level, i.e.~$y_1$, or on adjacent levels, i.e.~$y_1$ and $y_1+1$.
In the following, we show that none of these cases can happen, thus reaching
a contradiction from the assumption $\big|\out{\rho[\ell_1,\ell'_1]}\big| > 2 \cdot \bound$.
If $\ell_1$ were on the same level as $\ell'_1$, then clearly the factor
$\out{\rho[\ell_1,\ell'_1]}$ would lie on a single level and to the right
of $x_1$, and would produce an output longer than $\bound$.
Then, by using the contrapositive of Lemma \ref{lemma:simple-loop}, we could
find a loop $L'=[x'_1,x'_2]$ strongly contained in the interval $I=[x_1,n]$,
where $n$ is the rightmost position of the input, that captures the factor
$\out{\rho[\ell_1,\ell'_1]}$ with non-empty output.
We recall that $\ell'_1$ is the first location of the $\simeq$-equivalence
class $K$, and hence there is an inversion $(L'_1,\ell'_1,L'',\ell'')$, for some
location $\ell''$ that follows $\ell'_1$ along the run. We then define
$\ell=(x'_1,y_1)$ and we observe that this location is an anchor point
of $L'$ and it strictly precedes $\ell''$.
We thus get that $(L',\ell,L'',\ell'')$ is also an inversion. This, however,
is a contradiction because the inversion $(\ell,\ell'')$ intersects
the $\simeq$-equivalence class $K$, without being contained in it.
Let us now consider the second case, where $\ell_1$ is on level $y_1$ and
$\ell'_1$ is on level $y_1+1$.
Since $\rho[\ell_1,\ell'_1]$ spans across two levels and produces an
output longer than $ 2 \bound$, there is a factor
$\alpha$ of $\out{\rho[\ell_1,\ell'_1]}$ that lies entirely on a single
level -- either $y_1$ or $y_1+1$ -- and to the right of $x_1$, and
produces an output longer than $\bound$.
Then, by reasoning as in the previous case, we can get a contradiction
by finding an inversion $(L,\ell,L'',\ell'')$ that intersects $K$ without
being contained in it.

We have just shown that $\big|\out{\rho[\ell_1,\ell'_1]}\big| \le 2 \cdot \bound$.
By using symmetric arguments, we can also prove that
$\big|\out{\rho[\ell'_2,\ell_2]}\big| \le 2 \cdot \bound$.
Finally, we recall that, by Lemma \ref{lem:overlapping}, the period of
$\out{\rho[\ell'_1,\ell'_2]}$ is smaller than $ \bound$.
All together, this shows that the output produced between the
locations $\ell_1$ and $\ell_2$ is almost periodic with bound
$2 \cdot \bound$ and hence $[K]=(\ell_1,\ell_2)$ is a block.
\end{comment}
\end{proof}

The next lemma shows that blocks do not overlap along the input axis:

\begin{lem}\label{lem:consecutive-blocks-sweeping}
Suppose that $K_1$ and $K_2$ are two different non-singleton $\simeq$-classes
such that $\ell \lesstime \ell'$ for all $\ell \in K_1$ and $\ell' \in K_2$.
Let $\block{K_1}=[\ell_1,\ell_2]$ and $\block{K_2}=[\ell_3,\ell_4]$,
with $\ell_2=(x_2,y_2)$ and $\ell_3=(x_3,y_3)$.
Then $x_2 < x_3$.
\end{lem}

\begin{proof}
Suppose by contradiction that $K_1$ and $K_2$ are as in the
statement, but $x_2 \ge x_3$.
By Definition \ref{def:bounding-box-sweeping},
$x_2=\max(X_{\an{K_1}})$ and $x_3=\min(X_{\an{K_2}})$.
This implies the existence of some inversions
$(L,\ell,L',\ell')$ and $(L'',\ell'',L''',\ell''')$
such that $\ell=(x_2,y)$ and $\ell'''=(x_3,y''')$.
Moreover, since $\ell \leqtime \ell'''$ and $x_2 \ge x_3$,
we know that $(L,\ell,L''',\ell''')$ is also an inversion,
thus implying that $K_1=K_2$.
\end{proof}

For the sake of brevity, we call \emph{$\simeq$-block} any
factor of the form $\rho|\block{K}$ that is obtained by applying
Definition~\ref{def:bounding-box-sweeping} to a non-singleton $\simeq$-class $K$.
The results obtained so far imply that every location covered by an
inversion is also covered by an $\simeq$-block (Lemma \ref{lem:bounding-box-sweeping}),
and that the order of occurrence of $\simeq$-blocks is the same as the order of positions
(Lemma \ref{lem:consecutive-blocks-sweeping}).
So the $\simeq$-blocks can be used as factors for the $\bound$-decomposition
of $\rho$ we are looking for. Below, we show that the remaining
factors of $\rho$, which do not overlap the $\simeq$-blocks, are $\bound$-diagonals.
This will complete the construction of a $\bound$-decomposition of $\rho$.

Formally, we say that a factor $\rho[\ell,\ell']$
\emph{overlaps} another factor $\rho[\ell'',\ell''']$ if
$[\ell,\ell'] \:\cap\: [\ell'',\ell'''] \neq \emptyset$,
$\ell' \neq \ell''$, and $\ell \neq \ell'''$.

\begin{lem}\label{lem:diagonal-sweeping}
Let $\rho[\ell,\ell']$ be a %maximal
factor of $\rho$,
with $\ell=(x,y)$, $\ell'=(x',y')$, and $x\le x'$,
that does not overlap any $\simeq$-block.
Then $\rho[\ell,\ell']$ is a $\bound$-diagonal.
\end{lem}

\begin{proof}
Consider a factor $\rho[\ell,\ell']$, with $\ell=(x,y)$, $\ell'=(x',y')$,
and $x\le x'$, that does not overlap any $\simeq$-block.
We will focus on locations $\ell''$ with $\ell \leqtime \ell''
\leqtime \ell'$
% \anca{anchor points exist only because of loops, but loops were not
% mentioned at all here - I rephrased}
% that occur between $\ell$ and $\ell'$
% and
that are anchor points of some loop with $\out{\tr{\ell''}}\neq\emptystr$.
We denote by $A$ the set of all such locations.
%For all $y''\in\{y,\dots,y'\}$, we define $A_{y''}$ to be the restriction of $A$ to
%locations at level $y''$.

First, we show that the locations in $A$ are monotonic
\reviewOne[inline]{Monotonic$\to$Monotonous?
\olivier[inline]{we keep monotonic}%
w.r.t.~the position order. Formally,
we prove that for all $\ell_1,\ell_2\in A$, if $\ell_1=(x_1,y_1) \leqtime \ell_2=(x_2,y_2)$, then
$x_1 \le x_2$. Suppose that this were not the case, namely, that $A$ contained two anchor points
$\ell_1=(x_1,y_1)$ and $\ell_2=(x_2,y_2)$ with $\ell_1 \lesstime \ell_2$ and $x_1 > x_2$.
Let $L_1,L_2$ be the loops of $\ell_1,\ell_2$, respectively, and recall that
$\out{\tr{\ell_1}},\out{\tr{\ell_2}}\neq\emptystr$. This means that $(L_1,\ell_1,L_2,\ell_2)$
is an inversion, and hence $\ell_1 \simeq \ell_2$. But this contradicts the hypothesis that
$\rho[\ell,\ell']$ does not overlap any $\simeq$-block.
%Using similar arguments, one can prove that $A$ contains at most one anchor point at each {\sl odd}
%level (indeed, every two anchor points at the same odd level are $\simeq$-equivalence, and hence
%their existence would be against the hypothesis that $\rho[\ell,\ell']$ does not overlap any

Next, we identify the floors of our diagonal. Let $y_0,y_1,\dots,y_{n-1}$ be all the {\sl even}
levels that have locations in $A$. For each $i=0,\dots,n-1$, let $\ell_{2i+1}$ (resp.~$\ell_{2i+2}$)
be the first (resp.~last) anchor point of $A$ at level $y_i$. Further let $\ell_0=\ell$ and $\ell_{2n+1}=\ell'$.
Clearly, each factor $\rho[\ell_{2i+1},\ell_{2i+2}]$ is a floor. Moreover, thanks to the previous
arguments, each location $\ell_{2i}$ is to the left of the location $\ell_{2i+1}$.

It remains to prove that each factor $\rho[\ell_{2i},\ell_{2i+1}]$ produces an
output of length at most $2\hmax\bound$. By construction, $A$ contains no anchor
point at an even level and strictly between $\ell_{2i}$ and $\ell_{2i+1}$.
By Lemma \ref{lem:output-minimal-sweeping} this means that the outputs produced
by subfactors of $\rho[\ell_{2i},\ell_{2i+1}]$ that lie entirely at an {\sl even}
level have length at most $\bound$.
Let us now consider the subfactors $\alpha$ of $\rho[\ell_{2i},\ell_{2i+1}]$
that lie entirely at an {\sl odd} level, and let us prove that they produce outputs
of length at most $2\bound$. Suppose that this is not the case, namely, that
$|\out{\alpha}| > 2\bound$. In this case we show that an inversion
would exist at this level. Formally, we can find two locations $\ell'' \lesstime \ell'''$
in $\alpha$ such that the prefix of $\alpha$ that ends at location $\ell''$ and the suffix
of $\alpha$ that starts at location $\ell'''$ produce outputs of
length greater than $\bound$.
By Lemma \ref{lem:output-minimal-sweeping},
those two factors would not be output-minimal,
and hence $\alpha$ would contain disjoint loops $L_1,L_2$ with anchor points $\ell''_1,\ell''_2$
forming an inversion $(L_1,\ell''_1,L_2,\ell''_2)$. But this would imply that $\ell''_1,\ell''_2$
belong to the same non-singleton $\simeq$-equivalence class, which contradicts the hypothesis
that $\rho[\ell,\ell']$ does not overlap any $\simeq$-block.
We must conclude that the subfactors of $\rho[\ell_{2i},\ell_{2i+1}]$
produce outputs of length at most $2\bound$.
%\gabriele{This needs to be explained in a better way.}
%Similarly, from the previous arguments, we know that $A$ contains at most
%one location at each odd level and thus, by Lemma \ref{lem:output-minimal-sweeping},
%the outputs produced by subfactors of $\rho[\ell_{2i},\ell_{2i+1}]$ that lie
%entirely at an odd level have length at most $2\bound$.

Overall, this shows that the output produced by each factor $\rho[\ell_{2i},\ell_{2i+1}]$
has length at most $2\hmax\bound$.
%First, recall that by definition of $[K_1]$ and $[K_2]$, $y_1$ and $y_2$ are even,
%and there is no inversion involving a location $\ell$ such that $\ell_1 \leqtime \ell \leqtime \ell_2$.
%As there is no loops $L_1,L_2$ yielding to an inversion $(L_1,\ell_1,L_2,\ell_2)$, we focus on the anchor points of loops between
%those two locations. For any $y$ such that $y_1 \leq y \leq y_2$ we introduce the set
%$A_y = \{ (x,y) \ | \ \ell_1 \leqtime (x,y) \leqtime \ell_2 \text{ and } \exists L  \ (x,y) = \an{L} \}$, the set
%of anchor points at level $y$, between $\ell_1$ and $\ell_2$. We also define $A = \cup _{y} A_y $.
%As there is no loops $L_1,L_2$ creating an inversion $(L_1,\ell_1,L_2,\ell_2)$, we know that the locations of $A$
%are ordered along a diagonal: if $ (x,y) \leqtime (x',y') \in A$, then $x \leq x'$. As $\ell_1$
%and $\ell_2$ are the first and last location of a $\simeq$-block, we know that if $(x,y) \in A$,
%then $x_1 \leq x \leq x_2$, otherwise we would have an inversion whose locations
%would be $(x,y)$ and one in the $\simeq$-blocks.
%Moreoeachver, for the same reason, if $y$ is odd, then $A_y$ is at most a singleton (otherwise we would have
%an inversion between  two of the anchor points of $A_y$). We also know, by definition, that if $y$ is even,
%$\rho[\min{A_y}, \max{A_y}]$ is a floor. Thus it remains to bound the output between such floors to obtain
%a diagonal. Let us consider $ A_y$ and $A_{y'}$ that are non-empty, such that for all $y<y''<y'$, $A_{y''}$ is empty.
%and $\ell = \max{A_y}$ and $\ell ' = \min{A_{y'}}$. As there is no producing loop on the even levels
%between $y$ and $y'$, the output on those levels is smaller than $\bound$. Also, as there is at most one loop
%on the odd levels between $y$ and $y'$, the output on those levels is smaller than $3 \bound$. Thus,
%$\rho[\ell,\ell '] < 2(y' -y) \bound < 2 \hmax \bound $, and $rho[\ell_1, \ell_2]$ is indeed a diagonal.
\end{proof}

\begin{comment}
LICS proof for the 2-way case
\begin{proof}
% Let $\ell_i=(x_i,y_i)$ for both $i=1,2$, and
Suppose by contradiction that there is some $x\in[x_1,x_2]$
such that, for all locations $\ell=(x,y)$ between $\ell_1$ and $\ell_2$,
one of the following conditions holds:
\begin{enumerate}
\item $|\out{\rho\mid Z_\ell^\upperleft}| > \bound$,
where $Z_\ell^\upperleft = [\ell,\ell_2] \:\cap\: \big([0,x]\times\bbN\big)$,
\item $|\out{\rho\mid Z_\ell^\lowerright}| > \bound$,
where $Z_\ell^\lowerright = [\ell_1,\ell] \:\cap\: \big([x,\omega]\times\bbN\big)$.
\end{enumerate}
We claim first that for each condition above
there is some level $y$ at which it holds. Observe that for the
highest location $\ell$ of the run at position $x$, the set
$Z_\ell^\upperleft$ is empty, since the outgoing transition at $\ell$
is rightward. So condition 1 is trivially violated at $\ell$ as above, hence
condition 2 holds by the initial assumption. Symmetrically, condition
1 holds at the lowest location  of the run at position $x$.
% Assume for instance that there is no level $y$ such that condition 2 holds at $(x,y)$.
% This means that condition 1 holds at every level, including the highest
% location $\ell$ of the run at position $x$.
% This is impossible since $Z_\ell^\upperleft$ is empty
% and condition 1 entails $|\out{\rho\mid Z_\ell^\upperleft}| > \bound$.
% The case is symmetric if we assume that condition 1 never holds.
Let us now compare, for each condition, the levels where it holds.

Clearly, the lower the level of the location $\ell$,
the easier it is to satisfy condition 1, and symmetrically for condition 2.
So, let $\ell=(x,y)$ (resp.~$\ell'=(x,y')$) be the highest (resp.~lowest)
location at position $x$ that satisfies condition 1 (resp.~condition 2).

We claim that $y \ge y'$.
For this, we first observe that $y \ge y'-1$, since otherwise there would
exist a location $\ell=(x,y'')$, with $y < y'' < y'$, violating both conditions 1 and 2.
Moreover, $y$ must be odd, otherwise the transition departing from $\ell=(x,y)$
would be rightward oriented and the location $\ell''=(x,y+1)$ would still
satisfy condition 1, contradicting the fact that $\ell=(x,y)$ was chosen to
be the highest location.
For similar reasons, $y'$ must also be odd, otherwise there would be
a location $\ell''=(x,y'-1)$ that precedes $\ell'$ and satisfies condition 2.
But since $y \ge y'-1$ and both $y$ and $y'$ are odd, we need to have $y\ge y'$.

From the previous arguments we know that in fact $\ell=(x,y)$ satisfies both conditions
1 and 2. We can thus apply Theorem \ref{thm:simon2} to the sets
$Z_\ell^\lowerright$ and $Z_\ell^\upperleft$, deriving the existence of
two idempotent loops $L_1,L_2$ and two components $C_1,C_2$ of $L_1,L_2$,
respectively, such that
\begin{itemize}
\item $\max(L_2) < x < \min(L_1)$,
\item $\ell_1 \lesstime \an{C_1} \lesstime \ell \lesstime \an{C_2} \lesstime \ell_2$,
\item $\out{\tr{C_1}},\out{\tr{C_2}}\neq\emptystr$.
\end{itemize}
In particular, since $\an{C_1}$ is to the right of $\an{C_2}$ w.r.t.~the order
of positions, we know that $(L_1,C_1,L_2,C_2)$ is an inversion, and hence
$\an{C_1} \simeq \an{C_2}$. But this contradicts the assumption that
$\rho[\ell_1,\ell_2]$ does not overlap with any $\simeq$-block.
\end{proof}
\end{comment}

\begin{comment}
We consider the locations
that are not strictly covered by $\simeq$-blocks, formally, the
set $B = \{ \ell \:\mid\: \nexists\:(\ell_1,\ell_2)\text{ $\simeq$-block s.t.}~\ell_1<\ell<\ell_2\}$.
We equip $B$ with the natural ordering of locations induced by $\rho$.

We now consider some maximal convex subset $C$ of $B$.
Note that the left/right endpoint of $C$ coincides with the first/last
location of the run $\rho$ or with the right/left endpoint of some $\simeq$-block.
Below, we show how to decompose the subrun $\rho\mid C$ into a series of diagonals
and blocks. After this, we will be able to get a full decomposition of $\rho$ by
interleaving the $\simeq$- blocks that we defined above with the diagonals
and the  blocks that decompose each subrun $\rho\mid C$.

Let $D_C$ be the set of locations $\ell=(x,y)$ of $C$ such that
there is some loop $L=[x,x']$, with $x'\ge x$, whose trace at level $y$
lies entirely inside $C$ and
produces non-empty output.
We remark that the set $D_C$ may be non-empty. To see this, one can
imagine the existence of two consecutive $\simeq$- blocks (e.g.~$R_1$
and $R_2$ in Figure~\ref{fig:decomposition}) and a loop between them
that produces non-empty output (e.g.~the factor $F_2$). In a more
general scenario, one can find several loops between two consecutive
$\simeq$- blocks that span across different levels.
%\anca{how can it happen that such a loop exists? if the intercepted
%  factor lies within $C$, then some locations in $C$ are covered by
%  inversions - this is not possible with the definition of $C$. In
%  fact, I don't understand what is the shape of $C$  - does it
%  correspond to some degenerate case due to even levels? if so, it
%  should be stated.}
%\gabriele{To understand this, it is better to refer to Figure 1 (an example of decomposition). The boxes represent the  blocks $[K]$. In between these
%boxes we can still have loops, in fact several and on possibly different levels.
%The idea of what follows is essentially to show that these loops are arranged
%at even levels and as in a series of stairs, from lower left to upper right,
%which is still compatible with a one-way mechanism.
%If this were not the case, then we would indeed get a contradiction
%with the existence of an inversion.}
We can observe however that all the locations in $D_C$ are on even levels.
Indeed, if this were not the case for some $\ell=(x,y) \in D_C$, % (hence with $y$ odd),
%\felix{added that $ y $ is odd, but i didn't want to replace all the occurrences by $2p+1$, that seemed heavy}
then we could select a minimal loop $L=[x_1,x_2]$ such that $x_1\le x\le x_2$
and $\out{\tr{\ell}} \neq \varepsilon$. Since $y$ is odd,
$\ell_1=(x_2,y)$  and $ \ell_2=(x_1,y)$ are anchor points of $L$, and hence $(\ell_1,\ell_2)$ is an inversion.
%Since $\ell_1\le\ell\le\ell_2$ and since inversions are covered by
%$\simeq$-blocks, there is a $\simeq$-block that contains $\ell$,
%which contradicts the fact that $ \ell \in D_C \subseteq C$.
Since $\ell_1\le\ell\le\ell_2$ and all inversions are covered by
$\simeq$-blocks, there is a $\simeq$-block $(\ell'_1,\ell'_2)$ such
that $\ell'_1\le\ell\le\ell'_2$.
However, as $\ell'_1$ and $\ell'_2$ are at even levels,
$\ell$ must be different from these two locations, and
this would contradict the definition of $D_C$.
Using similar arguments, one can also show that the locations in $D_C$ are
arranged along a ``rising diagonal'', from lower left to upper right.
%\gabriele{I don't know. If you have energy you can detail this. The problem is that we star lacking space,
%          and still I would like to have something in the body, not everything in the appendix.}
%\felix{you're right, and it's actually very simple once you know they are on even levels, and thus entry points are the same for the sweeping and the one way}

The above properties suggest that the locations in $D_C$ identify some
diagonals and  blocks that form a decomposition of $\rho\mid C$.
The following lemma shows that this is indeed the case, namely, that
any two consecutive locations in $D_C$ form a diagonal or a block.

\begin{lem}\label{lemma:ladder}
Let $\ell_1=(x_1,y_1)$ and $\ell_2=(x_2,y_2)$ be two consecutive locations of $D_C$.
Then, $x_1\le x_2$ and $y_1\le y_2$ and the pair $(\ell_1,\ell_2)$ is a diagonal
or a block, depending on whether $y_1=y_2$ or $y_1<y_2$.
%\felix{you can leave the proof that $y_i$ are even to the appendix, i can do it in the proof of the lemma.}
%\gabriele{This is proved in a short way above}
\end{lem}
\begin{proof}
Recall that all the locations in $D_C$ are on even levels, so the lemma holds in particular for $\ell_1$ and $\ell_2$
If $y_1=y_2$, then $(\ell_1,\ell_2)$ is clearly a floor.
So let us assume that $y_1 \neq y_1$.
The fact that $x_1\le x_2$ and $y_1 < y_2$ holds follows from the arguments
given in part of the body that just preceded the lemma.
The first three conditions of the definition of blockare also satisfied because
$\ell_1 $ and $\ell_2 $ are consecutive locations in $D_C$.

Below, we verify that the output produced by the factor $\rho[\ell_1,\ell_2]$