Assume $\mathcal{G}_X \neq \varnothing$, otherwise the statement is trivial.

Construction of $M$. Let $L$ be the set of linear paths in $G$ that go through at least one operation in $\pi$. Consider the set of operations $O_L$ in $G$ given by the operations whose linear paths are contained in $L$. This defines a subgraph $G|_{O_L}$ of $G$. Since $\mathcal{G}_X \neq \varnothing$, there exists $H \in \mathcal{G}_X$. By assumption, $H$ is connected, and thus the anchors $\pi$ of $H$ are connected in $H$. There is therefore a connected component $M \subseteq G|_{O_L}$ that contains the set $\pi$.

Well-definedness of $M^\pi$. Consider the PSG $M^\pi$ of $M$. We must show that $M^\pi$ is a tree-like graph for the proposition statement to be well-defined. In other words, we must show that the interaction graph $\mathcal{I}$ of $M^\pi$ is acyclic and connected. $M$ is connected by construction, which implies connectedness of $M^\pi$ and thus of $\mathcal{I}$. It is acyclic because $width(M) = |\pi| + 1$ and $M$ has exactly $|\pi|$ operations on more than one linear path. $\mathcal{I}$ is a thus a tree.

$H \subseteq M$. For any subgraph $H \in \mathcal{G}_X$, its operations must be contained in $O_L$. Since any $H \in \mathcal{G}$ is connected and contains $\pi$, it must further hold that $H \subseteq M$.

We can now prove the $\Leftrightarrow$ equivalence of (1).

$\Leftarrow$: If $\tau_{r'}(P^{\pi'}) \subseteq \tau_r(M^\pi)$, then there exists $H' \subseteq M^\pi$ with rooted dual tree

Furthermore, by definition of $\subseteq$ on rooted trees, a $split$ map is defined on $H'$, given by the $split$ map of $M^\pi$ on the domain $H'$. Recall from section 4.3 that there is a map $\sigma$ that maps

$\Rightarrow$: Since $H \in \mathcal{G}_X$, we know from point 1 that $H \subseteq M$. Thus we can define an injective embedding $\varphi: P \to M$.

Operation splitting leaves the set of values from $H$ to $H^\pi$, as well as from $M$ to $M^\pi$ unchanged. Similarly, there is a bijection between values in $H^\pi$ and $M^\pi$ and thus between edges in $\tau_r(H^\pi)$ and $\tau_r(M^\pi)$. The pattern embedding $\varphi$ hence defines an injective map $\phi_E$ from tree edges in $\tau_r(H^\pi)$ to tree edges in $\tau_r(M^\pi)$. We extend this map to a map on the trees $\phi: \tau_r(H^\pi) \to \tau_r(M^\pi)$ by induction over the nodes set of $\tau_r(H^\pi)$. We start by the root map $\phi(r) = r$. Using $\phi_E$, we can then uniquely define the image of any child node of $r$ in $\tau_r(H^\pi)$, and so forth inductively.

We show now that the map $\phi$ thus defined is injective. Suppose $v, v'$ are nodes in $\tau_r(H^\pi)$ such that $\phi(v) = \phi(v')$. By the inductive construction there are paths from the root $r$ to $v$ and $v'$ respectively such that their image under $\phi_E$ are two paths from $r$ to $\phi(v) = \phi(v')$. But $\tau_r(M^\pi)$ is a tree, so both paths must be equal. By bijectivity of $\phi_E$, it follows $v = v'$, and thus $\phi$ is injective. Finally, the value and operation weights are invariant under pattern embedding and thus are preserved by definition.

Let $H \subseteq G$ be a connected subgraph of $G$ of width $w$. We prove inductively over $w$ that if $(X, S', H') =$CanonicalAnchors$(H, r,S)$ then there is a graph $G'$ such that $H' \subseteq G' \subseteq G$ such that

$(X, S', G') \in$ AllAnchors$(G, r, w, S)$

for all valid root operations $r$ of $H$ and all subsets of the linear paths of $H$ in seen_paths. The statement in the proposition directly follows this claim.

For the base case $w = 1$, CanonicalAnchors will return the anchors anchors = [op] as defined on line 19: there is only one linear path, and it is already in seen_paths, thus for every recursive call to CanonicalAnchors, the while condition on line 12 will always be satisfied until all operations have been exhausted and empty sets are returned. In AllAnchors, on the other hand, The only values of w1, w2 and w3 that satisfy the loop condition on line 27 for $w = 1$ are w1 $=$ w2 $=$ w3 $= 0$. As a result, given the w $=0$ base case on lines 6–7, the lines 35 and 36 of AllAnchors are only executed once, and the definition of anchors on line 36 is equivalent to its definition in CanonicalAnchors.

We now prove the claim for $w > 1$ by induction. As documented in AllAnchors, we can assume that every operation has at most 3 children. This simplifies the loop on lines 21–25 of CanonicalAnchors to, at most, three calls to CanonicalAnchors.

Consider a call to CanonicalAnchors for a graph $H \subseteq G$, a root operation $r$ in $H$ and a set $S$ of linear paths. Let $w_a$, $w_b$ and $w_c$ be the length of the values returned by the three recursive calls to CanonicalAnchors of line 22 for the execution of CanonicalAnchors with arguments $H$, $r$ and $S$. Let $c_a, c_b$ and $c_c$ be the three neighbours of $r$ in $H$. If the child $c_x$ does not exist, then one can set $w_x = 0$ and it can be ignored – the argument below still holds in that case. The definition of seen0 on line 20 in AllAnchors coincides with the update to the variable seen_paths on line 18 of CanonicalAnchors; similarly, the updates to G on lines 14 and 18 of AllAnchors are identical to the lines 11 and 15 of CanonicalAnchors that update H. Let the updated seen_paths be the set $S_a$, the updated G be $G_a$ and the updated $H$ be $H_a$, with $H_a \subseteq G_a$.

As every anchor operation reduces the number of unseen linear paths by exactly one (using the simplifying assumptions of section 4.2), it must hold that $w_a + w_b + w_c + 1 = w$. Thus, for a call to AllAnchors with the arguments $G$, $r$, $w$ and $S$, there is an iteration of the for loop on line 27 of AllAnchors such that w1 $= w_a$, w2 $= w_b$ and w3 $= w_c$. It follows that on line 29 of AllAnchors, the procedure is called recursively with arguments $(G_a, c_a, w_a, S_a)$. From the induction hypothesis, we obtain that there is an iteration of the for loop on line 29 in which the values of anchors1 and seen1 coincide with the values of the new_anchors and seen_paths variables after the first iteration of the for loop on line 21 of CanonicalAnchors. Call the value of seen1 (and seen_paths) $S_b$. Similarly, call the updated value of G in AllAnchors $G_b$ and the updated value of G in CanonicalAnchors $H_b$. We have, by the induction hypothesis, that $H_b \subseteq G_b$.

Repeating the argument, we obtain that there are iterations of the for loops on lines 30 and 32 of AllAnchors that correspond to the second and third recursive calls to CanonicalAnchors on line 22 of the procedure. Finally, the concatenation of anchor lists on line 36 of AllAnchors is equivalent to the repeated concatenations on line 25 of CanonicalAnchors, and so we conclude that the induction hypothesis holds for $w$.

Let $C_w$ be an upper bound for the length of the list returned by a call to AllAnchors for width $w$. For the base case $w = 0$, $C_0 = 1$. The returned all_anchors list is obtained by pushing anchor lists one by one on line 36. We can count the number of times this line is executed by multiplying the length of the lists returned by the recursive calls on lines 28–32, giving us the recursion relation

Since $C_w$ is meant to be an upper bound, we replace $\leq$ with equality above to obtain a recurrence relation for $C_w$. This recurrence relation is a generalisation of the well-known Catalan numbers Stanley, 2015Richard P. Stanley. 2015. Catalan Numbers. Cambridge University Press. doi: 10.1017/CBO9781139871495, equivalent to counting the number of ternary trees with $w$ internal nodes: a ternary tree with $w \geq 1$ internal nodes is made of a root along with three subtrees with $w_1,w_2$ and $w_3$ internal nodes respectively, with $w_1 + w_2 + w_3 = w-1$. A closed form solution to this problem can be found in Aval, 2008Jean-Christophe Aval. 2008. Multivariate Fuss–Catalan numbers. Discrete Mathematics 308, 20 (October 2008, 4660–4669). doi: 10.1016/j.disc.2007.08.100​:

satisfying the above recurrence relation with equality, where $c = 27/4 = 6.75$ is a constant obtained from the Stirling approximation:

We restrict Operations on line 9 to only return the first $d$ operations on the linear path in each direction, starting at the anchor operation: operations more than distance $d$ away from the anchor cannot be part of a pattern of depth $d$.

We use the bound on the length of the list returned by calls to AllAnchors of Proposition 4.10 to bound the runtime. We can ignore the non-constant runtime of the concatenation of the outputs of recursive calls on line 35, as the total size of the outputs is asymptotically at worst of the same complexity as the runtime of the recursive calls themselves. Excluding the recursive calls, the only remaining lines of AllAnchors that are not executed in constant time are the while loop on lines 15–18 and the Operations and sort calls on lines 9–11. Using the same argument as in CanonicalAnchors, we can ignore the latter two calls by replacing the queue of operations by a lazy iterator of operations. The next operation given op and the graph G can always be computed in $O(1)$ time using a depth-first traversal of G.

Consider the recursion tree of AllAnchors, i.e. the tree in which the nodes are the recursive calls to AllAnchors and the children are the executions spawned by the nested for loops on line 28–32. This tree has at most

leaves. A path from the root to a leaf corresponds to a stack of recursive calls to AllAnchors. Along this recursion path, seen_paths set is always strictly growing (line 35) and the operations removed from G on lines 14 and 18 are all distinct. For each linear path, at most $2d$ operations are traversed. Thus the total runtime of the while loop (lines 15–18) along a path from root to leaf in the recursion tree is in $O(w \cdot d)$. We can thus bound the overall complexity of executing the entire recursion tree by $O(C_w \cdot w \cdot d) = O(\frac{c^w \cdot d}{w^{1/2}})$.