Encoding Co-Lex Orders of Finite-State Automata in Linear Space

In this article we give a data structure for Problem 1 stated above. More precisely, we prove the following theorem. In what follows, we denote with $n$ the number of states and with $m$ the number of transitions of the NFA at hand.

Here space is measured in RAM words of $\mathrm{\Theta }(\log n)$ bits. In order to better put our result into context we observe that there are two trivial solutions to Problem 1. (1) Explicitly storing the $n^2$ pairs of the co-lex order yields a data structure for Problem 1 that takes $O(n^2)$ bits and supports queries in $O(1)$ time. (2) Storing the input NFA takes $O(m)$ space and the NFA inherently represents its maximum co-lex order ${\le }_{FS}$. It is however unclear how to support queries efficiently in this case. Both of these approaches require $\mathrm{\Omega }(n^2)$ bits to be stored in the worst-case as the number of transitions may be $\mathrm{\Theta }(n^2)$.

Our data structure that satisfies the properties in Theorem 2 relies on three main techniques. (i) We assume to have computed a co-lex extension $\le$, i.e., a total order that is a superset of the maximum co-lex order of a forward-stable NFA (see Definition 11 for the formal definition). Such a co-lex extension can be obtained by running the ordered partition refinement algorithm of Becker et al. [2]. (ii) For each state, we store a left-minimal infimum walk $P_u^{inf}$ and a right-maximal supremum walk $P_u^{sup}$ to $u$. An infimum (supremum) walk to a state $u$ is a walk encoding the lexicographic smallest (largest) string reaching $u$ from the initial state. An infimum (supremum) walk $P_u$ to a state $u$ is left-minimal (right-maximal) if, whenever it intersects with another infimum (supremum) walk $P_u^{\prime }$, then the predecessor in $P_u$ is smaller (larger) than or equal to the predecessor in $P_u^{\prime }$ according to the co-lex extension. We study this type of walks in Sections 3 and 6. (iii) For each state $u$, we furthermore store two integers $\varphi (u,P_u^{inf})$ and $\gamma (u,P_u^{sup})$ that we use in order to encode the deepest states on the infimum walk $P_u^{inf}$ (supremum walk $P_u^{sup}$) that is in infimum (supremum) conflict with $P_u^{inf}$ $(P_u^{sup})$. We introduce this concept of infimum and supremum conflicts in Section 4. Intuitively, a state $\overline{u}$ in $P_u^{inf}$ is in infimum conflict with $P_u^{inf}$ if there exists a state $\widehat{u}$ that is incomparable with $\overline{u}$ according to the maximum co-lex order and both $\overline{u}$ and $\widehat{u}$ can reach $u$ with the same string $\alpha$.

Figure 1 shows the decision tree used by our data structure in order to determine comparability with respect to the CFS order ${\le }_{FS}$ between two states $u$ and $v$ based on the above three concepts. Let $u$ and $v$ be two states. If $u=v$, then $u{\le }_{FS}v$ holds by reflexivity, case (a) in Figure 1. Otherwise, if (here means $v\le u$ with respect to the co-lex extension and $v\ne u$), we can conclude $\neg (u{\le }_{FS}v)$, case (b) in Figure 1. Otherwise, let $P_u^{sup}$ be the right-maximal supremum walk to $u$ and let $P_v^{inf}$ be the left-minimal infimum walk to $v$. Imagine traversing the two walks from $u$ and $v$ backwards yielding a sequence of pairs ${(u_i,v_i)}_{i\ge 1}$. While traversing the walks we can construct the strings $sup{I}_u$ and $inf{I}_v$. If $sup{I}_u\le inf{I}_v$, we know that $u{\le }_{FS}v$, case (c) in Figure 1. Otherwise, when comparing the pairs $u_i,v_i$ with respect to the co-lex extension $\le$, we are guaranteed to find a pair $u_j,v_j$ such that . We distinguish two cases, if for each $i\in [j-1]$, we have as in case (d) of Figure 1, then $\neg (u{\le }_{FS}v)$. Otherwise, there exists a minimal integer $j^{\prime }\le j$ such that $u_{j^{\prime }}=v_{j^{\prime }}$. In this case, the comparability of $u$ and $v$ can be decided using the infimum/supremum conflicts. Consider the maximum integer $h$ such that either $u_h$ is in sup conflict with $P_u^{sup}$ or $v_h$ is in inf conflict with $P_v^{inf}$. If $h\ge j^{\prime }$ (case (e) in Figure 1), we know $\neg (u{\le }_{FS}v)$. In fact, the opposite would imply that either $P_u^{sup}$ is not right-maximal or $P_u^{inf}$ is not left-minimal. Finally, if (case (f) in Figure 1), we conclude that $u{\le }_{FS}v$. The details of the data structure are presented in Section 5. We remark that the existence of our left-minimal infimum and right-maximal supremum walks is actually proved independently of the labels in the graph through an unlabeled analogue that we call leftmost/rightmost walks. These walks represent a combinatorial object in unlabeled directed graphs that may be of independent interest. As a central ingredient of our proof, we show constructively (i.e., through an algorithm) that such leftmost/rightmost walks are guaranteed to exist for any (unlabeled) directed graph and can be represented by a linear space function that encodes the predecessor of each node in their leftmost/rightmost walk. This is shown in Section 6.

Given an alphabet $\mathrm{\Sigma }$, we denote by ${\mathrm{\Sigma }}^{\ast }$ the set of all finite strings over $\mathrm{\Sigma }$, where $\epsilon \in {\mathrm{\Sigma }}^{\ast }$ is the empty string. Moreover, we define ${\mathrm{\Sigma }}^{\omega }$ as the set containing all strings formed by an infinite enumerable concatenation of characters from $\mathrm{\Sigma }$ (i.e., strings of infinite length). In particular, we consider right-infinite strings, meaning that $\alpha \in {\mathrm{\Sigma }}^{\omega }$ is constructed from $\epsilon$ by appending an infinite sequence of characters to its end. Therefore, the operation of prepending a character $a\in \mathrm{\Sigma }$ of $\alpha \in {\mathrm{\Sigma }}^{\omega }$ is well defined and yields the string $a\alpha$. The notation ${\alpha }^{\omega }$, with $\alpha \in {\mathrm{\Sigma }}^{\ast }$, denotes the concatenation of an infinite (enumerable) number of copies of $\alpha$. In this paper, we assume to have a fixed total order $\le$ over $\mathrm{\Sigma }$. We extend $\le$ to ${\mathrm{\Sigma }}^{\ast }\cup {\mathrm{\Sigma }}^{\omega }$ in order to obtain the lexicographic order on strings. For each $\alpha \in {\mathrm{\Sigma }}^{\ast }\cup {\mathrm{\Sigma }}^{\omega }$, $|\alpha |=l$ denotes the length of $\alpha$, where $l=\mathrm{\infty }$ if $\alpha \in {\mathrm{\Sigma }}^{\omega }$. In addition, for each integer $i$ with , ${\alpha }_i$ denotes the $i$-th character of $\alpha$, starting from the left. Finally, we denote with $\alpha [i,j]$, where $i,j$ are two integers such that , the string of ${\mathrm{\Sigma }}^{\ast }$ formed by the concatenation of characters ${\alpha }_i{\alpha }_{i+1}\mathrm{\dots }{\alpha }_j$.

A nondeterministic finite automaton (NFA) is a 4-tuple $(Q,\delta ,\mathrm{\Sigma },s)$, where $Q$ represents the set of the states, $\delta :Q\times \mathrm{\Sigma }\to 2^Q$ is the automaton’s transition function, $\mathrm{\Sigma }$ is the alphabet, and $s\in Q$ is the initial state. The standard definition of NFAs also includes a set of final states; however, we omitted them since we are not interested in distinguishing between final states and non-final states. Given an NFA $𝒜=(Q,\delta ,\mathrm{\Sigma },s)$, a state $u\in Q$, and a character $a\in \mathrm{\Sigma }$, we may use the shortcut ${\delta }_a(u)$ for $\delta (u,a)$. We make the following assumptions on NFAs: $(i)$ We assume the alphabet $\mathrm{\Sigma }$ to be effective; each character of $\mathrm{\Sigma }$ labels at least one edge of the transition function. $(ii)$ We assume that every state is reachable from the initial state. $(iii)$ We assume that $s$ has only one incoming edge, $s\in \delta (s,\mathrm{\#})$, where $\mathrm{\#}\in \mathrm{\Sigma }$ does not label any other edge of $𝒜$. $(iv)$ We do not require each state to have an outgoing edge for all possible characters of $\mathrm{\Sigma }$. $(v)$ We assume that our NFAs are input-consistent; an NFA is said to be input-consistent if all edges reaching the same state have the same label of $\mathrm{\Sigma }$. This assumption is not restrictive since any NFA can be transformed into an input-consistent NFA by replacing each state with at most $|\mathrm{\Sigma }|$ copies of itself, without changing its regular language. Given an NFA $𝒜=$($Q$, $\delta$, $\mathrm{\Sigma }$, $s$), and a state $u\in Q$, with $u\ne s$, we denote with $\lambda (u)$ the (unique) character of $\mathrm{\Sigma }$ that labels the incoming edges of $u$, thus $\lambda (s)=\mathrm{\#}$.

For each NFA there exists a unique coarsest forward-stable partition, i.e., the forward-stable partition with the lowest cardinality [2]. Henceforth, we call an NFA forward-stable if its coarsest forward-stable partition is formed by singleton sets.

Given an integer $j$, we denote by $[j]$ the set $\{1,\mathrm{\dots },j\}$. Given an NFA $𝒜=(Q,\delta ,\mathrm{\Sigma },s)$, and a state $u\in Q$, we say that a walk to $u$, denoted as $P_u={(u_i)}_{i=1}^l$, is a non-empty sequence of $l$ states from $Q$ that satisfies the following conditions: $(i)$ $u_1=u$, and $(ii)$ for each $i\in [l-1]$, $u_i\in {\delta }_a(u_{i+1})$ where $a=\lambda (u_i)$. Moreover, we denote by $P_u={(u_i)}_{i\ge 1}$ a walk of infinite length to $u\in Q$. We define $I_u$ as the set of all strings $\alpha \in {\mathrm{\Sigma }}^{\omega }$, for which there exists a walk $P_u={(u_i)}_{i\ge 1}$ such that $\alpha =\lambda (u_1)\lambda (u_2)\lambda (u_3)\mathrm{\dots }$. We now provide the definition of supremum and infimum strings of an NFA’s state, which was introduced by Conte et al. [5] and Kim et al. [13, Definition 7].

It is easy to demonstrate that for each $u\in Q$, the strings $inf{I}_u$ and $sup{I}_u$ exist (for instance, it follows from Observation 8 in the work of Kim et al. [13], see also [7]). We now provide the definition of infimum and supremum walks.

In other words, a walk to $u$ is an infimum (supremum) walk, if it is labeled with the infimum (supremum) string of $u$.

A partial order $\le$ on a set $U$ is a reflexive, antisymmetric and transitive relation on $U$. Given a partial order $\le$ on a set $U$, for each $u,v\in U$, we write if $u\le v$ and $u\ne v$. We now report the formal definition of co-lex order of an NFA, which was first introduced by Cotumaccio and Prezza [10, Definition 3.1].

Note that every NFA $𝒜=(Q,\delta ,\mathrm{\Sigma },s)$ admits a co-lex order; in fact, the partial order $\le ≔\{(u,u):u\in Q\}$ trivially satisfies the two axioms of Definition 6. We say that a co-lex order $\le$ of an automaton $𝒜$ is the maximum co-lex order of $𝒜$ if $\le$ is equal to the union of all co-lex orders of $𝒜$. Becker et al. [3, Lemma 3] showed that every forward-stable NFA admits a maximum co-lex order. Hereafter, we will denote by ${\le }_{FS}$ the maximum co-lex order of an NFA.

Consider the partial order $\le$ defined as follows; $\le ≔\{(z,z):z\in Q\}\cup \{(u,v)\}$. $\le$ is a co-lex order of $𝒜$, as it does not violate the axioms of Definition 6. Therefore, since ${\le }_{FS}$ is defined as the union of every co-lex order of $𝒜$, it follows that holds. $◀$

We start with the definition of preceding pairs [6, Definition 6].

Note that if $u,v\in Q$ are distinct states, then the pair $(u,v)$ trivially precedes itself. The following observation directly follows from Definition 8.

Preceding pairs characterize the maximum co-lex order of a forward-stable NFA as follows.

Let $u$ and $v$ be two distinct states. Following [6, Lemma 7], $(u,v)$ is contained in the maximum co-lex relation (see [6, Definition 4]) if and only if $\lambda (\overline{u})\le \lambda (\overline{v})$ for every pair $(\overline{u},\overline{v})$ with $(\overline{u},\overline{v})\rightrightarrows (u,v)$. The maximum co-lex order ${\le }_{FS}$ of a forward-stable NFA $𝒜$ is equal to its maximum co-lex relation according to [3, Lemma 3]. $◀$

Note that for any distinct states $u,v$ of $𝒜$, the statement holds if and only if there exists $(\overline{u},\overline{v})\rightrightarrows (u,v)$ with $\lambda (\overline{u})>\lambda (\overline{v})$. We now define co-lex extensions.

Due to Lemma 11 of the work of Becker et al. [2], it follows that the ordered partition refinement [2, Algorithm 1] represents a feasible algorithm for computing a co-lex extension.

According to Definition 11 implies . Corollary 10 then yields that there exists $(\overline{u},\overline{v})$ with $(\overline{u},\overline{v})\rightrightarrows (u,v)$ such that . $◀$

Let $C$ be the set consisting of all strings $sup{I}_u$’s and all strings $inf{I}_u$’s, and write $C=\{{\gamma }_1,{\gamma }_2,\mathrm{\dots },{\gamma }_{n^{\prime }}\}$ where . Then, $n^{\prime }\le 2n$. Notice that for every $u\in Q$, by the maximality of $sup{I}_u$ there exist $c_1\in \mathrm{\Sigma }$ and $u_1\in Q$ such that $sup{I}_u=c_{1}sup{I}_{u_1}$, and by the minimality of $inf{I}_v$ there exist $c_2\in \mathrm{\Sigma }$ and $u_2\in Q$ such that $inf{I}_u=c_{2}inf{I}_{u_2}$. This implies that for every $2\le i\le n^{\prime }$ there exist $c\in \mathrm{\Sigma }$ and $2\le i^{\prime }\le n^{\prime }$ such that ${\gamma }_i=c{\gamma }_{i^{\prime }}$. We define the array $\mathrm{𝖫𝖢𝖯}[2,n^{\prime }]$ such that $\mathrm{𝖫𝖢𝖯}[i]=\mathrm{𝗅𝖼𝗉}({\gamma }_{i-1},{\gamma }_i)$, where $\mathrm{𝗅𝖼𝗉}(\alpha ,\beta )$ is the length of the longest common prefix between $\alpha$ and $\beta$. To prove the lemma it is sufficient to show that $\mathrm{𝖫𝖢𝖯}[i]\le n^{\prime }-2$ for every $i$ with $2\le i\le n^{\prime }$. To prove this it is sufficient to show that if $\mathrm{𝖫𝖢𝖯}[i]=d$ for some $d\ge 1$ and $i$ with $2\le i\le n^{\prime }$, then there exists $j$ with $2\le j\le n^{\prime }$ such that $\mathrm{𝖫𝖢𝖯}[j]=d-1$, because then we obtain that $\mathrm{𝖫𝖢𝖯}$ has at least $d+1$ distinct entries, so $d+1\le n^{\prime }-1$, which implies $d\le n^{\prime }-2$. Assume that $\mathrm{𝖫𝖢𝖯}[i]=d$, with $d\ge 1$. Let $c_1,c_2\in \mathrm{\Sigma }$ and $2\le i^{\prime },i^{\prime \prime }\le n^{\prime }$ be such that ${\gamma }_i=c_1{\gamma }_{i^{\prime }}$ and ${\gamma }_{i-1}=c_2{\gamma }_{i^{\prime \prime }}$. Since $1\le d=\mathrm{𝖫𝖢𝖯}[i]=\mathrm{𝗅𝖼𝗉}({\gamma }_{i-1},{\gamma }_i)=\mathrm{𝗅𝖼𝗉}(c_1{\gamma }_{i^{\prime }},c_2{\gamma }_{i^{\prime \prime }})$, we have $c_1=c_2$ and from we obtain , which implies . Then, $\mathrm{𝖫𝖢𝖯}[i]=1+\mathrm{𝗅𝖼𝗉}({\gamma }_{i^{\prime }},{\gamma }_{i^{\prime \prime }})=1+{\min }_{i^{\prime }+1\le j\le i^{\prime \prime }}\mathrm{𝗅𝖼𝗉}({\gamma }_{j-1},{\gamma }_j)=1+{\min }_{i^{\prime }+1\le j\le i^{\prime \prime }}\mathrm{𝖫𝖢𝖯}[j]$, so there exists $i^{\prime }+1\le j\le i^{\prime \prime }$ such that $d=\mathrm{𝖫𝖢𝖯}[i]=1+\mathrm{𝖫𝖢𝖯}[j]$, which implies $\mathrm{𝖫𝖢𝖯}[j]=d-1$. $◀$

The following lemma treats the case in which the relation between the supremum and infimum of two states already implies their respective order with respect to ${\le }_{FS}$.

We show the contrapositive. Assume that . By Corollary 10, this implies the existence of a pair $(\overline{u},\overline{v})$ with $(\overline{u},\overline{v})\rightrightarrows (u,v)$ such that $\lambda (\overline{u})>\lambda (\overline{v})$. By Definition 8, this implies that there exist two walks $P_u={(u_i)}_{i=1}^l$ and $P_v={(v_i)}_{i=1}^l$ with $u_1=u,v_1=v,u_l=\overline{u},v_l=\overline{v}$ such that ${\alpha }^{\prime }={\beta }^{\prime }$ where ${\alpha }^{\prime }:=\lambda (u_1)\lambda (u_2)\mathrm{\dots }\lambda (u_{l-1})$ and ${\beta }^{\prime }:=\lambda (v_1)\lambda (v_2)\mathrm{\dots }\lambda (v_{l-1})$. Now recall that every state is reachable from the initial state $s$ and $s\in \delta (s,\mathrm{\#})$. Thus there exist infinite strings ${\alpha }^{\prime \prime }\in I_{\overline{u}}$ and ${\beta }^{\prime \prime }\in I_{\overline{v}}$. Note that ${\alpha }^{\prime \prime }>{\beta }^{\prime \prime }$ because $\lambda (\overline{u})>\lambda (\overline{v})$. Since $\alpha ={\alpha }^{\prime }{\alpha }^{\prime \prime }\in I_u$ and $\beta ={\beta }^{\prime }{\beta }^{\prime \prime }\in I_v$, we obtain $sup{I}_u\ge \alpha ={\alpha }^{\prime }{\alpha }^{\prime \prime }={\beta }^{\prime }{\alpha }^{\prime \prime }>{\beta }^{\prime }{\beta }^{\prime \prime }=\beta \ge inf{I}_v$, completing the proof. $◀$

With the next lemma we show a case in which we can determine if holds.

Consider $\alpha =sup{I}_u$ and $\beta =inf{I}_v$. Let $k$ be the maximal integer such that $\alpha [1,k-1]=\beta [1,k-1]$. Since $\alpha >\beta$, it holds that $\lambda (u_k)>\lambda (v_k)$. By Lemma 13, . Moreover, by Observation 7, $\lambda (u_k)>\lambda (v_k)$ implies which, by Definition 11, in turn implies . Therefore, if we define $j>1$ as the smallest integer for which , then clearly for each $i\in [j-1]$, $u_i\le v_i$. Moreover, since $j\le k$, and $\alpha [1,k-1]=\beta [1,k-1]$, for each $i\in [j-1]$, it holds that $\lambda (u_i)=\lambda (v_i)$. For the second part of the lemma, if (implying $u_i\ne v_i$) for each $i\in [j-1]$, then $(u_j,v_j)\rightrightarrows (u,v)$ by definition. Since , by Lemma 12, there exists $(\overline{u},\overline{v})\rightrightarrows (u_j,v_j)$ with $\lambda (\overline{u})>\lambda (\overline{v})$. Thus, by Observation 9 it holds that $(\overline{u},\overline{v})\rightrightarrows (u,v)$ which by Corollary 10 proves that . $◀$

We summarize what we achieved so far. Given two distinct states $u,v$, to understand whether or not holds we can proceed as follows. If according to a co-lex extension $\le$, the statement holds, by Definition 11, we know . If , then if $sup{I}_u\le inf{I}_v$, by Lemma 14, we know that . Otherwise, consider a supremum walk to $u$, ${(u_i)}_{i\ge 1}$, and an infimum walk to $v$, ${(v_i)}_{i\ge 1}$. If $sup{I}_u>inf{I}_v$, and there exists $j$ such that and for each $i\in [j-1]$, then by Lemma 15 . See Figure 2 for an example. The only remaining case to address is the existence of an integer $j^{\prime }\in [j-1]$ such that $u_{j^{\prime }}=v_{j^{\prime }}$. To study this case, we introduce left-minimal (right-maximal) walks.

We proceed with the definition of left-minimal infimum walks and right-maximal supremum walks. We first define infimum and supremum graphs.

We now prove a preliminary result concerning infimum/supremum graphs.

Let $u$ be a state of $𝒜$, and let $P_u={(u_i)}_{i\ge 1}$ be an arbitrary walk of infinite length. We prove this result for infimum walks, the proof for the supremum walks is analogous. Suppose for the sake of a contradiction that $P_u$ is not an infimum walk. We consider the largest integer $j$ for which there exists an infimum walk $P_u^{inf}={({\overline{u}}_i)}_{i\ge 1}$, such that, for each $i\in [j]$, ${\overline{u}}_i=u_i$. Thus, ${\overline{u}}_{j+1}\ne u_{j+1}$. By Definition 16, there exists a state $v$, an infimum walk $P_v^{inf}={(v_i)}_{i\ge 1}$, and an integer $k$ for which $v_k=u_j$ and $v_{k+1}=u_{j+1}$. Consider $\alpha =\lambda ({\overline{u}}_1)\mathrm{\dots }\lambda ({\overline{u}}_j)$, $\gamma =\lambda ({\overline{u}}_{j+1})\lambda ({\overline{u}}_{j+2})\mathrm{\dots }$, $\beta =\lambda (v_1)\mathrm{\dots }\lambda (v_k)$, ${\gamma }^{\prime }=\lambda (v_{k+1})\lambda (v_{k+2})\mathrm{\dots }$, we know $inf{I}_u=\alpha \gamma$, $inf{I}_v=\beta {\gamma }^{\prime }$. Moreover, consider the walks $P_u^{\prime }={({\widehat{u}}_i)}_{i\ge 1}$, where for each $i\in [j]$, ${\widehat{u}}_i={\overline{u}}_i$, and for each $i\ge j$, ${\widehat{u}}_i=v_{i+k-j}$, and $P_v^{\prime }={({\widehat{v}}_i)}_{i\ge 1}$, where, for each $i\in [k]$, ${\widehat{v}}_i=v_i$, and, for each $i\ge k$, ${\widehat{v}}_i={\overline{u}}_{i+j-k}$. We know that $\alpha {\gamma }^{\prime }\in I_u$ and $\beta \gamma \in I_v$. By Definition 5, $\alpha \gamma \le \alpha {\gamma }^{\prime }$ which implies $\gamma \le {\gamma }^{\prime }$, and $\beta {\gamma }^{\prime }\le \beta \gamma$ which implies ${\gamma }^{\prime }\le \gamma$. Thus $\gamma ={\gamma }^{\prime }$. Consequently, $P_u^{\prime }$ is an infimum walk. However, ${\widehat{u}}_j=u_j$ and ${\widehat{u}}_{j+1}=u_{j+1}$, a contradiction. $◀$

We now introduce leftmost/rightmost walks in directed (unlabeled) graphs.

We are now ready to introduce left-minimal and right-maximal walks.

The proof of existences of left-minimal and right-maximal walks in directed graphs is given in Theorem 25 in Section 6. The next corollary then follows together with Observation 17.

We prove the lemma for infimum walks and inf conflicts; the proof for supremum walks and sup conflicts is analogous. Consider an integer $j$ such that $u_j\sqcap P_u$ and an arbitrary integer $j^{\prime }$ with . Moreover, let ${({\overline{u}}_i)}_{i=1}^j$ be the walk for which state $u_j$ is in inf conflict with $P_u$. Clearly, ${({\overline{u}}_i)}_{i=1}^{j^{\prime }}$ satisfies condition (i) of Definition 21 for $u_{j^{\prime }}\sqcap P_u$. It remains to prove that . Note that for each $i$ with $j^{\prime }\le i\le j$, we have ${\overline{u}}_i\ne u_i$ and $\lambda ({\overline{u}}_i)=\lambda (u_i)$. Hence every preceding pair of $(u_j,{\overline{u}}_j)$ is a preceding pair of $(u_{j^{\prime }},{\overline{u}}_{j^{\prime }})$ and it follows from Corollary 10 that implies . This proves the lemma. $◀$

We introduce now two functions $\varphi$ and $\gamma$ which will be at the basis of our data structure.

In other words, the functions ${\varphi }^j(u,P_u^{inf})$ and ${\gamma }^j(u,P_u^{sup})$ intuitively represent the largest integer $k$ for which either $u_k\sqcap P_{u_i}^{inf}$ or $u_k^{\prime }\bigsqcup P_{u_i^{\prime }}^{sup}$ holds for an integer $i$ with .

$(\Rightarrow )$ By Corollary 10, implies the existence of a pair $(\overline{u},\overline{v})$ with $(\overline{u},\overline{v})\rightrightarrows (u,v)$ such that $\lambda (\overline{u})>\lambda (\overline{v})$. Let ${({\overline{u}}_i)}_{i=1}^{j^{\prime }}$ and ${({\overline{v}}_i)}_{i=1}^{j^{\prime }}$ be the walks for which $(\overline{u},\overline{v})\rightrightarrows (u,v)$ holds, respectively. Lemma 15 implies that $\lambda (u_i)=\lambda (v_i)$ for each $i\in [j]$ and . Furthermore, we have $\lambda ({\overline{u}}_i)\le \lambda (u_i)$ and $\lambda (v_i)\le \lambda ({\overline{v}}_i)$ for each $i\in [j^{\prime }]$ by the properties of supremum and infimum walks. By the properties of preceding pairs (see Definition 8), for each $i\in [j]$, it holds that $\lambda ({\overline{u}}_i)=\lambda ({\overline{v}}_i)$ and thus $\lambda ({\overline{u}}_i)=\lambda (u_i)$ and $\lambda (v_i)=\lambda ({\overline{v}}_i)$. Moreover, since $\lambda (\overline{u})>\lambda (\overline{v})$, it follows that $j^{\prime }>j$. Due to the walks ${({\overline{u}}_i)}_{i=j}^{j^{\prime }}$ and ${({\overline{u}}_i)}_{i=j}^{j^{\prime }}$, it holds that $(\overline{u},\overline{v})\rightrightarrows ({\overline{u}}_j,{\overline{v}}_j)$, which by Corollary 10 and $\lambda (\overline{u})>\lambda (\overline{v})$ implies . Now, define $h:=\max \{i\in [j-1]:{\overline{u}}_i=u_i\}$ and $h^{\prime }:=\max \{i\in [j-1]:{\overline{v}}_i=v_i\}$ and consider $P_{u_h}^{sup}={(u_i)}_{i\ge h}$ and $P_{v_{h^{\prime }}}^{inf}={(v_i)}_{i\ge h^{\prime }}$. In order to prove $\max \{{\gamma }^j(u,P_u^{sup}),{\varphi }^j(v,P_v^{inf})\}\ge j$, since , it is thus sufficient to prove that $A:=u_j\bigsqcup P_{u_h}^{sup}\vee v_j\sqcap P_{v_{h^{\prime }}}^{inf}$ holds. Due to the previous considerations, ${({\overline{u}}_i)}_{i=h}^j$ satisfies condition (i) of Definition 21 for $u_j\bigsqcup P_{u_h}^{sup}$, while ${({\overline{v}}_i)}_{i=h^{\prime }}^j$ satisfies condition (i) of Definition 21 for $v_j\sqcap P_{v_{h^{\prime }}}^{inf}$. Hence, $A$ holds if and only if or equivalently . Since $u_j=v_j$ and ${\le }_{FS}$ is transitive, the conclusion is implied by , which we argued above.

$(\Leftarrow )$ Consider the case where the maximum is attained by ${\gamma }^j(u,P_u^{sup})$ (the other case is analogous) and call that value $h$. We know $h\ge j$ by hypothesis. By Corollary 10, we have to prove the existence of a pair $(\overline{u},\overline{v})$ with $(\overline{u},\overline{v})\rightrightarrows (u,v)$ such that $\lambda (\overline{u})>\lambda (\overline{v})$. Let $k\in [j-1]$ be such that $\gamma (u_k,P_{u_k}^{sup})+k-1=h$. Due to Observation 17, the walk $P_{u_k}^{sup}={(u_i)}_{i\ge k}$ is a supremum walk to $u_k$. Since $u_h\bigsqcup P_{u_k}^{sup}$ and $j\le h$, by Lemma 22 it follows that $u_j\bigsqcup P_{u_k}^{sup}$. Therefore, by Definition 21 there exists a walk ${({\overline{u}}_i)}_{i=k}^j$ such that ${\overline{u}}_i\ne u_i$ and $\lambda ({\overline{u}}_i)=\lambda (u_i)$ for each $i$ with as well as . Now define ${\overline{u}}_i:=u_i$ for $i\in [k]$ and consider the two walks ${({\overline{u}}_i)}_{i=1}^j$ and ${(v_i)}_{i=1}^j$. Note that ${\overline{u}}_k=u_k$. From Definition 21 and Lemma 15 it follows that $\lambda ({\overline{u}}_i)=\lambda (v_i)$ for each $i\in [j]$. Suppose now that ${\overline{u}}_{i^{\prime }}=v_{i^{\prime }}$ for some $i^{\prime }$ with . We can then define a new supremum walk ${({\widehat{u}}_i)}_{i\ge 1}$ to $u$ as follows. We define (i) ${\widehat{u}}_i:={\overline{u}}_i$ for $i\in [i^{\prime }]$, (ii) ${\widehat{u}}_i:=v_i$ for $i$ with , and (iii) ${\widehat{u}}_i:=u_i$ for $i\ge j$. Since $u_j={\widehat{u}}_j$ and , we conclude that $P_u^{sup}$ is not a right-maximal supremum walk to $u$, a contradiction. Hence, ${\overline{u}}_i\ne v_i$ for all $i\in [j]$ and consequently $({\overline{u}}_j,v_j)\rightrightarrows (u,v)$. Note that $u_j=v_j$ holds by hypothesis. Finally, since , by Corollary 10, there exists $(\overline{u},\overline{v})$ with $(\overline{u},\overline{v})\rightrightarrows ({\overline{u}}_j,u_j)$ such that $\lambda (\overline{u})>\lambda (\overline{v})$. Observation 9 then implies $(\overline{u},\overline{v})\rightrightarrows (u,v)$. $◀$