Connectivity Oracle Under Vertex Failures by Shortcutting Unbreakable Decomposition

The oracle supports three phases:

• $\mathrm{■}$

  Preprocess: Given $G=(V,E)$ with $|V|=n$, $|E|=m$, and a parameter $k$, build a data structure. The preprocessing time is the time to build the structure; the space is its memory usage.

• $\mathrm{■}$

  Update: Given a failure set $S\subseteq V$ with $|S|\le k$, update the data structure in update time.

• $\mathrm{■}$

  Query: Given $u,v\in V$, decide whether $u$ and $v$ are connected in $G\setminus S$ in query time.

Typically, one update (for a batch $S$) is followed by many connectivity queries under the same failures.

There is a long line of work optimizing the tradeoffs among space, preprocessing time, update time, and query time. SPQR trees [10, 7] yield an optimal oracle that handles $k\le 2$ failures using $O(n)$ space, $O(m)$ preprocessing, and $O(1)$ update and query time. Very recently, Kosinas [15] extended this optimal oracle to $k=3$.

For general $k$, the first structures are due to Duan and Pettie [4, 5]. More recently, Long and Saranurak [18] gave a deterministic oracle whose parameters are simultaneously optimal up to $n^{o(1)}$ factors under fine-grained complexity hypotheses: $O(\min \{m,nk\}{\log }^{\ast }n)$ space, $m^{1+o(1)}+\tilde{O}(mk)$ preprocessing time¹¹1Throughout the paper, we use $\tilde{O}(\cdot )$ to hide polylog factors., $O(k^2{n}^{o(1)})$ update time, and $O(k)$ query time. Long and Wang [19] later improved the $n^{o(1)}$ factor in the update time to polylogarithmic. Although this landscape is essentially settled when mild $n$-dependence is allowed, these results share a common drawback: their update time still contains an $n$-dependent term (subpolynomial or polylogarithmic).

Existing results essentially fall into two camps. On the one hand, we have near-linear-space oracles with excellent $k$-dependence, but their update time still depends on $n$. On the other hand, only two known approaches achieve update and query times depending solely on $k$:

• $\mathrm{■}$

  The randomized oracle of van den Brand and Saranurak [22] uses algebraic techniques to obtain $O(k^{\omega })$ update time and $O(k^2)$ query time (where $\omega$ is the matrix multiplication exponent), but requires $O(n^2)$ space and $O(n^{\omega })$ preprocessing time.

• $\mathrm{■}$

  The deterministic approach of Pilipczuk et al. [21] is based on unbreakable decomposition. It achieves $n$-independent update time, but their oracle with linear space comes with doubly exponential dependence on $k$ (and very large preprocessing). They also obtained an alternative oracle with $\text{poly}(k)$ update and query time, but it is strictly worse than the oracle by [22] except being deterministic.

Thus, prior $n$-independent oracles either use $\mathrm{\Omega }(n^2)$ space or incur doubly exponential dependency on $k$. Moreover, the preprocessing time is far from linear. See Table 1.

We resolve both drawbacks: we design a deterministic vertex-failure connectivity oracle with near-linear space in $n$ (with only a $\mathrm{poly}(k)$ factor) and purely $\mathrm{poly}(k)$ update and query time, independent of $n$. Moreover, our preprocessing time is near-linear when $k=O(1)$.

Here ${\alpha }_c(n)$ denotes the extremely slowly growing inverse Ackermann function for any fixed constant $c$. For constant $k$, the space and preprocessing are near-linear, while update and query are constant-time.

The ideal dependence on $k$ would be $O(k^2)$ update time and $O(k)$ query time: this would be both $n$-independent and conditionally optimal under fine-grained conjectures [9, 18]. We take a step toward this frontier by showing that optimal $O(k)$ query time is achievable with purely $k$-dependent update time, via a tradeoff that allows an additional $2^{O(k^2)}n$ term in space (while keeping preprocessing near-linear for constant $k$).

The $O(k)$ query time in Theorem 2 is conditionally optimal [9]. Table 1 summarizes known vertex-failure connectivity oracles whose update times are independent of $n$ and compares them with our results.

Beyond connectivity queries, our oracle improves other basic connectivity tasks. We discuss a simple reduction (refining the DFS-based framework of [15]) that converts any vertex-failure connectivity oracle into a vertex-cut oracle²²2A vertex-cut oracle supports vertex-cut query: will deleting a given set of vertices disconnect the graph?. More interestingly, this reduction is nearly lossless, and thus it immediately opens up new trade-offs with $n$-independent query time for vertex-cut oracles (the current vertex-cut oracles [12, 15] all have their query times depending on $n$). For example, by plugging in our new $n$-independent connectivity oracle, it gives the following new vertex-cut oracle.

Furthermore, we show a similar reduction for the more generalized Steiner vertex-cut oracles problem. Previously, there were results [1] for the related problem of $k$-vertex-fault-tolerant Steiner connectivity labeling schemes, but there are still no explicit results³³3[1] states that [12]’s vertex-cut oracle “seems plausible to extend also to the Steiner variant”, but there is no explicit proof, and the reduction following [15]’s DFS-based framework will likely be simpler. for Steiner vertex-cut oracles. The new reduction immediately yields many new trade-offs for Steiner vertex-cut oracles, leveraging the rich body of existing results for vertex-failure connectivity oracles. However, compared with the first reduction, it incurs larger losses (one more $O(\log n)$ overhead on the query time), and therefore cannot yield reasonable trade-offs with $n$-independent query time.

We improve upon the oracle of [21] with $\mathrm{\Omega }(n^2)$ space using three key ideas. First, to improve the space to near-linear, we introduce the usage of shortcut on top of the tree that represents the unbreakable decomposition of the graph. Second, to improve the preprocessing time, we observe that we can bootstrap the construction of our $n$-independent-update oracle using $n$-dependent-update oracles (by e.g. [14, 19]). Third, to obtain the optimal query time, we introduce the patch sets. However, applying these three ideas at the same time is non-trivial.

Section 2 gives a high-level explanation of our results. Section 3 introduces preliminaries and tools. Section 4 describes the preprocessing and data structure. Section 5 gives the update and query algorithms and proves Theorem 2. Finally, Section 6 discusses open problems and future improvements.

Additional configurations and proof for Theorem 1 can be found in the full version [17]. The discussion about two closely related problems: the vertex-cut oracle and the Steiner vertex-cut oracle problem, with the formal statement of Theorem 3 also appear in the full version [17].

We start by introducing the framework inspired by [21] using unbreakable decomposition [13]. In a graph $G$, we say a set $B\subseteq V$ is $(q,k)$-unbreakable if for any subset $S\subseteq V(G)$ of at most $k$ vertices, there can be at most one connected component $C$ in $G\setminus S$ such that $|C\cap B|>q$ while $|B\setminus C|\le q$. A $(q,k)$-unbreakable decomposition of a graph $G$ is a tree decomposition $𝒯=(T,\text{bag})$ where the bag associated with each tree node $x\in V(T)$ is $(q,k)$-unbreakable in $G$. Additionally, we say that $𝒯$ is strongly $(q,k)$-unbreakable if every $\text{bag}(x)$ is $(q,k)$-unbreakable in the subgraph of $G$ induced by the union of all bags in the subtree of $T$ rooted at $x$. Throughout the paper, we will use a strongly $(k,k)$-unbreakable decomposition of adhesion $k$ given by [13], thus in this paper we always assume $q=k$.

Given the set of at most $k$ failed vertices $S$ and for each $u\in S$, we first identify the topmost node $x\in T$ where its bag contains $u$ and call the node $x$ important. Let $X$ be the set of all important nodes and let $Y$ be the least common ancestor closure of $X$ in $T$, adding the root if it is not already included. Note that $|X|\le k$ and $|Y|\le O(k)$. For each $x\in X$, we aim to compute the profile of $x$, which is a graph on the adhesion of $x$ where two vertices are adjacent if and only if they are connected in the subgraph of $G\setminus S$ induced by the union of all bags in the subtree rooted at $x$. We build these profiles bottom-up, starting from the lowest nodes in $Y$ and working all the way to the root. We use additional precomputed graphs called torsos to quickly jump between important nodes and skipping sections of the graph where no vertex failures occur. For any $x,y\in V(T)$ where $x$ is a strict ancestor of $y$, the graph $\text{torso}(x,y)$ is on the adhesions of $x$ and $y$. Two vertices in $\text{torso}(x,y)$ are adjacent if and only if there exists a path between them in $G$ whose interior lies entirely within the the induced subgraph on the union of all bags in the subtree rooted at $x$ and stopping at $y$.

Computing torsos is a main bottleneck in the preprocessing time from [21]. To speed up this, we observe that torso queries can be computed via standard connectivity queries with vertex failures. Therefore, we build another oracle using [14] to boost the preprocessing time.

To evaluate the query $u,v$, we first consider $u$ and repeat the same process for $v$. We first augment $u$ to the computed profile of its closest ancestor in $Y$ while maintaining its connectivity invariants. Then we identify all important nodes along the path from $u$ to the root, and working upward by augmenting $u$ to each of their profiles until the root. After this is repeated for $v$, we can simply check the profile of the root to determine if $u$ and $v$ are connected in $G\setminus S$.

To avoid quadratic space used in storing all torsos [21], we develop an approach using shortcuts. We observe that, suppose we have $x,y,z\in V(T)$ where $x$ is an ancestor of $y$ and $y$ is an ancestor of $z$ in $T$, then $\text{torso}(x,z)$ can be computed through $\text{torso}(x,y)$ and $\text{torso}(y,z)$ efficiently.

With this observation, we only need to store a subset of torsos in our oracle. We model this by a set of shortcut edges in $T$ that when $x$ is an ancestor of $z$, $x$ can reach $z$ through constant shortcut edges. Therefore, when $\text{torso}(x,z)$ is needed, we just use the stored torsos on those shortcut edges to compute $\text{torso}(x,z)$. From [3, 16], we only need $n{\alpha }_c(n)$ shortcut edges, and thus we only need to store $n{\alpha }_c(n)$ (instead of $n^2$) torsos.

Next, we introduce how our oracle can achieve $O(k)$ optimal query time instead of $\text{poly}(k)$ as in [21] with storing some additional information about patch sets. As standard local search in [21] still has $O(k^2)$ query time even in $(q,k)$-unbreakable graphs, it would be good to assume $G$ is $(q,k)$-unbreakable below while still capturing the hardness and our ideas.

We define a collection $𝒫$ of patch sets as follows. Start from an arbitrary vertex $v\in V$, we perform BFS in $V$ from $v$ until a set $P\subseteq V$ with $(k+1)$ vertices are visited. We add $P$ to $𝒫$, delete $P$ from $V$, and then repeat the procedure until there’s no connected component in $V$ with at least $(k+1)$ vertices. Finally, for each remaining component $P$, we add $P$ into $𝒫$. We say $P\in 𝒫$ is large if $|P|=k+1$ and small otherwise. A small patch set can only link to large patch sets.

We know that, for any failed vertex set $S$ with size at most $k$, there exists at most one large component $C$ in $G\setminus S$ with $|C|>k$. We say a patch set $P\in 𝒫$ is touched if $P\cap S\ne \mathrm{\varnothing }$, and untouched otherwise. For each vertex $v$ that’s in an touched patch $P$, we do BFS from $v$ in $G\setminus S$. By visiting at most $k+1$ vertices in $O(k^2)$ time, we either find all vertices connected with $v$ in $G\setminus S$, or certify $v\in C$. Since there are at most $k$ affected components, the total update time will be $O(k\cdot k\cdot k^2)=O(k^4)$.

Then consider any vertex $u\in V$. If $u$ is in an affected patch set $P$, we already know the component of $u$. If $u$ is in an unaffected large patch $P$, we also know $u\in C$. Otherwise, $u$ is in an unaffected small patch $P$. By enumerating at most $(k+1)$ neighbors of $P$, if $P$ is not a component itself, we will find some $u^{\prime }$ that’s in a large patch set and connected with $P$. We can then compute the component of $u$ by $u^{\prime }$. Therefore, given a query $u,v$, we can check if they are in the same connected component using $O(k)$ time.

We will use the standard notion of graphs. Throughout this paper, we will only consider undirected graphs. For any graph $G$, we use $V(G)$ to denote its vertex set and $E(G)$ to denote its edge set. Additionally, we use $n=|V(G)|$ and $m=|E(G)|$ to represent the size of the graph $G$. WLOG we can assume $m=O(nk)$ by a sparsification in [20] with $O(m)$ time. For any subset of vertices $S\subseteq V(G)$, we use $G[S]$ to denote the subgraph of $G$ induced by $S$, and we use $G\setminus S$ to denote the graph $G$ after removing the set of vertices $S$. We will often use the term BFS in $G$ as a short hand as breadth-first search in a graph $G$.

A rooted tree $T$ is a connected acyclic graph with a distinguished root $r$. For any node $x\in V(T)$, we use $\text{parent}(x)$ to represent the parent of $x$ and $\text{children}(x)$ to represent the set of children of $x$. Let $x,y\in V(T)$ be two nodes, we say that $x$ is an ancestor of $y$ and $y$ is a descendant of $x$ if $x$ is on the unique path from $y$ to $r$. Additionally, we say that $x$ is a strict ancestor of $y$ if $x$ is an ancestor of $y$ and $x\ne y$. For a node $x\in V(T)$, we let $T(x)$ represent the subtree of $T$ rooted at $x$ that contains all descendants of $x$. Also, for two nodes $x,y\in V(T)$, we denote the least common ancestor of $x$ and $y$ by $\text{lca}(x,y)$, and note that $x$ is an ancestor of $y$ if and only if $\text{lca}(x,y)=x$. Suppose $x$ is a strict ancestor of $y$, we define the $y$-directed child of $x$ as the child $z$ of $x$ such that $z$ is on the $y$-$x$ path. We denote such $z$ as $\text{dir}(x,y)$.

A tree decomposition of a graph $G$ is a pair $𝒯=(T,\text{bag})$ where $T$ is a rooted tree with root $r\in V(T)$ and $\text{bag}:V(T)\to 2^{V(G)}$ is a mapping that assigns every tree node $x\in V(T)$ a subset $\text{bag}(x)\subseteq V(G)$ called a bag. Furthermore, the following two conditions must be satisfied.

1. 1.

   For every vertex $v\in G$, the set of nodes $x\in T$ where $v\in \text{bag}(x)$ induces a subtree of $T$.

2. 2.

   For every edge $(u,v)\in E(G)$, there exists a node $x\in T$ such that $u,v\in \text{bag}(x)$.

For a node $x\in T$, we additionally define the following notions.

• $\mathrm{■}$

  The adhesion of $x$ is $\text{adh}(x)=\text{bag}(\text{parent}(x))\cap \text{bag}(x)$.

• $\mathrm{■}$

  The margin of $x$ is $\text{mrg}(x)=\text{bag}(x)\setminus \text{adh}(x)$.

• $\mathrm{■}$

  The cone at $x$ is the union of all $\text{bag}(y)$ where $y$ is a descendant of $x$, denoted by $\text{cone}(x)$.

• $\mathrm{■}$

  The component at $x$ is $\text{comp}(x)=\text{cone}(x)\setminus \text{adh}(x)$.

The adhesion of a tree decomposition $𝒯$ is defined as the size of the largest adhesion, which is ${\max }_{x\in V(T)}|\text{adh}(x)|$.

Without loss of generality, we will assume that any tree decomposition we work with is regular, which satisfies the following conditions for every non-root node $x\in V(T)$.

1. 1.

   The margin of $x$ is non-empty.

2. 2.

   The induced graph $G[\text{comp}(x)]$ is connected.

3. 3.

   Every vertex $u\in \text{adh}(x)$ has a neighbor $v\in \text{comp}(x)$.

The last two conditions would imply that for every pair of vertices $u,v\in \text{adh}(x)$ and for any node $x$, there must exist a $u$-$v$ path such that every vertex along this path except $u,v$ are contained in $\text{comp}(x)$.

A separation in a graph $G$ is two subsets of vertices $L,R\subseteq V(G)$ where $L\cup R=V(G)$ such that after removing its separator $L\cap R$ from $G$, there will be no edge between the vertices in $L\setminus R$ and $R\setminus L$ in $G\setminus (L\cap R)$. The order of a separation is the size of its separator. For a subset $X\subseteq V(G)$, we say that $X$ is $(q,k)$-unbreakable in $G$ if for every separation $(L,R)$ of order at most $k$, we either have $|L\cap X|\le q$ or $|R\cap X|\le q$.

A $(q,k)$-unbreakable decomposition of a graph $G$ is a tree decomposition $𝒯=(T,\text{bag})$ where for every node $x\in V(T)$, $\text{bag}(x)$ is $(q,k)$-unbreakable in $G$. Additionally, we say that $𝒯$ is strongly $(q,k)$-unbreakable if every $\text{bag}(x)$ is $(q,k)$-unbreakable in $G[\text{cone}(x)]$. We will use the following theorem to compute an unbreakable decomposition in this paper.

Let $𝒯=(T,\text{bag})$ be a regular tree decomposition of a graph $G$. For any node $x\in V(T)$, we define its bag graph in the following way, denoted by $\text{bgraph}(x)$. We start by initializing $\text{bgraph}(x)$ to be the subgraph $G[\text{bag}(x)]$, and we call the edges in this graph normal. Next, for each $z\in \text{children}(x)$, we add a copy of the edge $(u,v)$ for every pair of vertices $u,v\in \text{adh}(z)$ in $\text{bgraph}(x)$. We call these edges adhesion edges supported by $z$, and they would be labeled as such. Note that we allow multiple edges between some pair of $u,v\in \text{bag}(x)$ supported by different children of $x$, which means that $\text{bgraph}(x)$ is in fact a multigraph.

We claim that the total size of all bag graphs is linear to the total size of $G$ as in the lemma below. We include the proof in full version [17] for completeness.

For a regular tree decomposition $𝒯=(T,\text{bag})$ of $G$, a tree node $x$, and a subset $S\subseteq V(G)$, we define the $S$-restricted bag graph of $x$, which is denoted by ${\text{bgraph}}_S(x)$ and obtained in the following way. We start with $\text{bgraph}(x)$, and for each child $z$ of $x$, we consider all adhesion edges supported by $z$. We remove a $z$-supported adhesion edge $(u,v)$ from $\text{bgraph}(x)$ if and only if there does not exist a $u$-$v$ path in $G[\text{cone}(z)]\setminus S$. We obtain ${\text{bgraph}}_S(x)$ after considering all adhesion edges. Note that ${\text{bgraph}}_{\mathrm{\varnothing }}(x)=\text{bgraph}(x)$ as $𝒯$ is regular.

We now consider some vital properties of restricted bag graphs in unbreakable decompositions, captured in the following lemma. We include the proof in full version [17] for completeness.

We introduce an existing vertex-failure connectivity oracle presented in [14] that we will utilize in the preprocessing phase, summarized in the following theorem.

We now consider adding shortcuts to a tree. Formally, given a tree $T$, we want to add a small number of additional edges to $T$ such that for any nodes $x,y\in V(T)$ where $x$ is an ancestor of $y$, one can reach $x$ from $y$ via $h$ non-reversing edges where $h$ is a constant. The non-reversing edges mean that every edge taken from $y$ to reach $x$ travels towards the root. This is called a shortcutting of the tree $T$ with hop-diameter $h$. From [3, 16] we know that a good shortcutting can be computed efficiently on paths and trees. Explicitly, we can utilize the following theorem.

Although implicit in [16, 3], given any $x,y$, one can compute an $h$-hop path with shortcut edges in $O(h)$ constant time. Note that here ${\alpha }_c(n)$ means inverse Ackermann function as in [16]. For example, ${\alpha }_2(n)=O(\log n)$ and ${\alpha }_4(n)=O({\log }^{\ast }n)$, and so on.

We now design data structures that allow quick evaluations of the connectivity between vertices in the adhesions of tree nodes that speed up update and query times.

First, we introduce the notion of torsos. For any $x,y\in V(T)$ where $x$ is a strict ancestor of $y$, we define the torso graph between $x$ and $y$, denoted by $\text{torso}(x,y)$, in the following way. The vertex set of $\text{torso}(x,y)$ is $\text{adh}(x)\cup \text{adh}(y)$. Any two vertices $u,v\in V(\text{torso}(x,y))$ are adjacent if and only if there exists a $u$-$v$ path in $G[\text{cone}(x)\setminus \text{comp}(y)]$ whose interior is disjoint from $V(\text{torso}(x,y))$. Note that any torso graph consists of at most $2k$ vertices.

We often need torsos in the update and query phases. To do this quickly, we need a data structure that answers torso queries in constant time. We first show that we can compute all torsos quickly, by applying Theorem 7.

The claim enables fast preprocessing time of our oracle. The proof of the above claim appears in the full version [17]. Next, we design a structure that outputs torsos in constant time upon queries.

To maintain and determine connectivity in update and query, the data structure relies heavily on bag graphs. More specifically, for every node $x\in V(T)$, we store a version of ${\text{bgraph}}_{\mathrm{\varnothing }}(x)$ that is preprocessed, along with the patch set of $x$, denoted by $\text{pset}(x)$. Each $\text{pset}(x)$ contain patches, where a patch $P\subseteq \text{bag}(x)$ is simply a subset of vertices. We add patches to $\text{pset}(x)$ in the following way. Start by choosing an arbitrary vertex $v\in \text{bag}(x)$ and perform BFS in ${\text{bgraph}}_{\mathrm{\varnothing }}(x)$ starting from $v$ until $k+1$ vertices, including $v$, are visited. Let $P_1$ be a set that contains exactly these $k+1$ visited vertices, remove $P_1$ from ${\text{bgraph}}_{\mathrm{\varnothing }}(x)$, include $P_1$ in $\text{pset}(x)$, and repeat this process in ${\text{bgraph}}_{\mathrm{\varnothing }}(x)\setminus P_1$. This is repeated until in ${\text{bgraph}}_{\mathrm{\varnothing }}(x)\setminus ({\bigcup }_{P_i\in \text{pset}(x)}{P}_i)$ there is no connected component of size at least $k+1$. Finally, for any remaining connected component $C$, we include $C$ as one patch in $\text{pset}(x)$.

We say a patch $P\in \text{pset}(x)$ is big if $|P|=k+1$, and we say that it is small otherwise. Moreover, we call two patches $P_i,P_j\in \text{pset}(x)$ adjacent to each other if and only if there exist some $u\in P_i$ and $v\in P_j$ such that $u$ and $v$ are adjacent in ${\text{bgraph}}_{\mathrm{\varnothing }}(x)$. From the construction process, the following structural claim is clear.

We then proceed with a simple processing of bag graphs. For each vertex $v\in \text{bag}(x)$, store in ${\text{bgraph}}_{\mathrm{\varnothing }}(x)$ a pointer along with $v$ that points to $P_v$, where $P_v\in \text{pset}(x)$ is the patch such that $v\in P_v$.

Along side this, we also store some neighbor sets of the patches. Let $N(P)$ be the set of at most $k+1$ vertices $v\in \text{bag}(x)$ where $v\notin P$ and there exists a normal edge $(u,v)$ in ${\text{bgraph}}_{\mathrm{\varnothing }}(x)$ such that $u\in P$ (if there are more than $k+1$ such $v$, choosing an arbitrary subset of $k+1$ of them suffices). We call $N(P)$ the set of normal neighbors of $P$.

Moreover, for any patch $P\in \text{pset}(x)$, let $N_{\text{adh}}(P)$ be the set of neighbors $v$ such that there is an adhesion edge $(u,v)$ in ${\text{bgraph}}_{\mathrm{\varnothing }}(x)$ where $u\in P$ and $v\notin P$. We call this the set of adhesion neighbors of $P$. Each set $N_{\text{adh}}(P)$ stores at most $k^3+1$ such vertices, and we implement it as a doubly-linked list such that deletion can be done in constant time. We store along with each vertex $v\in N_{\text{adh}}(P)$ a counter indicating the number of adhesion edges $(u,v)$ where $u\in P$.

Now, suppose $P_1,\mathrm{\dots },P_{\mathrm{\ell }}\in \text{pset}(x)$ are all the small patches. We store with each $P_i\in \{P_1,\mathrm{\dots },P_{\mathrm{\ell }}\}$ the set $N(P_i)$ and $N_{\text{adh}}(P_i)$. Furthermore, we claim that we can compute and store all patch sets, processed bag graphs, and neighbor sets of small patches in time and space linear to the size of $G$.

In this section we consider the special case of single-child failure. Suppose $S$ is the set of failed vertices, for a node $x\in V(T)$, we say that it is in the case of single-child failure if $S$ is disjoint from $\text{bag}(x)$ and there is exactly one $z\in \text{children}(x)$ such that $\text{comp}(z)\cap S\ne \mathrm{\varnothing }$. We call such $z$ the single affected child of $x$. To speed up query time, we need $O(k)$ time access to some vital information about ${\text{bgraph}}_S(x)$ for nodes $x$ that are in this case, formally captured in the following lemma.