# A finite presentation of graphs of treewidth at most three

Amina Doumane, Samuel Humeau, Damien Pous

► To cite this version:

Amina Doumane, Samuel Humeau, Damien Pous. A finite presentation of graphs of treewidth at most three. 2024. hal-04560570

HAL Id: hal-04560570

https://hal.science/hal-04560570

Preprint submitted on 26 Apr 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A finite presentation of graphs of treewidth at most three

Amina Doumane, Samuel Humeau, Damien Pous

<figure><img src="image_1.png" /></figure>

To cite this version:

Amina Doumane, Samuel Humeau, Damien Pous. A finite presentation of graphs of treewidth at most three. 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)., Jul 2024, Tallinn, Estonia. 10.4230/LIPIcs.ICALP.2024.135 . hal-04560570v3

HAL Id: hal-04560570

https://hal.science/hal-04560570v3

Submitted on 21 Jan 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A finite presentation of graphs of treewidth at most three

Amina Doumane ☐

Plume, LIP, CNRS, ENS de Lyon, France

Samuel Humeau ☐

Plume, LIP, CNRS, ENS de Lyon, France

Damien Pous ☐

Plume, LIP, CNRS, ENS de Lyon, France

## Abstract

We provide a finite equational presentation of graphs of treewidth at most three, solving an instance of an open problem by Courcelle and Engelfriet.

We use a syntax generalising series-parallel expressions, denoting graphs with a small interface. We introduce appropriate notions of connectivity for such graphs (components, cutvertices, separation pairs). We use those concepts to analyse the structure of graphs of treewidth at most three, showing how they can be decomposed recursively, first canonically into connected parallel components, and then non-deterministically. The main difficulty consists in showing that all non-deterministic choices can be related using only finitely many equational axioms.

**2012 ACM Subject Classification** Theory of computation → Equational logic and rewriting; Mathematics of computing → Paths and connectivity problems

**Keywords and phrases** Graphs, treewidth, connectedness, axiomatisation, series-parallel expressions

**Digital Object Identifier** 10.4230/LIPIcs.ICALP.2024.143

**Related Version** Published version: https://doi.org/10.4230/LIPIcs.ICALP.2024.143 [12]

**Supplementary Material** Software: https://perso.ens-lyon.fr/damien-pous/hypergraph/

**Funding** This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

**Acknowledgements** The second author would like to thank Ugo Giocanti for several discussions about graph minors and connectivity.

## 1 Introduction

Treewidth is a graph parameter measuring how close a graph is from a forest. It is frequently encountered in parameterised complexity: many NP-complete problems become polynomial or even linear once parameterised using treewidth [4]. This parameter admits many equivalent definitions. It was discovered at least by Bertelè and Brioschi [3], Halin [13], and Robertson and Seymour [14] via tree decompositions for their celebrated graph minor theorem. It was subsequently characterised using *k*-trees [2], *k*-elimination graphs [18, 17, 16], and chordal graphs [14].

One may also consider syntaxes, most often generalising series-parallel expressions [1, 10, 8]. There, the idea is to use terms to denote graphs, and an important problem is to understand when two terms denote the same graph. To this end, Courcelle and Engelfriet gave an equational axiomatisation for arbitrary graphs [9, p. 117]: a structured set of equations on terms from which it is possible to equate all terms denoting a given graph. Unfortunately, this axiomatisation is infinite. They note how finite fragments of the syntax make it possible
# A finite presentation of graphs of treewidth at most three

Amina Doumane ☑

Plume, LIP, CNRS, ENS de Lyon, France

Samuel Humeau ☑

Plume, LIP, CNRS, ENS de Lyon, France

Damien Pous ☑●

Plume, LIP, CNRS, ENS de Lyon, France

## Abstract

We provide a finite equational presentation of graphs of treewidth at most three, solving an instance of an open problem by Courcelle and Engelfriet.

We use a syntax generalising series-parallel expressions, denoting graphs with a small interface. We introduce appropriate notions of connectivity for such graphs (components, cutvertices, separation pairs). We use those concepts to analyse the structure of graphs of treewidth at most three, showing how they can be decomposed recursively, first canonically into connected parallel components, and then non-deterministically. The main difficulty consists in showing that all non-deterministic choices can be related using only finitely many equational axioms.

**2012 ACM Subject Classification** Theory of computation → Equational logic and rewriting; Mathematics of computing → Paths and connectivity problems

**Keywords and phrases** Graphs, treewidth, connectedness, axiomatisation, series-parallel expressions

**Related Version** Published version: https://doi.org/10.4230/LIPIcs.ICALP.2024.135 [10]

**Supplementary Material** Software: https://perso.ens-lyon.fr/damien-pous/hypergraph/

**Funding** This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

**Acknowledgements** The second author would like to thank Ugo Giocanti for several discussions about graph minors and connectivity.

## 1 Introduction

Treewidth is a graph parameter measuring how close a graph is from a forest. It is frequently encountered in parameterised complexity: many NP-complete problems become polynomial or even linear once parameterised using treewidth [4]. This parameter admits many equivalent definitions. It was discovered at least by Bertelè and Brioschi [3], Halin [11], and Robertson and Seymour [12] via tree decompositions for their celebrated graph minor theorem. It was subsequently characterised using *k*-trees [2], *k*-elimination graphs [16, 15, 14], and chordal graphs [12].

One may also consider syntaxes, most often generalising series-parallel expressions [1, 8, 6]. There, the idea is to use terms to denote graphs, and an important problem is to understand when two terms denote the same graph. To this end, Courcelle and Engelfriet gave an equational axiomatisation for arbitrary graphs [7, p. 117]: a structured set of equations on terms from which it is possible to equate all terms denoting a given graph. Unfortunately, this axiomatisation is infinite. They note how finite fragments of the syntax make it possible
<figure><img src="image_2.png" /><figcaption>■ **Figure 1** Two parsings of a given graph.</figcaption></figure>

to capture precisely the graphs up to a given treewidth, while finite restrictions of their axiomatisation seem to be incomplete.

This brings them to the following question [9, p. 118]: for a given bound $k$, is there a finite equational presentation of graphs of treewidth at most $k$? The case of $k = 1$ concerns forests and is relatively easy. The case of $k = 2$ has been given a solution a few years ago [7, 11]. Here we give a positive answer for $k = 3$: we provide a syntax of terms with an interpretation map $g$ from terms to graphs whose image is exactly the set of graphs of treewidth at most three, and we give a finite list of equations whose equational theory ($\equiv$) characterises graph isomorphism ($\simeq$). In symbols, we prove that for all terms $t, u$,

$$g(t) \simeq g(u) \quad \text{if and only if} \quad t \equiv u$$

Like Arnborg, Courcelle, Proskurowski and Seese [1], we work with hypergraphs with a list of designated vertices, the *sources*, used as an interface to perform the following operations:

- *parallel composition* ($\parallel$): glue the graphs together along their sources.

- *permutation* (*pG*): given a permutation *p*, reorder the sources of *G* according to *p*.

- *lift* (*lG*): add an isolated vertex to *G* and append it as last source.

- *forget* (*fG*): remove the last source of *G* (keeping it as a mere vertex of the graph).

Consider the four graphs depicted in Figure 1, each with three sources denoted with numbered squares. The neighbours of each edge are ordered, which we indicate by drawing an arrow from the first to the second neighbour. The first graph on the left is the parallel composition of the three other ones. The second one can be obtained from a binary edge *a* (with interface its endpoints) by applying a lift to add a third isolated source and then swapping the last two sources: (23)la. The third one can be obtained from a ternary edge *b* (again with interface its endpoints), by forgetting the third source and adding a fresh one via a lift: lfb. The last one can be constructed as $f((24)lc \parallel (14)ld)$: reasoning top-down, we promote the inner vertex as a fourth source, and then we put in parallel two graphs each with a single ternary edge connecting three out of the four sources—both being obtained as appropriate permutations of lifted edges.

We call *parsings* the expressions we obtain when decomposing graphs as above.

The way we parsed the graph on the right generalises to all graphs: first promote all inner vertices as sources, and then build a large parallel composition of appropriately permuted and lifted edges. For instance, the first graph on the left also admits the following parsing:

$$\mathrm{ff}((23)llla \parallel (35)llb \parallel (24)llc \parallel (124)lld)$$

While such a parsing exists for all graphs, it goes through an intermediate graph with a large interface. Instead, the graphs of treewidth at most $k$ are exactly those for which we can find a parsing where all intermediate graphs have at most $k + 1$ sources (Proposition 4.1, [1,
<figure><img src="image_3.png" /><figcaption>Figure 1 Two parsings of a given graph.</figcaption></figure>

to capture precisely the graphs up to a given treewidth, while finite restrictions of their axiomatisation seem to be incomplete.

This brings them to the following question [7, p. 118]: for a given bound $k$, is there a finite equational presentation of graphs of treewidth at most $k$? The case of $k = 1$ concerns forests and is relatively easy. The case of $k = 2$ has been given a solution a few years ago [5, 9]. Here we give a positive answer for $k = 3$: we provide a syntax of terms with an interpretation map $g$ from terms to graphs whose image is exactly the set of graphs of treewidth at most three, and we give a finite list of equations whose equational theory ($\equiv$) characterises graph isomorphism ($\simeq$). In symbols, we prove that for all terms $t, u$,

$$g(t) \simeq g(u) \quad \text{if and only if} \quad t \equiv u$$

Like Arnborg, Courcelle, Proskurowski and Seese [1], we work with hypergraphs with a list of designated vertices, the *sources*, used as an interface to perform the following operations:

- *parallel composition* ($\parallel$): glue the graphs together along their sources.

- *permutation* (*pG*): given a permutation *p*, reorder the sources of *G* according to *p*.

- *lift* (*lG*): add an isolated vertex to *G* and append it as last source.

- *forget* (*fG*): remove the last source of *G* (keeping it as a mere vertex of the graph).

Consider the four graphs depicted in Figure 1, each with three sources denoted with numbered squares. The neighbours of each edge are ordered, which we indicate by drawing an arrow from the first to the second neighbour. The first graph on the left is the parallel composition of the three other ones. The second one can be obtained from a binary edge *a* (with interface its endpoints) by applying a lift to add a third isolated source and then swapping the last two sources: (23)la. The third one can be obtained from a ternary edge *b* (again with interface its endpoints), by forgetting the third source and adding a fresh one via a lift: lfb. The last one can be constructed as $f((24)lc \parallel (14)ld)$: reasoning top-down, we promote the inner vertex as a fourth source, and then we put in parallel two graphs each with a single ternary edge connecting three out of the four sources—both being obtained as appropriate permutations of lifted edges.

We call *parsings* the expressions we obtain when decomposing graphs as above.

The way we parsed the graph on the right generalises to all graphs: first promote all inner vertices as sources, and then build a large parallel composition of appropriately permuted and lifted edges. For instance, the first graph on the left also admits the following parsing:

$$ff((23)llla \parallel (35)llb \parallel (24)llc \parallel (124)lld)$$

While such a parsing exists for all graphs, it goes through an intermediate graph with a large interface. Instead, the graphs of treewidth at most $k$ are exactly those for which we can find a parsing where all intermediate graphs have at most $k + 1$ sources (Proposition 4.1, [1,
Proposition 4.1)). This syntax for denoting precisely the graphs of treewidth at most *k* is the starting point for the present work.

A derived operation is of particular interest. Consider three graphs *x*, *y*, *z* each with three sources, and combine them as depicted on the right to obtain a new graph ◦(*x*, *y*, *z*). This operation can be defined from the previous ones using the expression below.

<figure><img src="image_3.png" /></figure>

$$ \circled{0}(x, y, z) \triangleq f((14)lx \parallel (24)ly \parallel (34)lz) $$

It can be generalised into a *n*-ary operation on graphs with *n* sources, and when *n* = 2 we recover the usual notion of *series composition* (with its arguments reversed).

Our goal is then to understand which laws are satisfied by the previous operations. Amongst the natural ones, we have that parallel composition is associative and commutative, that permutations commute over parallel compositions, and that applying two permutations in a row amounts to applying the composite permutation. There are more involved ones. For instance, we may also parse the first graph of Figure 1 by keeping edges *a* and *c* together as long as possible, resulting in the expression written below it. We thus have two rather different parsings for the same graph, which our axiomatisation should equate.

We proceed in two steps. First we use connectivity arguments in order to decompose any graph into a parallel composition of permuted lifts of *full prime graphs*: non-empty graphs which are connected through paths not using sources except possibly at their endpoints. Figure 1 actually provided an example of such a decomposition, which is always unique for a given graph. Using a few natural axioms, we show that every term can be rewritten under such a form (Proposition 5.1). This makes it possible to focus on full prime graphs in the second step, which is where the main difficulties arise.

A key property of full prime graphs of bounded treewidth is that either they are *atomic* (i.e., reduced to a permutation of an edge), or they have a *forget point*: at least one of their inner vertices can be promoted into a source without increasing the treewidth, thus making it possible to parse the graph as a *forget operation*. The difficulty is that forget points are not unique, resulting in several ways of parsing non-atomic full prime graphs. Consider for instance the following tetrahedron on the left, with only two vertices marked as sources.

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

Each of the two inner vertices is a *forget point*, so that modulo appropriate permutations of edges, we may parse this graph as $f(\circled{0}(a, b, c) \parallel d)$ or as $f(\circled{0}(a, b, d) \parallel c)$. In this case, the two forget points are relatively close, and one of our axioms makes it possible to jump directly from one parsing to the other. A similar situation arises with the graph given on the right.

The cornerstone of our completeness proof is the fact that two parsings of a non-atomic full prime graph can always be rewritten so as to agree on their forget point. This is Lemma 5.4, and most of the paper is devoted to proving it.

To do so, we first delimit a class of vertices which we call *anchors*. Those can be thought of as a generalisation of cutvertices [10, Section 1.4]. When a full prime graph has an anchor, we show that we can use it as a universal agreement point (Lemma 7.1).
Proposition 4.1]). This syntax for denoting precisely the graphs of treewidth at most $k$ is the starting point for the present work.

A derived operation is of particular interest. Consider three graphs $x, y, z$ each with three sources, and combine them as depicted on the right to obtain a new graph $\circ(x, y, z)$. This operation can be defined from the previous ones using the expression below.

<figure><img src="image_4.png" /></figure>

$$ \circ(x, y, z) \triangleq f((14)lx \parallel (24)ly \parallel (34)lz) $$

It can be generalised into a $n$-ary operation on graphs with $n$ sources, and when $n = 2$ we recover the usual notion of *series composition* (with its arguments reversed).

Our goal is then to understand which laws are satisfied by the previous operations. Amongst the natural ones, we have that parallel composition is associative and commutative, that permutations commute over parallel compositions, and that applying two permutations in a row amounts to applying the composite permutation. There are more involved ones. For instance, we may also parse the first graph of Figure 1 by keeping edges $a$ and $c$ together as long as possible, resulting in the expression written below it. We thus have two rather different parsings for the same graph, which our axiomatisation should equate.

We proceed in two steps. First we use connectivity arguments in order to decompose any graph into a parallel composition of permuted lifts of *full prime graphs*: non-empty graphs which are connected through paths not using sources except possibly at their endpoints. Figure 1 actually provided an example of such a decomposition, which is always unique for a given graph. Using a few natural axioms, we show that every term can be rewritten under such a form (Proposition 5.1). This makes it possible to focus on full prime graphs in the second step, which is where the main difficulties arise.

A key property of full prime graphs of bounded treewidth is that either they are *atomic* (i.e., reduced to a permutation of an edge), or they have a *forget point*: at least one of their inner vertices can be promoted into a source without increasing the treewidth, thus making it possible to parse the graph as a *forget operation*. The difficulty is that forget points are not unique, resulting in several ways of parsing non-atomic full prime graphs. Consider for instance the following tetrahedron on the left, with only two vertices marked as sources.

<figure><img src="image_5.png" /></figure>

<figure><img src="image_6.png" /></figure>

Each of the two inner vertices is a *forget point*, so that modulo appropriate permutations of edges, we may parse this graph as $f(\circ(a, b, c) \parallel d)$ or as $f(\circ(a, b, d) \parallel c)$. In this case, the two forget points are relatively close, and one of our axioms makes it possible to jump directly from one parsing to the other. A similar situation arises with the graph given on the right.

The cornerstone of our completeness proof is the fact that two parsings of a non-atomic full prime graph can always be rewritten so as to agree on their forget point. This is Lemma 5.4, and most of the paper is devoted to proving it.

To do so, we first delimit a class of vertices which we call *anchors*. Those can be thought of as a generalisation of cutvertices [8, Section 1.4]. When a full prime graph has an anchor, we show that we can use it as a universal agreement point (Lemma 7.1).
<figure><img src="image_6.png" /><figcaption>■ **Figure 2** Separation pairs and graphs with several separation pairs.</figcaption></figure>

Unfortunately, there are graphs without anchors. We call them *hard*, they can be thought of as specific unseparable graphs [10, Section 1.4]. The rest of the proof consists in a structural analysis of hard graphs of treewidth at most three. We show that they admit *separation pairs*: every hard graph has the shape on the left of Figure 2, and every parsing can be rewritten as a double forget on some of these separation pairs (Lemma 8.5). However, as illustrated on the right, separation pairs are not unique. In order to finish the proof, we analyse how separation pairs relate to each other. There are easy cases like in the second graph of Figure 2 where the diagonal separation pair connects the two vertical ones, and previously encountered axioms make it possible to conclude. By analysing the shape of graphs excluding the triangle between their sources as a minor (Proposition 8.7—note that cycles may still appear in such graphs), we show that all other situations reduce to one of the two graphs on the right of Figure 2. There, the two outer-vertical pairs of inner vertices are the only separation pairs, and they are disjoint. They correspond to distinct parsings of the same graph, and we must include the corresponding equations to complete our list of axioms.

For the sake of readability, some proofs and details are deferred to the appendix. Statement headers contain hyperlinks to ease navigation.

**2 Graphs, treewidth**

A *ranked set* (or *signature*) is a set where every element has an associated natural number called its *arity*. Throughout the paper we fix a ranked set $\Sigma$ of *letters*, which we call the *alphabet*. Given a set $V$, we denote by $\mathcal{L}(V)$ the ranked set of duplicate-free lists over $V$, where the arity of a list is its length.

We consider labelled and ordered hypergraphs with interfaces, defined as follows:

**Definition 2.1.** A graph is a tuple $(V, E, n, l, i)$ where $V$ is a finite set of vertices, $E$ is a finite ranked set of edges, $i \in \mathcal{L}(V)$ is the interface, and $n: E \to \mathcal{L}(V)$ and $l: E \to \Sigma$ are arity-preserving functions respectively giving the neighbours and the label of each edge.

The *elements* of a graph are its vertices and edges. The vertices appearing in the interface of a graph are its *sources*. Vertices (resp. elements) which are not sources are called *inner vertices* (resp. *elements*). A vertex is *isolated* if it is not in the neighbourhood of any edge. The *size* of a graph $G$, written $|G|$, is its number of elements. The *arity* of a graph is that of its interface. Two graphs $G, H$ are *isomorphic*, written $G \simeq H$, if their vertex and edge sets are related by structure-preserving bijections (cf. Appendix A). A graph is:

- *empty* if its only elements are its sources;

- *atomic* if its only inner element is an edge, whose neighbours comprise all the sources.

Our choice of considering ordered hypergraphs with interfaces comes from the need to be able to substitute graphs for edges. A *substitution* is an arity-preserving function from the alphabet to graphs. Given a graph $G$ and a substitution $\sigma$, we write $G\sigma$ for the graph obtained from $G$ by replacing all its $a$-labelled edges by copies of the graph $\sigma(a)$, identifying pairwise the neighbours of the edges with the interfaces of the copies. We say that $G$ has
<figure><img src="image_7.png" /><figcaption>■ **Figure 2** Separation pairs and graphs with several separation pairs.</figcaption></figure>

Unfortunately, there are graphs without anchors. We call them *hard*, they can be thought of as specific unseparable graphs [8, Section 1.4]. The rest of the proof consists in a structural analysis of hard graphs of treewidth at most three. We show that they admit *separation pairs*: every hard graph has the shape on the left of Figure 2, and every parsing can be rewritten as a double forget on some of these separation pairs (Lemma 8.5). However, as illustrated on the right, separation pairs are not unique. In order to finish the proof, we analyse how separation pairs relate to each other. There are easy cases like in the second graph of Figure 2 where the diagonal separation pair connects the two vertical ones, and previously encountered axioms make it possible to conclude. By analysing the shape of graphs excluding the triangle between their sources as a minor (Proposition 8.7—note that cycles may still appear in such graphs), we show that all other situations reduce to one of the two graphs on the right of Figure 2. There, the two outer-vertical pairs of inner vertices are the only separation pairs, and they are disjoint. They correspond to distinct parsings of the same graph, and we must include the corresponding equations to complete our list of axioms.

For the sake of readability, some proofs and details are deferred to the appendix. Statement headers contain hyperlinks to ease navigation.

## 2 Graphs, treewidth

A *ranked set* (or *signature*) is a set where every element has an associated natural number called its *arity*. Throughout the paper we fix a ranked set $\Sigma$ of *letters*, which we call the *alphabet*. Given a set $V$, we denote by $\mathcal{L}(V)$ the ranked set of duplicate-free lists over $V$, where the arity of a list is its length.

We consider labelled and ordered hypergraphs with interfaces, defined as follows:

**Definition 2.1.** A graph is a tuple $(V, E, n, l, i)$ where $V$ is a finite set of vertices, $E$ is a finite ranked set of edges, $i \in \mathcal{L}(V)$ is the interface, and $n: E \to \mathcal{L}(V)$ and $l: E \to \Sigma$ are arity-preserving functions respectively giving the neighbours and the label of each edge.

The *elements* of a graph are its vertices and edges. The vertices appearing in the interface of a graph are its *sources*. Vertices (resp. elements) which are not sources are called *inner vertices* (resp. *elements*). A vertex is *isolated* if it is not in the neighbourhood of any edge. The *size* of a graph $G$, written $|G|$, is its number of elements. The *arity* of a graph is that of its interface. Two graphs $G, H$ are *isomorphic*, written $G \simeq H$, if their vertex and edge sets are related by structure-preserving bijections (cf. Appendix A). A graph is:

- *empty* if its only elements are its sources;

- *atomic* if its only inner element is an edge, whose neighbours comprise all the sources.

Our choice of considering ordered hypergraphs with interfaces comes from the need to be able to substitute graphs for edges. A *substitution* is an arity-preserving function from the alphabet to graphs. Given a graph $G$ and a substitution $\sigma$, we write $G\sigma$ for the graph obtained from $G$ by replacing all its $a$-labelled edges by copies of the graph $\sigma(a)$, identifying pairwise the neighbours of the edges with the interfaces of the copies. We say that $G$ has
shape $H$ when $G \simeq H\sigma$ for some substitution $\sigma$. For instance, the first graph of Figure 1 has
the following shapes (amongst other ones):

<figure><img src="image_7.png" /></figure>

(Note that the edge orientation is irrelevant in a graph used as a shape, as well as the labelling function—as long as it is injective, which will always be the case in the present paper.)

**Proposition 2.2.** For all graphs $G, H$ and all substitutions $\sigma, \rho$, if $G \simeq H$ and $\sigma(a) \simeq \rho(a)$ for all letters $a$, then $G\sigma \simeq H\rho$.

A graph in the sense of Definition 2.1 can be seen as a simple graph, its skeleton, by turning all its edges and its interface into cliques (removing duplicate edges if necessary). This operation makes it possible to use the standard notion of treewidth [10, Section 12.4]: the treewidth of a graph is that of its skeleton. Equivalently, we can define it as follows.

**Definition 2.3.** A tree decomposition of a graph is a tree whose nodes are labelled by sets of vertices, called bags, such that

- there is a bag containing all sources,

- for each edge there is a bag containing its neighbours,

- for each vertex, the bags containing it form a subtree.

The width of a tree decomposition is the size of its largest bag minus one. The treewidth of a graph is the minimal width of its possible tree decompositions.

Observe that since the sources of a graph must be contained in a bag for all tree decompositions, the treewidth of a graph is at least its arity minus one. Therefore, at treewidth at most three, we only have graphs of arity up to four. The same constraint holds for the edge arities.

**Proposition 2.4.** If a graph $G$ and the graphs in the image of a substitution $\sigma$ all have treewidth at most $k$, then so does $G\sigma$.

# 3 Graph operations

We can now define the operations discussed in the introduction.

**Definition 3.1.** Let $G, H$ be graphs of arity $k$.

- The parallel composition of $G$ and $H$, $G \parallel H$, is the graph of arity $k$ obtained from the disjoint union of $G$ and $H$ by pairwise merging their sources.

- If $k \ge 1$, the forget of $G$, $fG$, is the graph of arity $k-1$ obtained from $G$ by removing the last vertex from its interface (keeping it in the vertex set).

- The lift of $G$, $lG$, is the graph of arity $k+1$ obtained from $G$ by adding a new isolated vertex, and appending it to its interface.

- For a permutation $p$ of $[1, k]$, we denote by $pG$ the graph obtained from $G$ by permuting its interface according to $p$.

- We write $\emptyset_k$ for the empty graph of arity $k$, omitting $k$ when it is clear from the context.

- For a letter $a \in \Sigma$, we also write $a$ for the atomic graph whose edge is labelled $a$ and has its neighbours appearing in the same order as in the interface.
shape $H$ when $G \simeq H\sigma$ for some substitution $\sigma$. For instance, the first graph of Figure 1 has
the following shapes (amongst other ones):

<figure><img src="image_8.png" /></figure>

(Note that the edge orientation is irrelevant in a graph used as a shape, as well as the labelling function—as long as it is injective, which will always be the case in the present paper.)

**Proposition 2.2.** For all graphs $G, H$ and all substitutions $\sigma, \rho$, if $G \simeq H$ and $\sigma(a) \simeq \rho(a)$ for all letters $a$, then $G\sigma \simeq H\rho$.

A graph in the sense of Definition 2.1 can be seen as a simple graph, its *skeleton*, by turning all its edges and its interface into cliques (removing duplicate edges if necessary). This operation makes it possible to use the standard notion of treewidth [8, Section 12.4]: the *treewidth* of a graph is that of its skeleton. Equivalently, we can define it as follows.

**Definition 2.3.** A tree decomposition of a graph is a tree whose nodes are labelled by sets of vertices, called bags, such that

- there is a bag containing all sources,

- for each edge there is a bag containing its neighbours,

- for each vertex, the bags containing it form a subtree.

The width of a tree decomposition is the size of its largest bag minus one. The treewidth of a graph is the minimal width of its possible tree decompositions.

Observe that since the sources of a graph must be contained in a bag for all tree decompositions, the treewidth of a graph is at least its arity minus one. Therefore, at treewidth at most three, we only have graphs of arity up to four. The same constraint holds for the edge arities.

**Proposition 2.4.** If a graph $G$ and the graphs in the image of a substitution $\sigma$ all have treewidth at most $k$, then so does $G\sigma$.

# 3 Graph operations

We can now define the operations discussed in the introduction.

**Definition 3.1.** Let $G, H$ be graphs of arity $k$.

- The parallel composition of $G$ and $H$, $G \parallel H$, is the graph of arity $k$ obtained from the disjoint union of $G$ and $H$ by pairwise merging their sources.

- If $k \ge 1$, the *forget of* $G$, $fG$, is the graph of arity $k-1$ obtained from $G$ by removing the last vertex from its interface (keeping it in the vertex set).

- The *lift* of $G$, $lG$, is the graph of arity $k+1$ obtained from $G$ by adding a new isolated vertex, and appending it to its interface.

- For a permutation $p$ of $[1, k]$, we denote by $pG$ the graph obtained from $G$ by permuting its interface according to $p$.

- We write $\emptyset_k$ for the empty graph of arity $k$, omitting $k$ when it is clear from the context.

- For a letter $a \in \Sigma$, we also write $a$ for the atomic graph whose edge is labelled $a$ and has its neighbours appearing in the same order as in the interface.
# 6 A finite presentation of graphs of treewidth at most three

These operations all arise as substitutions of well chosen small graphs. By Proposition 2.4, this entails that they preserve treewidth (except of course for lifts, which may increase it when reaching the maximal arity). It remains to establish a few structural properties, in order to show that every graph of treewidth at most $k$ can be constructed from the above operations up to arity $k+1$ (Proposition 4.1 below).

A *path* in a graph is a sequence of elements such that any two consecutive elements consist of an edge and one of its neighbours. An *inner path* is a path made only of inner elements, except possibly for the endpoints.

**Definition 3.2.** A graph is prime if it is not empty and all its inner elements are connected by inner paths; it is full if none of its sources are isolated.

Observe that a graph is full prime iff all its elements are connected by inner paths. Amongst the graphs in Figure 1, the first one is full but not prime, the three other ones are prime, and only the last one is full prime.

**Lemma 3.3.** Every graph is isomorphic to a permutation of lifts of a full graph. This decomposition is unique up to permutation and isomorphism.

**Lemma 3.4.** Every graph is isomorphic to a parallel composition of prime graphs. This decomposition is unique up to reindexing and isomorphism.

We call (prime) components of a graph the prime graphs occurring in the latter decomposition. We call reduced components of a graph the full prime graphs obtained by removing isolated sources from its components.

We now give two key properties of full prime graphs of bounded treewidth. First, they are always atomic at maximal arity.

**Proposition 3.5.** Full prime graphs of treewidth at most $k$ and arity $k+1$ are atomic.

In the case of treewidth at most three, this means that when we decompose a graph of arity four into prime components, then except for a number of four-edges between the sources, we only get non-full components: drawing the graph as a tetrahedron between its sources, the non-atomic components are glued through the faces (or edges, or vertices, or nothing), and the interior of the tetrahedron remains empty. This corresponds to the characterisations of treewidth at most $k$ graphs as partial $k$-trees [2] or as subgraphs of chordal graphs whose cliques are of size at most $k+1$ [14].

Second, non-atomic full prime graphs have *forget points*, which we define as follows.

**Definition 3.6.** When $x$ is an inner vertex of a graph $G$, we write $(G, x)$ for the graph obtained from $G$ by appending $x$ to its interface; if this graph has treewidth at most $k$ then we say that $x$ is a $k$-forget point of $G$.

**Proposition 3.7.** Non-atomic full prime graphs of treewidth at most $k$ have $k$-forget points.

# 4 Terms and axioms

We finally provide a notion of term for denoting graphs. We use a multisorted syntax: the family $(\mathcal{T}_k)_{k \in \mathbb{N}}$ of sets of terms of a given arity is defined inductively by the following rules (where $p$ ranges over permutations of $[1, k]$ and $a$ over letters of arity $k$):

$$ \frac{t, u \in \mathcal{T}_k}{t \parallel u \in \mathcal{T}_k} $$

$$ \frac{t \in \mathcal{T}_k}{1t \in \mathcal{T}_{k+1}} $$

$$ \frac{t \in \mathcal{T}_{k+1}}{ft \in \mathcal{T}_k} $$

$$ \frac{t \in \mathcal{T}_k}{pt \in \mathcal{T}_k} $$

$$ \emptyset \in \mathcal{T}_k $$

$$ a \in \mathcal{T}_k $$
# 6 A finite presentation of graphs of treewidth at most three

These operations all arise as substitutions of well chosen small graphs. By Proposition 2.4, this entails that they preserve treewidth (except of course for lifts, which may increase it when reaching the maximal arity). It remains to establish a few structural properties, in order to show that every graph of treewidth at most $k$ can be constructed from the above operations up to arity $k+1$ (Proposition 4.1 below).

A *path* in a graph is a sequence of elements such that any two consecutive elements consist of an edge and one of its neighbours. An *inner path* is a path made only of inner elements, except possibly for the endpoints.

**Definition 3.2.** A graph is prime if it is not empty and all its inner elements are connected by inner paths; it is full if none of its sources are isolated.

Observe that a graph is full prime iff all its elements are connected by inner paths. Amongst the graphs in Figure 1, the first one is full but not prime, the three other ones are prime, and only the last one is full prime.

**Lemma 3.3.** Every graph is isomorphic to a permutation of lifts of a full graph. This decomposition is unique up to permutation and isomorphism.

**Lemma 3.4.** Every graph is isomorphic to a parallel composition of prime graphs. This decomposition is unique up to reindexing and isomorphism.

We call (prime) components of a graph the prime graphs occurring in the latter decomposition. We call reduced components of a graph the full prime graphs obtained by removing isolated sources from its components.

We now give two key properties of full prime graphs of bounded treewidth. First, they are always atomic at maximal arity.

**Proposition 3.5.** Full prime graphs of treewidth at most $k$ and arity $k+1$ are atomic.

In the case of treewidth at most three, this means that when we decompose a graph of arity four into prime components, then except for a number of four-edges between the sources, we only get non-full components: drawing the graph as a tetrahedron between its sources, the non-atomic components are glued through the faces (or edges, or vertices, or nothing), and the interior of the tetrahedron remains empty. This corresponds to the characterisations of treewidth at most $k$ graphs as partial $k$-trees [2] or as subgraphs of chordal graphs whose cliques are of size at most $k+1$ [12].

Second, non-atomic full prime graphs have *forget points*, which we define as follows.

**Definition 3.6.** When $x$ is an inner vertex of a graph $G$, we write $(G, x)$ for the graph obtained from $G$ by appending $x$ to its interface; if this graph has treewidth at most $k$ then we say that $x$ is a $k$-forget point of $G$.

**Proposition 3.7.** Non-atomic full prime graphs of treewidth at most $k$ have $k$-forget points.

# 4 Terms and axioms

We finally provide a notion of term for denoting graphs. We use a multisorted syntax: the family $(\mathcal{T}_k)_{k \in \mathbb{N}}$ of sets of terms of a given arity is defined inductively by the following rules (where $p$ ranges over permutations of $[1, k]$ and $a$ over letters of arity $k$):

$$ \frac{t, u \in \mathcal{T}_k}{t \parallel u \in \mathcal{T}_k} $$

$$ \frac{t \in \mathcal{T}_k}{1t \in \mathcal{T}_{k+1}} $$

$$ \frac{t \in \mathcal{T}_{k+1}}{ft \in \mathcal{T}_k} $$

$$ \frac{t \in \mathcal{T}_k}{pt \in \mathcal{T}_k} $$

$$ \emptyset \in \mathcal{T}_k $$

$$ a \in \mathcal{T}_k $$
This syntax matches the operations in Definition 3.1. Accordingly, we obtain a recursive
arity-preserving function *g* from terms to graphs. We say that a term *t* denotes the graph *G*,
or that *t* is a parsing of *G*, when *g*(*t*) ≅ *G*. For instance, the expressions below the graphs in
Figure 1, seen as terms, are parsings of these graphs. Note that the number of inner vertices
of a graph is the number of forgets appearing in any of its parsings.

We shall sometimes mention terms and refer implicitly to their graphs; for instance
writing that a term is prime to mean that its graph is so.

The width of a term is the maximal arity of its subterms, minus one.

**► Proposition 4.1.** A graph has treewidth at most *k* iff it has a parsing of width at most *k*.

Proof. The backward implication is proven by induction on terms, using Proposition 2.4 and the observation that all operations arise as substitutions. For the direct implication, we proceed by lexicographic induction on the size of the graph followed by *k* + 1 minus its arity (recall that the arity is always lower or equal to the treewidth plus one).

If the graph has isolated sources, we use Lemma 3.3 to write it as a permutation of lifts
and proceed recursively. Otherwise it is full, and we decompose it into primes via Lemma 3.4:

- if there are no components then the graph is empty and has a trivial parsing;

- if there are at least two components then they are smaller, and we proceed recursively;

- otherwise the graph is (full) prime; either it is atomic and it admits a permutation of a letter as a parsing, or, by Proposition 3.7, it can be written as the forget of a graph of the same size but increased arity, which we may parse recursively. ◀

The previous proposition holds for all bounds *k* on the treewidth. Some of our results below also hold generically, and we will discuss these generalisations in Section 9. Still, from this point on we focus on treewidth at most three.

**► Convention 4.2.** In the remainder, we only work with graphs of treewidth at most three. We simply call terms the terms of width at most three, and forget points the 3-forget points.

A (*term*) substitution is an arity-preserving function from the alphabet to terms. Such a
function $\sigma$ extends uniquely to a homomorphism $\hat{\sigma}$ from terms to terms:

$$
\begin{align*}
\hat{\sigma}(t \parallel u) &\triangleq \hat{\sigma}(t) \parallel \hat{\sigma}(u) & \hat{\sigma}(lt) &\triangleq l\hat{\sigma}(t) \\
\hat{\sigma}(\emptyset) &\triangleq \emptyset & \hat{\sigma}(ft) &\triangleq f\hat{\sigma}(t) \\
\hat{\sigma}(a) &\triangleq \sigma(a) & \hat{\sigma}(pt) &\triangleq p\hat{\sigma}(t)
\end{align*}
$$

A context of arity $i \to o$ is a term of arity $o$ with a single occurrence of a designated letter $h$
of arity $i$, called the *hole*. Given such a context $c$ and a term $t$ of arity $i$, we write $c[t]$ for
the term $c$ where the hole is replaced by $t$. Note that $c[t] = \hat{\sigma}_t(c)$ for the substitution $\sigma_t$
mapping $h$ to $t$ and fixing all other letters.

An *equational theory* is an equivalence relation *R* on terms, relating only terms of the
same arity, and which is closed under contexts and substitutions:

- $(t, u) \in R$ entails $(c[t], c[u]) \in R$ for all contexts $c$ of appropriate arity, and

- $(t, u) \in R$ entails $(\hat{\sigma}(t), \hat{\sigma}(u)) \in R$ for all substitutions $\sigma$.

Given two terms *t*, *u*, we write *t* ≅ *u* when *g*(*t*) ≅ *g*(*u*). Thanks to Proposition 2.2, this relation (≅) is an equational theory, and our goal is to provide a finite list of axioms that generates it.

We give such a list below; most axioms can be written explicitly, but three of them relate
rather large terms, which are best presented by their graphs. This is why we rely on the
following concept of forget axiom.
This syntax matches the operations in Definition 3.1. Accordingly, we obtain a recursive
arity-preserving function $g$ from terms to graphs. We say that a term $t$ denotes the graph $G$,
or that $t$ is a parsing of $G$, when $g(t) \simeq G$. For instance, the expressions below the graphs in
Figure 1, seen as terms, are parsings of these graphs. Note that the number of inner vertices
of a graph is the number of forgets appearing in any of its parsings.

We shall sometimes mention terms and refer implicitly to their graphs; for instance
writing that a term is prime to mean that its graph is so.

The width of a term is the maximal arity of its subterms, minus one.

**► Proposition 4.1.** A graph has treewidth at most *k* iff it has a parsing of width at most *k*.

**Proof.** The backward implication is proven by induction on terms, using Proposition 2.4 and the observation that all operations arise as substitutions. For the direct implication, we proceed by lexicographic induction on the size of the graph followed by $k + 1$ minus its arity (recall that the arity is always lower or equal to the treewidth plus one).

If the graph has isolated sources, we use Lemma 3.3 to write it as a permutation of lifts
and proceed recursively. Otherwise it is full, and we decompose it into primes via Lemma 3.4:

- if there are no components then the graph is empty and has a trivial parsing;

- if there are at least two components then they are smaller, and we proceed recursively;

- otherwise the graph is (full) prime; either it is atomic and it admits a permutation of a
letter as a parsing, or, by Proposition 3.7, it can be written as the forget of a graph of
the same size but increased arity, which we may parse recursively.

◀

The previous proposition holds for all bounds *k* on the treewidth. Some of our results below also hold generically, and we will discuss these generalisations in Section 9. Still, from this point on we focus on treewidth at most three.

**► Convention 4.2.** In the remainder, we only work with graphs of treewidth at most three. We simply call terms the terms of width at most three, and forget points the 3-forget points.

A (*term*) substitution is an arity-preserving function from the alphabet to terms. Such a
function $\sigma$ extends uniquely to a homomorphism $\hat{\sigma}$ from terms to terms:

$$
\begin{align*}
\hat{\sigma}(t \parallel u) &\triangleq \hat{\sigma}(t) \parallel \hat{\sigma}(u) & \hat{\sigma}(lt) &\triangleq l\hat{\sigma}(t) \\
\hat{\sigma}(\emptyset) &\triangleq \emptyset & \hat{\sigma}(ft) &\triangleq f\hat{\sigma}(t) \\
\hat{\sigma}(a) &\triangleq \sigma(a) & \hat{\sigma}(pt) &\triangleq p\hat{\sigma}(t)
\end{align*}
$$

A context of arity $i \to o$ is a term of arity $o$ with a single occurrence of a designated letter $h$
of arity $i$, called the *hole*. Given such a context $c$ and a term $t$ of arity $i$, we write $c[t]$ for
the term $c$ where the hole is replaced by $t$. Note that $c[t] = \hat{\sigma}_t(c)$ for the substitution $\sigma_t$
mapping $h$ to $t$ and fixing all other letters.

An *equational theory* is an equivalence relation *R* on terms, relating only terms of the
same arity, and which is closed under contexts and substitutions:

- $(t, u) \in R$ entails $(c[t], c[u]) \in R$ for all contexts $c$ of appropriate arity, and

- $(t, u) \in R$ entails $(\hat{\sigma}(t), \hat{\sigma}(u)) \in R$ for all substitutions $\sigma$.

Given two terms $t, u$, we write $t \cong u$ when $g(t) \simeq g(u)$. Thanks to Proposition 2.2, this
relation ($\cong$) is an equational theory, and our goal is to provide a finite list of axioms that
generates it.

We give such a list below; most axioms can be written explicitly, but three of them relate
rather large terms, which are best presented by their graphs. This is why we rely on the
following concept of forget axiom.
<figure><img src="image_8.png" /><figcaption>Figure 3 Forget axioms for anchors (swap and kite); x, y are the inner vertices.</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Figure 4 Forget axioms for hard graphs (cross and domino); x, y are the topmost inner vertices.</figcaption></figure>

A forget axiom for a graph $G$ with two forget points $x, y$ is an equation of the shape $ft \equiv fu$ for some parsings $t$ of $(G, x)$ and $u$ of $(G, y)$.

**► Definition 4.3 (Finite axiomatisation).** We write $\equiv$ for the least equational theory containing the following axioms, for letters $a, b, c$ of appropriate arities:

$$ \mathbf{A1.} \quad a \parallel (b \parallel c) \equiv (a \parallel b) \parallel c, a \parallel b \equiv b \parallel a, \text{ and } a \parallel \emptyset \equiv a; $$

$$ \mathbf{A2.} \quad pqa \equiv (p \circ q)a \text{ for all permutations } p, q, \text{ and } ida \equiv a \text{ where id is the identity permutation;} $$

$$ \mathbf{A3.} \quad p(a \parallel b) \equiv pa \parallel pb \text{ and } p\emptyset \equiv \emptyset \text{ for all permutations } p; $$

$$ \mathbf{A4.} \quad l(a \parallel b) \equiv la \parallel lb \text{ and } l\emptyset \equiv \emptyset; $$

$$ \mathbf{A5.} \quad pfa \equiv f\dot{p}a \text{ and } lpa \equiv \dot{l}pa \text{ where } \dot{p} \text{ is the extension of a permutation } p \text{ of } [1, k] \text{ to } [1, k+1]; $$

$$ \mathbf{A6.} \quad lfa \equiv frla \text{ and } lla \equiv rlla \text{ for the permutation } r \text{ that swaps the last two elements;} $$

$$ \mathbf{A7.} \quad fa \parallel b \equiv f(a \parallel lb); $$

**FS.** $ffa \equiv f\dot{f}ra$ for the permutation $r$ that swaps the last two elements; as well as three forget axioms for the graphs with forget points **FK**, **FX** and **FD** in Figures 3&4 (for some arbitrary choice of interface ordering, edge orientation, and injective edge labelling).

The first eight items are universally quantified over all appropriate arities. For instance, associativity of parallel composition (in **A1**) is an axiom at each arity, and $a, b$ and $\emptyset$ may have arity up to three in **A4**. Since we restrict globally to arities up to four, the list of axioms is nevertheless finite.

Also note that even though the axioms are expressed using letters, they yield laws which hold under all term substitutions since $\equiv$ is defined as an equational theory.

**FS** comprises three axioms depending on the arity of $a$ (2, 3, or 4), which we shall sometimes refer to as $FS_i$ (with $i = 0, 1$, or 2, respectively). These are forget axioms for the first three graphs in Figure 3, and we could have presented them as such. We cannot express $FS_3$ as it would require an edge of arity five; **FK** intuitively is a weakened version of it, expressible at treewidth three.

We shall see at the end of Section 5 that the concrete choice of parsings for the forget axioms **FK**, **FX**, and **FD** is irrelevant thanks to **A1-7**. The interested reader may find concrete equations for them in Appendix C.

**► Proposition 4.4 (Soundness).** If $t \equiv u$ then $t \cong u$.

**Proof.** Since $\cong$ is an equational theory, it suffices to check that the two members of each axiom denote the same graph. This is by definition for the forget axioms, and a routine verification for the other ones.

<figure><img src="image_10.png" /></figure>
<figure><img src="image_9.png" /><figcaption>Figure 3 Forget axioms for anchors (swap and kite); x, y are the inner vertices.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Figure 4 Forget axioms for hard graphs (cross and domino); x, y are the topmost inner vertices.</figcaption></figure>

A forget axiom for a graph $G$ with two forget points $x, y$ is an equation of the shape $ft \equiv fu$ for some parsings $t$ of $(G, x)$ and $u$ of $(G, y)$.

**► Definition 4.3 (Finite axiomatisation).** We write $\equiv$ for the least equational theory containing the following axioms, for letters $a, b, c$ of appropriate arities:

$$ \text{A1. } a \parallel (b \parallel c) \equiv (a \parallel b) \parallel c, a \parallel b \equiv b \parallel a, \text{ and } a \parallel \emptyset \equiv a; $$

$$ \text{A2. } pqa \equiv (p \circ q)a \text{ for all permutations } p, q, \text{ and } ida \equiv a \text{ where id is the identity permutation;} $$

$$ \text{A3. } p(a \parallel b) \equiv pa \parallel pb \text{ and } p\emptyset \equiv \emptyset \text{ for all permutations } p; $$

$$ \text{A4. } l(a \parallel b) \equiv la \parallel lb \text{ and } l\emptyset \equiv \emptyset; $$

$$ \text{A5. } pfa \equiv f\dot{p}a \text{ and } lpa \equiv \dot{l}pa \text{ where } \dot{p} \text{ is the extension of a permutation } p \text{ of } [1, k] \text{ to } [1, k+1]; $$

$$ \text{A6. } lfa \equiv frla \text{ and } lla \equiv rlla \text{ for the permutation } r \text{ that swaps the last two elements;} $$

$$ \text{A7. } fa \parallel b \equiv f(a \parallel lb); $$

**FS.** $ffa \equiv f\dot{f}ra$ for the permutation $r$ that swaps the last two elements; as well as three forget axioms for the graphs with forget points **FK**, **FX** and **FD** in Figures 3&4 (for some arbitrary choice of interface ordering, edge orientation, and injective edge labelling).

The first eight items are universally quantified over all appropriate arities. For instance, associativity of parallel composition (in **A1**) is an axiom at each arity, and $a, b$ and $\emptyset$ may have arity up to three in **A4**. Since we restrict globally to arities up to four, the list of axioms is nevertheless finite.

Also note that even though the axioms are expressed using letters, they yield laws which hold under all term substitutions since $\equiv$ is defined as an equational theory.

**FS** comprises three axioms depending on the arity of $a$ (2, 3, or 4), which we shall sometimes refer to as $FS_i$ (with $i = 0, 1$, or 2, respectively). These are forget axioms for the first three graphs in Figure 3, and we could have presented them as such. We cannot express $FS_3$ as it would require an edge of arity five; **FK** intuitively is a weakened version of it, expressible at treewidth three.

We shall see at the end of Section 5 that the concrete choice of parsings for the forget axioms **FK**, **FX**, and **FD** is irrelevant thanks to **A1-7**. The interested reader may find concrete equations for them in Appendix C.

**► Proposition 4.4 (Soundness).** If $t \equiv u$ then $t \cong u$.

**Proof.** Since $\cong$ is an equational theory, it suffices to check that the two members of each axiom denote the same graph. This is by definition for the forget axioms, and a routine verification for the other ones.

<figure><img src="image_11.png" /></figure>
The axioms given textually in Definition 4.3 (A1-7 and FS) intuitively correspond to
those given for arbitrary graphs by Courcelle and Engelfriet [9, p.117], restricted to terms of
width at most three. (Modulo some translation since our syntaxes and sets of operations
differ.) This finite restriction is however incomplete for graphs of treewidth at most three: in
their completeness proof, Courcelle and Engelfriet need axioms of the form $FS_i$ for arbitrary
large arity $i$, even when dealing with graphs of small treewidth. Somehow, we prove below
that the forget axioms $FS_0$, $FS_1$, $FS_2$, $FK$, $FX$, and $FD$ suffice at treewidth at most three
to fulfil the role played by this infinite family of axioms. Also observe that while $FK$ easily
generalises to deal with an arbitrary treewidth $k$ (by replacing the source touching the three
edges by $k-2$ sources), this is not the case for $FX$ and $FD$.

**5 Outline of the completeness proof**

Using the first seven axioms, we easily obtain the following proposition. Together with Lemmas 3.3 and 3.4, it makes it possible to normalise terms and to focus on full prime ones.

► **Proposition 5.1.** For all terms $t$, letters $a$, and graphs $G, H$, we have:

1. if $g(t) \cong \emptyset$ then $t \equiv \emptyset$;

2. if $g(t) \cong a$ then $t \equiv a$;

3. if $g(t) \cong pG$ then there is a parsing $u$ of $G$ such that $t \equiv pu$;

4. if $g(t) \cong lG$ then there is a parsing $u$ of $G$ such that $t \equiv lu$;

5. if $g(t) \cong G \parallel H$ then there are parsings $u$ of $G$ and $v$ of $H$ such that $t \equiv u \parallel v$.

**Proof sketch.** All items but the third are proven by induction on $t$. The first three items
only need A1-4; the fourth one needs A5-6; the last one rests on the fourth one and A7. ◀

An item is patently missing from the previous proposition, for the forget operation. In
fact, a statement similar to the third and fourth items does not hold for the forget operation:
when $t$ is a parsing of $fG$, nothing guarantees that $G$ has a parsing at all: its treewidth may
be four; we need to restrict to those cases where the forgotten vertex is a forget point.

Given a term $t$ denoting a graph $G$ with an inner vertex $x$, we say that $t$ reaches $x$ if
there is a parsing $t'$ of $(G, x)$ such that $t \equiv ft'$. We can easily prove the following property.

► **Lemma 5.2.** Every non-atomic full prime term reaches some forget point.

**Proof.** By induction on $t$, using Proposition 5.1 until we find a forget operation. ◀

<figure><img src="image_11.png" /></figure>

However, this property is not enough, because it gives no control on the forget point which
is reached; instead, we would like to obtain:

► **Statement 5.3 (Reaching forget points).** Full prime terms reach all their forget points.

This statement holds, but we do not know how to prove it directly: we only get it a *posteriori*,
from the completeness. We prove a variant of it in the next section (Lemma 7.1), for *anchors*.

Instead, the cornerstone of our proof is the following lemma: any two parsings of a
non-atomic full prime graph may reach a common forget point.

► **Lemma 5.4 (Forget point agreement).** For all parsings $t, u$ of a non-atomic full prime graph, there is a forget point reached by both $t$ and $u$.

The rest of the paper is devoted to proving this lemma, with which we conclude as follows.

► **Theorem 5.5 (Completeness).** For all parsings $t, u$ of a given graph, we have $t \equiv u$.
The axioms given textually in Definition 4.3 (A1-7 and FS) intuitively correspond to those given for arbitrary graphs by Courcelle and Engelfriet [7, p.117], restricted to terms of width at most three. (Modulo some translation since our syntaxes and sets of operations differ.) This finite restriction is however incomplete for graphs of treewidth at most three: in their completeness proof, Courcelle and Engelfriet need axioms of the form $FS_i$ for arbitrary large arity $i$, even when dealing with graphs of small treewidth. Somehow, we prove below that the forget axioms $FS_0$, $FS_1$, $FS_2$, $FK$, $FX$, and $FD$ suffice at treewidth at most three to fulfil the role played by this infinite family of axioms. Also observe that while $FK$ easily generalises to deal with an arbitrary treewidth $k$ (by replacing the source touching the three edges by $k-2$ sources), this is not the case for $FX$ and $FD$.

**5 Outline of the completeness proof**

Using the first seven axioms, we easily obtain the following proposition. Together with Lemmas 3.3 and 3.4, it makes it possible to normalise terms and to focus on full prime ones.

**Proposition 5.1.** For all terms $t$, letters $a$, and graphs $G, H$, we have:

1. if $g(t) \simeq \emptyset$ then $t \equiv \emptyset$;

2. if $g(t) \simeq a$ then $t \equiv a$;

3. if $g(t) \simeq pG$ then there is a parsing $u$ of $G$ such that $t \equiv pu$;

4. if $g(t) \simeq lG$ then there is a parsing $u$ of $G$ such that $t \equiv lu$;

5. if $g(t) \simeq G \parallel H$ then there are parsings $u$ of $G$ and $v$ of $H$ such that $t \equiv u \parallel v$.

**Proof sketch.** All items but the third are proven by induction on $t$. The first three items only need A1-4; the fourth one needs A5-6; the last one rests on the fourth one and A7. ◀

An item is patently missing from the previous proposition, for the forget operation. In fact, a statement similar to the third and fourth items does not hold for the forget operation: when $t$ is a parsing of $fG$, nothing guarantees that $G$ has a parsing at all: its treewidth may be four; we need to restrict to those cases where the forgotten vertex is a forget point.

Given a term $t$ denoting a graph $G$ with an inner vertex $x$, we say that $t$ reaches $x$ if there is a parsing $t'$ of $(G, x)$ such that $t \equiv ft'$. We can easily prove the following property.

**Lemma 5.2.** Every non-atomic full prime term reaches some forget point.

**Proof.** By induction on $t$, using Proposition 5.1 until we find a forget operation. ◀

<figure><img src="image_12.png" /></figure>

However, this property is not enough, because it gives no control on the forget point which is reached; instead, we would like to obtain:

**Statement 5.3 (Reaching forget points).** Full prime terms reach all their forget points.

This statement holds, but we do not know how to prove it directly: we only get it a *posteriori*, from the completeness. We prove a variant of it in the next section (Lemma 7.1), for *anchors*.

Instead, the cornerstone of our proof is the following lemma: any two parsings of a non-atomic full prime graph may reach a common forget point.

**Lemma 5.4 (Forget point agreement).** For all parsings $t, u$ of a non-atomic full prime graph, there is a forget point reached by both $t$ and $u$.

The rest of the paper is devoted to proving this lemma, with which we conclude as follows.

**Theorem 5.5 (Completeness).** For all parsings $t, u$ of a given graph, we have $t \equiv u$.
<figure><img src="image_12.png" /><figcaption>Figure 5 The series operations $s(\cdot; d)$, $s(a; d)$, $s(a, b; d)$, and $s(a, b, c; d)$.</figcaption></figure>

**Proof.** We follow the same pattern as in the proof of the forward implication of Proposition 4.1: we proceed by lexicographic induction on the size of the graph followed by 4 minus its arity. If the graph has isolated sources, we use Lemma 3.3 and Proposition 5.1(3,4) to rewrite the parsings into permuted lifts and proceed recursively. Otherwise it is full, and we decompose it into primes via Lemma 3.4:

- if there are no components then both parsings are equivalent to $\emptyset$ by Proposition 5.1(1);

- if there are at least two components then we use Proposition 5.1(5) on both parsings and we proceed recursively.

- otherwise the graph must be (full) prime. Either it is atomic and we conclude by Proposition 5.1(2,3), or Lemma 5.4 gives us two terms $t'$, $u'$ such that $t \equiv f(t')$, $t' \cong u'$, and $f(u') \equiv u$, and we can conclude since $t' \cong u'$ follows by induction hypothesis. ◀

We have only used Axioms A1-7 up to this point. We prove below that those axioms are complete when there are few forget points. Say that a graph is *easy* if each of its non-atomic reduced components $G$ has only one forget point $x$, and in turn $(G, x)$ is easy. (This definition is well-founded by the same lexicographic ordering as we used in the above proof.)

**Proposition 5.6.** For all parsings $t, u$ of an easy graph, we have $t \equiv u$.

**Proof.** By adapting the previous completeness proof. Lemma 5.2 may replace Lemma 5.4 when we attain non-atomic full prime graphs: those are reduced components of the starting graph and since those have only one forget point, all their parsings reach that one. ◀

None of the graphs in Figures 3 and 4 are easy: they are all full prime, each with two forget points $x, y$ (plus two symmetrical ones for **FX** and **FD**). Nevertheless, adding either $x$ or $y$ to their interface makes them easy (cf. Lemma D.1). This is why the precise choice of parsings does not matter when we use them as forget axioms in Definition 4.3.

# 6 Series decompositions

As explained in the introduction, there is a *series* operation on graphs which plays an important role. We slightly generalise it here, and we show how to use it to analyse graphs with a forget point.

Given $k$ graphs $G_1, \dots, G_k$ of arity $k$ and a graph $H$ of arity $k+1$, we define the following graph of arity $k+1$, where $p_i$ denotes the permutation which swaps $i$ and $k+1$.

$$s(G_1, \dots, G_k; H) \triangleq p_1 l G_1 \parallel \dots \parallel p_k l G_k \parallel H$$

As is explicit from its definition, this operation on graphs is also a derived operation on terms. We illustrate its behaviour at each arity in Figure 5. We recover the operation from the introduction when the last argument is empty, and using a forget operation: we have $\circ(u, v, w) = \text{fs}(u, v, w; \emptyset)$.

We use this operation in order to decompose full prime graphs along a given inner vertex.
<figure><img src="image_13.png" /><figcaption>Figure 5 The series operations s( ; d ), s( a ; d ), s( a, b ; d ), and s( a, b, c ; d ).</figcaption></figure>

**Proof.** We follow the same pattern as in the proof of the forward implication of Proposition 4.1: we proceed by lexicographic induction on the size of the graph followed by 4 minus its arity. If the graph has isolated sources, we use Lemma 3.3 and Proposition 5.1(3,4) to rewrite the parsings into permuted lifts and proceed recursively. Otherwise it is full, and we decompose it into primes via Lemma 3.4:

■ if there are no components then both parsings are equivalent to  by Proposition 5.1(1);

■ if there are at least two components then we use Proposition 5.1(5) on both parsings and we proceed recursively.

■ otherwise the graph must be (full) prime. Either it is atomic and we conclude by Proposition 5.1(2,3), or Lemma 5.4 gives us two terms t', u' such that t ≡ f(t'), t' ≅ u', and f(u') ≡ u, and we can conclude since t' ≅ u' follows by induction hypothesis. ◀

We have only used Axioms A1-7 up to this point. We prove below that those axioms are complete when there are few forget points. Say that a graph is *easy* if each of its non-atomic reduced components *G* has only one forget point *x*, and in turn (*G*, *x*) is easy. (This definition is well-founded by the same lexicographic ordering as we used in the above proof.)

► **Proposition 5.6.** For all parsings *t*, *u* of an easy graph, we have *t* ≡ *u*.

**Proof.** By adapting the previous completeness proof. Lemma 5.2 may replace Lemma 5.4 when we attain non-atomic full prime graphs: those are reduced components of the starting graph and since those have only one forget point, all their parsings reach that one. ◀

None of the graphs in Figures 3 and 4 are easy: they are all full prime, each with two forget points *x*, *y* (plus two symmetrical ones for **FX** and **FD**). Nevertheless, adding either *x* or *y* to their interface makes them easy (cf. Lemma D.1). This is why the precise choice of parsings does not matter when we use them as forget axioms in Definition 4.3.

6 Series decompositions

As explained in the introduction, there is a *series* operation on graphs which plays an important role. We slightly generalise it here, and we show how to use it to analyse graphs with a forget point.

Given *k* graphs *G*₁, ..., *G*ₖ of arity *k* and a graph *H* of arity *k* + 1, we define the following graph of arity *k* + 1, where *p*ᵢ denotes the permutation which swaps *i* and *k* + 1.

$$
s(G_1, \dots, G_k; H) \triangleq p_1 l G_1 \parallel \dots \parallel p_k l G_k \parallel H
$$

As is explicit from its definition, this operation on graphs is also a derived operation on
terms. We illustrate its behaviour at each arity in Figure 5. We recover the operation from
the introduction when the last argument is empty, and using a forget operation: we have
∘(*u*, *v*, *w*) = fs(*u*, *v*, *w*; ∅).

We use this operation in order to decompose full prime graphs along a given inner vertex.
**Proposition 6.1 (Series decomposition).** For all full prime graphs $G$ of arity $k$ with an inner vertex $x$, there are graphs $G_1, \dots, G_k, H$ such that $(G, x) \simeq s(G_1, \dots, G_k; H)$ and
1. all components of $H$ are full, and

2. if the $j$th source of a component of $G_i$ is isolated, then $i < j$.
Such a decomposition is unique up to isomorphism.

We call $G_i$ the $i$th series argument, and $H$ the series factor of such a decomposition (at $x$).

**Proof.** We decompose $(G, x)$ into prime components, which we classify according to their isolated sources. Since $G$ is full prime, $x$ is never isolated. Full components go into the series factor. Components where the first source is isolated go into the first series argument (under the permutation $p_1$, the first source gets swapped with $x$). Components where the second source is isolated but not the first one go into the second series argument. Et caetera. ◀

Also note that we can follow such decompositions at the term level, modulo A1-7:

**Proposition 6.2.** If a term $t$ reaches the last source of a graph of the form $s(G_1, \dots, G_k; H)$, then there are parsings $u_1, \dots, u_k, v$ of $G_1, \dots, G_k, H$ such that $t \equiv \text{fs}(u_1, \dots, u_k; v)$.

**Proof.** Consequence of Proposition 5.1. ◀

# 7 Anchors

In this section we define the concept of anchors—inner vertices with specific properties, and we prove the following variant of Statement 5.3:

**Lemma 7.1 (Reaching anchors).** Full prime terms reach all their anchors.

This lemma implies Lemma 5.4 when the considered graph has an anchor, by applying it to both parsings. Therefore, once Lemma 7.1 proved, it will only remain to prove Lemma 5.4 for anchor-free graphs (Section 8).

The definition of anchor is the following; we only consider them in full prime graphs.

**Definition 7.2.** An anchor in a (full prime) graph $G$ is an inner vertex $x$ such that either:
1. there are no full prime components in $(G, x)$, or

2. there is an edge whose neighbours comprise at least $x$ and all sources of $G$, or

3. there are two or more full prime components in $(G, x)$.

Using series decompositions, $x$ is an anchor whenever the series factor at $x$ is empty, or has only one edge, or has at least two components.

This last condition generalises the usual notion of cutvertex [10, Section 1.4]: such anchors at arity zero when there are only binary edges are exactly cutvertices as usual. Removing them disconnects the graph. The second branch in our definition may only arise with sources and/or hyperedges; it is convenient to have it for the present proof, but it would probably be more natural to disallow it in other contexts. Thanks to this alternative, all inner vertices in the graphs in Figure 3 are anchors. In contrast, the graphs in Figure 4 have no anchors.

We prove below that all forget points are anchors at arity three. The converse holds at all arities, but we only get it a posteriori, as a consequence of Lemma 7.1.

**Proposition 7.3.** At arity three, all forget points are anchors.

**Proof.** If $x$ is a forget point of a graph $G$ of arity three, the full prime components of $(G, x)$ must be atomic by Proposition 3.5. Thus $x$ is an anchor, by either the first or the second condition in Definition 7.2. ◀
**Proposition 6.1 (Series decomposition).** For all full prime graphs $G$ of arity $k$ with an inner vertex $x$, there are graphs $G_1, \dots, G_k, H$ such that $(G, x) \simeq s(G_1, \dots, G_k; H)$ and
1. all components of $H$ are full, and

2. if the $j$th source of a component of $G_i$ is isolated, then $i < j$.

Such a decomposition is unique up to isomorphism.

We call $G_i$ the *i*th series argument, and $H$ the series factor of such a decomposition (at $x$).

**Proof.** We decompose $(G, x)$ into prime components, which we classify according to their isolated sources. Since $G$ is full prime, $x$ is never isolated. Full components go into the series factor. Components where the first source is isolated go into the first series argument (under the permutation $p_1$, the first source gets swapped with $x$). Components where the second source is isolated but not the first one go into the second series argument. Et caetera. ◀

Also note that we can follow such decompositions at the term level, modulo A1-7:

**Proposition 6.2.** If a term $t$ reaches the last source of a graph of the form $s(G_1, \dots, G_k; H)$, then there are parsings $u_1, \dots, u_k, v$ of $G_1, \dots, G_k, H$ such that $t \equiv \text{fs}(u_1, \dots, u_k; v)$.

**Proof.** Consequence of Proposition 5.1. ◀

# 7 Anchors

In this section we define the concept of *anchors*—inner vertices with specific properties, and we prove the following variant of Statement 5.3:

**Lemma 7.1 (Reaching anchors).** *Full prime terms reach all their anchors.*

This lemma implies Lemma 5.4 when the considered graph has an anchor, by applying it to both parsings. Therefore, once Lemma 7.1 proved, it will only remain to prove Lemma 5.4 for anchor-free graphs (Section 8).

The definition of anchor is the following; we only consider them in full prime graphs.

**Definition 7.2.** An anchor in a (full prime) graph $G$ is an inner vertex $x$ such that either:
1. there are no full prime components in $(G, x)$, or

2. there is an edge whose neighbours comprise at least $x$ and all sources of $G$, or

3. there are two or more full prime components in $(G, x)$.

Using series decompositions, $x$ is an anchor whenever the series factor at $x$ is empty, or has only one edge, or has at least two components.

This last condition generalises the usual notion of cutvertex [8, Section 1.4]: such anchors at arity zero when there are only binary edges are exactly cutvertices as usual. Removing them disconnects the graph. The second branch in our definition may only arise with sources and/or hyperedges; it is convenient to have it for the present proof, but it would probably be more natural to disallow it in other contexts. Thanks to this alternative, all inner vertices in the graphs in Figure 3 are anchors. In contrast, the graphs in Figure 4 have no anchors.

We prove below that all forget points are anchors at arity three. The converse holds at all arities, but we only get it a *posteriori*, as a consequence of Lemma 7.1.

**Proposition 7.3.** *At arity three, all forget points are anchors.*

**Proof.** If $x$ is a forget point of a graph $G$ of arity three, the full prime components of $(G, x)$ must be atomic by Proposition 3.5. Thus $x$ is an anchor, by either the first or the second condition in Definition 7.2. ◀
We also find anchors easily at arities zero and one.

**► Proposition 7.4.** *Non-atomic full prime graphs of arity in {0, 1, 3} have some anchor.*

*Proof.* Every inner vertex is an anchor at arity zero, either because it is isolated (anchor of the first kind), or because it belongs to some edge (anchor of the second kind). Every immediate neighbour of the only source is an anchor at arity one (of the second kind). At arity three we use Propositions 7.3 and 3.7. ◀

We first prove Lemma 7.1 for graphs of arity three, and then we show how to reduce the other cases to that one (Section 7.2).

## 7.1 Parsing on anchors at arity three

A *checkpoint* between two vertices $y, z$ of a graph $G$ is an inner vertex $x$ such that every inner path from $y$ to $z$ goes through $x$. When $y, z$ are not mentioned explicitly, they are implicitly assumed to be sources. (This definition coincides with that from [7] at arity two.) Analysing the components of $(G, x)$ by the sources they touch, we see that the checkpoints of a graph $G$ of arity three are the inner vertices $x$ for which $G$ has the following shape:

<figure><img src="image_13.png" /></figure>

This characterisation shows that checkpoints are anchors of the first kind in Definition 7.2. Another important property at arity three is that if there are two anchors, then they must be checkpoints for the same sources:

**► Proposition 7.5.** *At arity three, every full prime graph with two distinct anchors x, y has the following shape:*

<figure><img src="image_14.png" /></figure>

**Proof of Lemma 7.1 at arity three.** We proceed by induction on the size of the graph.

Let $t$ be a parsing of a full prime graph $G$ of arity three, with an anchor $x$. By Lemma 5.2, $t$ reaches some forget point $y$. If $x = y$ then we are done. Otherwise, $y$ is a second anchor by Proposition 7.3, and $G$ has the shape given by Proposition 7.5. Call $A$ the graph between $i, k, y$, and $B$ the one between $j, k, y$. Since $t$ reaches $y$ we have a parsing $t'$ of $(G, y)$ such that $t \equiv ft'$. By analysing the full prime decomposition of $(G, y)$, we can put $t'$ under the form $(j4)lu \parallel (i4)lv$, where $u$ is a parsing of $A$ and $v$ a parsing of $B$. Then we observe that $x$ is a checkpoint in $A$, and thus an anchor, so that $u$ reaches $x$ by induction hypothesis. Therefore, $u \equiv fu'$ for some parsing $u'$ of $(A, x)$. By analysing the full prime decomposition of $(A, x)$ as before, we deduce that $t$ reaches $x$ using *FK*. ◀

## 7.2 Parsing on anchors at lower arities

We now finish the proof of Lemma 7.1 by showing how to reduce the other cases to that of arity three. We use for that the two following lemmas. The first one intuitively makes it possible to zoom on a specific inner vertex by going under a forget operation. The second one states that under some conditions, an anchor in $f^iG$ is also an anchor in $G$, allowing to use the case of arity three.
We also find anchors easily at arities zero and one.

**► Proposition 7.4.** *Non-atomic full prime graphs of arity in {0, 1, 3} have some anchor.*

*Proof.* Every inner vertex is an anchor at arity zero, either because it is isolated (anchor of the first kind), or because it belongs to some edge (anchor of the second kind). Every immediate neighbour of the only source is an anchor at arity one (of the second kind). At arity three we use Propositions 7.3 and 3.7. ◀

We first prove Lemma 7.1 for graphs of arity three, and then we show how to reduce the other cases to that one (Section 7.2).

## 7.1 Parsing on anchors at arity three

A *checkpoint* between two vertices $y, z$ of a graph $G$ is an inner vertex $x$ such that every inner path from $y$ to $z$ goes through $x$. When $y, z$ are not mentioned explicitly, they are implicitly assumed to be sources. (This definition coincides with that from [5] at arity two.) Analysing the components of $(G, x)$ by the sources they touch, we see that the checkpoints of a graph $G$ of arity three are the inner vertices $x$ for which $G$ has the following shape:

<figure><img src="image_14.png" /></figure>

This characterisation shows that checkpoints are anchors of the first kind in Definition 7.2. Another important property at arity three is that if there are two anchors, then they must be checkpoints for the same sources:

**► Proposition 7.5.** *At arity three, every full prime graph with two distinct anchors x, y has the following shape:*

<figure><img src="image_15.png" /></figure>

**Proof of Lemma 7.1 at arity three.** We proceed by induction on the size of the graph.

Let $t$ be a parsing of a full prime graph $G$ of arity three, with an anchor $x$. By Lemma 5.2, $t$ reaches some forget point $y$. If $x = y$ then we are done. Otherwise, $y$ is a second anchor by Proposition 7.3, and $G$ has the shape given by Proposition 7.5. Call $A$ the graph between $i, k, y$, and $B$ the one between $j, k, y$. Since $t$ reaches $y$ we have a parsing $t'$ of $(G, y)$ such that $t \equiv ft'$. By analysing the full prime decomposition of $(G, y)$, we can put $t'$ under the form $(j4)lu \parallel (i4)lv$, where $u$ is a parsing of $A$ and $v$ a parsing of $B$. Then we observe that $x$ is a checkpoint in $A$, and thus an anchor, so that $u$ reaches $x$ by induction hypothesis. Therefore, $u \equiv fu'$ for some parsing $u'$ of $(A, x)$. By analysing the full prime decomposition of $(A, x)$ as before, we deduce that $t$ reaches $x$ using *FK*. ◀

## 7.2 Parsing on anchors at lower arities

We now finish the proof of Lemma 7.1 by showing how to reduce the other cases to that of arity three. We use for that the two following lemmas. The first one intuitively makes it possible to zoom on a specific inner vertex by going under a forget operation. The second one states that under some conditions, an anchor in $f^iG$ is also an anchor in $G$, allowing to use the case of arity three.
**Lemma 7.6.** Let $t$ be a term of arity up to two with an inner vertex $x$ in a full prime component. There is a term $u$ such that $t \equiv \text{fu}$ and $x$ is either the last source of $u$ or an inner vertex of a full prime component of $u$.

**Lemma 7.7.** For $i > 0$ let $f^i G$ be a full prime graph of arity $k$ and $x, y$ two distinct inner vertices in a full prime component $C$ of $G$. If $x$ is an anchor of $f^i G$ and is in one of the first $k$ series arguments of the series decomposition of $C$ at $y$, then $x$ is a checkpoint in $C$.

(Note that the only isolated sources of the components of the $i$ last series arguments in the decomposition of $C$ as above, are the $i$ forgotten sources in $f^i G$.)

Before we finish the proof of Lemma 7.1, also observe that **FS** implies $f^jpu \equiv f^jqu$ for all terms $u$ of arity $k$ and permutations $p, q$ agreeing on the first $k-j$ elements.

**Proof of Lemma 7.1, at all arities.** We prove the following generalisation, by induction on the lexicographic product of $|C|$ and $3-k$:

For all terms $t$ of arity $k \le 3$, for all $i \le k$, if $f^i t$ is full prime with an anchor $x$ in a full prime component $C$ of $t$, then $f^i t$ reaches $x$.

If $k < 3$ then we use Lemma 7.6 to obtain $u$ such that $f^i t \equiv f^{i+1} u$; if $x$ is the last source of $u$ then we are done, otherwise we conclude by induction, since $x$ lies in a component of $C$.

We now assume $k=3$, and we rewrite $t$ as $t_C \parallel t'$, where $t_C$ is the full prime component containing $x$. By Lemma 5.2, $t_C$ reaches some forget point $y$. Take a series decomposition $t_C \equiv \text{fs}(t_1, t_2, t_3; u)$ of $t_C$ at $y$. The series factor $u$ cannot contain $x$ since all its components are atomic by Proposition 3.5. Thus $x$ must be in a series argument.

If $x$ is in one of the first $3-i$ series arguments, then by Lemma 7.7 $x$ must be a checkpoint, and thus an anchor of $t_C$. Using Lemma 7.1 at arity three (Section 7.1), we obtain that $t_C$ reaches $x$. So does $t$ by **A7**, and finally $f^i t$ by **FS**.

Otherwise, $x$ is in one of the last $i$ series arguments, say the $j$th one. The $j$th source $s_j$ is the only source that is necessarily isolated in this argument. It is a source that is forgotten by the operations $f^i$ (see the adjacent figure for an illustration). Our goal is to “swap” this $j$th source for $y$ in order to decrease the size of $C$. Indeed the new component containing $x$ will then be contained in $t_3$, which is smaller in size than $C$.

<figure><img src="image_15.png" /></figure>

Let $S$ be the set of non-isolated sources in the component $C'$ of $s(t_1, t_2, t_3; u)$ containing $x$. Using **FS** we get a term $t''$ such that $f^i t \equiv f^{|S|} t''$ and $t''$ denotes $g(t)$ with the inner vertices in $S$ upgraded as sources. By definition of $t''$, $C'$ is a full prime component of it. Furthermore, up to isolated sources, $C'$ is the same component as the one of $s(t_1, t_2, t_3; u)$ containing $x$. This gives $|C'| < |C|$ and we conclude by induction on $f^{|S|} t''$. ◀

At this point, we have used axioms **A1-7**, **FS**, and **FK**, but not **FX** and **FD**.

## 8 Separation pairs

We call *hard* the non-atomic anchor-free full prime graphs. Examples of such graphs were given in Figure 2. Hard graphs have arity two by Propositions 7.4 and 3.5, and it only remains to prove Lemma 5.4 for these graphs.

A *forget pair* in a graph $G$ is a pair $(x, y)$ of inner vertices such that $(G, x, y)$ has treewidth at most three. A parsing $t$ of a graph $G$ reaches a pair $(x, y)$ of inner vertices if there is some parsing $t'$ of $(G, x, y)$ such that $t \equiv \text{ftt}'$. By definition, a term may only reach forget pairs.
**Lemma 7.6.** Let $t$ be a term of arity up to two with an inner vertex $x$ in a full prime component. There is a term $u$ such that $t \equiv \text{fu}$ and $x$ is either the last source of $u$ or an inner vertex of a full prime component of $u$.

**Lemma 7.7.** For $i > 0$ let $f^i G$ be a full prime graph of arity $k$ and $x, y$ two distinct inner vertices in a full prime component $C$ of $G$. If $x$ is an anchor of $f^i G$ and is in one of the first $k$ series arguments of the series decomposition of $C$ at $y$, then $x$ is a checkpoint in $C$.

(Note that the only isolated sources of the components of the $i$ last series arguments in the decomposition of $C$ as above, are the $i$ forgotten sources in $f^i G$.)

Before we finish the proof of Lemma 7.1, also observe that **FS** implies $f^jpu \equiv f^jqu$ for all terms $u$ of arity $k$ and permutations $p, q$ agreeing on the first $k-j$ elements.

**Proof of Lemma 7.1, at all arities.** We prove the following generalisation, by induction on the lexicographic product of $|C|$ and $3-k$:

For all terms $t$ of arity $k \le 3$, for all $i \le k$, if $f^i t$ is full prime with an anchor $x$ in a full prime component $C$ of $t$, then $f^i t$ reaches $x$.

If $k < 3$ then we use Lemma 7.6 to obtain $u$ such that $f^i t \equiv f^{i+1} u$; if $x$ is the last source of $u$ then we are done, otherwise we conclude by induction, since $x$ lies in a component of $C$.

We now assume $k=3$, and we rewrite $t$ as $t_C \parallel t'$, where $t_C$ is the full prime component containing $x$. By Lemma 5.2, $t_C$ reaches some forget point $y$. Take a series decomposition $t_C \equiv \text{fs}(t_1, t_2, t_3; u)$ of $t_C$ at $y$. The series factor $u$ cannot contain $x$ since all its components are atomic by Proposition 3.5. Thus $x$ must be in a series argument.

If $x$ is in one of the first $3-i$ series arguments, then by Lemma 7.7 $x$ must be a checkpoint, and thus an anchor of $t_C$. Using Lemma 7.1 at arity three (Section 7.1), we obtain that $t_C$ reaches $x$. So does $t$ by **A7**, and finally $f^i t$ by **FS**.

Otherwise, $x$ is in one of the last $i$ series arguments, say the $j$th one. The $j$th source $s_j$ is the only source that is necessarily isolated in this argument. It is a source that is forgotten by the operations $f^i$ (see the adjacent figure for an illustration). Our goal is to “swap” this $j$th source for $y$ in order to decrease the size of $C$. Indeed the new component containing $x$ will then be contained in $t_3$, which is smaller in size than $C$.

<figure><img src="image_16.png" /></figure>

Let $S$ be the set of non-isolated sources in the component $C'$ of $s(t_1, t_2, t_3; u)$ containing $x$. Using **FS** we get a term $t''$ such that $f^i t \equiv f^{|S|} t''$ and $t''$ denotes $g(t)$ with the inner vertices in $S$ upgraded as sources. By definition of $t''$, $C'$ is a full prime component of it. Furthermore, up to isolated sources, $C'$ is the same component as the one of $s(t_1, t_2, t_3; u)$ containing $x$. This gives $|C'| < |C|$ and we conclude by induction on $f^{|S|} t''$. ◀

At this point, we have used axioms **A1-7**, **FS**, and **FK**, but not **FX** and **FD**.

## 8 Separation pairs

We call *hard* the non-atomic anchor-free full prime graphs. Examples of such graphs were given in Figure 2. Hard graphs have arity two by Propositions 7.4 and 3.5, and it only remains to prove Lemma 5.4 for these graphs.

A *forget pair* in a graph $G$ is a pair $(x, y)$ of inner vertices such that $(G, x, y)$ has treewidth at most three. A parsing $t$ of a graph $G$ reaches a pair $(x, y)$ of inner vertices if there is some parsing $t'$ of $(G, x, y)$ such that $t \equiv \text{ftt}'$. By definition, a term may only reach forget pairs.
<figure><img src="image_16.png" /><figcaption>Figure 6 Separation pairs $(y \diamond x)$, and partial order on vertices $(y \prec x)$.</figcaption></figure>

By **FS**, a term reaches $(x, y)$ iff it reaches $(y, x)$; it follows that every term reaching $(x, y)$ reaches both $x$ and $y$.

Given two inner vertices $x, y$ of a full prime graph of arity two, we write $y \diamond x$ when the graph has the shape on the left of Figure 6, and $y \prec x$ when the graph has the shape on the right (equivalently, when $y$ is a checkpoint between $x$ and some source). In the first case, we say that $(x, y)$ is a *separation pair*. We prove a few properties about such inner vertices.

**Lemma 8.1.** If $y \prec x$ or $y \diamond x$ in a full prime graph $G$, then $y$ is an anchor in $(G, x)$, and every parsing of $G$ reaching $x$ also reaches $(x, y)$.

**Proof.** In both cases, there is no full prime component in $(G, x, y)$, so that $y$ is indeed an anchor in $(G, x)$. Now if $t \equiv ft'$ for some parsing $t'$ of $(G, x)$, then $t'$ reaches $y$ by Lemma 7.1: $t' \equiv ft''$ for some parsing $t''$ of $(G, x, y)$. Thus $t$ reaches $(x, y)$. ◀

It follows that a full prime term reaches a separation pair iff it reaches any of its constituents.

We write $S(x)$ for the series factor of a graph at some inner vertex $x$. When the graph is hard, $x$ is not an anchor, so that $S(x)$ must be full prime and cannot contain just one edge.

**Proposition 8.2.** For all hard graphs, $\prec$ is well-founded.

**Proof.** Observe that if $y \prec x$ then $|S(y)| < |S(x)|$. ◀

**Proposition 8.3.** For all vertices $x, y, z$ such that $y \prec x$ and $x \diamond z$, we have $y \diamond z$.

**Proof.** Consider an inner path between the two sources; we have to show that it visits either $y$ or $z$. It visits either $x$ or $z$ since $(x, z)$ is a separation pair. If it visits $x$ then it also visits $y$ since $y$ is a checkpoint between $x$ and one of the two sources. ◀

When the graph is hard in the previous proposition, it must have the following shape:

<figure><img src="image_17.png" /></figure>

In such a case, we intuitively prefer the separation pair $(y, z)$ to $(x, z)$. This leads us to the notion of minimal separation pair. A vertex $x$ is *minimal* if there is no vertex $y$ such that $y \prec x$. A pair of vertices is minimal when its two elements are so.

The proposition below makes it possible to get separation pairs out of minimal vertices.

**Proposition 8.4.** Let $x$ be a forget point in a hard graph. For all forget points $y$ of $S(x)$, we have either $y \prec x$ or $y \diamond x$.

**Proof.** Let us classify the components of $(G, x, y)$ by their isolated sources. Full components cannot exist as by Proposition 3.5 they would be edges and both $x$ and $y$ would be anchors in $G$. So $G$ must have the following shape:

<figure><img src="image_18.png" /></figure>
<figure><img src="image_17.png" /><figcaption>Figure 6 Separation pairs $(y \diamond x)$, and partial order on vertices $(y \prec x)$.</figcaption></figure>

By **FS**, a term reaches $(x, y)$ iff it reaches $(y, x)$; it follows that every term reaching $(x, y)$ reaches both $x$ and $y$.

Given two inner vertices $x, y$ of a full prime graph of arity two, we write $y \diamond x$ when the graph has the shape on the left of Figure 6, and $y \prec x$ when the graph has the shape on the right (equivalently, when $y$ is a checkpoint between $x$ and some source). In the first case, we say that $(x, y)$ is a *separation pair*. We prove a few properties about such inner vertices.

**Lemma 8.1.** If $y \prec x$ or $y \diamond x$ in a full prime graph $G$, then $y$ is an anchor in $(G, x)$, and every parsing of $G$ reaching $x$ also reaches $(x, y)$.

**Proof.** In both cases, there is no full prime component in $(G, x, y)$, so that $y$ is indeed an anchor in $(G, x)$. Now if $t \equiv ft'$ for some parsing $t'$ of $(G, x)$, then $t'$ reaches $y$ by Lemma 7.1: $t' \equiv ft''$ for some parsing $t''$ of $(G, x, y)$. Thus $t$ reaches $(x, y)$. ◀

It follows that a full prime term reaches a separation pair iff it reaches any of its constituents.

We write $S(x)$ for the series factor of a graph at some inner vertex $x$. When the graph is hard, $x$ is not an anchor, so that $S(x)$ must be full prime and cannot contain just one edge.

**Proposition 8.2.** For all hard graphs, $\prec$ is well-founded.

**Proof.** Observe that if $y \prec x$ then $|S(y)| < |S(x)|$. ◂

**Proposition 8.3.** For all vertices $x, y, z$ such that $y \prec x$ and $x \diamond z$, we have $y \diamond z$.

**Proof.** Consider an inner path between the two sources; we have to show that it visits either $y$ or $z$. It visits either $x$ or $z$ since $(x, z)$ is a separation pair. If it visits $x$ then it also visits $y$ since $y$ is a checkpoint between $x$ and one of the two sources. ◂

When the graph is hard in the previous proposition, it must have the following shape:

<figure><img src="image_18.png" /></figure>

In such a case, we intuitively prefer the separation pair $(y, z)$ to $(x, z)$. This leads us to the notion of minimal separation pair. A vertex $x$ is *minimal* if there is no vertex $y$ such that $y \prec x$. A pair of vertices is minimal when its two elements are so.

The proposition below makes it possible to get separation pairs out of minimal vertices.

**Proposition 8.4.** Let $x$ be a forget point in a hard graph. For all forget points $y$ of $S(x)$, we have either $y \prec x$ or $y \diamond x$.

**Proof.** Let us classify the components of $(G, x, y)$ by their isolated sources. Full components cannot exist as by Proposition 3.5 they would be edges and both $x$ and $y$ would be anchors in $G$. So $G$ must have the following shape:

<figure><img src="image_19.png" /></figure>
If there is no inner path avoiding $y$ between the sources in the bottom component, then $y \diamond x$. If there is no inner path avoiding $y$ from $x$ to one of the sources, then $y \prec x$. Otherwise there are at least two full prime components in $(G, y)$, making $y$ an anchor of $G$, which contradicts $G$ being hard. ◀

It follows easily that every hard graph has some separation pair—even a minimal one, which will be useful to reduce the number of cases to study. However, we need to be more precise and to keep track of terms.

**► Lemma 8.5.** Every hard term reaches some minimal separation pair.

**Proof.** Let $t$ be a hard term. By Lemma 5.2 $t$ reaches some forget point $x$, which we can choose minimal by Proposition 8.2 and Lemma 8.1. Accordingly, let $t'$ be a parsing of $(G, x)$ such that $t \equiv ft'$. As $S(x)$ is full prime and non-atomic, it has a forget point $y$. Since $x$ is minimal, $(x, y)$ is a separation pair by Proposition 8.4. We can choose $y$ to be minimal by Proposition 8.3, and $t$ reaches $(x, y)$ by Lemma 8.1. ◀

As before with forget points, separation pairs are not unique (even minimal ones), and we need to show how to move from one separation pair to another.

When studying the possible shapes of a hard graph $H$ with distinct separation forget pairs, we end up with a few shapes $S$ such as the following one:

<figure><img src="image_19.png" /></figure>

In such situations, we know that $(H, x)$ has treewidth at most three, but $(S, x)$ has treewidth four. Therefore, for an appropriate notion of *minor*, $(S, x)$ cannot be a minor of $(H, x)$: the treewidth may not increase when taking minors. We use this information in order to refine the actual shape of $H$.

We use *sourced simple graphs* in order to define such a notion of minor. Those are triples $(V, E, S)$ made of a set $V$ of *vertices*, a set $E$ of unordered binary *edges*, and a subset $S \subseteq V$ of *sources*. We write $K_k$ for the clique over $k$ sources. *Tree decompositions* and *treewidth* [10, Section 12.4] are adapted to sourced simple graphs by requiring the subset of sources to be contained in some bag. A *sourced minor of a (sourced simple) graph* is a (sourced simple) graph obtained from it by a sequence of the following operations: remove an edge, contract an edge, remove an isolated vertex. Those operations do not increase the treewidth.

The *footprint* of a graph is the sourced simple graph obtained from it by replacing each edge by a clique over its neighbours, forgetting labels, and turning the interface into a mere set—note that we do not add a clique on the sources. A graph and its footprint have the same tree decompositions, and thus the same treewidth. A *sourced minor of a graph* is a sourced minor of its footprint.

Note that graphs excluding $K_3$ as a sourced minor need not be acyclic, as cycles may occur away from the sources. The point of using sourced minors is that they behave well with respect to substitutions, and thus shapes:

**► Proposition 8.6.** Given a graph $G$ and a substitution $\sigma$, if $K_k$ is a sourced minor of $\sigma(a)$ for all letters $a$ of arity $k$, then the footprint of $G$ is a sourced minor of $G\sigma$.

Now observe that full prime graphs of arity two admit the sourced edge $K_2$ as a sourced minor. At arity three, we have the following property instead.
If there is no inner path avoiding $y$ between the sources in the bottom component, then $y \diamond x$. If there is no inner path avoiding $y$ from $x$ to one of the sources, then $y \prec x$. Otherwise there are at least two full prime components in $(G, y)$, making $y$ an anchor of $G$, which contradicts $G$ being hard. ◀

It follows easily that every hard graph has some separation pair—even a minimal one, which will be useful to reduce the number of cases to study. However, we need to be more precise and to keep track of terms.

**► Lemma 8.5.** Every hard term reaches some minimal separation pair.

*Proof.* Let $t$ be a hard term. By Lemma 5.2 $t$ reaches some forget point $x$, which we can choose minimal by Proposition 8.2 and Lemma 8.1. Accordingly, let $t'$ be a parsing of $(G, x)$ such that $t \equiv ft'$. As $S(x)$ is full prime and non-atomic, it has a forget point $y$. Since $x$ is minimal, $(x, y)$ is a separation pair by Proposition 8.4. We can choose $y$ to be minimal by Proposition 8.3, and $t$ reaches $(x, y)$ by Lemma 8.1. ◀

As before with forget points, separation pairs are not unique (even minimal ones), and we need to show how to move from one separation pair to another.

When studying the possible shapes of a hard graph $H$ with distinct separation forget pairs, we end up with a few shapes $S$ such as the following one:

<figure><img src="image_20.png" /></figure>

In such situations, we know that $(H, x)$ has treewidth at most three, but $(S, x)$ has treewidth four. Therefore, for an appropriate notion of *minor*, $(S, x)$ cannot be a minor of $(H, x)$: the treewidth may not increase when taking minors. We use this information in order to refine the actual shape of $H$.

We use *sourced simple graphs* in order to define such a notion of minor. Those are triples $(V, E, S)$ made of a set $V$ of *vertices*, a set $E$ of unordered binary *edges*, and a subset $S \subseteq V$ of *sources*. We write $K_k$ for the clique over $k$ sources. *Tree decompositions* and *treewidth* [8, Section 12.4] are adapted to sourced simple graphs by requiring the subset of sources to be contained in some bag. A *sourced minor of a (sourced simple) graph* is a (sourced simple) graph obtained from it by a sequence of the following operations: remove an edge, contract an edge, remove an isolated vertex. Those operations do not increase the treewidth.

The *footprint* of a graph is the sourced simple graph obtained from it by replacing each edge by a clique over its neighbours, forgetting labels, and turning the interface into a mere set—note that we do not add a clique on the sources. A graph and its footprint have the same tree decompositions, and thus the same treewidth. A *sourced minor of a graph* is a sourced minor of its footprint.

Note that graphs excluding $K_3$ as a sourced minor need not be acyclic, as cycles may occur away from the sources. The point of using sourced minors is that they behave well with respect to substitutions, and thus shapes:

**► Proposition 8.6.** Given a graph $G$ and a substitution $\sigma$, if $K_k$ is a sourced minor of $\sigma(a)$ for all letters $a$ of arity $k$, then the footprint of $G$ is a sourced minor of $G\sigma$.

Now observe that full prime graphs of arity two admit the sourced edge $K_2$ as a sourced minor. At arity three, we have the following property instead.
**Proposition 8.7.** Every graph of arity three either has the sourced triangle $K_3$ as a sourced minor, or has one of the two following shapes:

<figure><img src="image_20.png" /></figure>

Let us continue our example and come back to the previous hard graph $H$. Assume that the binary edges in the given shape are instantiated by full prime graphs, and consider the three graphs instantiating the ternary edges. If those three graphs have the triangle as a sourced minor, then the footprint of $(S, x)$ must be a sourced minor of $(H, x)$, which is not possible. Therefore, at least one of them must have one of the shapes given by Proposition 8.7. By considering the different possibilities and continuing the same kind of reasoning, we end up proving that in this case, $H$ must have shape **FX**. In the general case, we obtain the following classification.

**Proposition 8.8.** Let $G$ be a hard graph with two minimal separation forget pairs $(x, y)$ and $(x', y')$. Possibly up to swapping $x$ and $y$, and/or $x'$ and $y'$, either $(x, y')$ is a separation pair (**Case Z**), or $G$ has one of the following shapes, where in the leftmost case, $z$ is minimal and $x', y'$ appear in the rightmost component:

<figure><img src="image_21.png" /><figcaption>Case IH</figcaption></figure>

<figure><img src="image_22.png" /><figcaption>Case X</figcaption></figure>

<figure><img src="image_23.png" /><figcaption>Case D</figcaption></figure>

The proof we provide in Appendix F actually establishes that in the case where $(x, y')$ is a separation pair, then $G$ has one of the following shapes:

<figure><img src="image_24.png" /><figcaption>Case Z1</figcaption></figure>

<figure><img src="image_25.png" /><figcaption>Case Z2</figcaption></figure>

<figure><img src="image_26.png" /><figcaption>Case Z3</figcaption></figure>

We finally deduce that hard terms reach all their minimal separation forget pairs.

**Lemma 8.9.** Let $G$ be a hard graph with minimal separation forget pair $(x', y')$. All parsings $t$ of $G$ reaching a minimal separation pair $(x, y)$ also reach $(x', y')$.

**Proof.** We fix $G, x', y'$, we proceed by induction on the size of the component of $(G, x, y)$ containing $x'$, and we use Proposition 8.8. If $(x, y')$ is a separation pair (**Case Z**), then we use Proposition 8.1 twice: $t$ reaches $x$, thus $(x, y')$, thus $y'$ in particular, thus $(x', y')$. In **Case IH** we proceed by induction on $(x, z)$, which is reached by $t$ by similar reasoning, and for which the induction measure decreases. In **Case X** and **Case D**, we conclude directly by **FX** and **FD**, respectively. (In those latter two cases, we first need to rewrite $t$ so that it agrees syntactically with the shape of the axiom we use. We use Lemma 7.1 for that, which requires showing that some of the inner vertices are anchors in appropriate subgraphs. To do so, we exploit the fact that $G$ is hard, so that the subgraphs corresponding to the edges of the exhibited shape must be connected enough.) ◀

Together with Lemma 8.5, Lemma 5.4 follows, which concludes our completeness proof.
**Proposition 8.7.** Every graph of arity three either has the sourced triangle $K_3$ as a sourced minor, or has one of the two following shapes:

<figure><img src="image_21.png" /></figure>

Let us continue our example and come back to the previous hard graph $H$. Assume that the binary edges in the given shape are instantiated by full prime graphs, and consider the three graphs instantiating the ternary edges. If those three graphs have the triangle as a sourced minor, then the footprint of $(S, x)$ must be a sourced minor of $(H, x)$, which is not possible. Therefore, at least one of them must have one of the shapes given by Proposition 8.7. By considering the different possibilities and continuing the same kind of reasoning, we end up proving that in this case, $H$ must have shape **FX**. In the general case, we obtain the following classification.

**Proposition 8.8.** Let $G$ be a hard graph with two minimal separation forget pairs $(x, y)$ and $(x', y')$. Possibly up to swapping $x$ and $y$, and/or $x'$ and $y'$, either $(x, y')$ is a separation pair (**Case Z**), or $G$ has one of the following shapes, where in the leftmost case, $z$ is minimal and $x', y'$ appear in the rightmost component:

<figure><img src="image_22.png" /></figure>

The proof we provide in Appendix F actually establishes that in the case where $(x, y')$ is a separation pair, then $G$ has one of the following shapes:

<figure><img src="image_23.png" /></figure>

We finally deduce that hard terms reach all their minimal separation forget pairs.

**Lemma 8.9.** Let $G$ be a hard graph with minimal separation forget pair $(x', y')$. All parsings $t$ of $G$ reaching a minimal separation pair $(x, y)$ also reach $(x', y')$.

**Proof.** We fix $G, x', y'$, we proceed by induction on the size of the component of $(G, x, y)$ containing $x'$, and we use Proposition 8.8. If $(x, y')$ is a separation pair (**Case Z**), then we use Proposition 8.1 twice: $t$ reaches $x$, thus $(x, y')$, thus $y'$ in particular, thus $(x', y')$. In **Case IH** we proceed by induction on $(x, z)$, which is reached by $t$ by similar reasoning, and for which the induction measure decreases. In **Case X** and **Case D**, we conclude directly by **FX** and **FD**, respectively. (In those latter two cases, we first need to rewrite $t$ so that it agrees syntactically with the shape of the axiom we use. We use Lemma 7.1 for that, which requires showing that some of the inner vertices are anchors in appropriate subgraphs. To do so, we exploit the fact that $G$ is hard, so that the subgraphs corresponding to the edges of the exhibited shape must be connected enough.) ◀

Together with Lemma 8.5, Lemma 5.4 follows, which concludes our completeness proof.
# 9 Conclusion and future work

We have provided a finite presentation of graphs of treewidth at most three. Our axiomatisation comprises axioms for dealing with full prime decompositions (A1-7), axioms for reaching anchors (FS, FK), and two axioms for hard graphs (FX and FD).

An obvious question for future work is whether the approach presented here generalises to the case of graphs of treewidth at most *k*.

It does so up to Section 7. The syntax we use readily characterises those graphs (Proposition 4.1), and the seven first axioms as well as the results in Section 5 are not specific to the case *k* = 3. Axioms for anchors (Figure 3) also generalise. Accordingly, our results about series decomposition and anchors (Lemma 7.1) extend easily. In particular, non-atomic full prime graphs of arity 0, 1 and *k* would always have an anchor.

This means we also have finite presentations for bounds *k* = 1, 2. (For *k* = 2 this axiomatisation differs from the one previously proposed [7, 11], because the chosen syntax is different: there, graphs of arity three are not considered, and parallel composition may be applied to graphs of distinct arities.)

However, the results from Section 8 are specific to the case *k* = 3, and getting finite presentations for larger values of *k* seems difficult. Following the strategy presented here, we would need to prove the forget point agreement lemma (Lemma 5.4) for new hard graphs, which may have arities between 2 and *k* − 1.

Still, we would like to emphasise the utility of such a generalisation in the context of graph theory. Robertson and Seymour proved [15] that for all integers *k* there must be a finite list of excluded minors characterising the class of treewidth at most *k* graphs. Consider a minimal one amongst them, say *H*, along with a maximal clique over vertices *x*₁, ..., *x*ᵢ. It is not difficult to prove that either *H* is *K*<sub>*k*+2</sub>, or (*H*, *x*₁, ..., *x*ᵢ) is hard. Thus, studying hard graphs of treewidth *k* + 1 might lead to a better understanding of excluded minors for treewidth at most *k*.
# 9 Conclusion and future work

We have provided a finite presentation of graphs of treewidth at most three. Our axiomatisation comprises axioms for dealing with full prime decompositions (A1-7), axioms for reaching anchors (FS, FK), and two axioms for hard graphs (FX and FD).

An obvious question for future work is whether the approach presented here generalises to the case of graphs of treewidth at most *k*.

It does so up to Section 7. The syntax we use readily characterises those graphs (Proposition 4.1), and the seven first axioms as well as the results in Section 5 are not specific to the case *k* = 3. Axioms for anchors (Figure 3) also generalise. Accordingly, our results about series decomposition and anchors (Lemma 7.1) extend easily. In particular, non-atomic full prime graphs of arity 0, 1 and *k* would always have an anchor.

This means we also have finite presentations for bounds *k* = 1, 2. (For *k* = 2 this axiomatisation differs from the one previously proposed [5, 9], because the chosen syntax is different: there, graphs of arity three are not considered, and parallel composition may be applied to graphs of distinct arities.)

However, the results from Section 8 are specific to the case *k* = 3, and getting finite presentations for larger values of *k* seems difficult. Following the strategy presented here, we would need to prove the forget point agreement lemma (Lemma 5.4) for new hard graphs, which may have arities between 2 and *k* − 1.

Still, we would like to emphasise the utility of such a generalisation in the context of graph theory. Robertson and Seymour proved [13] that for all integers *k* there must be a finite list of excluded minors characterising the class of treewidth at most *k* graphs. Consider a minimal one amongst them, say *H*, along with a maximal clique over vertices *x*₁, ..., *x*ᵢ. It is not difficult to prove that either *H* is *K*<sub>*k*+2</sub>, or (*H*, *x*₁, ..., *x*ᵢ) is hard. Thus, studying hard graphs of treewidth *k* + 1 might lead to a better understanding of excluded minors for treewidth at most *k*.
References

1 Stefan Arnborg, Bruno Courcelle, Andrzej Proskurowski, and Detlef Seese. An algebraic theory of graph reduction. *J. ACM*, 40(5):1134–1164, 1993. doi:10.1145/174147.169807.

2 Stefan Arnborg and Andrzej Proskurowski. Characterization and recognition of partial 3-trees. *SIAM Journal on Algebraic Discrete Methods*, 7(2):305–314, 1986. doi:10.1137/0607033.

3 Umberto Bertelè and Francesco Brioschi. On non-serial dynamic programming. *J. Comb. Theory, Ser. A*, 14(2):137–148, 1973. doi:10.1016/0097-3165(73)90016-2.

4 Hans L. Bodlaender. Treewidth: Algorithmic techniques and results. In Igor Prívara and Peter Ruzicka, editors, *Proc. MFCS*, volume 1295 of LNCS, pages 19–36. Springer, 1997. doi:10.1007/BFB0029946.

5 Enric Cosme-Llópez and Damien Pous. K4-free graphs as a free algebra. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, *Proc. MFCS*, volume 83 of LIPIcs, pages 76:1–76:14. Schloss Dagstuhl, 2017. doi:10.4230/LIPICS.MFCS.2017.76.

6 Bruno Courcelle. Graph grammars, monadic second-order logic and the theory of graph minors. In Neil Robertson and Paul D. Seymour, editors, *Proc. Graph Structure Theory*, volume 147 of *Contemporary Mathematics*, pages 565–590. American Mathematical Society, 1991.

7 Bruno Courcelle and Joost Engelfriet. *Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach*, volume 138 of *Encyclopedia of mathematics and its applications*. Cambridge University Press, 2012.

8 Reinhard Diestel. *Graph Theory*, 4th Edition, volume 173 of *Graduate texts in mathematics*. Springer, 2012.

9 Christian Doczkal and Damien Pous. Treewidth-two graphs as a free algebra. In Igor Potapov, Paul G. Spirakis, and James Worrell, editors, *Proc. MFCS*, volume 117 of LIPIcs, pages 60:1–60:15. Schloss Dagstuhl, 2018. doi:10.4230/LIPICS.MFCS.2018.60.

10 Amina Doumane, Samuel Humeau, and Damien Pous. A finite presentation of graphs of treewidth at most three graphs. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, *Proc. ICALP*, pages 143:1–143:18. Schloss Dagstuhl, 2024. doi:10.4230/LIPIcs.ICALP.2024.143.

11 Rudolf Halin. S-functions for graphs. *Journal of geometry*, 8:171–186, 1976. doi:10.1007/BF01917434.

12 Neil Robertson and Paul D. Seymour. Graph minors. II. algorithmic aspects of tree-width. *J. Algorithms*, 7(3):309–322, 1986. doi:10.1016/0196-6774(86)90023-4.

13 Neil Robertson and Paul D. Seymour. Graph minors. XX. wagner's conjecture. *J. Comb. Theory, Ser. B*, 92(2):325–357, 2004. doi:10.1016/J.JCTB.2004.08.001.

14 Daniel P. Sanders. *Linear algorithms for graphs of tree-width at most four*. PhD thesis, Georgia Institute of Technology, 1993. URL: http://hdl.handle.net/1853/30061.

15 Petra Scheffler. Linear-time algorithms for NP-complete problems restricted to partial k-trees. Technical report, Academy of Sciences of the GDR, 1987.

16 Thomas V. Wimer. *Linear Algorithms on k-Terminal Graphs*. PhD thesis, Clemson University, 1993. URL: https://tigerprints.clemson.edu/arv_dissertations/28.
References

1. Stefan Arnborg, Bruno Courcelle, Andrzej Proskurowski, and Detlef Seese. An algebraic theory of graph reduction. *J. ACM*, 40(5):1134–1164, 1993. doi:10.1145/174147.169807.

2. Stefan Arnborg and Andrzej Proskurowski. Characterization and recognition of partial 3-trees. *SIAM Journal on Algebraic Discrete Methods*, 7(2):305–314, 1986. doi:10.1137/0607033.

3. Umberto Bertelè and Francesco Brioschi. On non-serial dynamic programming. *J. Comb. Theory, Ser. A*, 14(2):137–148, 1973. doi:10.1016/0097-3165(73)90016-2.

4. Hans L. Bodlaender. Treewidth: Algorithmic techniques and results. In Igor Prívara and Peter Ruzicka, editors, *Proc. MFCS*, volume 1295 of LNCS, pages 19–36. Springer, 1997. doi:10.1007/BFB0029946.

5. Enric Cosme-Llópez and Damien Pous. K4-free graphs as a free algebra. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, *Proc. MFCS*, volume 83 of LIPIcs, pages 76:1–76:14. Schloss Dagstuhl, 2017. doi:10.4230/LIPICS.MFCS.2017.76.

6. Bruno Courcelle. Graph grammars, monadic second-order logic and the theory of graph minors. In Neil Robertson and Paul D. Seymour, editors, *Proc. Graph Structure Theory*, volume 147 of *Contemporary Mathematics*, pages 565–590. American Mathematical Society, 1991.

7. Bruno Courcelle and Joost Engelfriet. *Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach*, volume 138 of *Encyclopedia of mathematics and its applications*. Cambridge University Press, 2012.

8. Reinhard Diestel. *Graph Theory*, 4th Edition, volume 173 of *Graduate texts in mathematics*. Springer, 2012.

9. Christian Doczkal and Damien Pous. Treewidth-two graphs as a free algebra. In Igor Potapov, Paul G. Spirakis, and James Worrell, editors, *Proc. MFCS*, volume 117 of LIPIcs, pages 60:1–60:15. Schloss Dagstuhl, 2018. doi:10.4230/LIPICS.MFCS.2018.60.

10. Amina Doumane, Samuel Humeau, and Damien Pous. A Finite Presentation of Graphs of Treewidth at Most Three. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, *51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)*, volume 297 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 135:1–135:18, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.135, doi:10.4230/LIPIcs.ICALP.2024.135.

11. Rudolf Halin. S-functions for graphs. *Journal of geometry*, 8:171–186, 1976. doi:10.1007/BF01917434.

12. Neil Robertson and Paul D. Seymour. Graph minors. II. algorithmic aspects of tree-width. *J. Algorithms*, 7(3):309–322, 1986. doi:10.1016/0196-6774(86)90023-4.

13. Neil Robertson and Paul D. Seymour. Graph minors. XX. wagner's conjecture. *J. Comb. Theory, Ser. B*, 92(2):325–357, 2004. doi:10.1016/J.JCTB.2004.08.001.

14. Daniel P. Sanders. *Linear algorithms for graphs of tree-width at most four*. PhD thesis, Georgia Institute of Technology, 1993. URL: http://hdl.handle.net/1853/30061.

15. Petra Scheffler. Linear-time algorithms for NP-complete problems restricted to partial k-trees. Technical report, Academy of Sciences of the GDR, 1987.

16. Thomas V. Wimer. *Linear Algorithms on k-Terminal Graphs*. PhD thesis, Clemson University, 1993. URL: https://tigerprints.clemson.edu/arv_dissertations/28.
**A Proofs for Section 2 (Graphs, treewidth)**

We first give a formal definition of graph isomorphism.

**Definition A.1.** Two graphs $G = (V_G, E_G, n_G, l_G, i_G)$ and $H = (V_H, E_H, n_H, l_H, i_H)$ are isomorphic if there are bijections $\varphi: V_G \to V_H$ and $\psi: E_G \to E_H$ such that

- $n_H \circ \psi = \mathcal{L}\varphi \circ n_G$ (preservation of neighbourhoods),

- $l_H \circ \psi = l_G$ (preservation of labels),

- and $i_H = \mathcal{L}\varphi(i_G)$ (preservation of the interface), where $\mathcal{L}\varphi$ denotes the pointwise extension of $\varphi$ to duplicate-free lists.

**Proposition 2.4.** If a graph $G$ and the graphs in the image of a substitution $\sigma$ all have treewidth at most $k$, then so does $G\sigma$.

**Proof.** Starting from a tree decomposition $T$ for $G$, we obtain a tree decomposition for $G\sigma$ by adding, for each $a$-labelled edge $e$ of $G$, a copy $T_e$ of a tree decomposition for $\sigma(a)$, and an edge connecting a bag of $T$ containing the neighbours of $e$ to a bag of $T_e$ containing the sources of $\sigma(a)$. This construction does not create bags, and thus preserves their maximal size. ▶

**B Proofs for Section 3 (Graph operations)**

**Lemma 3.3.** Every graph is isomorphic to a permutation of lifts of a full graph. This decomposition is unique up to permutation and isomorphism.

**Proof.** Starting from $G$, build a full graph $G'$ by removing all isolated sources both from the graph and from the interface. The graph $G$ can be obtained from $G'$ using as many lifts as there were isolated sources, followed by a permutation to move those isolated sources at their original places in the interface. ▶

**Lemma 3.4.** Every graph is isomorphic to a parallel composition of prime graphs. This decomposition is unique up to reindexing and isomorphism.

**Proof.** The relation $C$ on inner elements such that $xCy$ when $x$ and $y$ are connected via an inner path is an equivalence relation. Its equivalence classes seen as subgraphs provide the desired components. ▶

**Proposition 3.5.** Full prime graphs of treewidth at most $k$ and arity $k+1$ are atomic.

**Proof.** Let $G$ be a full prime graph of treewidth at most $k$ and arity $k+1$. We use the fact that graphs of treewidth at most $k$ cannot have the clique with $k+2$ vertices as a minor. If $G$ has an inner vertex $x$, then $x$ must be connected by inner paths to all vertices; we can thus contract all the inner vertices onto $x$, and obtain a clique with the sources and $x$, a contradiction. Thus the only inner elements of $G$ are edges; there must be exactly one since $G$ is prime, and it must connect all sources since $G$ is full. Therefore $G$ is atomic. ▶

**Lemma B.1.** Graphs of treewidth and arity at most $k$, and with an inner vertex, have $k$-forget points.

**Proof.** Take a tree decomposition of width at most $k$. If there is an isolated inner vertex, then it is a forget point. Otherwise, the given inner vertex is in the neighbourhood of an edge, and there are bags containing inner vertices. Take one of the shortest paths from a bag containing the sources to a bag containing some inner vertex $x$. By minimality, all bags along
**A Proofs for Section 2 (Graphs, treewidth)**

We first give a formal definition of graph isomorphism.

**Definition A.1.** Two graphs $G = (V_G, E_G, n_G, l_G, i_G)$ and $H = (V_H, E_H, n_H, l_H, i_H)$ are isomorphic if there are bijections $\varphi: V_G \to V_H$ and $\psi: E_G \to E_H$ such that

- $n_H \circ \psi = \mathcal{L}\varphi \circ n_G$ (preservation of neighbourhoods),

- $l_H \circ \psi = l_G$ (preservation of labels),

- and $i_H = \mathcal{L}\varphi(i_G)$ (preservation of the interface),
  where $\mathcal{L}\varphi$ denotes the pointwise extension of $\varphi$ to duplicate-free lists.

**Proposition 2.4.** If a graph $G$ and the graphs in the image of a substitution $\sigma$ all have treewidth at most $k$, then so does $G\sigma$.

**Proof.** Starting from a tree decomposition $T$ for $G$, we obtain a tree decomposition for $G\sigma$ by adding, for each $a$-labelled edge $e$ of $G$, a copy $T_e$ of a tree decomposition for $\sigma(a)$, and an edge connecting a bag of $T$ containing the neighbours of $e$ to a bag of $T_e$ containing the sources of $\sigma(a)$. This construction does not create bags, and thus preserves their maximal size. ◀

**B Proofs for Section 3 (Graph operations)**

**Lemma 3.3.** Every graph is isomorphic to a permutation of lifts of a full graph. This decomposition is unique up to permutation and isomorphism.

**Proof.** Starting from $G$, build a full graph $G'$ by removing all isolated sources both from the graph and from the interface. The graph $G$ can be obtained from $G'$ using as many lifts as there were isolated sources, followed by a permutation to move those isolated sources at their original places in the interface. ◀

**Lemma 3.4.** Every graph is isomorphic to a parallel composition of prime graphs. This decomposition is unique up to reindexing and isomorphism.

**Proof.** The relation $C$ on inner elements such that $xCy$ when $x$ and $y$ are connected via an inner path is an equivalence relation. Its equivalence classes seen as subgraphs provide the desired components. ◀

**Proposition 3.5.** Full prime graphs of treewidth at most $k$ and arity $k+1$ are atomic.

**Proof.** Let $G$ be a full prime graph of treewidth at most $k$ and arity $k+1$. We use the fact that graphs of treewidth at most $k$ cannot have the clique with $k+2$ vertices as a minor. If $G$ has an inner vertex $x$, then $x$ must be connected by inner paths to all vertices; we can thus contract all the inner vertices onto $x$, and obtain a clique with the sources and $x$, a contradiction. Thus the only inner elements of $G$ are edges; there must be exactly one since $G$ is prime, and it must connect all sources since $G$ is full. Therefore $G$ is atomic. ◀

**Lemma B.1.** Graphs of treewidth and arity at most $k$, and with an inner vertex, have $k$-forget points.

**Proof.** Take a tree decomposition of width at most $k$. If there is an isolated inner vertex, then it is a forget point. Otherwise, the given inner vertex is in the neighbourhood of an edge, and there are bags containing inner vertices. Take one of the shortest paths from a bag containing the sources to a bag containing some inner vertex $x$. By minimality, all bags along
this path but the last one must contain only sources. Add $x$ to all of them to obtain a tree decomposition for $(G, x)$ of width at most $k$, establishing that $x$ is a $k$-forget point of $G$. ◀

► **Proposition 3.7.** *Non-atomic full prime graphs of treewidth at most *k* have *k*-forget points.*

**Proof.** Direct consequence of Proposition 3.5 and Lemma B.1. ◀

**C Proofs for Section 4 (Terms and axioms)**

We give possible choices of concrete terms for the forget axioms in Definition 4.3. To ease notation, we first define the following three derived operations:

$$u \bullet v \triangleq \circ(u, v, \emptyset)$$

$$u^{\circ} \triangleq (12)u$$

$$\star(u, v, w) \triangleq \circ((21)lv, (13)lw, (23)lu)$$

<figure><img src="image_27.png" /></figure>

<figure><img src="image_28.png" /></figure>

<figure><img src="image_29.png" /></figure>

Observe that **FK** is just associativity of $\bullet$, i.e., $a \bullet (b \bullet c) \equiv (a \bullet b) \bullet c$. We can write the two other axioms as follows, using the edge orientations and labelling given on the right:

$$ \begin{array}{l} \text{FX:} \\ \quad \mathrm{ff}((23)\mathrm{lla} \parallel (42)\mathrm{llb} \parallel (14)\mathrm{l}(\star(d, e^{\circ}, c) \parallel \star(f, h^{\circ}, g))) \\ \qquad \equiv \end{array} $$

$$ \mathrm{ff}((13)\mathrm{lle} \parallel (14)\mathrm{llh} \parallel (24)\mathrm{l}(\star(a, g^{\circ}, c^{\circ}) \parallel \star(b, f^{\circ}, d^{\circ}))) $$

<figure><img src="image_30.png" /></figure>

$$ \begin{array}{l} \text{FD:} \\ \quad \mathrm{ff}((23)\mathrm{lla} \parallel (42)\mathrm{llb} \parallel (14)\mathrm{l}(\circ(\star(i^{\circ}, h^{\circ}, c), \star(f, g^{\circ}, e), \star(d, k^{\circ}, j^{\circ}))) \\ \qquad \equiv \end{array} $$

$$ \mathrm{ff}((13)\mathrm{llk} \parallel (14)\mathrm{llh} \parallel (24)\mathrm{l}(\circ(\star(g, i, j), \star(b, f^{\circ}, d^{\circ}), \star(a, c^{\circ}, e^{\circ}))) $$

<figure><img src="image_31.png" /></figure>

**D Proofs for Section 5 (Outline of the completeness proof)**

► **Proposition 5.1.** For all terms $t$, letters $a$, and graphs $G, H$, we have:

1. if $g(t) \cong \emptyset$ then $t \equiv \emptyset$;

2. if $g(t) \cong a$ then $t \equiv a$;

3. if $g(t) \cong pG$ then there is a parsing $u$ of $G$ such that $t \equiv pu$;

4. if $g(t) \cong 1G$ then there is a parsing $u$ of $G$ such that $t \equiv lu$;

5. if $g(t) \cong G \parallel H$ then there are parsings $u$ of $G$ and $v$ of $H$ such that $t \equiv u \parallel v$.

**Proof.** All items but the third one are proven by induction on $t$.

1. Here $t$ cannot be a letter or a forget; in the other cases we use **A1-4**.

2. We show that for all permutations $p$, $g(t) \cong pa$ implies $t \equiv pa$; $t$ cannot be $\emptyset$, a forget or a lift; in the other cases we use **A1-2** and the previous item. The initial statement follows by choosing the identity permutation.

3. We take $u = p^{-1}t$ and use **A2**.

4. We show by induction on $t$ that for all permutations $p$ and graphs $G$ such that $g(t) \cong plG$, there is a parsing $u$ of $G$ such that $t \equiv plu$; the initial statement follows by choosing the identity permutation. The term $t$ cannot be a letter; if it is $\emptyset$ then we take $u = \emptyset$ and we conclude using **A3-4**; if it is a parallel composition we use the induction hypothesis and **A3-4** again. It remains three cases:
this path but the last one must contain only sources. Add $x$ to all of them to obtain a tree decomposition for $(G, x)$ of width at most $k$, establishing that $x$ is a $k$-forget point of $G$. ◀

► **Proposition 3.7.** *Non-atomic full prime graphs of treewidth at most *k* have *k*-forget points.*

**Proof.** Direct consequence of Proposition 3.5 and Lemma B.1. ◀

**C Proofs for Section 4 (Terms and axioms)**

We give possible choices of concrete terms for the forget axioms in Definition 4.3. To ease notation, we first define the following three derived operations:

$$u \bullet v \triangleq \circ(u, v, \emptyset)$$

$$u^{\circ} \triangleq (12)u$$

$$\star(u, v, w) \triangleq \circ((21)lv, (13)lw, (23)lu)$$

<figure><img src="image_24.png" /></figure>

<figure><img src="image_25.png" /></figure>

<figure><img src="image_26.png" /></figure>

Observe that **FK** is just associativity of $\bullet$, i.e., $a \bullet (b \bullet c) \equiv (a \bullet b) \bullet c$. We can write the two other axioms as follows, using the edge orientations and labelling given on the right:

$$ \begin{array}{l} \text{FX:} \\ \quad \mathrm{ff}((23)\mathrm{lla} \parallel (42)\mathrm{llb} \parallel (14)\mathrm{l}(\star(d, e^{\circ}, c) \parallel \star(f, h^{\circ}, g))) \\ \quad \equiv \end{array} $$

$$ \mathrm{ff}((13)\mathrm{lle} \parallel (14)\mathrm{llh} \parallel (24)\mathrm{l}(\star(a, g^{\circ}, c^{\circ}) \parallel \star(b, f^{\circ}, d^{\circ}))) $$

<figure><img src="image_27.png" /></figure>

$$ \begin{array}{l} \text{FD:} \\ \quad \mathrm{ff}((23)\mathrm{lla} \parallel (42)\mathrm{llb} \parallel (14)\mathrm{l}(\circ(\star(i^{\circ}, h^{\circ}, c), \star(f, g^{\circ}, e), \star(d, k^{\circ}, j^{\circ}))) \\ \quad \equiv \end{array} $$

$$ \mathrm{ff}((13)\mathrm{llk} \parallel (14)\mathrm{llh} \parallel (24)\mathrm{l}(\circ(\star(g, i, j), \star(b, f^{\circ}, d^{\circ}), \star(a, c^{\circ}, e^{\circ}))) $$

<figure><img src="image_28.png" /></figure>

**D Proofs for Section 5 (Outline of the completeness proof)**

► **Proposition 5.1.** For all terms $t$, letters $a$, and graphs $G, H$, we have:

1. if $g(t) \cong \emptyset$ then $t \equiv \emptyset$;

2. if $g(t) \cong a$ then $t \equiv a$;

3. if $g(t) \cong pG$ then there is a parsing $u$ of $G$ such that $t \equiv pu$;

4. if $g(t) \cong 1G$ then there is a parsing $u$ of $G$ such that $t \equiv lu$;

5. if $g(t) \cong G \parallel H$ then there are parsings $u$ of $G$ and $v$ of $H$ such that $t \equiv u \parallel v$.

**Proof.** All items but the third one are proven by induction on $t$.

1. Here $t$ cannot be a letter or a forget; in the other cases we use **A1-4**.

2. We show that for all permutations $p$, $g(t) \cong pa$ implies $t \equiv pa$; $t$ cannot be $\emptyset$, a forget or a lift; in the other cases we use **A1-2** and the previous item. The initial statement follows by choosing the identity permutation.

3. We take $u = p^{-1}t$ and use **A2**.

4. We show by induction on $t$ that for all permutations $p$ and graphs $G$ such that $g(t) \cong plG$, there is a parsing $u$ of $G$ such that $t \equiv plu$; the initial statement follows by choosing the identity permutation. The term $t$ cannot be a letter; if it is $\emptyset$ then we take $u = \emptyset$ and we conclude using **A3-4**; if it is a parallel composition we use the induction hypothesis and **A3-4** again. It remains three cases:
- if $t = qt'$ for some permutation $q$, then $g(t') \simeq q^{-1}plG$. By induction we find a parsing $u$ of $G$ such that $t' \equiv (q^{-1} \circ p)lu$. We deduce $t \equiv plu$ using **A2**;

- if $t = ft'$, then $g(t) = f(g(t')) \simeq plG$ so that, adding the source corresponding to the forget operation to $G$, there is a graph $G'$ such that $G \simeq fG'$ and $g(t') \simeq \dot{p}rlG'$, where $r$ is the permutation that swaps the last two elements, and $\dot{p}$ is the extension of $p$ (fixing the last element). By induction we find a parsing $u$ of $G'$ such that $t' \equiv (\dot{p} \circ r)lu$. Then we have

$$ t = ft' \equiv f(\dot{p} \circ r)lu \\ \equiv f\dot{p}rlu \qquad (\text{by A2}) $$

$$ \equiv pfrlu \qquad (\text{by A5}) $$

$$ \equiv plfu \qquad (\text{by A6}) $$

- if $t = lt'$ and $g(t) = l(g(t')) \simeq plG$ then there are two cases:

- if the two lift operations in the latter graph isomorphism concern the same source in $G$, then it is the last one and $p$ must fix the last element, i.e., $p = \dot{q}$ for some permutation $q$ and $g(t') \simeq qG$. By the third item we find a parsing $u$ of $G$ such that $t' \equiv qu$, and we have $t = lt' \equiv lqu \equiv \dot{q}lu = plu$ using **A5**;

- otherwise, the source $s$ corresponding to the lift operation in $plG$ must be isolated in $g(t')$, and the last element is not fixed by $p$. We assume it is mapped to the $i$th one. By Lemma 3.3 restricted to the source $s$ only there is a permutation $q$ such that $g(t') \simeq qlG'$, the lift corresponds to $s$, and $q$ maps the $i$th element to the last one. The permutation $r^{-1} \circ \dot{q}^{-1} \circ p$ must fix its last element so we assume it is equal to $\dot{q}'$ for some $q'$. By definition we have that $p = \dot{q} \circ r \circ \dot{q}'$. By induction and **A2** we find a parsing $u$ of $G'$ such that $t' \equiv qlu$. Then we have

$$ t = lt' \equiv lqlu \\ \equiv \dot{q}llu \qquad (\text{by A5}) $$

$$ \equiv \dot{q}rllu \qquad (\text{by A6}) $$

$$ \equiv \dot{q}rl(q' \circ q'^{-1})lu \qquad (\text{by A2}) $$

$$ \equiv \dot{q}r\dot{q}'lq'^{-1}lu \qquad (\text{by A5}) $$

$$ = plq'^{-1}lu $$

5. The cases where $t$ is $\emptyset$, a letter, a lift or a permutation are easy. In the case where $t = t_1 \parallel t_2$, we split $G$ and $H$ accordingly: $G \simeq G_1 \parallel G_2$, and $H \simeq H_1 \parallel H_2$ such that $g(t_1) \simeq G_1 \parallel H_1$ and $g(t_2) \simeq G_2 \parallel H_2$; we use the induction hypothesis on $t_1$ and $t_2$ and we conclude using associativity and commutativity.

The forget case is the interesting one. In that case, $t = ft'$, then $g(t) = fg(t') \simeq G \parallel H$ and we may assume without loss of generality that the forget point appears in $G: G \simeq fG'$ for some graph $G'$ such that $g(t') \simeq G' \parallel lH$. By induction hypothesis we obtain parsings $u$ of $G'$ and $v'$ of $lH$ such that $t' \equiv u \parallel v'$. By the fourth point we get a parsing $v$ of $H$ such that $v' \equiv lv$. We conclude using **A7**: $fu$ and $v$ are parsings of $G$ and $H$ such that $t = ft' \equiv f(u \parallel lv) \equiv fu \parallel v$. $\quad$

**Lemma D.1.** For all graphs $G$ with forget points $x, y$ in Figures 3 and 4, both $(G, x)$ and $(G, y)$ are easy.

**Proof.** By symmetry, it suffices to prove the statement for $(G, x)$.
- if $t = qt'$ for some permutation $q$, then $g(t') \simeq q^{-1}plG$. By induction we find a parsing $u$ of $G$ such that $t' \equiv (q^{-1} \circ p)lu$. We deduce $t \equiv plu$ using **A2**;

- if $t = ft'$, then $g(t) = f(g(t')) \simeq plG$ so that, adding the source corresponding to the forget operation to $G$, there is a graph $G'$ such that $G \simeq fG'$ and $g(t') \simeq \dot{p}rlG'$, where $r$ is the permutation that swaps the last two elements, and $\dot{p}$ is the extension of $p$ (fixing the last element). By induction we find a parsing $u$ of $G'$ such that $t' \equiv (\dot{p} \circ r)lu$. Then we have

$$t = ft' \equiv f(\dot{p} \circ r)lu \\ \equiv f\dot{p}rlu \qquad (\text{by A2})$$

$$\equiv pfrlu \qquad (\text{by A5})$$

$$\equiv plfu \qquad (\text{by A6})$$

- if $t = lt'$ and $g(t) = l(g(t')) \simeq p\dot{l}G$ then there are two cases:

- if the two lift operations in the latter graph isomorphism concern the same source in $G$, then it is the last one and $p$ must fix the last element, i.e., $p = \dot{q}$ for some permutation $q$ and $g(t') \simeq qG$. By the third item we find a parsing $u$ of $G$ such that $t' \equiv qu$, and we have $t = lt' \equiv lqu \equiv \dot{q}lu = plu$ using **A5**;

- otherwise, the source $s$ corresponding to the lift operation in $plG$ must be isolated in $g(t')$, and the last element is not fixed by $p$. We assume it is mapped to the $i$th one. By Lemma 3.3 restricted to the source $s$ only there is a permutation $q$ such that $g(t') \simeq q\dot{l}G'$, the lift corresponds to $s$, and $q$ maps the $i$th element to the last one. The permutation $r^{-1} \circ \dot{q}^{-1} \circ p$ must fix its last element so we assume it is equal to $\dot{q}'$ for some $q'$. By definition we have that $p = \dot{q} \circ r \circ \dot{q}'$. By induction and **A2** we find a parsing $u$ of $G'$ such that $t' \equiv q\dot{l}u$. Then we have

$$t = lt' \equiv l\dot{l}u \\ \equiv \dot{q}\dot{l}u \qquad (\text{by A5})$$

$$\equiv \dot{q}r\dot{l}u \qquad (\text{by A6})$$

$$\equiv \dot{q}r\dot{l}(q' \circ q'^{-1})lu \qquad (\text{by A2})$$

$$\equiv \dot{q}r\dot{q}'lq'^{-1}lu \qquad (\text{by A5})$$

$$= plq'^{-1}lu$$

5. The cases where $t$ is $\emptyset$, a letter, a lift or a permutation are easy. In the case where $t = t_1 \parallel t_2$, we split $G$ and $H$ accordingly: $G \simeq G_1 \parallel G_2$, and $H \simeq H_1 \parallel H_2$ such that $g(t_1) \simeq G_1 \parallel H_1$ and $g(t_2) \simeq G_2 \parallel H_2$; we use the induction hypothesis on $t_1$ and $t_2$ and we conclude using associativity and commutativity.

The forget case is the interesting one. In that case, $t = ft'$, then $g(t) = fg(t') \simeq G \parallel H$ and we may assume without loss of generality that the forget point appears in $G: G \simeq fG'$ for some graph $G'$ such that $g(t') \simeq G' \parallel lH$. By induction hypothesis we obtain parsings $u$ of $G'$ and $v'$ of $lH$ such that $t' \equiv u \parallel v'$. By the fourth point we get a parsing $v$ of $H$ such that $v' \equiv lv$. We conclude using **A7**: $fu$ and $v$ are parsings of $G$ and $H$ such that $t = ft' \equiv f(u \parallel lv) \equiv fu \parallel v$. ◀

► **Lemma D.1.** For all graphs $G$ with forget points $x, y$ in Figures 3 and 4, both $(G, x)$ and $(G, y)$ are easy.

**Proof.** By symmetry, it suffices to prove the statement for $(G, x)$.
- This is trivial for $FS_i$ and $FK$: for each of them, $(G, x)$ as only one inner vertex left.

- For $FX$, observe that $(FX, x)$ is full prime and its only forget point is the vertex depicted below $x$ (call it $x'$); then $(FX, x, x')$ has four reduced components: two edges and two graphs which are easy since they have only one inner vertex.

- For $FD$, $(FD, x)$ is full prime and its only forget point is the bottom-most vertex below $x$ (call it $x'$); then $(FD, x, x')$ has three reduced components: two edges with the source on the left, and the remainder of the graph. Again, there is a single forget point: the middle inner vertex on the right. From there we reach three reduced components, each with only one inner vertex.

(In those arguments, in order to see that an inner vertex cannot be a forget point, it often suffices to show that it would give a full prime graph of arity four which is not atomic.) ◀

## E Proofs for Section 7 (Anchors)

In the rest of the appendices we use some usual notations for paths. We call *simple* a path without vertex repetition. Every (inner) path can be reduced to a simple (inner) path with the same endpoints.

**Convention E.1.** In the rest of the appendices, we only work with simple paths, except if stated otherwise.

Given a path $P$ and $x$ a vertex in $P$, we write $xP$ for the suffix of $P$ starting at $x$, and $Px$ prefix of $P$ stopping at $x$. Given two inner disjoint paths $P$ and $Q$ such that $P$ ends at $Q$'s first vertex, we note $PQ$ for their concatenation. We write $\bar{P}$ for the reversal of a path $P$. We extend these notations whenever they make sense on simple paths. For example we may write $xQy\bar{P}zR$. Given subgraphs $H$ and $K$ of a graph $G$, we call $H-K$ path a path from an inner vertex of $H$ to one of $K$ that meets $H$ and $K$ only at its endpoints. Most often $H$ will be just a vertex and $K$ will be a path.

See [10] for a reference; there paths are called walks, and simple paths just paths.

**Lemma E.2.** Let $G$ be a full prime graph with two inner vertices $x, y$. If $x$ is in the $i$th series argument at $y$, then $y$ is a checkpoint between $x$ and the $i$th source in $G$.

**Proof.** By definition the $i$th series argument of a series decomposition of $G$ does not contain its $i$th source. Let $P$ be an inner path from $x$ to the $i$th source of $G$. It must start in the $i$th series argument at $x$ and end outside at the $i$th source, as was just observed. As $P$ is inner, it can only get out from the $i$th series argument at $y$. ◀

**Lemma E.3.** Let $G$ be a graph with two inner vertices $x$ and $y$ and two designated sources $s_x$ and $s_y$. If $x$ is a checkpoint between $y$ and $s_y$ and $y$ a checkpoint between $x$ and $s_x$, then $x$ and $y$ are both checkpoints between $s_x$ and $s_y$.

**Proof.** By symmetry, it suffices to show that $x$ is a checkpoint between $s_x$ and $s_y$. Let $P$ be an inner path from $s_x$ to $s_y$. Consider a shortest $y-P$ inner path $Q$ in $G$. Such a path exists as $G$ is full prime and $y$ is thus inner connected to any inner element of $P$. Say $Q$ is from $y$ to $z$ for some $z$ in $P$. The inner path $QzP$ goes from $y$ to $s_y$, so that it must contain $x$ by assumption. If $x$ belongs to $zP$ then we are done. Otherwise $x$ belongs to $Qz$. In that case, the inner path $xQz\bar{P}$ goes from $x$ to $s_x$ and must contain $y$ by assumption, which contradicts the minimality assumption about $Q$. ◀

**Lemma E.4.** In a full prime graph of arity three, the series factor at each anchor cannot contain inner vertices.
- This is trivial for $FS_i$ and $FK$: for each of them, $(G, x)$ as only one inner vertex left.

- For $FX$, observe that $(FX, x)$ is full prime and its only forget point is the vertex depicted below $x$ (call it $x'$); then $(FX, x, x')$ has four reduced components: two edges and two graphs which are easy since they have only one inner vertex.

- For $FD$, $(FD, x)$ is full prime and its only forget point is the bottom-most vertex below $x$ (call it $x'$); then $(FD, x, x')$ has three reduced components: two edges with the source on the left, and the remainder of the graph. Again, there is a single forget point: the middle inner vertex on the right. From there we reach three reduced components, each with only one inner vertex.

(In those arguments, in order to see that an inner vertex cannot be a forget point, it often suffices to show that it would give a full prime graph of arity four which is not atomic.) ◀

## E Proofs for Section 7 (Anchors)

In the rest of the appendices we use some usual notations for paths. We call *simple* a path without vertex repetition. Every (inner) path can be reduced to a simple (inner) path with the same endpoints.

**Convention E.1.** In the rest of the appendices, we only work with simple paths, except if stated otherwise.

Given a path $P$ and $x$ a vertex in $P$, we write $xP$ for the suffix of $P$ starting at $x$, and $Px$ prefix of $P$ stopping at $x$. Given two inner disjoint paths $P$ and $Q$ such that $P$ ends at $Q$'s first vertex, we note $PQ$ for their concatenation. We write $\bar{P}$ for the reversal of a path $P$. We extend these notations whenever they make sense on simple paths. For example we may write $xQy\bar{P}zR$. Given subgraphs $H$ and $K$ of a graph $G$, we call $H-K$ path a path from an inner vertex of $H$ to one of $K$ that meets $H$ and $K$ only at its endpoints. Most often $H$ will be just a vertex and $K$ will be a path.

See [8] for a reference; there paths are called *walks*, and simple paths just *paths*.

**Lemma E.2.** Let $G$ be a full prime graph with two inner vertices $x, y$. If $x$ is in the $i$th series argument at $y$, then $y$ is a checkpoint between $x$ and the $i$th source in $G$.

**Proof.** By definition the $i$th series argument of a series decomposition of $G$ does not contain its $i$th source. Let $P$ be an inner path from $x$ to the $i$th source of $G$. It must start in the $i$th series argument at $x$ and end outside at the $i$th source, as was just observed. As $P$ is inner, it can only get out from the $i$th series argument at $y$. ◀

**Lemma E.3.** Let $G$ be a graph with two inner vertices $x$ and $y$ and two designated sources $s_x$ and $s_y$. If $x$ is a checkpoint between $y$ and $s_y$ and $y$ a checkpoint between $x$ and $s_x$, then $x$ and $y$ are both checkpoints between $s_x$ and $s_y$.

**Proof.** By symmetry, it suffices to show that $x$ is a checkpoint between $s_x$ and $s_y$. Let $P$ be an inner path from $s_x$ to $s_y$. Consider a shortest $y-P$ inner path $Q$ in $G$. Such a path exists as $G$ is full prime and $y$ is thus inner connected to any inner element of $P$. Say $Q$ is from $y$ to $z$ for some $z$ in $P$. The inner path $QzP$ goes from $y$ to $s_y$, so that it must contain $x$ by assumption. If $x$ belongs to $zP$ then we are done. Otherwise $x$ belongs to $Qz$. In that case, the inner path $xQz\bar{P}$ goes from $x$ to $s_x$ and must contain $y$ by assumption, which contradicts the minimality assumption about $Q$. ◀

**Lemma E.4.** In a full prime graph of arity three, the series factor at each anchor cannot contain inner vertices.
**Proof.** We use the fact that graphs of treewidth at most three cannot have the clique $K_5$ over five vertices as a minor. Let $x$ be an anchor in a full prime graph $G$ of arity three and assume by contradiction that the series factor at $x$ has a component $C$ with some inner vertex $y$. There are two cases:

- $C$ is the only component of the series factor. Since $x$ is an anchor, $C$ must have an edge $e$ containing $x$ and the three sources. As $C$ is full prime and contains $y$, $e$ must contain another inner vertex of $C$ (possibly $y$): its arity is at least five, a contradiction.

- The series factor has (at least) one other component $D$. Since components of series factors are full prime, all inner vertices of $D$ are inner connected to all sources of $G$ and $x$, and similarly for the inner vertices of $C$. Contract all inner vertices of $D$ onto $x$, and all inner vertices of $C$ onto $y$. This yields a minor with edges between $x$ and each and every source, similarly for $y$, and an edge between $x$ and $y$. Since we can always assume a clique between the sources, we have obtained $K_5$ as a minor of $G$, a contradiction. ◀

**Proposition 7.5.** *At arity three, every full prime graph with two distinct anchors $x, y$ has the following shape:*

<figure><img src="image_32.png" /></figure>

**Proof.** By Lemma E.4, $x$ (resp. $y$) cannot be in the series factor of $G$ at $y$ (resp. $x$): it must be in a series argument of the series decomposition on $y$ (resp. $x$), say the $i$th (resp. $j$th) one. By Lemma E.2 this makes $x$ (resp. $y$) a checkpoint between $y$ (resp. $x$) and the $i$th (resp. $j$th) source of $G$. We conclude with Lemma E.3. ◀

**Lemma 7.6.** *Let $t$ be a term of arity up to two with an inner vertex $x$ in a full prime component. There is a term $u$ such that $t \equiv fu$ and $x$ is either the last source of $u$ or an inner vertex of a full prime component of $u$.*

**Proof.** We do a proof by induction on the size of the component $C$ of $t$ containing $x$. First we use Proposition 5.1 to find a parsing $t_x$ of $C$ and a term $t'$ such that $t \equiv t_x \parallel t'$. By hypothesis $t_x$ is full prime. Hence we can use Lemma 5.2 to find a term $u$ such that $t_x \equiv fu$.

If $u$ is a parsing of $(gt_x, x)$, or if $x$ is in a full prime component of $u$ then we conclude using **A7**.

Otherwise $x$ is in a component $D$ of $u$ that is smaller in size than $C$ but not full prime. We use Proposition 5.1 to find terms $u_x$ and $u'$ and a permutation $p$ such that $u \equiv pl^i u_x \parallel u'$ where $u_x$ is a parsing of the reduced component associated to $D$.

As $u_x$ is full prime and contains $x$ we can use the induction hypothesis: there exists a term $v$ such that $u_x \equiv fv$ and either $v$'s last source is $x$ or $x$ is in a full prime component of $v$. Let $y$ be the last source of $v$; in subsequent term equations we write $f_y$ for the forget operation that forgets $y$.

At this point we have:

$$t \equiv f(pl^i f_y v \parallel u') \parallel t' \qquad (\text{by A6})$$

$$\equiv f(p f_y(r1)^i v \parallel u') \parallel t' \qquad (\text{by A5})$$

$$\equiv ff_y((\dot{p}(r1))^i v \parallel 1u') \parallel lt' \qquad (\text{by A7})$$

$$\equiv f_y \text{ fr}((\dot{p}(r1))^i v \parallel 1u') \parallel lt' \qquad (\text{by FS})$$
**Proof.** We use the fact that graphs of treewidth at most three cannot have the clique $K_5$ over five vertices as a minor. Let $x$ be an anchor in a full prime graph $G$ of arity three and assume by contradiction that the series factor at $x$ has a component $C$ with some inner vertex $y$. There are two cases:

- $C$ is the only component of the series factor. Since $x$ is an anchor, $C$ must have an edge $e$ containing $x$ and the three sources. As $C$ is full prime and contains $y$, $e$ must contain another inner vertex of $C$ (possibly $y$): its arity is at least five, a contradiction.

- The series factor has (at least) one other component $D$. Since components of series factors are full prime, all inner vertices of $D$ are inner connected to all sources of $G$ and $x$, and similarly for the inner vertices of $C$. Contract all inner vertices of $D$ onto $x$, and all inner vertices of $C$ onto $y$. This yields a minor with edges between $x$ and each and every source, similarly for $y$, and an edge between $x$ and $y$. Since we can always assume a clique between the sources, we have obtained $K_5$ as a minor of $G$, a contradiction. ◀

**Proposition 7.5.** *At arity three, every full prime graph with two distinct anchors $x, y$ has the following shape:*

<figure><img src="image_29.png" /></figure>

**Proof.** By Lemma E.4, $x$ (resp. $y$) cannot be in the series factor of $G$ at $y$ (resp. $x$): it must be in a series argument of the series decomposition on $y$ (resp. $x$), say the $i$th (resp. $j$th) one. By Lemma E.2 this makes $x$ (resp. $y$) a checkpoint between $y$ (resp. $x$) and the $i$th (resp. $j$th) source of $G$. We conclude with Lemma E.3. ◀

**Lemma 7.6.** *Let $t$ be a term of arity up to two with an inner vertex $x$ in a full prime component. There is a term $u$ such that $t \equiv fu$ and $x$ is either the last source of $u$ or an inner vertex of a full prime component of $u$.*

**Proof.** We do a proof by induction on the size of the component $C$ of $t$ containing $x$. First we use Proposition 5.1 to find a parsing $t_x$ of $C$ and a term $t'$ such that $t \equiv t_x \parallel t'$. By hypothesis $t_x$ is full prime. Hence we can use Lemma 5.2 to find a term $u$ such that $t_x \equiv fu$.

If $u$ is a parsing of $(gt_x, x)$, or if $x$ is in a full prime component of $u$ then we conclude using **A7**.

Otherwise $x$ is in a component $D$ of $u$ that is smaller in size than $C$ but not full prime. We use Proposition 5.1 to find terms $u_x$ and $u'$ and a permutation $p$ such that $u \equiv pl^i u_x \parallel u'$ where $u_x$ is a parsing of the reduced component associated to $D$.

As $u_x$ is full prime and contains $x$ we can use the induction hypothesis: there exists a term $v$ such that $u_x \equiv fv$ and either $v$'s last source is $x$ or $x$ is in a full prime component of $v$. Let $y$ be the last source of $v$; in subsequent term equations we write $f_y$ for the forget operation that forgets $y$.

At this point we have:

$$t \equiv f(pl^i f_y v \parallel u') \parallel t' \qquad (\text{by A6})$$

$$\equiv f(p f_y (r1)^i v \parallel u') \parallel t' \qquad (\text{by A5})$$

$$\equiv ff_y((\dot{p}(r1))^i v \parallel 1u') \parallel lt' \qquad (\text{by A7})$$

$$\equiv f_y \text{ fr}((\dot{p}(r1))^i v \parallel 1u') \parallel lt' \qquad (\text{by FS})$$
where $\tilde{p}$ is the extension of $p$ fixing the last element and $r$ is the permutation swapping the last two elements (at various arities, here).

If $x$ is $v$'s last source, then $x = y$ and the derivation above proves that there exists a term $w$ such that $t \equiv fw$ and $w$'s last source is $x$. Otherwise $x$ is in a full prime component of $v$ and to end the proof we show that it is also in a full prime component of $w \triangleq \text{fr}((\tilde{p}(rl))^i v \parallel lu') \parallel lt'$), i.e. that $x$ is inner connected to all sources in $w$.

Call $z$ the source forgotten by the forget operation in $w$, and consider the shape of $(gt, y)$ given by the definition of $w$:

<figure><img src="image_33.png" /></figure>

In this picture, the red triangle is used to represent all sources of $t$ that are not sources of $v$ (those corresponding to the operation $(rl)^i$), and the green pentagon is used to represent the common sources of $t$ and $v$.

As $x$ is in a full prime component of $v$, we easily get that $x$ is inner connected to $y$, $z$, and to all sources represented by the green pentagon.

Moreover, $z$ is a checkpoint between $x$ and all sources represented by the red triangle. As $x$ is in a full prime component of $t$, there must be inner paths from $z$ to any such source in $t'$, and hence in $w$ too. By transitivity, $x$ is also inner connected to all sources represented by the red triangle. ◄

**Lemma 7.7.** For $i > 0$ let $f^i G$ be a full prime graph of arity $k$ and $x, y$ two distinct inner vertices in a full prime component $C$ of $G$. If $x$ is an anchor of $f^i G$ and is in one of the first $k$ series arguments of the series decomposition of $C$ at $y$, then $x$ is a checkpoint in $C$.

**Proof.** We reason by case analysis on the conditions that may apply to make $x$ an anchor in $f^i G$. We note $x_1, \dots, x_i$ the sources of $G$ forgotten by the operations $f^i$ in the latter graph.

Suppose that $x$ is in the $j$th series argument of $C$ at $y$. By Lemma E.2, $y$ is a checkpoint between $x$ and the $j$th source $s$ in $C$ and furthermore in $G$.

In particular no edge can contain both $x$ and $s$. As $j \le k$, $s$ is also a source of $f^i G$ and $x$ cannot be an anchor of the second kind in Definition 7.2.

If $x$ is an anchor of the first type in Definition 7.2 then the series factor of $f^i G$ at $x$ must be empty and inner vertices of $f^i G$ must be in the associated series arguments. This is the case of all $x_i$s. Assume, for example, that $x_1$ is in the $n$th series argument. By Lemma E.2 $x$ is a checkpoint between $x_1$ and the $j$th source in $f^i G$. This obviously remains true in $C$.

We can now assume that $x$ is an anchor of the third kind in $f^i G$: there are at least two full prime components in the series factor of $f^i G$ at $x$. At least one of these components does not contain $y$. Being full prime, this component provides us with an inner path $P$ from $x$ to the $j$th source $s$ in $f^i G$ that does not contain $y$. It cannot be an inner path in $G$ as in $G$, $y$ is a checkpoint between $x$ and $s$. As $G$ and $f^i G$ differ only on their sources, this means that $P$ must contain some $x_k$.

Vertices $x_k$ and $y$ being in different components in the series decomposition of $f^i G$ at $x$, $x$ is a checkpoint between $x_k$ to $y$ in $f^i G$, and it remains so in $G$ and hence in $C$ as all inner paths of $C$ are inner paths of both $G$ and $f^i G$.

We have shown that in $C$, $x$ is a checkpoint between the source $x_k$ and $y$, and $y$ is a checkpoint between $x$ and the $j$th source. We conclude using Lemma E.3. ◄
where $\tilde{p}$ is the extension of $p$ fixing the last element and $r$ is the permutation swapping the last two elements (at various arities, here).

If $x$ is $v$'s last source, then $x = y$ and the derivation above proves that there exists a term $w$ such that $t \equiv fw$ and $w$'s last source is $x$. Otherwise $x$ is in a full prime component of $v$ and to end the proof we show that it is also in a full prime component of $w \triangleq \text{fr}((\tilde{p}(rl))^i v \parallel lu') \parallel lt'$), i.e. that $x$ is inner connected to all sources in $w$.

Call $z$ the source forgotten by the forget operation in $w$, and consider the shape of $(gt, y)$ given by the definition of $w$:

<figure><img src="image_30.png" /></figure>

In this picture, the red triangle is used to represent all sources of $t$ that are not sources of $v$ (those corresponding to the operation $(rl)^i$), and the green pentagon is used to represent the common sources of $t$ and $v$.

As $x$ is in a full prime component of $v$, we easily get that $x$ is inner connected to $y$, $z$, and to all sources represented by the green pentagon.

Moreover, $z$ is a checkpoint between $x$ and all sources represented by the red triangle. As $x$ is in a full prime component of $t$, there must be inner paths from $z$ to any such source in $t'$, and hence in $w$ too. By transitivity, $x$ is also inner connected to all sources represented by the red triangle. ◀

**Lemma 7.7.** For $i > 0$ let $f^i G$ be a full prime graph of arity $k$ and $x, y$ two distinct inner vertices in a full prime component $C$ of $G$. If $x$ is an anchor of $f^i G$ and is in one of the first $k$ series arguments of the series decomposition of $C$ at $y$, then $x$ is a checkpoint in $C$.

**Proof.** We reason by case analysis on the conditions that may apply to make $x$ an anchor in $f^i G$. We note $x_1, \dots, x_i$ the sources of $G$ forgotten by the operations $f^i$ in the latter graph.

Suppose that $x$ is in the $j$th series argument of $C$ at $y$. By Lemma E.2, $y$ is a checkpoint between $x$ and the $j$th source $s$ in $C$ and furthermore in $G$.

In particular no edge can contain both $x$ and $s$. As $j \le k$, $s$ is also a source of $f^i G$ and $x$ cannot be an anchor of the second kind in Definition 7.2.

If $x$ is an anchor of the first type in Definition 7.2 then the series factor of $f^i G$ at $x$ must be empty and inner vertices of $f^i G$ must be in the associated series arguments. This is the case of all $x_i$s. Assume, for example, that $x_1$ is in the $n$th series argument. By Lemma E.2 $x$ is a checkpoint between $x_1$ and the $j$th source in $f^i G$. This obviously remains true in $C$.

We can now assume that $x$ is an anchor of the third kind in $f^i G$: there are at least two full prime components in the series factor of $f^i G$ at $x$. At least one of these components does not contain $y$. Being full prime, this component provides us with an inner path $P$ from $x$ to the $j$th source $s$ in $f^i G$ that does not contain $y$. It cannot be an inner path in $G$ as in $G$, $y$ is a checkpoint between $x$ and $s$. As $G$ and $f^i G$ differ only on their sources, this means that $P$ must contain some $x_k$.

Vertices $x_k$ and $y$ being in different components in the series decomposition of $f^i G$ at $x$, $x$ is a checkpoint between $x_k$ to $y$ in $f^i G$, and it remains so in $G$ and hence in $C$ as all inner paths of $C$ are inner paths of both $G$ and $f^i G$.

We have shown that in $C$, $x$ is a checkpoint between the source $x_k$ and $y$, and $y$ is a checkpoint between $x$ and the $j$th source. We conclude using Lemma E.3. ◀
**F Proofs for Section 8 (Separation pairs)**

The following three lemmas (Lemmas F.1, F.2, F.3), as well as Proposition 8.7, hold without any restriction on the treewidth.

**Lemma F.1.** Let $G$ be a graph of arity three with three inner paths $P_1, P_2$, and $P_3$, respectively from the first to the second, the second to the third, and the third to the first sources. If no vertex is shared by the three paths then $G$ admits $K_3$ as a sourced minor.

**Proof.** Endpoints and vertices of paths are preserved by taking the footprint of a graph: the lemma holds for a graph whenever it holds for its footprint. Hence we may assume that $G$ is a sourced simple graph.

We write $s_1, s_2, s_3$ for the three sources of $G$.

We reason by induction on the sum of the lengths of the paths, with the length of a path being the number of inner elements it contains.

If $P_1, P_2$, and $P_3$ are all of length 1 then they are reduced to edges connecting pairs of sources. Said otherwise, $G$ contains $K_3$ as a subgraph, and by extension as a minor.

Otherwise, at least one of the paths $P_i$, say $P_1$, has an inner vertex. We note $e$ for the first edge and $x$ for the first inner vertex of $P_1$.

If $x$ does not appear in either $P_2$ or $P_3$ then we contract $e$ in $G$, obtaining a graph $G/e$. This shortens $P_1$, while retaining the hypothesis: we conclude by induction on $G/e$.

Otherwise, $x$ appears in, say, $P_3$. We distinguish two possibilities:

1. $x$ is not the last inner vertex of $P_3$. In this case, we replace $P_3$ by the shorter path $P_3xes_1$.

Path $P_1, P_2$, and $P_3xes_1$, still have no vertex common to all three: so we conclude by induction hypothesis.

2. $x$ is the last inner vertex of $P_3$, and is followed by an edge $e'$: $P_3 = P_3xe'$. Note that $e = e'$ is possible but not necessary. We then contract both $e$ and $e'$ and conclude again by induction hypothesis on the resulting minor. (Note that $x$ not being in $P_2$ guarantees that contracting $e$ and $e'$ does not modify $P_2$). ▼

**Lemma F.2.** Let $G$ be a full prime graph of arity $k$. For all $i \le k$, $G$ admits the following sourced simple graph $H_i$ as a sourced minor: $H_i$ has the same sources as $G$, and its only inner elements are $k-1$ edges between the $i$th source and the other sources.

**Proof.** If $G$ has no inner vertex then it must be atomic, it admits the clique on the $k$ sources as a sourced minor, and thus in particular the graphs $H_i$ from the statement. Otherwise, starting from the footprint of $G$, contract all inner vertices onto a single one, say $x$, which is connected to all sources since $G$ was full prime. For each $i$, it suffices to contract the edge between $x$ and the $i$th source to obtain $H_i$ as a sourced minor. ▼

**Proposition 8.7.** Every graph of arity three either has the sourced triangle $K_3$ as a sourced minor, or has one of the two following shapes:

<figure><img src="image_34.png" /></figure>

**Proof.** Suppose $G$ is a graph of arity three that does not admit $K_3$ as a sourced minor.

If $G$ has no full prime components, then it has the triangle as a shape. Not having $K_3$ as a sourced minor implies that some edge of this shape does not have any full prime component in $G$, making it possible to refine the triangle shape into the left-hand side one in the statement.
**F Proofs for Section 8 (Separation pairs)**

The following three lemmas (Lemmas F.1, F.2, F.3), as well as Proposition 8.7, hold without any restriction on the treewidth.

**Lemma F.1.** Let $G$ be a graph of arity three with three inner paths $P_1, P_2$, and $P_3$, respectively from the first to the second, the second to the third, and the third to the first sources. If no vertex is shared by the three paths then $G$ admits $K_3$ as a sourced minor.

**Proof.** Endpoints and vertices of paths are preserved by taking the footprint of a graph: the lemma holds for a graph whenever it holds for its footprint. Hence we may assume that $G$ is a sourced simple graph.

We write $s_1, s_2, s_3$ for the three sources of $G$.

We reason by induction on the sum of the lengths of the paths, with the length of a path being the number of inner elements it contains.

If $P_1, P_2$, and $P_3$ are all of length 1 then they are reduced to edges connecting pairs of sources. Said otherwise, $G$ contains $K_3$ as a subgraph, and by extension as a minor.

Otherwise, at least one of the paths $P_i$, say $P_1$, has an inner vertex. We note $e$ for the first edge and $x$ for the first inner vertex of $P_1$.

If $x$ does not appear in either $P_2$ or $P_3$ then we contract $e$ in $G$, obtaining a graph $G/e$. This shortens $P_1$, while retaining the hypothesis: we conclude by induction on $G/e$.

Otherwise, $x$ appears in, say, $P_3$. We distinguish two possibilities:

1. $x$ is not the last inner vertex of $P_3$. In this case, we replace $P_3$ by the shorter path $P_3xes_1$. Path $P_1, P_2$, and $P_3xes_1$, still have no vertex common to all three: so we conclude by induction hypothesis.

2. $x$ is the last inner vertex of $P_3$, and is followed by an edge $e'$: $P_3 = P_3xe'$. Note that $e = e'$ is possible but not necessary. We then contract both $e$ and $e'$ and conclude again by induction hypothesis on the resulting minor. (Note that $x$ not being in $P_2$ guarantees that contracting $e$ and $e'$ does not modify $P_2$). ▼

**Lemma F.2.** Let $G$ be a full prime graph of arity $k$. For all $i \le k$, $G$ admits the following sourced simple graph $H_i$ as a sourced minor: $H_i$ has the same sources as $G$, and its only inner elements are $k-1$ edges between the $i$th source and the other sources.

**Proof.** If $G$ has no inner vertex then it must be atomic, it admits the clique on the $k$ sources as a sourced minor, and thus in particular the graphs $H_i$ from the statement. Otherwise, starting from the footprint of $G$, contract all inner vertices onto a single one, say $x$, which is connected to all sources since $G$ was full prime. For each $i$, it suffices to contract the edge between $x$ and the $i$th source to obtain $H_i$ as a sourced minor. ▼

**Proposition 8.7.** Every graph of arity three either has the sourced triangle $K_3$ as a sourced minor, or has one of the two following shapes:

<figure><img src="image_31.png" /></figure>

**Proof.** Suppose $G$ is a graph of arity three that does not admit $K_3$ as a sourced minor.

If $G$ has no full prime components, then it has the triangle as a shape. Not having $K_3$ as a sourced minor implies that some edge of this shape does not have any full prime component in $G$, making it possible to refine the triangle shape into the left-hand side one in the statement.
If $G$ has two or more full prime components, we can use Lemma F.2 on these two components and two distinct sources of $G$ to get $K_3$ as sourced minor.

It remains to deal with the case where $G$ is full prime. We prove in that case that there is a vertex $x$ which is a checkpoint between all pairs of sources: it follows easily that $G$ has the right-hand side shape from the statement.

Write $s_1, s_2$, and $s_3$ for the sources of $G$. Let $P_1, P_2$, and $P_3$ be three paths in $G$ respectively from $s_1$ to $s_2$, $s_2$ to $s_3$, and $s_3$ to $s_1$, each of minimal length. By Lemma F.1, there is a vertex $x$ shared by these three paths.

Since segments such as $P_1x$ and $\overline{P_3x}$ share their endpoints, they must have equal length: otherwise one could be replaced by the other to obtain a shorter triple of paths. Without loss of generality, we may actually chose them to be equal. Accordingly, we write $Q_1$ for $P_1x = \overline{P_3x}$, $Q_2$ for $P_2x = \overline{P_1x}$, and $Q_3$ for $P_3x = \overline{P_2x}$. Note that $Q_i$ is a path from $s_i$ to $x$.

The paths $Q_i$ are pairwise inner disjoint. Indeed, would $Q_1$ and $Q_2$ share an inner vertex (for instance), then $P_1 = Q_1\overline{Q_2}$ would visit that vertex twice and would not be minimal.

We finally prove that all inner paths between any two sources must contain $x$. Let $Q$ be an inner path between two sources, say $s_1$ and $s_2$ without loss of generality, and assume by contradiction that $Q$ avoids $x$.

By Lemma F.1, there is a vertex $y$ shared by $Q$, $P_2$, and $P_3$. Since $Q_1$ and $Q_2$ are inner disjoint, $y$ must belong to $Q_3$.

The path $Q$ starts at $s_1$, ends at $s_2$, and meets $Q_3$ at $y$. It cannot always remain on $Q_1$ as it does not contain $x$. Let $z$ be the last vertex of $Q$ in common with $Q_1$, and $z'$ be the first vertex after $z$ on $Q$ that meets $Q_j$ for $j \in \{2, 3\}$. Note that the inner part of $R = zQz'$ is disjoint from all $Q_i$s. As $z$ and $z'$ cannot be $x$, we are in the following situation:

<figure><img src="image_35.png" /></figure>

It follows easily, using the fact that most drawn paths are disjoint, that $K_3$ is a sourced minor of $G$, a contradiction. ◀

**Lemma F.3.** Let $(x, y)$ be a separation pair in a graph $G$ of arity two. All paths from one source to the other in $G$ must visit either $x$ or $y$. If furthermore $G$ is hard then there exists a path that contains $x$ (resp. $y$) but not $y$ (resp. $x$).

**Proof.** By definition of separation pairs, and using the fact that hard graphs are full prime and may not have checkpoints. ◀

**Proposition 8.8.** Let $G$ be a hard graph with two minimal separation forget pairs $(x, y)$ and $(x', y')$. Possibly up to swapping $x$ and $y$, and/or $x'$ and $y'$, either $(x, y')$ is a separation pair (Case Z), or $G$ has one of the following shapes, where in the leftmost case, $z$ is minimal and $x'$, $y'$ appear in the rightmost component:

<figure><img src="image_36.png" /><figcaption>Case IH</figcaption></figure>

<figure><img src="image_37.png" /><figcaption>Case X</figcaption></figure>

<figure><img src="image_38.png" /><figcaption>Case D</figcaption></figure>
If $G$ has two or more full prime components, we can use Lemma F.2 on these two components and two distinct sources of $G$ to get $K_3$ as sourced minor.

It remains to deal with the case where $G$ is full prime. We prove in that case that there is a vertex $x$ which is a checkpoint between all pairs of sources: it follows easily that $G$ has the right-hand side shape from the statement.

Write $s_1, s_2$, and $s_3$ for the sources of $G$. Let $P_1, P_2$, and $P_3$ be three paths in $G$ respectively from $s_1$ to $s_2$, $s_2$ to $s_3$, and $s_3$ to $s_1$, each of minimal length. By Lemma F.1, there is a vertex $x$ shared by these three paths.

Since segments such as $P_1x$ and $\overline{P_3x}$ share their endpoints, they must have equal length: otherwise one could be replaced by the other to obtain a shorter triple of paths. Without loss of generality, we may actually chose them to be equal. Accordingly, we write $Q_1$ for $P_1x = \overline{P_3x}$, $Q_2$ for $P_2x = \overline{P_1x}$, and $Q_3$ for $P_3x = \overline{P_2x}$. Note that $Q_i$ is a path from $s_i$ to $x$.

The paths $Q_i$ are pairwise inner disjoint. Indeed, would $Q_1$ and $Q_2$ share an inner vertex (for instance), then $P_1 = Q_1\overline{Q_2}$ would visit that vertex twice and would not be minimal.

We finally prove that all inner paths between any two sources must contain $x$. Let $Q$ be an inner path between two sources, say $s_1$ and $s_2$ without loss of generality, and assume by contradiction that $Q$ avoids $x$.

By Lemma F.1, there is a vertex $y$ shared by $Q$, $P_2$, and $P_3$. Since $Q_1$ and $Q_2$ are inner disjoint, $y$ must belong to $Q_3$.

The path $Q$ starts at $s_1$, ends at $s_2$, and meets $Q_3$ at $y$. It cannot always remain on $Q_1$ as it does not contain $x$. Let $z$ be the last vertex of $Q$ in common with $Q_1$, and $z'$ be the first vertex after $z$ on $Q$ that meets $Q_j$ for $j \in \{2, 3\}$. Note that the inner part of $R = zQz'$ is disjoint from all $Q_i$s. As $z$ and $z'$ cannot be $x$, we are in the following situation:

<figure><img src="image_32.png" /></figure>

It follows easily, using the fact that most drawn paths are disjoint, that $K_3$ is a sourced minor of $G$, a contradiction. ◀

**Lemma F.3.** Let $(x, y)$ be a separation pair in a graph $G$ of arity two. All paths from one source to the other in $G$ must visit either $x$ or $y$. If furthermore $G$ is hard then there exists a path that contains $x$ (resp. $y$) but not $y$ (resp. $x$).

**Proof.** By definition of separation pairs, and using the fact that hard graphs are full prime and may not have checkpoints. ◀

**Proposition 8.8.** Let $G$ be a hard graph with two minimal separation forget pairs $(x, y)$ and $(x', y')$. Possibly up to swapping $x$ and $y$, and/or $x'$ and $y'$, either $(x, y')$ is a separation pair (Case Z), or $G$ has one of the following shapes, where in the leftmost case, $z$ is minimal and $x'$, $y'$ appear in the rightmost component:

<figure><img src="image_33.png" /><figcaption>Case IH</figcaption></figure>

<figure><img src="image_34.png" /><figcaption>Case X</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>Case D</figcaption></figure>
**Proof.** Let $G$ be a hard graph with $(x, y)$ and $(x', y')$ two minimal separation forget pairs. If $\{x, y\}$ meets $\{x', y'\}$ then we are trivially in **Case Z** (in fact, **Case Z1** by analysing paths between the two sources). Thus we assume in the sequel that $\{x, y\}$ and $\{x', y'\}$ are disjoint.

We consider the graph from the point of view of the first separation pair $(x, y)$: by hypothesis $G$ has the following shape:

<figure><img src="image_39.png" /></figure>

We respectively write $s_1$ and $s_2$ for the first and second sources. We assume by symmetry that $x'$ appears in $G_1$, and we proceed by case analysis on whether $y'$ also appears together with $x'$ in $G_1$, or on the opposite side of $(x, y)$, in $G_2$.

**1. when $x'$ is in $G_1$ and $y'$ is in $G_2$.** First observe that either $x'$ is a checkpoint between $x$ and $s_2$ in $G_1$ or $y'$ is a checkpoint between $s_1$ and $x$ in $G_2$. Indeed, if we had both an $y$'-free path $P$ from $s_1$ to $x$ and an $x$'-free path $Q$ from $x$ to $s_2$, then their concatenation $PQ$ would be a path from $s_1$ to $s_2$ contradicting Lemma F.3. Therefore, either $(x', y)$ or $(x, y')$ is a separation pair, and we are in **Case Z**. We show below that we are actually in **Case Z2**.

Up to permutation of $x'$ and $y'$, assume that $x'$ is a checkpoint between $x$ and $s_2$ in $G_1$. By symmetry, we also have that either $x'$ is a checkpoint between $y$ and $s_2$ in $G_1$ or $y'$ is a checkpoint between $s_1$ and $y$ in $G_2$. We now prove that only the latter case is possible. By contradiction suppose that $x'$ is a checkpoint both between $s_2$ and $y$ and between $s_2$ and $x$. Consider $P$ a $s_1-s_2$ path. By Lemma F.3, $P$ contains either $x$ or $y$. In the respective cases, $xP$ or $yP$ must contain $x'$ as $x'$ is a checkpoint between $x$ and $s_2$ and between $y$ and $s_2$ in $G_1$. Hence $x$ is a checkpoint in $G$, contradicting $G$ being hard.

We end up with the following shape for $G$:

<figure><img src="image_40.png" /></figure>

Assume an inner $x-y$ path $P$ in either $H_2$ or $H_3$. Note that $(x, y')$ and $(x', y)$ are separation pairs. By Lemma F.3 let be an inner path $Q$ (resp. $R$) from $s_1$ to $s_2$ containing $x$ (resp. $y$) but not $y'$ (resp. $x'$). The concatenation $QxPyR$ is a $s_1-s_2$ path in $G$ containing neither $x'$ nor $y'$, contradicting Lemma F.3.

Hence inner $x-y$ paths in $H_2$ or $H_3$ do not exist, meaning there are no reduced components of either $H_2$ or $H_3$ with both $x$ and $y$ as sources: we fall into **Case Z2**.

**2. when $x'$ and $y'$ are both in $G_1$.** We first prove that $s_2$ is isolated in all components of $G_1$ not containing $x'$ nor $y'$. Let $C$ be such a component and suppose by contradiction that $s_2$ is not isolated. If $x$ and $y$ are both isolated in $C$, then $C$ is actually a component of $G$, contradicting the fact $G$ is prime. Otherwise, assume, without loss of generality, that $x$ is not isolated in $C$. Let $Q$ be an $x-s_2$ path in $C$. By Lemma F.3, let $P$ be an $s_1-s_2$ path in $G$ containing $x$ but not $y$. The path $PxQ$ is from $s_1$ to $s_2$, and contains neither $x'$ nor $y'$ as it intersects $H$ only at $x$ and $s_2$, a contradiction by Lemma F.3.

Without loss of generality, we can move all those components from $G_2$ to $G_1$, so that either $G_1$ becomes prime and contains both $x'$ and $y'$, or $G_1$ has exactly two prime components, respectively containing $x'$ and $y'$.
**Proof.** Let $G$ be a hard graph with $(x, y)$ and $(x', y')$ two minimal separation forget pairs. If $\{x, y\}$ meets $\{x', y'\}$ then we are trivially in **Case Z** (in fact, **Case Z1** by analysing paths between the two sources). Thus we assume in the sequel that $\{x, y\}$ and $\{x', y'\}$ are disjoint.

We consider the graph from the point of view of the first separation pair $(x, y)$: by hypothesis $G$ has the following shape:

<figure><img src="image_36.png" /></figure>

We respectively write $s_1$ and $s_2$ for the first and second sources. We assume by symmetry that $x'$ appears in $G_1$, and we proceed by case analysis on whether $y'$ also appears together with $x'$ in $G_1$, or on the opposite side of $(x, y)$, in $G_2$.

**1. when $x'$ is in $G_1$ and $y'$ is in $G_2$.** First observe that either $x'$ is a checkpoint between $x$ and $s_2$ in $G_1$ or $y'$ is a checkpoint between $s_1$ and $x$ in $G_2$. Indeed, if we had both an $y'$-free path $P$ from $s_1$ to $x$ and an $x'$-free path $Q$ from $x$ to $s_2$, then their concatenation $PQ$ would be a path from $s_1$ to $s_2$ contradicting Lemma F.3. Therefore, either $(x', y)$ or $(x, y')$ is a separation pair, and we are in **Case Z**. We show below that we are actually in **Case Z2**.

Up to permutation of $x'$ and $y'$, assume that $x'$ is a checkpoint between $x$ and $s_2$ in $G_1$. By symmetry, we also have that either $x'$ is a checkpoint between $y$ and $s_2$ in $G_1$ or $y'$ is a checkpoint between $s_1$ and $y$ in $G_2$. We now prove that only the latter case is possible. By contradiction suppose that $x'$ is a checkpoint both between $s_2$ and $y$ and between $s_2$ and $x$. Consider $P$ a $s_1-s_2$ path. By Lemma F.3, $P$ contains either $x$ or $y$. In the respective cases, $xP$ or $yP$ must contain $x'$ as $x'$ is a checkpoint between $x$ and $s_2$ and between $y$ and $s_2$ in $G_1$. Hence $x$ is a checkpoint in $G$, contradicting $G$ being hard.

We end up with the following shape for $G$:

<figure><img src="image_37.png" /></figure>

Assume an inner $x-y$ path $P$ in either $H_2$ or $H_3$. Note that $(x, y')$ and $(x', y)$ are separation pairs. By Lemma F.3 let be an inner path $Q$ (resp. $R$) from $s_1$ to $s_2$ containing $x$ (resp. $y$) but not $y'$ (resp. $x'$). The concatenation $QxPyR$ is a $s_1-s_2$ path in $G$ containing neither $x'$ nor $y'$, contradicting Lemma F.3.

Hence inner $x-y$ paths in $H_2$ or $H_3$ do not exist, meaning there are no reduced components of either $H_2$ or $H_3$ with both $x$ and $y$ as sources: we fall into **Case Z2**.

**2. when $x'$ and $y'$ are both in $G_1$.** We first prove that $s_2$ is isolated in all components of $G_1$ not containing $x'$ nor $y'$. Let $C$ be such a component and suppose by contradiction that $s_2$ is not isolated. If $x$ and $y$ are both isolated in $C$, then $C$ is actually a component of $G$, contradicting the fact $G$ is prime. Otherwise, assume, without loss of generality, that $x$ is not isolated in $C$. Let $Q$ be an $x-s_2$ path in $C$. By Lemma F.3, let $P$ be an $s_1-s_2$ path in $G$ containing $x$ but not $y$. The path $PxQ$ is from $s_1$ to $s_2$, and contains neither $x'$ nor $y'$ as it intersects $H$ only at $x$ and $s_2$, a contradiction by Lemma F.3.

Without loss of generality, we can move all those components from $G_2$ to $G_1$, so that either $G_1$ becomes prime and contains both $x'$ and $y'$, or $G_1$ has exactly two prime components, respectively containing $x'$ and $y'$.
**2.1. when** $G_1 \simeq H_1 \parallel H_2$ **with** $x'$ **in** $H_1$, $y'$ **in** $H_2$, **and** $H_1, H_2$ **prime.** We prove that $x'$ is a checkpoint between $x$ and $s_2$ in $H_1$. Up to replacing $x$ by $y$, and/or $x'$ by $y'$, this gives that $x'$ is also a checkpoint between $y$ and $s_2$ in $H_1$, and the same properties for $y'$ but in $H_2$.

Consider an $x-s_2$ inner path $P$ in $H_1$. By Lemma F.3, let be $Q$ an $s_1-s_2$ inner path in $G$ that contains $x$ but not $y$. The path $QxP$ is from $s_1$ to $s_2$, and cannot contain $y'$, as it intersects $H_2$ only at $x$ and $s_2$. By Lemma F.3, $(x', y')$ being a separation pair, $QxP$ must contain $x'$. It can do so only in $P$ as $x'$ is inner in $H_1$.

We end up with the following shape for $G$:

<figure><img src="image_41.png" /></figure>

Name $L$ this shape. A simple verification shows that $(L, x')$ has treewidth 4. Note how, as $G$ is hard, the 2-edges in $L$ must have full prime components in $G$. By Proposition 8.6, if all subgraphs of $G$ corresponding to the 3-edges in $L$ had $K_3$ as a sourced minor, $(G, x')$ would have the footprint of $(L, x')$ as a minor, contradicting the treewidth of the former graph. Hence one at least of $G_2$, $L_1$, or $L_2$ has a shape given by Proposition 8.7. Say this applies to $G_2$. The other cases are treated similarly and they all lead to the same final shape (**Case X**).

A simple verification shows that the only possibility given by Proposition 8.7 for $G_2$ that keeps $G$ a hard graph and $x$ and $y$ minimal is the following:

<figure><img src="image_42.png" /></figure>

Name $S$ this shape. Again $(S, x')$ has treewidth 4, and both $L_1$ and $L_2$ cannot have $K_3$ as a sourced minor by Proposition 8.6. By symmetry, we can assume that a shape from Proposition 8.7 applies to $L_1$. There is again only one possibility that keeps $G$ hard and $x'$ minimal:

<figure><img src="image_43.png" /></figure>

Once again this shape with $x'$ as an added source has treewidth 4, by Proposition 8.6 $L_2$ cannot have $K_3$ as a sourced minor, and the only possibility given by Proposition 8.7 for $L_2$ gives the shape of **Case X** for $G$.

**2.2. when** $G_1 = H$ **is prime.** As $x$ and $y$ are forget points, $H$ has treewidth at most 3 as a component of $(G, x, y)$. Furthermore, $G$ being hard, $H = G_1$ must be full prime. As it contains at least two inner vertices $x'$ and $y'$, it must have a forget point $z$. Assume $z' \prec z$, i.e. $z'$ is a checkpoint between $z$ and a source of $G$. We prove that $z'$ is a forget point of $H$. First, we show that $z'$ is inner in $H$. If $z'$ is a checkpoint between $z$ and $s_2$, then this is obvious. Otherwise $z'$ is a checkpoint between $z$ and $s_1$. As $H$ is full prime, there are inner paths in $H$ from $z'$ to either $x$ or $y$. By Lemma F.3, there are inner paths in $G_2$ from $x$ (resp. $y$) to $s_1$ not containing $y$ (resp. $x$). The concatenation of the latter with the former proves that neither $x$ nor $y$ can be $z'$, and that if $z'$ is in $G_2$, then it would be a checkpoint between $x$ and $s_1$, and between $y$ and $s_1$. In particular, it would be a checkpoint in $G$, contradicting
**2.1. when** $G_1 \simeq H_1 \parallel H_2$ **with** $x'$ **in** $H_1$, $y'$ **in** $H_2$, **and** $H_1, H_2$ **prime.** We prove that $x'$ is a checkpoint between $x$ and $s_2$ in $H_1$. Up to replacing $x$ by $y$, and/or $x'$ by $y'$, this gives that $x'$ is also a checkpoint between $y$ and $s_2$ in $H_1$, and the same properties for $y'$ but in $H_2$.

Consider an $x-s_2$ inner path $P$ in $H_1$. By Lemma F.3, let be $Q$ an $s_1-s_2$ inner path in $G$ that contains $x$ but not $y$. The path $QxP$ is from $s_1$ to $s_2$, and cannot contain $y'$, as it intersects $H_2$ only at $x$ and $s_2$. By Lemma F.3, $(x', y')$ being a separation pair, $QxP$ must contain $x'$. It can do so only in $P$ as $x'$ is inner in $H_1$.

We end up with the following shape for $G$:

<figure><img src="image_38.png" /></figure>

Name $L$ this shape. A simple verification shows that $(L, x')$ has treewidth 4. Note how, as $G$ is hard, the 2-edges in $L$ must have full prime components in $G$. By Proposition 8.6, if all subgraphs of $G$ corresponding to the 3-edges in $L$ had $K_3$ as a sourced minor, $(G, x')$ would have the footprint of $(L, x')$ as a minor, contradicting the treewidth of the former graph. Hence one at least of $G_2$, $L_1$, or $L_2$ has a shape given by Proposition 8.7. Say this applies to $G_2$. The other cases are treated similarly and they all lead to the same final shape (**Case X**).

A simple verification shows that the only possibility given by Proposition 8.7 for $G_2$ that keeps $G$ a hard graph and $x$ and $y$ minimal is the following:

<figure><img src="image_39.png" /></figure>

Name $S$ this shape. Again $(S, x')$ has treewidth 4, and both $L_1$ and $L_2$ cannot have $K_3$ as a sourced minor by Proposition 8.6. By symmetry, we can assume that a shape from Proposition 8.7 applies to $L_1$. There is again only one possibility that keeps $G$ hard and $x'$ minimal:

<figure><img src="image_40.png" /></figure>

Once again this shape with $x'$ as an added source has treewidth 4, by Proposition 8.6 $L_2$ cannot have $K_3$ as a sourced minor, and the only possibility given by Proposition 8.7 for $L_2$ gives the shape of **Case X** for $G$.

**2.2. when** $G_1 = H$ **is prime.** As $x$ and $y$ are forget points, $H$ has treewidth at most 3 as a component of $(G, x, y)$. Furthermore, $G$ being hard, $H = G_1$ must be full prime. As it contains at least two inner vertices $x'$ and $y'$, it must have a forget point $z$. Assume $z' \prec z$, i.e. $z'$ is a checkpoint between $z$ and a source of $G$. We prove that $z'$ is a forget point of $H$. First, we show that $z'$ is inner in $H$. If $z'$ is a checkpoint between $z$ and $s_2$, then this is obvious. Otherwise $z'$ is a checkpoint between $z$ and $s_1$. As $H$ is full prime, there are inner paths in $H$ from $z'$ to either $x$ or $y$. By Lemma F.3, there are inner paths in $G_2$ from $x$ (resp. $y$) to $s_1$ not containing $y$ (resp. $x$). The concatenation of the latter with the former proves that neither $x$ nor $y$ can be $z'$, and that if $z'$ is in $G_2$, then it would be a checkpoint between $x$ and $s_1$, and between $y$ and $s_1$. In particular, it would be a checkpoint in $G$, contradicting
the fact that $G$ is hard. Hence $z'$ is inner in $H$. By Lemma 8.1 $z'$ is an anchor in $(G, z)$, and hence in $H$. Up-to permutation of $z$ and $z'$ we can always assume that $z$ is minimal.

Look at the series decomposition of $H$ at $z$. The series factor must be reduced to a parallel composition of edges by Proposition 3.5. We prove that no such edge can exist. By contradiction, assume there is one. It provides an $x-s_2$ path $Q$ in $H$ that contains neither $x'$ nor $y'$. By Lemma F.3, let $P$ be a $s_1-s_2$ path containing $x$ but not $y$. The path $PxQ$ is from $s_1$ to $s_2$, and contains neither $x'$ nor $y'$, a contradiction to Lemma F.3.

Naming $H_i$ the series arguments, $G$ has the following shape:

<figure><img src="image_44.png" /></figure>

Consider the case when $z \in \{x', y'\}$. Without loss of generality, suppose that $z = y'$. If $x'$ is in $H_1$, then we easily prove that there are no $x-s_2$ inner paths in $H_3$ or $y-s_2$ inner paths in $H_2$. By contradiction assume, for example, $Q$ to be a $x-s_2$ inner path in $H_3$. By Lemma F.3, let $Q$ be a $s_1-s_2$ path in $G$ containing $x$ but not $y$. The path $PxQ$ is from $s_1$ to $s_2$, but contains neither $x'$ nor $y'$, contradicting Lemma F.3. Hence $G$ has the following shape:

<figure><img src="image_45.png" /></figure>

There, $y'$ is a checkpoint, which contradicts $G$ being hard.

Still assuming $z = y'$, we now assume that $x'$ is in $H_3$. Up-to permuting $x$ and $y$, and by extension, $H_2$ and $H_3$, this takes care of the case with $x'$ in $H_2$. Using Lemma F.3 and similar reasoning as above, $x'$ must be a checkpoint between $x$ and $s_2$ in $H_3$, giving the shape of **Case Z3**.

Thus we may assume $z \notin \{x', y'\}$, and we do a case analysis depending on which $H_i$ contain $x'$ and/or $y'$.

Assume that $x'$ and $y'$ are both in $H_1$. By Lemma F.3 applied to the separation pair $(x, y)$, any $x-s_2$ inner path in $H_3$ or $H_2$ gives rise to a $s_1-s_2$ path containing neither $x'$ nor $y'$, a contradiction to the latter lemma applied to $(x', y')$; $G$ has the following shape:

<figure><img src="image_46.png" /></figure>

As before, $z$ is a checkpoint in $G$ which is not possible as $G$ is hard.

Assume that $x'$ and $y'$ are both in $H_3$. By symmetry this will take care of the case with $x'$ and $y'$ both being in $H_2$. By Lemma F.3 again there cannot be $y-s_2$ inner paths in $H_2$: we get the shape of **Case IH** with $z$ being indeed minimal.

Assume $x'$ is in $H_3$ and $y'$ in $H_1$. By symmetry the cases of $x'$ in $H_2$ and $y'$ in $H_1$ and/or of permuting $x'$ and $y'$ are taken care of by the following too. Again by Lemma F.3, $y-s_2$ inner paths do not exist in $H_2$, and, without loss of generality, $H_2$ can be assumed empty. Similar reasoning as above using Lemma F.3 can be used to prove the following: $x'$ is a checkpoint between $x$ and $z$, and between $x$ and $s_2$ in $H_3$, and $y'$ is a checkpoint between $y$ and $z$ and between $x$ and $z$ in $H_1$. This is an instance of **Case Z3**.
the fact that $G$ is hard. Hence $z'$ is inner in $H$. By Lemma 8.1 $z'$ is an anchor in $(G, z)$, and hence in $H$. Up-to permutation of $z$ and $z'$ we can always assume that $z$ is minimal.

Look at the series decomposition of $H$ at $z$. The series factor must be reduced to a parallel composition of edges by Proposition 3.5. We prove that no such edge can exist. By contradiction, assume there is one. It provides an $x-s_2$ path $Q$ in $H$ that contains neither $x'$ nor $y'$. By Lemma F.3, let $P$ be a $s_1-s_2$ path containing $x$ but not $y$. The path $PxQ$ is from $s_1$ to $s_2$, and contains neither $x'$ nor $y'$, a contradiction to Lemma F.3.

Naming $H_i$ the series arguments, $G$ has the following shape:

<figure><img src="image_41.png" /></figure>

Consider the case when $z \in \{x', y'\}$. Without loss of generality, suppose that $z = y'$. If $x'$ is in $H_1$, then we easily prove that there are no $x-s_2$ inner paths in $H_3$ or $y-s_2$ inner paths in $H_2$. By contradiction assume, for example, $Q$ to be a $x-s_2$ inner path in $H_3$. By Lemma F.3, let $Q$ be a $s_1-s_2$ path in $G$ containing $x$ but not $y$. The path $PxQ$ is from $s_1$ to $s_2$, but contains neither $x'$ nor $y'$, contradicting Lemma F.3. Hence $G$ has the following shape:

<figure><img src="image_42.png" /></figure>

There, $y'$ is a checkpoint, which contradicts $G$ being hard.

Still assuming $z = y'$, we now assume that $x'$ is in $H_3$. Up-to permuting $x$ and $y$, and by extension, $H_2$ and $H_3$, this takes care of the case with $x'$ in $H_2$. Using Lemma F.3 and similar reasoning as above, $x'$ must be a checkpoint between $x$ and $s_2$ in $H_3$, giving the shape of **Case Z3**.

Thus we may assume $z \notin \{x', y'\}$, and we do a case analysis depending on which $H_i$ contain $x'$ and/or $y'$.

Assume that $x'$ and $y'$ are both in $H_1$. By Lemma F.3 applied to the separation pair $(x, y)$, any $x-s_2$ inner path in $H_3$ or $H_2$ gives rise to a $s_1-s_2$ path containing neither $x'$ nor $y'$, a contradiction to the latter lemma applied to $(x', y')$; $G$ has the following shape:

<figure><img src="image_43.png" /></figure>

As before, $z$ is a checkpoint in $G$ which is not possible as $G$ is hard.

Assume that $x'$ and $y'$ are both in $H_3$. By symmetry this will take care of the case with $x'$ and $y'$ both being in $H_2$. By Lemma F.3 again there cannot be $y-s_2$ inner paths in $H_2$: we get the shape of **Case IH** with $z$ being indeed minimal.

Assume $x'$ is in $H_3$ and $y'$ in $H_1$. By symmetry the cases of $x'$ in $H_2$ and $y'$ in $H_1$ and/or of permuting $x'$ and $y'$ are taken care of by the following too. Again by Lemma F.3, $y-s_2$ inner paths do not exist in $H_2$, and, without loss of generality, $H_2$ can be assumed empty. Similar reasoning as above using Lemma F.3 can be used to prove the following: $x'$ is a checkpoint between $x$ and $z$, and between $x$ and $s_2$ in $H_3$, and $y'$ is a checkpoint between $y$ and $z$ and between $x$ and $z$ in $H_1$. This is an instance of **Case Z3**.
Finally, assume $x'$ and $y'$ are in $H_3$ and $H_2$ respectively. Using Lemma F.3, we prove, following the same reasoning as above, that $x'$ is a checkpoint between $x$ and $s_2$ in $H_3$ and $y'$ between $y$ and $s_2$ in $H_2$. Said otherwise, $G$ has the following shape:

<figure><img src="image_47.png" /></figure>

Name $L$ this shape. The graph $(L, x')$ has treewidth 4. As has been done above, we can use Propositions 8.6 and 8.7 repeatedly to refine the shapes of the subgraphs of $G$ corresponding to the 3 edges of $L$. In all possible cases, retaining minimality of $x$, $x'$, $y$, and $y'$, as well as the fact $G$ is hard gives the shape of **Case D**. ◀
Finally, assume $x'$ and $y'$ are in $H_3$ and $H_2$ respectively. Using Lemma F.3, we prove, following the same reasoning as above, that $x'$ is a checkpoint between $x$ and $s_2$ in $H_3$ and $y'$ between $y$ and $s_2$ in $H_2$. Said otherwise, $G$ has the following shape:

<figure><img src="image_44.png" /></figure>

Name $L$ this shape. The graph $(L, x')$ has treewidth 4. As has been done above, we can use Propositions 8.6 and 8.7 repeatedly to refine the shapes of the subgraphs of $G$ corresponding to the 3 edges of $L$. In all possible cases, retaining minimality of $x, x', y$, and $y'$, as well as the fact $G$ is hard gives the shape of **Case D**. $\blacksquare$