
\subsection{Proof of Proposition~\ref{prop:eva-reduc}}

We include here a formal definition of extended VA. An extended VA is a tuple $\bigcal{A} = (Q, \Sigma, \bigcal{X}, q_0, \Delta, F)$ where $Q$ is a finite set of states, $\Sigma$ is the input alphabet, $\bigcal{X}$ is a finite set of variables, $\Delta$ is a set consisting of {\it letter transitions} $(p, a, q)$ where $a\in\Sigma$ and $p,q\in Q$ or {\it extended variable transitions} $(p, S, q)$ where $S\subseteq \{\varop{x} , \varcl{x}\mid x\in\bigcal{X}\}$ and $S$ is nonempty; and $F\subseteq Q$. A run $\rho$ over a document $d = a_1\ldots a_n$ is a sequence
$$
\rho = q_0  \xrightarrow{S_1} p_0 \xrightarrow{a_1} 
q_1  \xrightarrow{S_2} p_1 \xrightarrow{a_2} \cdots 
\xrightarrow{a_n} q_n  \xrightarrow{S_{n+1}} p_n
$$
where each $S_i$ is a possibly empty set of markers, $(p_i, a_{i+1}, q_{i+1})\in \Delta$, and if $S_i$ is nonempty, then $(q_i, S_{i+1}, p_i)\in \Delta$, and if it is, then $p_i = q_i$. We say that a run is accepting if $p_n\in F$. Also, we say that a run $\rho$ is {\it valid} if variables are opened and closed in a correct manner: every marker $\varop{x}$ and $\varcl{x}$ must appear at most once each among the sets $S_1\ldots S_{n+1}$, and if they do, they both appear, and if $\varop{x}\in S_i$ and $\varcl{x}\in S_j$ then it holds that $i\leq j$. For a valid run $\rho$, we define the mapping $\mu^\rho$ that maps $x$ to $\spanc{i}{j}$ iff $\varop{x}\in S_i$ and $\varcl{x}\in S_j$. Lastly, we define the spanner $\sem{A}$ by the function $\sem{\bigcal{A}}(d) = \{\mu^\rho\mid \rho \text{ is an accepting and valid run of $\bigcal{A}$ over $d$}\}$. Like in varable-set automata, we say that $\bigcal{A}$ is sequential if every accepting run of $\bigcal{A}$ is valid. Also, we say that $\bigcal{A}$ is unambiguous if for every document $d$ and $\mu\in\bigcal{A}(d)$, there is only one accepting run $\rho$ of $\bigcal{A}$ over $d$ such that $\mu = \mu^\rho$.

Now let us describe the reduction. Let $\bigcal{A} = (Q, \Sigma, \bigcal{X}, q_0, \Delta, F)$ be an unambiguous sequential extended VA. We build an annotated automaton $\bigcal{A}' = (Q', \Sigma\cup\{\texttt{\#}\}, \Omega, \Delta', q_0, F')$ as follows.  Let $Q' = Q \cup \{q^*\}$ for some fresh state $q^*$, and let $F' = \{q^*\}$. Let $\Omega = 2^{\{\varop{x} , \varcl{x}\mid x\in\bigcal{X}\}}$ and let $\Delta' = \{(p,a,q)\mid a\in \Sigma\text{ and }(p,a,q)\in\Delta\} \cup \{(p,(a, S), q)\mid (p,S,q'),(q',a,q)\in\Delta \text{ for some }q'\in Q\} \cup \{(p,\texttt{\#}, q^*)\mid p\in F\} \cup \{(p,(\texttt{\#}, S), q^*)\mid (p,S,q)\in\Delta\text{ for some }q\in F\}$.

To see the equivalence between $\bigcal{A}$ and $\bigcal{A}'$, let $d = a_1\ldots a_n$ be a document over $\Sigma$, and let $\rho$ be an accepting run of $\bigcal{A}$ over $d$:
$$
\rho = q_0  \xrightarrow{S_1} p_0 \xrightarrow{a_1} 
q_1  \xrightarrow{S_2} p_1 \xrightarrow{a_2} \cdots 
\xrightarrow{a_n} q_n  \xrightarrow{S_{n+1}} p_n
$$
We define $\rho'$ as the following sequence:
$$
\rho' = q_0  \xrightarrow{b_1} 
q_1  \xrightarrow{b_2} \cdots 
\xrightarrow{b_n} q_n  \xrightarrow{b_{n+1}} q^*
$$
where $b_i  = (a_i, S_i)$ if $S_i$ is nonempty, and $b_i = a_i$ if it is for each $i\in[1, n]$. We define $b_{n+1} = (\texttt{\#}, S_i)$ if $S_i$ is nonempty, and $b_{n+1} = \texttt{\#}$ if it is. Since $\bigcal{A}$ is sequential, $\rho$ is a valid run which defines a mapping $\mu^\rho\in\sem{\bigcal{A}}(d)$. We can straightforwardly check that $\mu^\rho$ is equivalent to $\textsf{ann}(\rho')$.
It can also be seen directly from the construction that $\rho'$ is a run from $\bigcal{A}'$ over $d\texttt{\#}$, and since $\rho'$ is uniquely defined from $\rho$, we conclude that for every document $d$ each $\mu\in\sem{\bigcal{A}}(d)$ is equivalent to some unique $\nu\in\sem{\bigcal{A}'}(d\texttt{\#})$.
 
To see the equivalence on the opposite way, consider an accepting run $\rho'$ of $\bigcal{A}'$ over $d\texttt{\#}$ that is written as above, where each $b_i$ might be either $a_i$ or a pair $(a_i, S)$. From the construction, it can be seen that if $b_i = a_i$, for $i\in[1, n]$, there exists a transition $(q_{i-1},a_i, q_i)\in\Delta$. If $b_i = (a_i, S)$, for $i\in[1, n]$, there exist transitions $(q_{i-1},S, q'),(q',a_i,q_i)\in\Delta$ for some $q'\in Q$. Also, if $b_{n+1} = \texttt{\#}$ that means that $q_n\in F$ and if $b_{n+1} = (\texttt{\#}, S)$ there exists $(q_n,S,q')\in\Delta$ for some $q'\in F$. We define $\rho$ as a run of $\bigcal{A}$ over $d$ based on these transitions, and we note first that this run is accepting and valid, and since $\bigcal{A}$ is unambiguous, $\rho$ must be uniquely defined. For example, when replacing $(q_{i-1}, (a_i, S), q_i)$, we know there exist transitions $(q_{i-1}, S, q')$ and $(q', a_i, q_i)$ in $\Delta$. We also know this $q'$ must be unique, otherwise we could define a different accepting run with that defines the same mapping. We see that $\textsf{ann}(\rho')$ is equivalent to $\mu^\rho$, so we conclude that each annotation $\nu\in\sem{\bigcal{A}}(d)$ is equivalent to some unique mapping $\mu\in\sem{\bigcal{A}}(d)$. We also conclude that $\bigcal{A}'$ is unambiguous, otherwise for two runs $\rho_1'$ and $\rho_2'$ that render the same annotation, and that differ in some $q_i$, we would be able to build runs $\rho_1$ and $\rho_2$ that also differ in some $q_i$ that define the same mapping.

\subsection{Proof of Theorem~\ref{theo-algo-succ}}

For this proof, we will use an extension of Shift-ECSs\xspace called {\it succinct Shift-ECSs\xspace}.
A succinct Shift-ECSs\xspace as a tuple $\tilde{\bigcal{D}} = (\bigcal{S}, V, \mathcal{l}\!, \mathcal{r}, \lambda, \bot, \epsilon)$ as a Shift-ECS\xspace, with the difference that the output set has been replaced by a SERS $\bigcal{S}$. The set of strings associated to a node $v\in \tilde{D}$ is defined as follows: If $\lambda(v) = r\in R$, where $R$ is the set of representations in $\bigcal{S}$, then $\sem{\tilde{D}}(v) = \bigcal{L}(r)\times\{1\}$. The rest of the sets $\sem{\tilde{D}}(v)$ for union, product, and shift nodes $v$ remain unchanged, and so are the notions of duplicate-free, $k$-bounded and $\varepsilon$-safe nodes, along with the operations for $\mathsf{add}$, $\prod$, $\mathsf{union}$ and $\mathsf{shift}$.

\begin{proposition}\label{prop:ds-succ}
	The operations $\prod$, $\mathsf{union}$ and $\mathsf{shift}$ over succinct Shift-ECSs\xspace{} extended with empty- and $\epsilon$-nodes take constant time, and the operation $\mathsf{add}$ with a representation $r$ as argument takes time $O(|r|)$. Furthermore, if we start from an empty succinct Shift-ECS\xspace{} $\bigcal{D}$ and apply $\mathsf{add}$, $\prod$, $\mathsf{union}$, and $\mathsf{shift}$ over $\epsilon$-safe nodes, the resulting node $v'$ is always an $\epsilon$-safe node, and the set $\sem{\bigcal{D}}(v)$ can be enumerated with output-linear delay without preprocessing for every node $v$.
\end{proposition}
\begin{proof}
	For this proof, we need to be a bit more specific regarding the  enumeration algorithm $\bigcal{E}$ of an SERS. Precisely, we assume that $\bigcal{E}$ has an associated function $\texttt{yield}$ and a constant $c$, and its procedure is to receive $r$ and then allow up to $|\bigcal{L}(r)|$ calls to $\texttt{yield}$. Each of these calls produces a different annotation $\oout\in \bigcal{L}(r)$ and takes time $c\cdot (|\oout|+1)$. Each of these annotations carries a flag ${\tt end}$ which is true if, and only if, it is the last output of the set. We also assume that a sequence of $|\bigcal{L}(r)|$ calls to $\texttt{yield}$ might happen again with the same time bounds after the last call set ${\tt end}$ to true.
	
	We start this proof by re-stating that every definition in the Shift-ECS\xspace data structure is unchanged in its succinct version. The only difference is the definition of $\sem{\tilde{\bigcal{D}}}(v)$ for a bottom node $v\in\tilde{\bigcal{D}}$.
	
	First, we shall prove a version of Proposition~\ref{prop:lindelay} in this model, namely, that if a succinct Shift-ECS\xspace $\tilde{\bigcal{D}}$ is duplicate-free and $k$-bounded, then the set $\sem{\tilde{\bigcal{D}}}(v)$ can be enumerated with output-linear delay for every $v\in \bigcal{D}$. We do this by adapting the proof of Proposition~\ref{prop:lindelay} to handle this new type of bottom node. Let $\bigcal{S} = (\bigcal{R}, \Omega, |\cdot |, \bigcal{L}, \bigcal{E})$ be the SERS associated to $\tilde{\bigcal{D}}$ and let $c'$ be the constant associated to $\bigcal{E}$. In a bottom node $v$, the subroutines ${\tt first}(v, s)$, ${\tt next}(v, s)$ and ${\tt curr}(v, s)$ are defined as follows: To call ${\tt first}(v, s)$, we assume that the procedure ${\tt yield}$ from $\bigcal{E}$ has either not been called over $r$, or that the last call over $r$ set its flag ${\tt end}$ to true. 
	The procedure ${\tt first}(v, s)$ then calls ${\tt yield}$ over $r = \lambda(v)$  and obtains an annotation $\oout$ in time $c'(|\oout| + 1)$ and prints $(\oout, s + 1)$ as output. The procedure ${\tt next}(v, s)$ does the same, but it the opposite is assumed. That is, that the last call to ${\tt yield}$ over $r$ did not set ${\tt end}$ to true. Both of these calls store the last annotation $\oout$ locally. Then, the procedure ${\tt curr}(v, s)$ returns $(\oout, s)$ using the $\oout$ that was stored from the last call. Each of these procedures returns ${\tt end}$ if and only if the call to ${\tt yield}$ that was just made (or the previous one in the case of ${\tt curr}$) set its own flag ${\tt end}$ to true. It can be seen now that calling ${\tt first}(v, s)$ and then ${\tt next}(v, s)$ until one of these calls returns ${\tt end}$, then this prints the entire set  $\mathsf{sh}(\sem{\tilde{D}}(v), s) = \bigcal{L}(r)\times\{s + 1\}$ without repetitions. This was the inductive assumption that used to prove correctness of the enumeration algorithm, so it holds.
	
	To show the time bounds, we just bring attention to the fact that the only difference in the algorithm time-wise is the time spent printing each pair $(\oout, i)$, as now this takes  $c'(|\oout| + 1)$. However, this does not affect output-linear delay since, when taking all pairs that belong to an output, the accumulate time is proportional to the total size of it plus its length.
	
	The rest of the proof pertains the operations $\mathsf{add}$, $\prod$, $\mathsf{union}$ and $\mathsf{shift}$, but it is not hard to see that they can be kept unchanged and maintain all the conditions in the statement, with the sole exception of $\mathsf{add}(r)$, which now adds a representation $r$ to the structure and takes $|r|$ time. This concludes the proof. 
\end{proof}

The algorithm that we give to prove the statement is exactly Algorithm~\ref{alg:evaluation} line-by-line, with the sole exception of lines 10-11, which now read: $\textbf{for each }(p,a,\oout, q) \in \Delta$: $M_a[p,q] \gets \mathsf{union}(M_a[p,q],\, \mathsf{add}(\oout))$. The rest of the proof follows from the reasoning of the proof of Theorem~\ref{theo:evaluation}, and by noticing that the definition of the set $\sem{\tilde{D}}(v) = \bigcal{L}(r) \times \{1\}$ satisfies what is expected for an index $M_a[p,q]$. That is, that for every partial run $\rho$ of $\bigcal{T}\!$ over $a$ that starts on $p$ and end on $q$, all annotations from the set $\textsf{ann}(\rho)$ are included. The fact that the operations are done duplicate-free follows from the unambiguous condition over $\bigcal{T}\!$ as well.



\subsection{Proof of Proposition~\ref{prop:va-reduc}}

The SERS that we will consider are Enumerable Compact Sets as they were presented in~\cite{MunozR22}, defined over the output set $\Omega = \{\varop{x} , \varcl{x}\mid x\in\bigcal{X}\}$, with the sole difference that the sets of outputs stored in a node no longer contain strings in $\Omega^*$, but subsets of $\Omega$ instead. This difference is merely technical and has no influence in the time bounds of an ECS, as long as it is guaranteed to be duplicate-free (called {\it unambiguous} in~\cite{MunozR22}). 

First we assume that all transitions in $\bigcal{A}$ are reachable from $q_0$, and all of them reach an accepting state. We know that in the VA $\bigcal{A}$, the graph induced by the variable transitions is a DAG, otherwise it would not be sequential. We start with an empty ECS $\bigcal{D}$ and define a matrix $K[p,q]$, that first starts with the empty node in each index except the diagonal, which have the $\varepsilon$ node. The idea is that at the end of this algorithm, $\bigcal{L}_{\bigcal{D}}(K[p,q])$ contains all sets of variable markers that can be seen in a path from $p$ to $q$ that does not contain any letter transition. We build this matrix by iterating over the variable transitions in $\bigcal{A}$ following some topological order of the DAG, starting from a root. For each variable transition $(p,V,q)$, let $u\gets\mathsf{add}(V)$ and for each $p'\in Q$ that has a lower value in the topological order assign $K[p',q] \gets \mathsf{union}(K[p',q], \prod(K[p', p], \mathsf{add}(V)))$. The time of this algorithm is $|Q|\times|\bigcal{A}|$.

After doing this, we perform a construction analogous to the one done in Proposition~\ref{prop:eva-reduc}, in which we replace the extended variable transitions $(p,S,q)$ by the indices in which $K[p,q]$ is not the empty node. The proof follows from that result as well.
 
\subsection{Proof of Proposition~\ref{prop:lindelay}}

\newcommand{\mathsf{len}}{\mathsf{len}}

The algorithm that we present is a depth-first traversal of the DAG, done in a particular way to ensure that after retrieving some output the next one can be found in $O(k\cdot \ell)$ time, where $\ell$ is the size of the next output. First we will assume that the algorithm receives a duplicate-free and $k$-bounded $\bigcal{D}$ and a bottom or product node $v$, and then extend it to the case of a union or shift node.

This algorithm uses subroutines ${\tt first}(v, s)$, ${\tt next}(v, s)$ and ${\tt curr}(v, s)$ defined only for product and bottom nodes which print the first element in $\mathsf{sh}(\sem{\bigcal{D}}(v), s)$ (according to an order that is induced by the algorithm itself), the element that follows the previous one printed, and the same element as the one previously printed respectively. We use the word ``print'' to refer to the fact that these elements are given as a global output of the algorithm, not in the local subroutine. This means that the pairs $(\oout, i)$ are given as output as soon as some of these calls is done over a bottom node $v$ for which $\lambda(v) = \oout$. We also assume that each of these subroutines returns (locally) a flag ${\tt end}$ whenever the output printed is the last one of the set. We will inductively assume that calling ${\tt first}(v, s)$, and then ${\tt next}(v, s)$ repeatedly until some of these calls returns ${\tt end}$ prints the entire set $\mathsf{sh}(\sem{\bigcal{D}}(v), s)$ without repetitions.

In a bottom node $v$, the subroutines ${\tt first}(v, s)$ and ${\tt curr}(v, s)$ each print the element $(\lambda(v), s + 1)$ and return ${\tt end}$. We assume that ${\tt next}(v, s)$ is never called on a bottom node.

We now describe the subroutines for a product node $v$. First, we will assume there are no shift nodes that are descendants of $v$ in $\bigcal{D}$, and afterwards we will adapt the algorithm for shift nodes. Also, consider a procedure $St\gets {\tt trav}(u)$ defined over a union node $u$ which does a traversal over the left descendants of $u$ until it sees a product or bottom node. These nodes are added to the stack $St$. Also, consider a procedure ${\tt move}(St)$ which pops the last two nodes from $St$, and let $u'$ be the second node. Then, $St'\gets{\tt trav}(r(u'))$ is performed and the nodes in $St'$ are added to $St$ in the same order. We assume that ${\tt move}(St)$ cannot be applied if $St$ has only one node. An example of the result of these procedures can be seen in Figure~\ref{fig-enum-stacks}.

\begin{figure}[t]
	\centering
	\input{enumfig.tex}
	\caption{An example iteration of ${\tt trav}$ and ${\tt move}$. The sequences of nodes joined by dashed lines represent a stack $St$, where the first one was obtained after calling ${\tt trav}$ over the topmost union node, and the following five are obtained by repeated applications of ${\tt move}(St)$.}
	\label{fig-enum-stacks}
\end{figure}


Now, ${\tt first}(v, s)$ operates as follows: We perform $St_1 \gets {\tt trav}(\ell(u))$, and $St_2 \gets {\tt trav}(r(u))$, and let $v_1$ and $v_2$ be the nodes at the top of each stack. Then the first output is produced by calling ${\tt first}(v_1, s)$ and ${\tt first}(v_2, s)$. We define ${\tt next}(v, s)$ as follows: First, check if the last call to $v_2$ returned ${\tt end}$, and if it did not, call ${\tt curr}(v_1, s)$ and ${\tt next}(v_2, s)$. If it did return ${\tt end}$, then check if $St_2$ has more than one element, and if it does, we apply ${\tt move}(St_2)$, and then call ${\tt curr}(v_1, s)$ and ${\tt first}(v_2', s)$ where $v_2'$ is the new node at the top of $St_2$. If it has only one node, we check if the last call to $v_1$ returned ${\tt end}$, and if it did not, we call ${\tt next}(v_1, s)$. If it did, then we assume $St_1$ has more than one element, so we apply ${\tt move}(St_1)$ and call ${\tt first}(v_1', s)$, where $v_1'$ is the new node at the top of $St_1$. After a call is done over $v_1$ in any of these cases, we perform $St_2 \gets {\tt trav}(r(u))$, and then call ${\tt first}(v_2, s)$. In ${\tt next}(v)$, the flag ${\tt end}$ is returned when both calls to $v_1$ and $v_2$ return ${\tt end}$ and both stacks $St_1$ and $St_2$ have only one element. We now have to prove that calling ${\tt first}(v, s)$ and then ${\tt next}(v, s)$ repeatedly until one of these returns ${\tt end}$ effectively prints the entire set $\mathsf{sh}(\sem{\bigcal{D}}(v), s)$ without repetitions. First, let us introduce the concept of a {\it union-descendant} of a node $u$. We say that $u$ is an union-descendant of itself, and that its children also are union-descendants of it, but only if $u$ is a union node. Alternatively, we say that $u'$ is a union-descendant of $u$ if $u'$ can be reached starting from $u$ and following a path where all the intermediate nodes are union nodes. Let $w$ be an element in $\mathsf{sh}(\sem{\bigcal{D}}(v), s)$. Since $\bigcal{D}$ is duplicate-free, there exists a unique $w_1$ and $w_2$ such that $w_1\in\mathsf{sh}(\sem{\bigcal{D}}(\ell(v)), s)$ and $w_2\in\mathsf{sh}(\sem{\bigcal{D}}(r(v)), s)$ and $w = w_1\cdot w_2$. Again, since $
\bigcal{D}$ is duplicate-free, there exist a unique union-descendant $v_1$ of $\ell(v)$ such that $w_1\in\mathsf{sh}(\sem{\bigcal{D}}(v_1), s)$. The same can be said for $w_2$ and a node $v_2$ which is a union-descendant of $r(v)$. From the algorithm it can be seen that for each pair of output nodes $v_1'$ and $v_2'$ which are union-descendants of $r(v)$ and $\ell(v)$ respectively the following calls are made: first ${\tt first}(v_1, s)$ and ${\tt first}(v_2, s)$ is called; then, ${\tt curr}(v_1, s)$ and ${\tt next}(v_2, s)$ is called until ${\tt next}(v_2, s)$ (or ${\tt first}(v_2, s)$) returns ${\tt end}$; then, ${\tt next}(v_1, s)$ and ${\tt first}(v_2, s)$ is called; then ${\tt curr}(v_1, s)$ and ${\tt next}(v_2, s)$ again until ${\tt next}(v_2, s)$ returns ${\tt end}$; this is done until ${\tt curr}(v_1, s)$ (or ${\tt first}(v, s)$) returns ${\tt end}$, and ${\tt next}(v_2, s)$ (or ${\tt first}(v_2, s)$) also returns ${\tt end}$. This, altogether, means that for each $w_1'\in \mathsf{sh}(\sem{\bigcal{D}}(\ell(v)), s)$ and $w_2'\in \mathsf{sh}(\sem{\bigcal{D}}(r(v)), s)$ the string $w_1'\cdot w_2'$ is printed, as we assumed that the calls ${\tt first}$, ${\tt next}$ and ${\tt curr}$ work as specified. This proves that each output $w\in \mathsf{sh}(\sem{\bigcal{D}}(v), s)$ is printed, and this happens exactly once since $w_1$ and $w_2$ are uniquely defined, are found in exactly one pair of output-node union-descendants $v_1$ of $\ell(v)$ and $v_2$ of $r(v)$, and in both of these nodes every output is printed exactly once.

To account for shift nodes, we modify ${\tt trav}$ so it stores pairs $(u, s')$ in the stack, where $u$ is a union or output node, and $s'$ is the sum of all shift nodes seen in the path from $v$ to $u$. Then, whenever ${\tt first}$, ${\tt next}$ or ${\tt curr}$ is called, it is instead called over ${\tt first}(u, s + s')$, ${\tt next}(u, s + s')$ and ${\tt curr}(u, s + s')$. To do this, we keep a variable $s^*$, and whenever a shift node is seen in the traversal, its shift value is added to $s^*$. Then, when a union node is seen, it is added to the stack alongside the value $s^*$. It can be seen that this modification accounts for all the needed shifts in any of the calls to ${\tt first}$, ${\tt next}$ and ${\tt curr}$ on an union-descendant of $\ell(v)$ and $r(v)$, so we conclude that the set $\mathsf{sh}(\sem{\bigcal{D}}(\ell(v)), s)$ is printed correctly.

To show the time bounds of this procedure, first we note the fact that each pair $(\oout, i)$ is printed directly so we do not take this time into account, as it only adds constant time per element in the output. Call $\mathsf{len}(w)$ the length of $w$, as in, the number of pairs $(\oout, i)$ in it. Let $c$ be the time needed to do the constant-time operations utilized in the algorithm, such as pushing and popping from the stack, navigating to some child of a node, etc. We inductively assume that for any product or bottom node $u$, a call to ${\tt first}(u, s)$ to ${\tt next}(u, s)$ and ${\tt curr}(u, s)$ each take at most $2c\cdot (k+2)\cdot (\mathsf{len}(w)-1)$ time, where $w$ is the output produced. Note that this follows trivially for a bottom node, since the time taken is merely what is needed to print the single pair associated to it, which we already accounted for, and the extra time is 0.
For a product node $v$, the call ${\tt first}(v, s)$ takes time at most $c\cdot 2(k+1)$ to build the stacks $St_1$ and $St_2$, and then $2c\cdot (k+2)\cdot (\mathsf{len}(w_1^*) + \mathsf{len}(w_2^*) - 2)$ to call ${\tt first}(v_1, s')$ and ${\tt first}(v_2, s'')$, which print $w_1^*$ and $w_2^*$ respectively. Therefore, by using that $\mathsf{len}(w^*) = \mathsf{len}(w_1^*) + \mathsf{len}(w_2)$ the call to ${\tt first}(v)$ takes time at most $2c\cdot (k+2)\cdot (\mathsf{len}(w^*)-1)$. For the call ${\tt next}(v, s)$, we have to account for several cases, but we simply note that the case which uses the most operations besides the calls to $v_1$ and $v_2$ is the one where both previous calls to $v_1$ and $v_2$ returned ${\tt end}$, and $St_2$ has only one node. In this case ${\tt move}(St_1)$ has to be called, and $St_1\gets {\tt trav}(r(v))$ has to be called, which take at most time $c(k+2)$ and $c(k+1)$ respectively. Adding this time to the time needed to make a call to $v_1$ and $v_2$ gives a total time at most $2c\cdot (k+2)\cdot (\mathsf{len}(w^*)-1)$. This proves that the set $\mathsf{sh}(\sem{\bigcal{D}}(v), s)$ is enumerated with output-linear delay.

Finally, we refer to the case in which the enumeration is done over a union or shift node $v$. This case is handled in the same way the product-node case was. More precisely, we start by calling $St\gets {\tt trav}(v)$, and then proceed in the exact same way as described in the subroutines for the product node, by calling ${\tt first}(v_1, s)$, then ${\tt next}(v_1, s)$ util they return ${\tt end}$ and then applying ${\tt move}(St)$ and calling ${\tt first}(v_1, s)$ again. This adds constant time $c\cdot(k+2)$ to produce each output, which maintains the output-linear delay bounds we showed. This completes the proof.


\subsection{Proof of Theorem~\ref{theo:data-structure}}

The operations $\mathsf{add}$, $\prod$, and $\mathsf{shift}$ were defined in the body of the paper, so what is remaining is to go over the cases for $\mathsf{union}$ that were not defined. That is, the cases where at least one node among $v_3$ and $v_4$ is a shift node with an output node as its left child.

Without loss of generality, assume that $v_3$ has an output node as its left child. We extend $\bigcal{D}$ with nodes $v'$, $v''$ and $v'''$, where $\ell(v) = \lambda(v_3)$, $\lambda(v') = \cup$ and $\lambda(v''')  = \lambda(v_4) - \lambda(v_3)$, $\ell(v) = v''$, $\ell(v) = \ell(v_3)$, $r(v) = v'''$ and $\ell(v''') = \ell(v_3)$. This construction is illustrated in FIgure~\ref{fig-theo-ds}. It can be seen that $v'$ is a safe node since the left child of $v''$ is an output node, and $v'''$ has output depth at most 2, either if $\ell(v_4)$ is an output node, or if $\ell(v_4)$ is a union node whose left child is an output node. Since $\bigcal{D}$ was assumed to be 3-bounded, and this operation only adds nodes with output depth at most 2, the new version of $\bigcal{D}$ is 3-bounded as well. 

The fact that the set $\sem{D}(v)$ can be enumerated with output-linear delay for every node $v$ in $\bigcal{D}$ follows from Proposition~\ref{prop:lindelay}, since the operations are restricted to keep $\bigcal{D}$ duplicate-free and they result in a new version of $\bigcal{D}$ that is 3-bounded.

\begin{figure}
	\centering
	\begin{tikzpicture}[every label/.style={black!60}, ->,>=stealth',roundnode/.style={circle,inner sep=1pt},squarednode/.style={rectangle,inner sep=2pt}, scale=0.85]
		\node[squarednode] (0) at (0, 0) {$\ell(v_3)$};
		\node[squarednode, draw, label=180:\footnotesize{$v_3\!:$}] (2) at (2, 1) {$k_1$};
		\node[squarednode] (3) at (4, 0) {$\ell(v_4)$};
		\node[squarednode, draw, label=180:\footnotesize{$v_4\!:$}] (5) at (6, 1) {$k_2$};
		\node[squarednode, label=180:\footnotesize{$v'''\!:$}] (7) at (5.5, 1.7) {$(k_2-k_1)$};
		\node[squarednode, label=180:\footnotesize{$v''\!:$}] (8) at (3, 2.6) {$\cup$};
		\node[squarednode, draw, label=180:\footnotesize{$v'\!:$}] (9) at (4.5, 3.6) {$k_1$};
		\draw[dashed] (2.south west) to[out=-135,in=45] (0);
		\draw[dashed] (5.south west) to[out=-135,in=45] (3);
		\draw[dashed] (7.south west) to[out=-135,in=90] (3);
		\draw (8) to[out=-45,in=135] (7.north west);
		\draw[dashed] (8) to[out=-135,in=90] (0);
		\draw[dashed] (9.south west) to[out=-135,in=90] (8);
		
	\end{tikzpicture}
	\caption{Gadget used in Theorem~\ref{theo:data-structure}.}
	\label{fig-theo-ds}
\end{figure}


\subsection{Proof of Theorem~\ref{theo:data-structure-eps}}

Extending these four operations to deal with empty nodes is straightforward, and it has been explained in the body, so we will focus on operations that deal with the $\varepsilon$-node.

First, we add the condition that for any Shift-ECS\xspace $\bigcal{D}$ the $\varepsilon$-node is either disconnected to the rest of the structure (parent-less), or if it has a parent, then this must be a union node, and $\varepsilon$ must be its left child. We call this the {\it $\varepsilon$ condition}. We will see that any node that might be the result of applying the operations $\mathsf{add}$, $\prod$, $\mathsf{union}$ and $\mathsf{shift}$ is equivalent to a node in a Shift-ECS\xspace $\bigcal{D}$ that satisfies this. 

The notions of output-depth, duplicate-free, and $k$-boundedness are mostly unchanged in this setting: If $v$ is the $\varepsilon$-node, then $\mathsf{odepth}(v) = 0$, and if $v$ is a union node with the $\varepsilon$-node as its left child, $\mathsf{odepth}(v) = 1$, the rest of the nodes have no descendants that are the $\varepsilon$-node, so the definition of output depth remains the same; and the definitions of duplicate-free and $k$-bounded remain unchanged as well. By assuming the $\varepsilon$ condition, we can state the following claim which is a direct consequence of Proposition~\ref{prop:lindelay}:

\begin{claim}\label{prop:lindelayeps}
	Fix $k\in\mathbb{N}$. Let $\bigcal{C}_k$ be the class of all  duplicate-free and $k$-bounded Shift-ECSs\xspace{} that satisfy the $\varepsilon$ condition. Then one can solve the problem $\textsc{ShiftECSEnum}[\bigcal{C}_k]$ with output-linear delay and without preprocessing (i.e. constant preprocessing time).
\end{claim}


We now define the notion of {\it $\varepsilon$-safe} nodes. These are nodes $v$ which satisfy one of three conditions: (1) $v$ is the $\varepsilon$-node, (2) $v$ is safe and none of its descendants is the $\varepsilon$-node, and (3) $v$ is a union node, its left child is the $\varepsilon$-node, and its right child is a safe node for which none of its descendants is the $\varepsilon$-node. 
To guide the constructions, we call these conditions 1, 2 and 3.
These conditions will allow us to use the constructions already given for $\prod$, $\mathsf{union}$, and $\mathsf{shift}$ over safe nodes, such as node $v$, in the case of condition 2, or $r(v)$, in the case of condition 3.
The rest of this proof will be extending these operations to work over $\varepsilon$-safe nodes, and check that they can be done in constant time, return an $\varepsilon$-safe node, maintain the $\varepsilon$ condition in the Shift-ECS\xspace, and satisfy the specifications of each operation (i.e., that for the resulting node $v'$ the set $\sem{D}(v')$ contains what it should). 

The operation $\mathsf{add}$ is defined the same as in a Shift-ECS\xspace without $\varepsilon$. The operation $\mathsf{add}(\varepsilon)$ is not defined since the $\varepsilon$-node is always part of $\bigcal{D}$.

The $\prod$ case is somewhat more involved. First, assume that some node among $v_1$ and $v_2$ is the $\varepsilon$-node (condition 1). Without loss of generality, assume that $v_1$ is. If $v_2$ is the $\varepsilon$-node as well, we simply return $v_1$; and if $v_2$ is not the $\varepsilon$-node (conditions 2 or 3), we simply return $v_2$. The requirements of the construction follow trivially. Now, assume that both $v_1$ and $v_2$ satisfy condition 2. For this case we simply return $\prod(v_1, v_2)$ as it was defined for a Shift-ECS\xspace without $\varepsilon$. Lastly, assume at least one node among $v_1$ and $v_2$ satisfies condition 3 (and none of them are the $\varepsilon$-node). These cases are depicted in Figure~\ref{fig-prod-multi-gadget}, and are formally described as follows, using the operations $\mathsf{union}$ and $\prod$ as they were defined for a Shift-ECS\xspace without $\varepsilon$:
\begin{itemize}
	\item[(a)] $v_1$ satisfies condition 2 and $v_2$ satisfies condition 3. Let $v'' \gets \prod( v_1, r(v_2))$, and let $v' \gets \mathsf{union}( v_1, v'')$.
	\item[(b)] $v_1$ satisfies condition 3 and $v_2$ satisfies condition 2. Let $v'' \gets \prod( r(v_1), v_2)$, and let $v' \gets \mathsf{union}( v'', v_2)$.
	\item[(c)] Both $v_1$ and $v_2$ satisfy condition 3. Let $v'' \gets \prod( r(v_1), r(v_2))$, let $v^3 \gets \mathsf{union}( v'', r(v_2))$, and let $v^4 \gets \mathsf{union}( r(v_1), v^3)$. Lastly, let $\lambda(v') = \cup$, $\ell(v') = \varepsilon$, and $r(v') = v^4$.
\end{itemize}

It can be seen that these constructions work as expected. That is, that $\sem{\bigcal{D}'}(v) = \sem{\bigcal{D}}(v_1)\cdot\sem{\bigcal{D}}(v_2)$. Also, if $v_1$ and $v_2$ are $\varepsilon$-safe, then $v'$ is $\varepsilon$-safe as well. Also, each construction does a fixed number of steps, so they take constant time.

\begin{figure}[t]
	\centering
	\begin{tikzpicture}[->,>=stealth',roundnode/.style={circle,draw,inner sep=1.2pt},squarednode/.style={rectangle,inner sep=2pt}, scale=1]
		\node [squarednode] (c) at (1.12, -0.6) {$(a)$};
		\node [squarednode] (0) at (0.8, 2.75) {$\mathsf{union}$};
		\node [squarednode] (6) at (-0.05, 2.75) {$v'\gets$};
		\node [squarednode] (1) at (0, 1) {$v_1$};
		\node [squarednode] (2) at (1.6, 1.75) {$\prod$};
		\node [squarednode] (3) at (1.6, 1) {$v_2$};
		\node [squarednode] (4) at (0.8, 0) {$\varepsilon$};
		\node [squarednode] (5) at (2.4, 0) {$r(v_2)$};
		\draw[dashed] (0) to[out=-135,in=90] (1);
		\draw (0) to[out=-45,in=120] (2);
		\draw (2) to[out=-45,in=90] (5);
		\draw[dashed] (3) to[out=-135,in=60] (4);
		\draw (3) to[out=-45,in=120] (5);
		\draw[dashed] (2) to (1);
	\end{tikzpicture}
	\begin{tikzpicture}[->,>=stealth',roundnode/.style={circle,draw,inner sep=1.2pt},squarednode/.style={rectangle,inner sep=2pt}, scale=1]
		\node [squarednode] (c) at (1.6, -0.6) {$(b)$};
		\node [squarednode] (0) at (2.5, 2.75) {$\mathsf{union}$};
		\node [squarednode] (6) at (1.65, 2.75) {$v'\gets$};
		\node [squarednode] (1) at (3, 1) {$v_2$};
		\node [squarednode] (2) at (1.90, 1.75) {$\ \prod$};
		\node [squarednode] (3) at (0.85, 1) {$v_1$};
		\node [squarednode] (4) at (0.2, 0) {$\varepsilon$};
		\node [squarednode] (5) at (1.5, 0) {$r(v_1)$};
		\draw (0) to[out=-60,in=90] (1);
		\draw[dashed] (0) to[out=-135,in=70] (2);
		\draw[dashed] (2) to[out=-120,in=90] (5);
		\draw[dashed] (3) to[out=-135,in=60] (4);
		\draw (3) to[out=-45,in=120] (5);
		\draw (2) to (1);
	\end{tikzpicture}
	\begin{tikzpicture}[->,>=stealth',roundnode/.style={circle,draw,inner sep=1.1pt},squarednode/.style={rectangle,inner sep=2pt},scale=1.1]
		\node [squarednode] (c) at (1.6, -0.5) {$(c)$};
		\node [squarednode] (0) at (1.5, 2.75) {$\cup$};
		\node [squarednode] (11) at (0.88, 2.8) {$v'\gets$};
		\node [squarednode] (1) at (0.75, 2.25) {$\varepsilon$};
		\node [squarednode] (2) at (2.25, 2.25) {$\mathsf{union}$};
		\node [squarednode] (3) at (3, 1.75) {$\mathsf{union}$};
		\node [squarednode] (4) at (2.1, 1) {$\prod$};
		\node [squarednode] (5) at (3.2, 1) {$v_2$};
		\node [squarednode] (6) at (2.5, 0) {$\varepsilon$};
		\node [squarednode] (7) at (4, 0) {$r(v_2)$};
		\node [squarednode] (8) at (0.5, 1) {$v_1$};
		\node [squarednode] (9) at (0, 0) {$\varepsilon$};
		\node [squarednode] (10) at (1, 0) {$r(v_1)$};
		\draw[dashed] (0) to (1);
		\draw (0) to (2);
		\draw[dashed] (2) to[out=-135,in=70] (10);
		\draw[dashed] (4) to (10);
		\draw (4) to[out=-45,in=145] (7);
		\draw[dashed] (5) to[out=-135,in=60] (6);
		\draw (5) to[out=-45,in=120] (7);
		\draw (3) to[out=-45,in=90] (7);
		\draw[dashed] (3) to (4);
		\draw (2) to (3);
		\draw (8) to[out=-50,in=100] (10);
		\draw[dashed] (8) to[out=-125,in=80] (9);
	\end{tikzpicture}
	\caption{Gadgets for $\prod$ as defined for an Shift-ECS\xspace with the $\varepsilon$-node.}
	\label{fig-prod-multi-gadget}
\end{figure}


We now address the $\mathsf{union}$ case:
\begin{itemize}
	\item Assume $v_3$ is the $\varepsilon$-node (condition 1). (1) If $v_4$ also is the $\varepsilon$-node, then we simply return $v'\gets\varepsilon$. (2) If $v_3$ satisfies condition 2, let $v'$ be a union node such that $\ell(v') = \varepsilon$ and $r(v') = v_4$. It can be seen that $v'$ satisfies condition 3 and that its $\varepsilon$-safe. (3) If $v_4$ satisfies condition 3, we simply return $v'\gets v_4$.
	\item Assume $v_3$ satisfies condition 2. (1) If $v_4$ is the $\varepsilon$-node, we return $v'\gets \mathsf{union}( v_4, v_3)$ using the construction for the case (2) in the previous item. (2) If $v_4$ satisfies condition 2, then we return $v'\gets \mathsf{union}( v_3, v_4)$ as it was defined for Shift-ECSs\xspace without $\varepsilon$. (3) If $v_4$ satisfies condition 3, let $v'' \gets \mathsf{union}( v_3, r(v_4))$, and let $v'$ be a union node such that $\ell(v') = \varepsilon$ and $r(v) = v''$. Again, it can be seen that $v'$ is $\varepsilon$-safe.
	\item Assume $v_3$ satisfies condition 3. (1) If $v_4$ is the $\varepsilon$-node, we simply return $v'\gets\varepsilon$. (2) If $v_4$ satisfies condition 2, we follow the construction given in case (3) of the previous item. (3) If $v_4$ satisfies condition 3, let $v''\gets\mathsf{union}( r(v_3), r(v_4))$ and let $v'$ be a union node such that $\ell(v') = \varepsilon$ and $r(v) = v''$. It can be seen that $v'$ is $\varepsilon$-safe.
\end{itemize}

Clearly, in each of these cases we have that $\sem{\bigcal{D}}(v') = \sem{\bigcal{D}}(v_3)\cup \sem{\bigcal{D}}(v_4)$, and if $v_3$ and $v_4$ are $\varepsilon$-safe, then $v'$ is $\varepsilon$-safe as well. Plus, they all take constant time and in each case the new version of $\bigcal{D}$ satisfies the $\varepsilon$ condition.

The operation $\mathsf{shift}( v, k)$ is defined as follows: If $v$ is the $\varepsilon$-node, we return $v'\gets\varepsilon$. If $v$ satisfies condition 2, we return $v'\gets\mathsf{shift}( v, k)$ as it was defined for Shift-ECSs\xspace without $\varepsilon$. If $v$ satisfies condition 3, let $v''\gets\mathsf{shift}(r(v), k)$ and let $v'$ be a union node such that $\ell(v') =\varepsilon$ and $r(v) = v''$. It can be seen that $v'$ is $\varepsilon$-safe.

We conclude the proof by stating that the operations $\mathsf{add}$, $\prod$, $\mathsf{union}$ and $\mathsf{shift}$, when done over $\varepsilon$-safe nodes, can be done in constant time, return an $\varepsilon$-safe node, maintain the $\varepsilon$ condition in the Shift-ECS\xspace, and satisfy the specifications of each operation. Furthermore, by virtue of Claim~\ref{prop:lindelayeps}, for each node $v$ in $\bigcal{D}$ the set $\sem{D}(v)$ can be enumerated with output-linear delay.

\subsection{Proof of Lemma~\ref{lem:ecsext}}

Let $\bigcal{D}$ be the succinct Shift-ECS\xspace associated to the query data structure for $S$ and $\bigcal{A}$ and let $\tilde{R} = R' \setminus R$ be the set of new rules in $S'$. Consider the DAG that is induced by this set. We can go over these new rules $\tilde{A}\to BC$ in a bottom-up fashion, starting from the ones where $B,C\in N$, and define the nodes $M_{\tilde{A}}[p,q] = (M_{B}\otimes \mathsf{shift}(M_C,|\operatorname{doc}(B)|))[p,q]$ for each $p,q\in Q$. Then, we build the nodes $v_{\tilde{A}}$ for each new non-terminal $\tilde{A}$ as defined. The new nodes are created by application of the Shift-ECS\xspace operations $\mathsf{add}$, $\mathsf{union}$, $\prod$ and $\mathsf{shift}$ which create the succinct Shift-ECS\xspace $\bigcal{D}'$ that defines the query data structure for $S'$ and $\bigcal{A}$. The procedure takes $O(|Q|^3\cdot|\tilde{N}|)$ time.

\subsection{Proof of Theorem~\ref{theo:evaluation}}

As the time bounds are explained in the body, this proof will only regard correctness of Algorithm~\ref{alg:evaluation}.

The proof will follow after proving that for each $M_X$, for an $X\in\Sigma\cup N$ that is reachable from $S_0$, the set $\sem{\bigcal{D}}(M_X[p,q])$ contains all partial annotations of a run of $\bigcal{A}$ over $\operatorname{doc}(X)$ that starts on $p$ and ends on $q$. First let $X = a\in\Sigma$. This case can be quickly verified by inspecting the procedure {\sc Terminal}$(a)$, as for each index, the set $\sem{\bigcal{D}}(M_a[p,q])$ contains $\varepsilon$, and the annotations $\oout$ in the pair $(\oout, 1)$ whenever they correspond. Now, let $X$ be a non-terminal and let $R(X) = \alpha$. Let $\alpha'$ be a nonempty prefix of $\alpha$, and let $Y$ be its last symbol. Note that for the empty string, a run of size one is always valid, so we can safely consider that the set $M_X$, as declared in line 16 effectively stores nodes properly for the runs that start and end on the same node, and read the empty string. The proof will follow inductively by proving that $M_X$, at the iteration of line 18 that $Y$ was read in line 19, satisfies that $\sem{\bigcal{D}}(M_X[p,q])$ contains all partial annotations from a run of $\bigcal{A}$ over $\operatorname{doc}(\alpha Y)$ that starts on $p$ and ends on $q$; that is, after assuming that in line 24, the set $\sem{\bigcal{D}}(M_X[p,q])$ contained all partial annotations from a run of $\bigcal{A}$ over $\operatorname{doc}(\alpha)$ that starts on $p$ and ends on $q$. We have assumed that the nodes in $M_Y$ store all annotations properly, so the inductive hypothesis is proven from the definition of the operator $\otimes$, as any possible annotation that should be added can be described by two partial runs, one that starts on $p$, reads $\operatorname{doc}(\alpha)$ and ends on $q'$, and a second that starts on $q'$, reads $\operatorname{doc}(Y)$ and ends on $q$, so it is properly added to the $\sem{\bigcal{D}}(M_X[p,q])$ as the operator $\otimes$ does consider this $q'$. Plus, it can be seen that the positions that were obtained from $M_Y$ are properly shifted when added to $M_X$ by assuming the $\operatorname{len}_X$ variable is storing the correct length. From this reasoning it can be concluded that the set $\sem{\bigcal{D}}(v)$, as enumerated in line 7, contains exactly the annotations from $\sem{A}(S)$.

To see that the operators $\mathsf{add}$, $\mathsf{union}$, $\prod$ and $\mathsf{shift}$ are done following all assumptions, we just have to note that $\mathsf{union}$ and $\prod$ are always called by respecting the duplicate-free property. In the case of $\prod$, this is straight forward, since it is only done in line 25, and the positions on the left side (i.e., the ones taken from $M_X$) are all less or equal than the value $\operatorname{len}_X$ has at that point, so by shifting the values from $M_Y$ by this amount, the sets from either side do not contain any annotation in common. In the case of $\mathsf{union}$, one can visually check that in lines 11 and 13, this is done properly, since transitions do not appear more than once, and one can check that in line 25, if any of the calls to $\mathsf{union}$ done inside the $\otimes$ operation is done with duplicates, this implies that there is some annotation that appears in two distinct calls, since each of the $\mathsf{union}$ calls is done over a different index in the matrices $M_Y$ and $M_X$, which contradicts the assumption that $\bigcal{A}$ is unambiguous. From this reasoning we conclude that the operators $\mathsf{add}$, $\mathsf{union}$, $\prod$ and $\mathsf{shift}$ are done properly, and the statement of the theorem follows.
\subsection{Proof of Lemma~\ref{ra:det}}

We use the standard determinization scheme for regular automata. Namely, let $\bigcal{A} = (Q, \Sigma, \Omega, \Delta, q_0, F)$, and let $\bigcal{A}' = (Q', \Sigma, \Omega, \Delta', \{q_0\}, F')$ where $Q' = 2^Q$, $\Delta' = \{(S, a, T) \mid S, T\subseteq Q \text{ and $T$ is the set of states $q$ for which there exists a $p\in S$ such that }(p,a,q)\in \Delta  \} \cup 
 \{(S, (a,\oout), T) \mid S, T\subseteq Q \text{ and $T$ is the set of states $q$ for which there exists a } p\in S \text{ such that }$ $(p,(a,\oout),q) \in \Delta \}$, and $F' = \{S\mid S\cap F\neq\emptyset\}$. It can be seen that $\bigcal{A}'$ is deterministic. To show that $\sem{\bigcal{A}}(d) = \sem{\bigcal{A}'}(d)$ for every document $d\in\Sigma^*$, we define the {\it language} of an annotated automaton $\bigcal{A}$ as 
 \begin{multline*}
 	 L(\bigcal{A}) = \{\bar{d}\mid \bar{d} \text{ is a document over $\Sigma$ annotated with symbols in $\Omega$ that}\\ \text{is accepted when fed to $\bigcal{A}$ as if it was a regular automaton}\}
 \end{multline*}
It is straightforward to see that $L(\bigcal{A}) = L(\bigcal{A}')$, and from here it can be deduced that for each document $d\in\Sigma^*$ it holds that $\sem{\bigcal{A}}(d) = \sem{\bigcal{A}'}(d)$.








\section{Introduction}\label{sec:introduction}
	
	\input{intro}
	
	\section{Setting and main problem}\label{sec:setting}
	
	\input{setting}
	
	\section{Enumerable Compact Sets with Shifts}\label{sec:ecs}
	
	\input{ecsnew}
	
	\section{Evaluation of annotatated automata over SLP-compressed strings}\label{sec:evaluation}
	
	\input{eval}
	
	\section{Applications in Regular Spanners}\label{sec:spanners}
	
	\input{appl}
	
	\section{Constant delay-preserving Complex Document Editing}\label{sec:edits}
	
	\input{edits}
	
	\section{Future Work}\label{sec:conclusions}
	
	\input{concl}
	
	\newpage
	\bibliographystyle{abbrv}
	

