inherit their local and non-local witnesses from ${\ensuremath{\mathfrak{A}}}'$, and ${\ensuremath{\mathfrak{A}}}'$ only uses elements from $Z$ as non-local witnesses.

Now we present the automata-based approach. As discussed above, this approach only yields an exponential space algorithm, yet it will later be used as the basis for a decision algorithm for a larger fragment.

\[lemma:succorder\] For every constraint problem $C$ there is a non-deterministic finite state automaton ${{\cal A}\xspace}$ such that $C$ has a finite $({\ensuremath{{S}}},<)$-solution if and only if $L({{\cal A}\xspace})$ is non-empty.

Here $L({{\cal A}\xspace})$ denotes the language recognized by ${{\cal A}\xspace}$.

Assume that $C {\ensuremath{\mathrel{\smash{\stackrel{\scriptscriptstyle{
    \text{def}}}{=}}}} \;}(C_\exists, C_\forall)$ is a constraint problem over a signature $T \cup \{{\ensuremath{{S}}}, <\}$. Let $\Sigma {\ensuremath{\mathrel{\smash{\stackrel{\scriptscriptstyle{
    \text{def}}}{=}}}} \;}\Sigma_T$ and $\Gamma {\ensuremath{\mathrel{\smash{\stackrel{\scriptscriptstyle{
    \text{def}}}{=}}}} \;}\Gamma_T$.

Without loss of generality we assume that the witnesses requested by the existential constraints of $C$ do not contradict universal constraints. More precisely, for an existential constraint $(\sigma, E)$ and every $(d, \gamma, \tau) \in E$ we assume that there is no universal constraint $(\sigma, d, \gamma, \tau)$.

We construct a finite state automaton ${{\cal A}\xspace}$ such that ${{\cal A}\xspace}$ accepts a word over $\Sigma$ if and only if $C$ has a solution. Intuitively the automaton ${{\cal A}\xspace}$ interprets words 