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

HAL
open science

# Proving Termination of Linear DPO Graph Rewriting Systems using Weighted Type Graphs

Qi Qiu

► To cite this version:

Qi Qiu. Proving Termination of Linear DPO Graph Rewriting Systems using Weighted Type Graphs. Université Claude Bernard Lyon 1 (UCBL), Lyon, FRA. 2024. hal-04729748v2

HAL Id: hal-04729748

https://hal.science/hal-04729748v2

Submitted on 15 Oct 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Proving Termination of Linear DPO Graph
Rewriting Systems using Weighted Type Graphs

QI QIU[0000-0002-8350-2748]

Universite Claude Bernard Lyon 1, CNRS, INSA Lyon,
LIRIS, UMR5205, 69622 Villeurbanne, France

qi.qiu@univ-lyon1.fr

**Abstract.** We improve a termination technique initially developed by Zantema et al. for cycle rewriting, later extended to graph rewriting by Bruggink et al., and generalized by Endrullis et al., which uses weighted type graphs, to prove the relative termination of arrow-labeled multi-graph rewriting systems with the double pushout approach. We establish a machine-checkable condition that considers the number of morphisms from graphs with multiple edges under specific conditions, a factor previously overlooked. Our enhancement resolves cases that prior methods could not and simplifies termination proofs for certain systems.

**Keywords:** Termination · Rewrite system · Automated reasoning · Program verification · Graph transformation · Weighted type graph

# 1 Introduction

Distributed systems are essential for enhancing performance, scalability, and efficiency in modern computing. Ensuring the correctness of distributed systems is both crucial and challenging due to their complexity [31, 28].

While interactive theorem proving [27, 34] offers a promising formal verification method [26, 40, 16], it requires proficiency in proof assistants, making the process demanding and time-consuming. Automatic methods that generate certificates, which can be verified by proof assistants, offer a practical alternative [10, 11]. Therefore, it is crucial to develop techniques that enable the automated verification of distributed systems.

Our research addresses this issue within the context of graph rewriting: computation entities are represented as nodes, relationships as edges, and operations as graph rewriting rules that rely exclusively on local knowledge. We model distributed systems using algebraic graph rewriting systems that use double pushout (DPO) to define the graph transformation based on rules. The DPO approach, introduced in [21], is the first algebraic methods for graph transformation. Since its introduction, it has been widely studied and applied across various areas of computer science [see 15, 25, 6].

We focus on relative termination [29, 23], a critical property that guarantees a system only allows a finite number of steps from one set of rules. It ensures
controlled execution and is crucial for proving the correctness of systems with multiple rule sets.

In this context, a powerful automated method known as the weighted type graph technique has been developed for proving the relative termination of graph rewriting systems with the DPO approach. Initially introduced by Zantema et al. in [41] for cycle rewriting systems, this method has since been generalized for arrow-labeled directed multigraphs by Bruggink et al. in [9, 8] and further extended for more structures and DPO variants by Endrullis et al. in [22]. However, the termination of the graph rewriting system presented in Example 41 could not be established using any existing versions of this method as pointed out by Endrullis et al. in [22]. This limitation prompted the need for refining the method to address such cases.

To address this specific problem, we improve upon the existing technique. Unlike existing versions of this method that focused on changes in the number of morphisms from nodes and edges when a graph is transformed, we investigate how the number of morphisms from graphs with multiple edges changes. We establish a machine-checkable sufficient condition that guarantees the relative terminations of graph rewriting systems. Our enhancement not only successfully proves the termination of systems like the one described in Example 41, which existing formulations of the type graph method cannot address, but also address the termination of Example 43, which other advanced termination techniques for graph rewriting fail to prove. Additionally, it simplifies termination proofs for cases like Example 40.

Section 2 recalls usual concepts and notation on the relative termination of linear DPO graph rewriting systems. After describing the type graph method in Section 3, we present our contribution in Section 5.

# 2 Preliminaries

Starting with arrow-labeled multigraphs, we use the concept of pushout from category theory to define linear graph rewriting systems using the DPO approach. We focus on proving the relative termination of such rewriting systems.

## 2.1 Graphs

Let $\Sigma$ be a finite set of labels. To establish a foundational framework for our study, we begin by defining unlabeled graphs and their homomorphisms, followed by $\Sigma$-labeled graphs and their homomorphisms, following the presentation from [2] and [18]. Additionally, we introduce a method for visualizing graph homomorphisms presented in [38].

**Definition 1 (Unlabeled graph [2]).** An *unlabeled graph* $G$ consists of a set of *nodes* (also called *objects*) and a set of *arrows*, where each arrow has a *specific source* (or *domain*) node and a *target* (or *codomain*) node. An *unlabeled graph* is called *finite* if it has a finite number of nodes and arrows.
For an unlabeled graph $G$, we denote by $G_0$ its set of nodes, $G_1$ its set of arrows, **dom** the domain function, and **cod** the codomain function. We denote by $a : s \to t$ the arrow $a$ from $s$ to $t$.

A homomorphism of unlabeled graphs is a mapping between the nodes and edges of two graphs that preserves the graph structure.

**Definition 2 (Homomorphism of unlabeled graph).** Let $G$ and $H$ be unlabeled graphs. A homomorphism $h : G \to H$ is a pair of functions $h_0 : G_0 \to H_0$ and $h_1 : G_1 \to H_1$ such that for every arrow $a : s \to t$ in $G$, the image $h_1(a)$ is an arrow from $h_0(s)$ to $h_0(t)$ in $H$.

**Definition 3 (Graph [18]).** A graph is an ordered pair $(G, \lambda)$ where $G$ is an unlabelled graph and $\lambda : G_1 \to \Sigma$ is a labeling function.

We denote $a : s \stackrel{l}{\to} t$ the arrow $a$ labeled by $l$ from $s$ to $t$. A homomorphism of labeled graphs is a homomorphism of unlabeled graphs that preserves the labels assigned to the edges.

**Definition 4 (Graph homomorphism).** A homomorphism $h : (G, \lambda) \to (H, \lambda')$ is a homomorphism of unlabeled graphs such that for each arrow $a$ in $G$, we have $\lambda'(h_1(a)) = \lambda(a)$.

*Remark 5.* To visualize graph homomorphisms, we use the notation from [38]. Graphs are enclosed in boxes with their names displayed in the top-left corner. Nodes and arrows are assigned subsets of $\mathbb{N}$ as identifiers, chosen such that:

- Each node or arrow $y$ in the codomain graph is assigned the union of the identifiers of all nodes or arrows in the domain graph that map to $y$.

- The graph homomorphism $h$ is uniquely determined by this assignment.

To improve readability, we represent sets by listing their elements and omit identifiers when it does not lead to confusion. This is illustrated in the following representation of a homomorphism $h : G \to H$:

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

In this example, the sets $\{1\}$, $\{2\}$, $\{3\}$, $\{4\}$, and $\{3, 4\}$ are represented as 1, 2, 3, 4, and 3 4, respectively. Arrow identifiers are omitted for simplicity.
## 2.2 Pushouts

To establish the categorical foundations necessary for our work, we follow the presentation from [2], where a category is viewed as an unlabeled directed graph equipped with additional structure. In this framework, we recall key concepts such as monomorphisms, spans, cospans, commutative diagrams, and pushouts. We then focus on pushouts with monomorphisms within the category of graphs.

**Definition 6 (Category [2]).** A category *C* is an unlabeled graph *C* together with a total function *u* : *C*₀ → *C*₁ and a partial function ⋆ from *C*₁ × *C*₁ to *C*₁ such that

- for all arrows $f : X \to Y$ and $g : Y \to Z$, the arrow $f \star g : X \to Z$ is defined, and

- for every node $X$, we have $u(X) : X \to X$, and

- for every $f : X \to Y$, we have $u(X) \star f = f = f \star u(Y)$, and

- for all arrows $f, g$, and $h$, we have $(f \star g) \star h = f \star (g \star h)$ whenever either side is defined.

Arrows are called **morphisms**. The function $\star$ is called **composition**. If $X$ is an object of $\mathcal{C}$, the arrow $u(X)$ is denoted $\mathrm{id}_X$ and is called the **identity** of the object $X$. $\mathcal{C}$ is called the **underlying graph** of the category $\mathcal{C}$.

**Example 7.** The collection of all graphs and their homomorphisms forms a category. This category is referred to as **Graph**. In this category, the objects are graphs, and the morphisms are graph homomorphisms.

**Remark 8 (Notation).** The composition of morphisms $f : X \to Y$ and $g : Y \to Z$ is denoted $f \star g$, rather than the common $g \circ f$ notation, because it is more convenient to use.

**Definition 9 (Monomorphism [2]).** In a category, a morphism $f$ is said to be **monic** if for all morphisms $g$ and $h$, if $g \star f = h \star f$ then $g = h$. A monic morphism $f : X \to Y$ is called a **monomorphism** and will be denoted by $f : X \to Y$.

In the category **Graph**, a monomorphism is an injective homomorphism.

**Definition 10 (Span [33]).** An ordered pair $(\alpha : A \to B, \beta : A \to C)$ of morphisms sharing the same domain is called a **span**, denoted by $B \stackrel{\alpha}{\hookrightarrow} A \stackrel{\beta}{\twoheadrightarrow} C$.

**Definition 11 (Cospan).** An ordered pair $(\beta' : B \to D, \alpha' : C \to D)$ of morphisms sharing the same codomain is called a **cospan**. A cospan will be denoted by $B \stackrel{\beta'}{\twoheadrightarrow} D \stackrel{\alpha'}{\hookrightarrow} C$.

**Definition 12 (Diagram [2]).** Let $G$ be an unlabeled graph and $\mathcal{C}$ a category. A **diagram** (in $\mathcal{C}$ of shape $G$) is a homomorphism of unlabeled graphs $h : G \to \mathcal{C}$ where $\mathcal{C}$ is the underlying unlabeled graph of the category $\mathcal{C}$. A diagram is **commutative** if for all nodes $u, v$ and any two paths from $u$ to $v$ in the unlabeled graph $G$
<figure><img src="image_4.png" /></figure>

the equality $h(s_1) \star h(s_2) \star \dots \star h(s_{n-1}) = h(t_1) \star h(t_2) \star \dots \star h(t_{n-1})$ holds.

**Definition 13 (Pushout [2, 35]).** In a category, a **pushout** of a span $B \stackrel{\alpha}{\hookrightarrow}$

<figure><img src="image_5.png" /><figcaption>Fig. 1: pushout of span $(\alpha, \beta)$</figcaption></figure>

$A \xrightarrow{\beta} C$, depicted in Figure 1, is defined as a cospan $B \xrightarrow{\beta'} D \xleftarrow{\alpha'} C$ such that

$$ - \alpha \star \beta' = \beta \star \alpha', \text{ and} $$

- for every cospan $B \xrightarrow{\gamma'} E \xleftarrow{\delta} C$ if $\alpha \star \gamma' = \beta \star \gamma$ holds, then there exists a unique morphism $\delta: D \to E$ such that $\gamma' = \beta' \star \delta$ and $\gamma = \alpha' \star \delta$.

The diagram involving $\alpha, \beta, \alpha'$, and $\beta'$ is referred to as the **pushout square**, $D$ as the **pushout object**, and the existence of the unique morphism is known as the **universal mapping property (UMP) of the pushout**.

In the category **Graph** pushouts always exist, and their construction is straightforward when dealing with monomorphisms (injective graph homomorphisms). We denote $X \uplus Y$ the union of two disjoint sets. By possibly renaming nodes, a span of injective graph homomorphisms can be represented as $A \uplus B' \stackrel{\alpha}{\hookrightarrow} A \xrightarrow{\beta} A \uplus C'$ where $A, B', C'$ are disjoint sets and $\alpha$ and $\beta$ are inclusion function. A pushout of this span is then given by $A \uplus B' \xrightarrow{\beta'} A \uplus B' \uplus C' \stackrel{\alpha'}{\hookrightarrow} A \uplus C'$ where $\alpha'$ and $\beta'$ are inclusion function. This situation can be depicted by the diagram in Figure 2 where $B'$ and $C'$ are colored to make evident this decomposition in a concrete example within **Graph** in Example 14, where nodes and arrows are colored accordingly.

**Example 14.** The following diagram
<figure><img src="image_6.png" /><figcaption>Fig. 2: Construction of the pushout of a span of monomorphisms in **Graph**</figcaption></figure>

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

is a pushout square in the category **Graph** where nodes and arrows are colored to visualize the decomposition as in Figure 2.

To demonstrate that the diagram above is a pushout square, consider an object $X$ and morphisms $f : A \uplus B' \to X$ and $g : A \uplus C' \to X$ such that $\alpha \star f = \beta \star g$. Since $\alpha$ and $\beta$ are inclusion maps, it follows that $f$ and $g$ agree on $A$. Therefore, the morphism $h : A \uplus B' \uplus C' \to X$ defined by $h(x) = f(x)$ if $x \in A \uplus B'$ and $h(x) = g(x)$ otherwise is the unique morphism such that $\beta' \star h = f$ and $\alpha' \star h = g$. Thus, the object $A \uplus B' \uplus C'$, together with the morphisms $\beta'$ and $\alpha'$, satisfies the universal property of the pushout. Furthermore, the compositions $\alpha \star \beta'$ and $\beta \star \alpha'$ both map elements from $A$ to $A \uplus B' \uplus C'$ via inclusion function. Since all maps are inclusions and $A, B',$ and $C'$ are disjoint, the square commutes $\alpha \star \beta' = \beta \star \alpha'$. Therefore, the diagram is indeed a pushout square.

**Proposition 15 ([30]).** In the category **Graph**, pushouts along monomorphisms are also pullbacks.

*Remark 16 (Notation).* When only one morphism from node $A$ to node $B$ is relevant, it is sometimes denoted by $h_{AB}$. Furthermore, when the morphisms are clear from context, diagrams will be referred to by their nodes, similar to standard practice in geometry. For example, consider the diagram depicted in Figure 1. The sub-diagram involving morphisms $\alpha, \beta, \alpha', \beta'$ is denoted by ACDB or $\square$ACDB, and the sub-diagram involving $\alpha', \gamma, \delta$ is denoted by CDE or $\triangle$CDE.

## 2.3 Linear DPO rewriting system

This section recalls the notion of a linear DPO graph rewriting system with monic matches [see 15, 24, 30, 22]. In addition, we illustrate how a rewriting step with a linear rule can be visualized and constructed.
Although the linear DPO graph rewriting system with monic matches offers fewer features compared to other DPO variants [5, 6, 7] and more powerful algebraic approaches (e.g., [20, 4, 3, 19, 14, 12, 13, 39]), we focus on it because the type graph method is formulated within the DPO framework and it suffices for our purpose to have linear rule and monic match. Specifically, our aim is to provide a graph rewriting setting to model the graph rewriting rule described in Example 19 whose termination cannot be established using the methods in [22], and then propose a method to prove the termination of the rule within the proposed graph rewriting setting.

**Definition 17 (Rewriting rule [15, 30]).** A Linear DPO rewriting rule is a span $L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$ where the common source object K is called the **interface**, L the **input** and R the **output**.

*Example 18 ([Bruggink 9, Example 6]).* The span in the category **Graph** depicted below is a linear DPO rewriting rule, where *L* is the input graph, *K* is the interface graph and *R* is the output graph.

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

*Example 19 ([Plump 17, Example 6]).* The span on the category **Graph** depicted below is a linear DPO rewriting rule where *L* is the input graph, *K* is the interface graph and *R* is the output graph.

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

**Definition 20 (Match, Rewriting step [22]).** A match of a linear DPO rewriting rule $\rho: L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$ within a host object *G* is a monomorphism *m*: *L* $\rightarrow$ *G* from the input to the host object. A diagram with double pushouts (DPO)

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

defines a DPO rewriting step from *G* to *H* with the rule $\rho$ on the match *m*, denoted as $G \Rightarrow_{\rho,m} H$ or simply as $G \Rightarrow_{\rho} H$ if *m* is not relevant.
Consider a diagram representing a rewriting step in the category **Graph** using a linear Double Pushout (DPO) rewriting rule, as depicted in [Definition 20]. Since all morphisms are inclusion functions, we can decompose the graphs as follows: $L$ as $K \uplus L'$, $R$ as $K \uplus R'$, $C$ as $K \uplus C'$, $G$ as $L' \uplus K \uplus C'$, and $H$ as $R' \uplus K \uplus C'$ where $K, L', C', R'$ are pairwise disjoint sets. This allows us to visualize a rewriting step with a linear rule in **Graph** as in Figure 3 where the sets are colored by different colors:

<figure><img src="image_11.png" /><figcaption>Fig. 3: Rewriting step with a linear rule in **Graph**</figcaption></figure>

To illustrate this decomposition more clearly, Figure 4 presents a concrete DPO diagram, with nodes and arrows colored based on their corresponding sets in the decomposition presented in Figure 3.

<figure><img src="image_12.png" /><figcaption>Fig. 4: Example of a rewriting step with a linear rule in **Graph**</figcaption></figure>

**Definition 21 (Rewriting relation [22]).** Let $\mathcal{R}$ be a set of linear DPO rewriting rules. The binary relation $\Rightarrow_{\mathcal{R}}$ on graphs, which consists of DPO rewriting steps with rules from $\mathcal{R}$, defines a linear DPO rewriting relation.
## 2.4 Termination

In this section, we focus on the concept of relative termination, a critical property that ensures a rewriting relation allows only a finite number of steps from a specific set of rules. Originally formulated by Klop [29] for binary relations, as referenced by Geser [23], this concept has been used in previous works on the type graph method [41, 9, 8, 22] and in [37].

**Definition 22 (Relative termination [22]).** Let $\rightarrow$ and $\rightsquigarrow$ be two graph rewriting systems. We say that $\rightarrow$ is **terminating relative to** $\rightsquigarrow$ if in any infinite derivation $G_0 \rightarrow \cup \rightsquigarrow G_1 \rightarrow \cup \rightsquigarrow \dots$, only finite number of $\rightarrow$-steps occur.

The following proposition is an instance of a proposition in [Geser 23, page 31].

**Proposition 23 (Relative termination criterion).** Let $\rightarrow$ and $\rightsquigarrow$ be two linear DPO graph rewriting relations. $\rightarrow$ is **terminating relative to** $\rightsquigarrow$ if and only if there exists a measure $\mu$ from graphs to $\mathbb{N}$ such that:

- for all $G \rightarrow H$, we have $\mu(G) > \mu(H)$, and

- for all $G \rightsquigarrow H$, we have $\mu(G) \ge \mu(H)$.

## 3 Type Graph Method

The **type graph method** is a technique initially developed for the cycle rewriting in [41], later extended to DPO graph rewriting in [9, 8], and further generalized for various DPO graph rewriting variants and categories in [22].

This method is an interpretation approach [see 1] for proving termination. It begins by fixing a finite type graph $T$ and an ordered set $(S, \ge)$, whose elements are called *weights*, to associate weights to graphs. The process involves:

- **Morphism Interpretation:** A graph $G$ is represented as a finite set of morphisms from $G$ to $T$.

- **Weight Assignment:** Each morphism $f: G \rightarrow T$ is assigned a weight from $S$, converting the set of morphisms into weights.

- **Aggregation:** An aggregator function $\alpha: \mathcal{P}(S) \rightarrow S$ combines the set of weights into a single element in $S$.

To prove the relative termination of linear DPO graph rewriting systems, we employ a restricted version of the type graph method as presented in [22]. Specifically, each graph is interpreted as a unique morphism to a finite type graph $T_\Sigma$ (see Definition 24), which is assigned a weight from the ordered set $(\mathbb{N}, \le)$.

**Definition 24 (Type graph).** The **type graph** $T_\Sigma$ is defined as a graph comprising a single node $v$ and a collection of loops on $v$, with one loop for each label in $\Sigma$.
**Remark 25 (Notation).** For enhanced readability, we adopt the notation from [22, Notation 3.3]:

- For morphisms $\alpha : A \to B$ and $\gamma : A \to C$, we define

$$ \{\alpha \star - = \gamma\} \stackrel{\text{def}}{=} \{\beta \in \operatorname{Hom}(B, C) \mid \alpha \star \beta = \gamma\}. $$

- For morphisms $\beta : B \to C$ and $\gamma : A \to C$, we define

$$ \{-\star\beta = \gamma\} \stackrel{\text{def}}{=} \{\alpha \in \operatorname{Hom}(A, B) \mid \alpha \star \beta = \gamma\}. $$

- For a set $S \subseteq \operatorname{Hom}(A, B)$ and a morphism $\beta : B \to C$, we define

$$ S \star \beta \stackrel{\text{def}}{=} \{\alpha \star \beta \mid \alpha \in S\}. $$

Given a type graph $\mathcal{T}_\Sigma$, the weight of a graph $G$ is determined by the weight of the unique morphism $\phi : G \to \mathcal{T}_\Sigma$, which is equal to the number of morphisms from $X$ to $G$.

**Definition 26 (Weighing morphisms and objects [22]).** Let $\mathcal{T}_\Sigma$ be a type graph.

- The weight of the morphism $\phi : G \to \mathcal{T}_\Sigma$ is defined as

$$ w_{\mathcal{T}_{\Sigma}}(\phi) \stackrel{\text{def}}{=} |\operatorname{Hom}(X, G)|. $$

- The weight of the graph $G$ relative to $\mathcal{T}_\Sigma$ is defined as

$$ w_{\mathcal{T}_{\Sigma}}(G) \stackrel{\text{def}}{=} w_{\mathcal{T}_{\Sigma}}(\phi). $$

In certain scenarios, it is necessary to exclude specific morphisms when calculating the weight of a morphism. Given a set $\Gamma \subseteq \operatorname{Hom}(A, G)$, we define

$$ \Gamma' \stackrel{\text{def}}{=} \{\iota \in \operatorname{Hom}(X, G) \mid \exists \alpha \in \Gamma, \exists \zeta, \zeta \star \alpha = \iota\}. $$

This set comprises all morphisms from $X$ to $G$ that factor through some morphism $\alpha \in \Gamma$. Equivalently, it comprises all morphisms from $X$ to $G$ that can be decomposed as $\zeta \star \alpha$ with $\alpha \in \Gamma$, as depicted below.

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

The weight of the morphism $\phi : G \to \mathcal{T}_\Sigma$ excluding morphisms in $\Gamma'$ is defined as the number of morphisms from $X$ to $G$ that do not factor through any $\alpha \in \Gamma$.

**Definition 27 (Weight excluding specific morphisms [22]).** The weight of $\phi$ excluding morphisms in $\Gamma'$ is defined as

$$ w_{\mathcal{T}_{\Sigma}}(\phi - \Gamma) \stackrel{\text{def}}{=} |\operatorname{Hom}(X, G) \setminus \Gamma'| $$

**Remark 28.** If $\Gamma$ is a singleton $\{\alpha\}$, we may simplify the notation by writing $w_{\mathcal{T}_\Sigma}(\phi - \alpha)$ instead of $w_{\mathcal{T}_\Sigma}(\phi - \{\alpha\})$.
# 4 A new termination criterion by weighted type graph

In practice, applying the termination criterion from Proposition 23 can be challenging due to the potentially infinite number of rewriting steps involved. To address this issue, we introduce a machine-checkable termination criterion that relies solely on the finite set of rewriting rules and the conditions defining when and how a rewriting step can occur.

Let $X$ be a connected graph with at least one arrow. Our approach involves defining a special subgraph $R_x$ of the output graph $R$ associated with each linear DPO rewriting rule. Intuitively, $R_x$ includes every subgraph of $R$ that, together with a subgraph containing at least one arrow from some context graph $C$, can form the image of a graph homomorphism from $X$.

**Definition 29.** Let $X$ be a connected graph with at least one arrow, and let $L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$ be a linear double-pushout (DPO) rewriting rule. We define $\mathbf{R}_X$ as the smallest subgraph of $R$ containing $r(K)$ such that for every commutative diagram of the form:

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

where $h_{R'X}$ is not an isomorphism, we have $\mathrm{Im}(h_{R'R}) \subseteq R_x$.

To illustrate the role of $R_x$, consider Figures 5a and 5b. After applying a linear DPO rewriting rule, the resulting graph $H$ can be understood as the result of gluing the context graph $C$ and the output graph $R$ along the interface graph $K$ (see Figure 5a). The subgraph $R_x$ (depicted as the red area in Figure 5b) is the minimal subgraph of $R$ such that, for any morphism $\phi: X \to H$ that maps at least on arrow to $C$, the intersection $\mathrm{Im}(\phi) \cap R$ is included in $R_x$.

<figure><img src="image_15.png" /><figcaption>Fig. 5</figcaption></figure>

*Example 30.* Consider the following graph rewriting rule
<figure><img src="image_16.png" /></figure>

Let $X$ be the graph $\bullet \xrightarrow{s} \bullet \xleftarrow{s} \bullet$. The graph $R_x$ is

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

*Example 31.* Consider the following graph rewriting rule

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

Let $X$ be $\bullet \xrightarrow{a} \bullet \xleftarrow{a} \bullet$. The subgraph $R_x$ is

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

**Proposition 32.** Let $X$ be a connected graph with at least one arrow, and let $L \stackrel{l}{\longleftarrow} K \stackrel{r}{\longrightarrow} R$ be a linear DPO rewriting rule. There exists a unique $R_x$.

We now define a crucial property of rewriting rules that will form the basis of our termination criterion. Intuitively, this property ensures that for every morphism $\phi: X \to R$ that maps some part of $X$ into $R_x$, there is a corresponding morphism $\phi': X \to L$. This correspondence is essential for demonstrating a decrease in the number of morphisms from $X$ to the involved graphs, which is a key aspect of our termination argument.

**Definition 33.** Let $X$ be a connected graph with at least one arrow. Let $\rho = (L \stackrel{l}{\longleftarrow} K \stackrel{r}{\longrightarrow} R)$ be a linear DPO graph rewriting rule. We say that $\rho$ **decreases** the number of morphisms from $X$ if there exist a graph homomorphism $h_{RxL}: R_x \to L$ injective on arrows, and two injective graph homomorphisms $h_{KR_x}: K \to R_x$ and $h_{RxR}: R_x \to R$ such that

- For all $a \in R_x$, we have $h_{RxL}(a) \in l(K)$ if and only if $a \in h_{KR_x}(K)$ holds, and

- The following diagram commutes
<figure><img src="image_20.png" /></figure>

The hosting graph $\mathcal{H}$ can be understood as the result of gluing the context graph $\mathcal{C}$ and the input graph $\mathcal{L}$ along their shared interface graph $\mathcal{K}$ (see Figure 6a). Consider a rule $\rho$ that has the property. The image of $R_x$ under the graph homomorphism $h_{R_x L}$ is a subgraph of $\mathcal{L}$ that includes the interface graph $\mathcal{K}$ and satisfies the specified properties (depicted as the red area in Figure 6b). Since, every morphism $\phi: X \to R$ (whose image is represented by the blue rectangle in Figure 5b) can be understood as a morphism $\phi': X \to R_x$, the morphism $\phi' \star h_{R_x L}$ is a morphism from $X$ to $\mathcal{L}$, with the image shown as the blue area in Figure 6c.

<figure><img src="image_21.png" /><figcaption>Fig. 6</figcaption></figure>

*Example 34.* Consider the graph rewriting rule depicted by the bottom span of the following diagram

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

It decreases the number of morphisms from the graph • $\xrightarrow{s}$ • $\leftarrow$ • because there are graph homomorphisms making the commutative diagram depicted below.
*Example 35.* Consider the graph rewriting rule depicted by the bottom span of the following diagram

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

It decreases the number of morphisms from $\bullet \xrightarrow{a} \bullet \xleftarrow{a} \bullet$ because there are graph homomorphisms satisfying all required properties and forming the commutative diagram above.

With this property in place, we can show that the difference $|\mathrm{Hom}(X, G)| - |\mathrm{Hom}(X, H)|$ is bounded below by $|\mathrm{Hom}(X, L)| - |\mathrm{Hom}(X, R)|$, which depends only on the rewriting rule. We formalize this relationship in the following lemmas.

**Lemma 36.** Consider the following pushout square

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

For any connected graph $X$ with at least one arrow, we have

$$w_{T_X}(D) = w_{T_X}(\beta' \star \phi) + w_{T_X}(\alpha' \star \phi - \beta) + w_{T_X}(\phi - \{\alpha', \beta'\})$$

**Lemma 37.** Let $X$ be a connected graph with at least one arrow. Let $L \stackrel{l}{\hookrightarrow} K \stackrel{r}{\twoheadrightarrow} R$ be a linear DPO graph rewriting rule that decreases the number of morphisms from $X$. Consider the following commutative diagram:

<figure><img src="image_25.png" /></figure>
where □KLGC, □KCHR and □KCH'Rₓ are pushout squares. Let t_G, t_H' and t_H be the unique homorphisms from G, H' and H to T_Σ, respectively. We have

$$w_{T_{\Sigma}}(t_G - \{h_{LG}, h_{CG}\}) \geq w_{T_{\Sigma}}(t_{H'} - \{h_{R_x H'}, h_{CH'}\}) \geq w_{T_{\Sigma}}(t_H - \{h_{RH}, h_{CH}\})$$

**Lemma 38.** Let X be a connected graph with at least one arrow. Let $L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$ be a linear DPO graph rewriting rule which decreases the number of morphisms from X. Consider the commutative diagram in Lemma 37. Let $t_L, t_R$ be the unique morphisms from L, R to T_Σ. We have

$$w_{T_{\Sigma}}(G) - w_{T_{\Sigma}}(H) \geq |\mathrm{Hom}(X, L)| - |\mathrm{Hom}(X, R)|$$

*Proof.* Let $t_C, t_K, t_G, t_H, t_{H'}$ be the unique morphisms from C, K, G, H, H' to T_Σ. We have

$$
\begin{align*}
w_{T_{\Sigma}}(G) \\
&=w_{T_{\Sigma}}(h_{LG} \star t_G) + w_{T_{\Sigma}}(h_{CG} \star t_G - h_{KC}) + w_{T_{\Sigma}}(t_G - \{h_{LG}, h_{CG}\}) \quad \text{by Lemma 36} \\
&=w_{T_{\Sigma}}(t_L) + w_{T_{\Sigma}}(t_C - h_{KC}) + w_{T_{\Sigma}}(t_G - \{h_{LG}, h_{CG}\}) \\
&\geq w_{T_{\Sigma}}(t_L) + w_{T_{\Sigma}}(t_C - h_{KC}) + w_{T_{\Sigma}}(t_{H'} - \{h_{R_x H'}, h_{CH'}\}) \quad \text{by Lemma 37} \\
&=|\mathrm{Hom}(X, L)| + (w_{T_{\Sigma}}(t_C - h_{KC}) + w_{T_{\Sigma}}(t_{H'} - \{h_{R_x H'}, h_{CH'}\}))
\end{align*}
$$

and

$$
\begin{align*}
w_{T_{\Sigma}}(H) \\
&=(w_{T_{\Sigma}}(h_{RH} \star t_H) + w_{T_{\Sigma}}(h_{CH} \star t_H - h_{KC})) + w_{T_{\Sigma}}(t_H - \{h_{RH}, h_{CH}\}) \quad \text{by Lemma 36} \\
&=w_{T_{\Sigma}}(t_R) + w_{T_{\Sigma}}(t_C - h_{KC}) + w_{T_{\Sigma}}(t_H - \{h_{RH}, h_{CH}\}) \\
&\leq w_{T_{\Sigma}}(t_R) + w_{T_{\Sigma}}(t_C - h_{KC}) + w_{T_{\Sigma}}(t_{H'} - \{h_{R_x H'}, h_{CH'}\}) \quad \text{by Lemma 37} \\
&=|\mathrm{Hom}(X, R)| + (w_{T_{\Sigma}}(t_C - h_{KC}) + w_{T_{\Sigma}}(t_{H'} - \{h_{R_x H'}, h_{CH'}\}))
\end{align*}
$$

We now present our main termination theorem, which leverages these results to provide a machine-checkable criterion for relative termination.

**Theorem 39.** Let A and B be sets of linear DPO graph rewriting rules. Suppose there is a connected graph X with at least one arrow such that the following conditions are satisfied:

- Every rule $\rho \in A \cup B$ decreases the number of morphisms from X.

- For every rule $(L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R) \in A$, we have $|\mathrm{Hom}(X, L)| > |\mathrm{Hom}(X, R)|$.

- For every rule $(L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R) \in B$, we have $|\mathrm{Hom}(X, L)| \geq |\mathrm{Hom}(X, R)|$.

Under these conditions, $\Rightarrow_A$ is terminating relative to $\Rightarrow_B$.
# 5 Implementation and examples

The technique has been implemented in a tool, named Anonymous <fnref n="1" />, for automatically proving termination of graph rewriting systems. The tool is implemented in OCaml. Each example in this section is proven to terminate in under 0.5 seconds on a laptop with an i5-1038NG7 CPU (4 cores, 2 GHz base clock, 3.8 GHz boost), demonstrating the efficiency of our approach.

*Example 40.* Consider the following commutative diagram

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

The graph rewriting rule presented in [Bruggink et al. 9, Example 6] is depicted by the bottom span of the diagram. Let $X$ be the graph $\bullet \xrightarrow{a} \bullet \xleftarrow{a} \bullet$. The rewriting rule decreases the number of morphisms from the graph $X$ because there exist morphisms satisfying all required properties and forming the commutative diagram above. Furthermore, we have $|\operatorname{Hom}(X, L)| = 1 > 0 = |\operatorname{Hom}(X, R)|$. Thus, the rewriting rule terminates by Theorem 39.

*Example 41.* Consider the following commutative diagram

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

A graph rewriting rule presented in [Plump 17, Example 6] is depicted by the bottom span of the diagram. Let $X$ be the graph $\bullet \xrightarrow{s} \bullet \xleftarrow{s} \bullet$. The rewriting rule decreases the number of morphisms from $X$ as there are morphisms satisfying all required properties and forming the commutative diagram above.

<footnote n="1">¹ The source code can be accessed at https://osf.io/qwt2s/?view_only=34a3233b28b5427c8a5d430e0678c4fe</footnote>
Moreover, we observe that $|\mathrm{Hom}(X, L)| = 1 > 0 = |\mathrm{Hom}(X, R)|$. Thus, the rewriting rule terminates by Theorem 39.

However, as noted in [Endrullis et al. 22], the termination of this graph rewriting rule could not be established using any prior versions of type graph method due to the existence of a surjective graph homomorphism from $R$ to $L$.

*Example 42.* Consider the following commutative diagram

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

The graph rewriting rule presented in [Overbeek et al. 37, Example 52] is depicted by the bottom span of the diagram. Let $X$ be the graph $\bullet \stackrel{s}{\rightleftarrows} \bullet$. The rewriting rule decreases the number of morphisms from $X$ because there exist morphisms satisfying all required properties and forming the commutative diagram above. Moreover, we observe that $|\mathrm{Hom}(X, L)| = 1 > 0 = |\mathrm{Hom}(X, R)|$. Thus, the rewriting rule terminates by Theorem 39.

However, the termination of this rule cannot be established by the method proposed in [Overbeek et al. 37] due to its discrete interface graph.

*Example 43.* Consider the following commutative diagram

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

The rewriting rule depicted by the bottom span of the diagram is a variant of the rewriting rule presented in [Example 41]. Let $X$ be the graph $\bullet \xrightarrow{s} \bullet \xleftarrow{s} \bullet$. The rewriting rule decreases the number of morphisms from $X$ because there are morphisms satisfying all required properties and forming the commutative diagram. Furthermore, we have $|\mathrm{Hom}(X, L)| = 1 > 0 = |\mathrm{Hom}(X, R)|$. As a result, it terminates by Theorem 39.

However, its termination cannot be proved by the existing formulations of the type graph method, for the same reasons as the rewriting rule in [Example 41]. Furthermore, the termination of this rewriting rule cannot be proven using the
measure proposed in [Plump 17], because if the context is the empty graph than we have $3^k < 2^k+2^k+3^k$ for all $k \in \mathbb{N}$, nor by the method proposed in [Overbeek et al. 37], due to the discrete interface.

These results can be summarized in Table 1.

<table><caption>Table 1: Comparison of termination techniques</caption><thead><tr><th></th><th>Example 40</th><th>Example 41</th><th>Example 42</th><th>Example 43</th></tr></thead><tbody><tr><td>Plump 2018</td><td>✗</td><td>✓</td><td>✗</td><td>✗</td></tr><tr><td>Bruggink et al. 2014</td><td></td><td></td><td></td><td></td></tr><tr><td>Bruggink et al. 2015</td><td>✓</td><td>✗</td><td>✓</td><td>✗</td></tr><tr><td>Endrullis et al. 2023</td><td></td><td></td><td></td><td></td></tr><tr><td>Overbeek et al. 2023</td><td>✓</td><td>✓</td><td>✗</td><td>✗</td></tr><tr><td>Our Approach</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr></tbody></table>

# 6 Conclusion and future work

The weighted type graph method has proven to be highly effective, enabling the automatic and efficient verification of termination in complex graph rewriting systems, such as the one presented in [32]. Our approach builds upon previous research on the type graph method [41, 9, 8, 22]. Unlike prior research on the type graph method, our approach considers the number of morphisms from graphs with more than one edge, at the cost of restricting our focus to finite arrow-labeled multigraphs. Other relevant works include [36, 17]. For a comprehensive comparison of these methods, we refer the reader to [22, 37].

We have proposed a termination criterion to enhance this method for proving termination of linear DPO rewriting systems on directed arrow-labeled multigraphs. Our enhancement not only successfully proves the termination of systems like the one described in [Plump 17, Example 6], which existing formulations of the type graph method cannot address, but also address the termination of Example 43, which other advanced termination techniques for graph rewriting fail to prove. Additionally, it simplifies termination proofs for cases like [Bruggink et al. 9, Example 4].

There are several interesting directions for future work. One interesting direction is to investigate whether the performance of the method introduced in [Overbeek et al. 37] can be enhanced when dealing with discrete interfaces by applying ideas similar to those presented in this article. Additionally, exploring the possibility of extending this approach to other categories beyond the current scope could significantly broaden its applicability.

**Acknowledgments.** This study was partially funded by the project SAPPORO, ANR, 2019-CE25-0005.
References

[1] F. Baader and T. Nipkow. *Term rewriting and all that*. Cambridge university press, 1998.

[2] M. Barr and C. Wells. *Category Theory for Computing Science*. Vol. 1. Prentice Hall New York, 1990.

[3] M. Bauderon and H. Jacquet. "Pullback as a Generic Graph Rewriting Mechanism". In: *Applied Categorical Structures* 9 [2001], pp. 65–82. doi: 10.1023/A:1010659322914.

[4] Michel Bauderon. "A Uniform Approach to Graph Rewriting: The Pullback Approach". In: *Graph-Theoretic Concepts in Computer Science*. Ed. by Manfred Nagl. Vol. 1017. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1995, pp. 101–115. ISBN: 978-3-540-60618-5. doi: 10.1007/3-540-60618-1_69.

[5] N. Behr, R. Harmer, and J. Krivine. "Concurrency theorems for non-linear rewriting theories". In: *International Conference on Graph Transformation*. Springer. 2021, pp. 3–21.

[6] N. Behr, R. Harmer, and J. Krivine. "Fundamentals of Compositional Rewriting Theory". In: *Journal of Logical and Algebraic Methods in Programming* 135 [2023]. doi: 10.1016/j.jlamp.2023.100893.

[7] B. Braatz, U. Golas, and T. Soboll. "How to delete categorically—two pushout complement constructions". In: *Journal of Symbolic Computation* 46.3 [2011], pp. 246–271.

[8] H.J.S. Bruggink, B. König, D. Nolte, and H. Zantema. "Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings". In: *Proc. Conf. on Graph Transformation (ICGT). Vol. 9151*. LNCS. Springer, 2015, pp. 52–68. doi: 10.1007/978-3-319-21145-9_4.

[9] H.J.S. Bruggink, B. König, and H. Zantema. "Termination Analysis for Graph Transformation Systems". In: *Proc. Conf. on Theoretical Computer Science (TCS). Vol. 8705*. LNCS. Springer, 2014, pp. 179–194. doi: 10.1007/978-3-662-44602-7_15.

[10] *Certified Termination Competition*. https://termination-portal.org/wiki/Certified_Termination. Last accessed: October 9, 2024.

[11] E. Contejean, C. Marché, B. Monate, and X. Urbain. "Proving Termination of Rewriting with CiME". In: *Extended Abstracts of the 6th International Workshop on Termination, WST'03*. 2003, pp. 71–73.

[12] A. Corradini, D. Duval, R. Echahed, F. Prost, and L. Ribeiro. "AGREE-Algebraic Graph Rewriting with Controlled Embedding". In: *International Conference on Graph Transformation*. Vol. 9151. Lecture Notes in Computer Science. Cham: Springer, 2015, pp. 35–51. ISBN: 978-3-319-21145-9. doi: 10.1007/978-3-319-21145-9_3.

[13] A. Corradini, D. Duval, R. Echahed, F. Prost, and L. Ribeiro. "The PBPO Graph Transformation Approach". In: *Journal of Logical and Algebraic Methods in Programming* 103 [2019], pp. 213–231. doi: 10.1016/j.jlamp.2018.12.003.
[14] A. Corradini, T. Heindel, F. Hermann, and Barbara König. "Sesqui-Pushout Rewriting". In: *Graph Transformations*. Ed. by A. Corradini, H. Ehrig, U. Montanari, L. Ribeiro, and G. Rozenberg. Vol. 4178. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2006, pp. 30–45. ISBN: 978-3-540-38872-2. DOI: 10.1007/11841883_3.

[15] A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel, and M. Löwe. "Algebraic Approaches to Graph Transformation - Part I: Basic Concepts and Double Pushout Approach". In: *Handbook of Graph Grammars*. 1997.

[16] P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. "Certified Universal Gathering in $\mathbb{R}^2$ for Oblivious Mobile Robots". In: *Distributed Computing*. Ed. by C. Gavoille and D. Ilcinkas. Berlin, Heidelberg: Springer Berlin Heidelberg, 2016, pp. 187–200. ISBN: 978-3-662-53426-7.

[17] P. Detlef. "Modular Termination of Graph Transformation". In: *Graph Transformation, Specifications, and Nets: In Memory of Hartmut Ehrig* [2018], pp. 231–244.

[18] H. Ehrig, K. Ehrig, U. Golas, and G. Taentzer. *Fundamentals of Algebraic Graph Transformation*. Vol. XIV. 2006. DOI: 10.1007/3-540-31188-2.

[19] H. Ehrig, A. Habel, J. Padberg, and U. Prange. "Adhesive High-Level Replacement Categories and Systems". In: *Graph Transformations*. Ed. by H. Ehrig, G. Engels, F. Parisi-Presicce, and G. Rozenberg. Vol. 3256. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2004, pp. 144–160. ISBN: 978-3-540-30203-2. DOI: 10.1007/978-3-540-30203-2_12.

[20] H. Ehrig, Reiko Heckel, Michael Korff, Michael Löwe, L. Ribeiro, Annika Wagner, and A. Corradini. "Algebraic Approaches to Graph Transformation – Part II: Single Pushout Approach and Comparison with Double Pushout Approach". In: *Handbook of Graph Grammars and Computing by Graph Transformation*. Ed. by G. Rozenberg. Singapore: World Scientific, 1997, pp. 247–312. DOI: 10.1142/9789812384720_0004.

[21] Hartmut Ehrig, Michael Pfender, and Hans Jürgen Schneider. "Graph-grammars: An algebraic approach". In: *14th Annual symposium on switching and automata theory (swat 1973)*. IEEE. 1973, pp. 167–180.

[22] J. Endrullis and R. Overbeek. *Generalized Weighted Type Graphs for Termination of Graph Transformation Systems*. 2023. arXiv: 2307.07601 [cs.LO].

[23] A. Geser. "Relative Termination". In: 1990.

[24] Annegret Habel, Jürgen Müller, and Detlef Plump. "Double-pushout approach with injective matching". In: *International Workshop on Theory and Application of Graph Transformations*. Springer, 1998, pp. 103–116.

[25] Annegret Habel, Jürgen Müller, and Detlef Plump. "Double-pushout graph transformation revisited". In: *Mathematical Structures in Computer Science* 11.5 [2001], pp. 637–688.

[26] J. Harrison. "Formal Verification". In: *Software and Systems Safety*. IOS Press, 2011, pp. 103–157.
[27] J. Harrison, J. Urban, and F. Wiedijk. "History of Interactive Theorem Proving". In: *Handbook of the History of Logic*. Vol. 9. Elsevier, 2014, pp. 135–214.

[28] G. Heiser, J. Andronick, K. Elphinstone, G. Klein, I. Kuz, and L. Ryzhyk. "The Road to Trustworthy Systems". In: *Proceedings of the Fifth ACM Workshop on Scalable Trusted Computing*. 2010, pp. 3–10.

[29] J.W. Klop. "Term Rewriting Systems: A Tutorial". In: *Bulletin of the European Association for Theoretical Computer Science* [1987].

[30] S. Lack and P. Sobociński. "Adhesive Categories". In: *International Conference on Foundations of Software Science and Computation Structures*. Springer. 2004, pp. 273–288.

[31] L. Lamport, R. Shostak, and M. Pease. "The Byzantine Generals Problem". In: *ACM Transactions on Programming Languages and Systems* 4.3 [1982], pp. 382–401. DOI: 10.1145/357172.357176.

[32] I. Litovsky, Y. Métivier, and É. Sopena. "Checking Global Graph Properties by Means of Local Computations: The Majority Problem". In: *Electronic Notes in Theoretical Computer Science* 2 [1995], pp. 199–206.

[33] M. Löwe. "Graph Rewriting in Span-Categories". In: *Graph Transformations*. Ed. by H. Ehrig, A. Rensink, G. Rozenberg, and A. Schürr. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010.

[34] F. Maric. "A Survey of Interactive Theorem Proving". In: *Zbornik radova* 18.26 [2015], pp. 173–223.

[35] R. Overbeek and J. Endrullis. "A PBPO+ Graph Rewriting Tutorial". In: *TERMGRAPH@FSCD*. 2023.

[36] R. Overbeek and J. Endrullis. "Termination of Graph Transformation Systems Using Weighted Subgraph Counting". In: *International Conference on Graph Transformation*. Springer. 2023, pp. 81–101.

[37] R. Overbeek and J. Endrullis. "Termination of Graph Transformation Systems Using Weighted Subgraph Counting". In: *ArXiv abs/2303.07812* [2023].

[38] R. Overbeek, J. Endrullis, and A. Rosset. "Graph Rewriting and Relabeling with PBPO+: A Unifying Theory for Quasitoposes". In: *Journal of Logical and Algebraic Methods in Programming* 133 [2023]. DOI: https://doi.org/10.1016/j.jlamp.2023.100873.

[39] R. Overbeek, J. Endrullis, and A. Rosset. "Graph Rewriting and Relabeling with PBPO+: A Unifying Theory for Quasitoposes". In: *Journal of Logical and Algebraic Methods in Programming* 133 [2023], p. 100873. ISSN: 2352-2208. DOI: 10.1016/j.jlamp.2023.100873.

[40] M. Potop-Butucaru, N. Sznajder, S. Tixeuil, and X. Urbain. "Formal Methods for Mobile Robots". In: *Distributed Computing by Mobile Entities: Current Research in Moving and Computing* [2019], pp. 278–313.

[41] H. Zantema, B. König, and H.J.S. Bruggink. "Termination of Cycle Rewriting". In: *International Conference on Rewriting Techniques and Applications*. Springer. 2014, pp. 476–490.
# Appendix A : Pullbacks

## Definition 44 (Pullback [2, 35]).

<figure><img src="image_30.png" /><figcaption>Fig. 7: pullback of $(\beta', \alpha')$</figcaption></figure>

In a category, a **pullback** of a cospan $B \xrightarrow{\beta'} D \xleftarrow{\alpha'} C$, depicted in Figure 7, is defined as a span $B \stackrel{\alpha}{\hookrightarrow} A \xrightarrow{\beta} C$ such that for every span $B \stackrel{\alpha'}{\hookleftarrow} E \xrightarrow{\gamma} C$ if $\gamma' \star \beta' = \gamma \star \alpha'$ holds, then there exists a unique morphism $\delta : E \to A$ such that $\gamma' = \delta \star \alpha$ and $\gamma = \delta \star \beta$. The diagram involving $\alpha, \beta, \alpha'$, and $\beta'$ is referred to as the **pullback square**, *A* as the **pullback object**, and the existence of the unique morphism is known as the **universal mapping property (UMP) of the pullback**.

In the category **Graph**, pullbacks always exist, and their construction is straightforward when dealing with monomorphisms (injective graph homomorphisms). We denote $X \uplus Y$ the union of two disjoint sets. Similarly, a cospan of injective graph homomorphisms, possibly with renamed nodes, takes the form $A \uplus B' \xrightarrow{\beta'} A \uplus B' \uplus C' \xleftarrow{\alpha'} A \uplus C'$ where $A, B', C'$ are disjoint sets and $\alpha', \beta'$ are inclusion function. A pullback of this cospan is $A \uplus B' \xrightarrow{\alpha} A \xrightarrow{\beta} A \uplus C'$ where $\alpha$ and $\beta$ are inclusion function. The diagram is depicted below:

<figure><img src="image_31.png" /><figcaption>Fig. 8</figcaption></figure>

*Example 45.* The diagram in Figure 9 is a pullback square in the category **Graph** where nodes and arrows are colored to visualize the decomposition as in Figure 8.
<figure><img src="image_32.png" /><figcaption>Fig. 9: Example of the pullback of cospan of monomorphism in **Graph**</figcaption></figure>

The compositions $\beta' \circ \alpha$ and $\alpha' \circ \beta$ both map elements from $A$ to $A \uplus B' \uplus C'$ via inclusion function. Since all maps are inclusions and $A, B',$ and $C'$ are disjoint, the square commutes $\beta' \circ \alpha = \alpha' \circ \beta$.

To demonstrate that Figure 8 is a pullback square, suppose we have an object $X$ and morphisms $f: X \to A \uplus B'$ and $g: X \to A \uplus C'$ such that $\alpha' \circ f = \beta' \circ g$. Our goal is to prove that there exists a unique morphism $h: X \to A$ such that $\alpha \circ h = f$ and $\beta \circ h = g$.

Since $\alpha'$ and $\beta'$ are inclusion maps into $A \uplus B' \uplus C'$, and $\alpha' \circ f = \beta' \circ g$, it follows that for all $x \in X$, $f(x) = g(x) \in A \uplus B' \uplus C'$. Because $B'$ and $C'$ are disjoint and their images under $\alpha'$ and $\beta'$ are also disjoint in $A \uplus B' \uplus C'$, the only way $\alpha' \circ f(x) = \beta' \circ g(x)$ is if both $f(x)$ and $g(x)$ are in $A$ and map to the same element in $A \uplus B' \uplus C'$. Therefore, $f(x), g(x) \in A$ and $f(x) = g(x)$. We can now define $h: X \to A$ by $h(x) = f(x) = g(x)$ for all $x \in X$.

We need to verify that $\alpha \circ h = f$ and $\beta \circ h = g$. Since $\alpha$ and $\beta$ are inclusion maps of $A$ into $A \uplus B'$ and $A \uplus C'$, respectively, it follows that $\alpha \circ h(x) = \alpha(f(x)) = f(x)$, since $h(x) = f(x)$ and $\alpha$ is inclusion. Similarly, $\beta \circ h(x) = \beta(g(x)) = g(x)$.

Suppose there exists another morphism $h': X \to A$ satisfying $\alpha \circ h' = f$ and $\beta \circ h' = g$. Then for all $x \in X$, $f(x) = \alpha \circ h'(x)$, $g(x) = \beta \circ h'(x)$. Since $\alpha$ and $\beta$ are inclusions, $\alpha \circ h'(x) = h'(x)$ in $A \uplus B'$ and $\beta \circ h'(x) = h'(x)$ in $A \uplus C'$. Therefore, $f(x) = h'(x) = g(x)$. But we already have $h(x) = f(x) = g(x)$, so $h'(x) = h(x)$ for all $x \in X$. Thus, $h$ is unique.

Since there exists a unique morphism $h: X \to A$ such that $\alpha \circ h = f$ and $\beta \circ h = g$, the diagram in Figure 8 satisfies the universal property of the pullback. Therefore, the diagram is indeed a pullback square.

**Proposition 46** ([30]). In the category **Graph**, pushouts along monomorphisms are also pullbacks.
# Appendix B : Proof of Lemma 36

**Lemma 36** Consider the following pushout square

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

For any connected graph $X$ with at least one arrow, we have

$$w_{T_{\Sigma}}(D) = w_{T_{\Sigma}}(\beta' \star \phi) + w_{T_{\Sigma}}(\alpha' \star \phi - \beta) + w_{T_{\Sigma}}(\phi - \{\alpha', \beta'\})$$

*Proof.* By Definition 26, we have

$$ 
\begin{align*}
w_{T_{\Sigma}}(G) &\stackrel{\text{def}}{=} |\operatorname{Hom}(X, D)| \\
w_{T_{\Sigma}}(\beta' \star \phi) &\stackrel{\text{def}}{=} |\operatorname{Hom}(X, B)| \\
w_{T_{\Sigma}}(\alpha' \star \phi - \beta) &\stackrel{\text{def}}{=} |\{\iota \in \operatorname{Hom}(X, C) \mid \#\zeta : X \to A. \iota = \zeta \star \beta\}| \\
w_{T_{\Sigma}}(\phi - \{\alpha', \beta'\}) &\stackrel{\text{def}}{=} |\{\iota \in \operatorname{Hom}(X, D) \mid (\#\zeta : X \to B. \iota = \zeta \star \beta') \wedge (\#\zeta : X \to C. \iota = \zeta \star \alpha')\}|
\end{align*}
$$

It suffices to prove that

$$|\operatorname{Hom}(X, D)| = |\operatorname{Hom}(X, B)| + |\Psi_{C-A}| + |\Psi_{\neg B, \neg C}|$$

where

$$ 
\begin{align*}
\Psi_{C-A} &\stackrel{\text{def}}{=} \{\iota \in \operatorname{Hom}(X, C) \mid \#\zeta : X \to A. \iota = \zeta \star \beta\} \\
\Psi_{\neg B, \neg C} &\stackrel{\text{def}}{=} \{\iota \in \operatorname{Hom}(X, D) \mid (\#\zeta : X \to B. \iota = \zeta \star \beta') \wedge (\#\zeta : X \to C. \iota = \zeta \star \alpha')\}
\end{align*}
$$

From

$$\operatorname{Hom}(X, D) = \Phi_B \text{[+]} \Phi_{C-A} \text{[+]} \Psi_{\neg B, \neg C}$$

where

$$ 
\begin{align*}
\Phi_B &\stackrel{\text{def}}{=} \{\iota \in \operatorname{Hom}(X, D) \mid \exists\zeta : X \to B. \iota = \zeta \star \beta'\} \\
\Phi_{C-A} &\stackrel{\text{def}}{=} \{\iota \in \operatorname{Hom}(X, D) \mid (\#\zeta : X \to B. \iota = \zeta \star \beta') \wedge (\exists\eta : X \to C. \iota = \eta \star \alpha')\}
\end{align*}
$$

we deduce

$$|\operatorname{Hom}(X, D)| = |\Phi_B| + |\Phi_{C-A}| + |\Psi_{\neg B, \neg C}|$$

Hence, it suffices to prove

$$|\operatorname{Hom}(X, B)| = |\Phi_B|$$

and

$$|\Phi_{C-A}| = |\Psi_{C-A}|$$
Claim. $|\operatorname{Hom}(X, B)| = |\Phi_B|$

- Define $\Psi_B \stackrel{\text{def}}{=} \operatorname{Hom}(X, B) \star \beta'$.

- The inclusion $\Psi_B \subseteq \Phi_B$ holds because if a morphism $\iota : X \to D$ is an element of $\Psi_B$, then, according to the definition of $\Psi_B$, there exists a morphism $\zeta : X \to B$ satisfying $\iota = \zeta \star \beta'$. Consequently, $\iota$ is also an element of $\Phi_B$.

- The inclusion $\Psi_B \supseteq \Phi_B$ holds because if a morphism $\iota : X \to D$ is an element of $\Phi_B$, then, according to the definition of $\Phi_B$, there exists a morphism $\zeta : X \to B$ satisfying $\iota = \zeta \star \beta'$. Since $\zeta \in \operatorname{Hom}(X, B)$, it follows that $\iota = \zeta \star \beta'$ is in $\operatorname{Hom}(X, B) \star \beta' = \Psi_B$.

- Thus, $\Psi_B = \Phi_B$ and consequently $|\Psi_B| = |\Phi_B|$.

- We have $|\operatorname{Hom}(X, B)| = |\Psi_B|$, by the monicity of $\beta'$.

- Hence, the equality $|\operatorname{Hom}(X, B)| = |\Phi_B|$ holds.

Claim. $|\Psi_{C-A}| = |\Phi_{C-A}|$

- The inclusion $\Psi_{C-A} \star \alpha' \subseteq \Phi_{C-A}$ can be justified as follows. Suppose that $\iota : X \to D$ is an element of $\Psi_{C-A} \star \alpha'$. According to the definition of $\Psi_{C-A} \star \alpha'$, there exists $\eta : X \to C$ in $\Psi_{C-A}$ such that $\iota = \eta \star \alpha'$. We need to show that no $\zeta : X \to B$ exists such that $\iota = \zeta \star \beta'$. Assuming the contrary, that such a $\zeta$ exists. Under this assumption, the following commutative diagram holds:

- The inclusion $\Psi_{C-A} \star \alpha' \subseteq \Phi_{C-A}$ can be justified as follows: Suppose $\iota : X \to D$ is an element of $\Psi_{C-A} \star \alpha'$. By the definition of $\Psi_{C-A} \star \alpha'$, there exists a morphism $\eta : X \to C$ in $\Psi_{C-A}$ such that $\iota = \eta \star \alpha'$. To demonstrate that $\iota$ also belongs to $\Phi_{C-A}$, consider if there were a $\zeta : X \to B$ such that $\iota = \zeta \star \beta'$. Assuming this contrary scenario, the following commutative diagram would need to be satisfied:

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

The pushout square $\Box ABDC$ is also a pullback square, by Proposition 46. The universal mapping property of the pullback provides a morphism $\gamma : X \to A$ such that $\eta = \gamma \star \beta$, contradicting the assumption that $\eta \in \Psi_{C-A}$. Thus, $\iota$ is also an element of $\Phi_{C-A}$.

- The inclusion $\Psi_{C-A} \star \alpha' \supseteq \Phi_{C-A}$ can be justified as follows. Suppose that $\iota : X \to D$ is an element of $\Phi_{C-A}$. According to the definition of $\Phi_{C-A}$, there exists $\eta : X \to C$ making $\iota = \eta \star \alpha'$. We show that morphism $\eta$ is an element of $\Psi_{C-A}$, by showing no morphism $\zeta : X \to A$ satisfying $\eta = \zeta \star \beta$.
Assume the contrary, and observe:

$$
\begin{align*}
\iota &\stackrel{\text{def}}{=} \eta \star \alpha' \\
&\stackrel{\text{def}}{=} (\zeta \star \beta) \star \alpha' && \text{by assumption} \\
&\stackrel{\text{def}}{=} \zeta \star (\beta \star \alpha') && \text{by associativity} \\
&\stackrel{\text{def}}{=} \zeta \star (\alpha \star \beta') && \text{by commutativity of } \Box ABDC \\
&\stackrel{\text{def}}{=} (\zeta \star \alpha) \star \beta' && \text{by associativity of } \Box ABDC
\end{align*}
$$

There is a contradiction concerning $\iota$, which can be demonstrated as follows.
Let $h \stackrel{\text{def}}{=} \zeta \star \alpha$. The morphism $h$ is an element of $\operatorname{Hom}(X, B)$ and satisfies
$\iota = h \star \beta'$. However, since $\iota$ is an element of $\Phi_{C-A}$, no such morphism $h$
should exist, as it would contradict the definition of $\Phi_{C-A}$. Therefore, there
is no $\zeta : X \to A$ such that $\eta = \zeta \star \beta$, confirming $\eta$ as an element of $\Psi_{C-A}$.
Consequently, $\iota = \eta \star \alpha'$ is an element of $\Psi_{C-A} \star \alpha'$.

- From $\tilde{\Psi}_{C-A} \star \alpha' \subseteq \tilde{\Phi}_{C-A}$ and $\tilde{\Psi}_{C-A} \star \alpha' \supseteq \tilde{\Phi}_{C-A}$, we conclude $\tilde{\Psi}_{C-A} \star \alpha' = \tilde{\Phi}_{C-A}$ and $|\tilde{\Psi}_{C-A} \star \alpha'| = |\tilde{\Phi}_{C-A}|$. Since $\alpha'$ is monic, $|\tilde{\Psi}_{C-A}| = |\tilde{\Psi}_{C-A} \star \alpha'|$. Therefore, $|\tilde{\Psi}_{C-A}| = |\tilde{\Phi}_{C-A}|$.
## Appendix C: Proof of Lemma 37

Let $X$ be a connected graph with at least one arrow, and let $\rho = (l, r)$ be a rewriting rule that has more morphisms from $X$ to the input graph than to the output graph. Consider the commutative diagram depicted below, where the squares $\square KLGC$, $\square KCHR$, and $\square KCH'R_x$ are pushout squares:

<figure><img src="image_35.png" /><figcaption>Fig. 10</figcaption></figure>

Let $t_X, t_G, t_{H'},$ and $t_H$ be the unique graph homomorphisms from $X, G, H'$, and $H$ to $T_X^X$, as defined in Definition 24. We define

$$ \Psi_{\neg L, \neg C} \stackrel{\text{def}}{=} \{ \iota : X \to G \mid \begin{aligned}[t] & \nexists \zeta : X \to L. \iota = \zeta \star h_{LG} \wedge \\ & \nexists \eta : X \to C. \iota = \eta \star h_{CG} \wedge \\ & t_X = \iota \star t_G \end{aligned} \} $$

$$ \Psi_{\neg R_x, \neg C} \stackrel{\text{def}}{=} \{ \iota : X \to H' \mid \begin{aligned}[t] & \nexists \zeta : X \to R_x. \iota = \zeta \star h_{R_x H'} \wedge \\ & \nexists \eta : X \to C. \iota = \eta \star h_{CH'} \wedge \\ & t_X = \iota \star t_{R_x} \end{aligned} \} $$

$$ \Psi_{\neg R, \neg C} \stackrel{\text{def}}{=} \{ \iota : X \to H \mid \begin{aligned}[t] & \nexists \zeta : X \to R. \iota = \zeta \star h_{RH} \wedge \\ & \nexists \eta : X \to C. \iota = \eta \star h_{CH} \wedge \\ & t_X = \iota \star t_H \end{aligned} \} $$

**Lemma 37**

We have

$$ w_{T_X^X}(t_G - \{h_{LG}, h_{CG}\}) \ge w_{T_X^X}(t_{H'} - \{h_{R_x H'}, h_{CH'}\}) \ge w_{T_X^X}(t_H - \{h_{RH}, h_{CH}\}) $$

*Proof.* By Definition 26,

$$ w_{\tau_X}(t_G - \{h_{LG}, h_{CG}\}) = |\Psi_{\neg L, \neg C}| $$

$$ w_{\tau_X}(t_{H'} - \{h_{R_x H'}, h_{CH'}\}) = |\Psi_{\neg R_x, \neg C}| $$

$$ w_{\tau_X}(t_H - \{h_{RH}, h_{CH}\}) = |\Psi_{\neg R, \neg C}| $$
Therefore, it is equivalent to prove

$$|\Psi_{\neg R, \neg C}| \leq |\Psi_{\neg R_x, \neg C}| \leq |\Psi_{\neg L, \neg C}|$$

By Lemma 51 and Lemma 53, there exists an injective function $\mathbb{F}: \Psi_{\neg R_x, \neg C} \to \Psi_{\neg L, \neg C}$. Hence, $|\Psi_{\neg R_x, \neg C}| \leq |\Psi_{\neg L, \neg C}|$.

By Lemma 56 and Lemma 57, there exists an injective function $\mathbb{G}: \Psi_{\neg R, \neg C} \to \Psi_{\neg R_x, \neg C}$. Thus, $|\Psi_{\neg R, \neg C}| \leq |\Psi_{\neg R_x, \neg C}|$.

**Lemma 47.** Consider the pushout square in Graph of form

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

- If $b \in B$ and $c \in C$ such that $h_{BD}(b) = h_{CD}(c)$ then there is $a \in A$ such that $h_{AB}(a) = b$ and $h_{AC}(a) = c$.

- For all $b \in B \setminus \text{Im}(a)$ and $c \in C$, we have $\beta'(b) \neq \alpha'(c)$.

*Proof.* The pushout square $\Delta$ is also a pullback square, by Proposition 46. The conclusion is trivial.

□

**Lemma 48.** Consider the commutative diagram depicted below:

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

If $h_{XH'} \in \Psi_{\neg R_x, \neg C}$, then we have $\text{Im}(h_{C'C}) \not\subseteq \text{Im}(h_{KC})$ and $\text{Im}(h_{R'R_x}) \not\subseteq \text{Im}(h_{KR_x})$

*Proof.* Suppose $h_{XH'} \in \Psi_{\neg R_x, \neg C}$. By symmetry, it suffices to prove that $\text{Im}(h_{C'C}) \not\subseteq \text{Im}(h_{KC})$.

Suppose, by contradiction, that

$$\text{Im}(h_{C'C}) \subseteq \text{Im}(h_{KC}) \qquad (\text{hyp1})$$

We will show that this assumption leads to the existence of a morphism $\zeta: X \to R_x$ such that $h_{XH'} = \zeta \star h_{R_x H'}$, which contradicts the premise $h_{XH'} \in \Psi_{\neg R_x, \neg C}$, where no such morphism $\zeta$ should exist.
Given the monicity of $h_{KC}$ and (hyp1), we can define a graph homomorphism $h_{C'K}$ such that for any $c' \in C'$, we define $h_{C'K}(c') \stackrel{\text{def}}{=} k \in K$, where $k$ is the unique element in $K$ satisfying $h_{KC}(k) = h_{C'C}(c')$. We then have:

$$h_{C'K} \star h_{KC} = h_{C'C} \qquad (0)$$

The following equation follows:

$$(h_{K'C'} \star h_{C'K} \star h_{KR_x}) \star h_{R_x H'} = (h_{K'R'} \star h_{R'R_x}) \star h_{R_x H'} \qquad (1)$$

because:

$$ \begin{align*} & (h_{K'C'} \star h_{C'K} \star h_{KR_x}) \star h_{R_x H'} \\ &= h_{K'C'} \star h_{C'K} \star (h_{KR_x} \star h_{R_x H'}) && \text{by associativity} \\ &= h_{K'C'} \star h_{C'K} \star (h_{KC} \star h_{CH'}) && \text{by commutativity of } \square KCH'R_x \\ &= h_{K'C'} \star (h_{C'K} \star h_{KC}) \star h_{CH'} && \text{by associativity} \\ &= h_{K'C'} \star h_{C'C} \star h_{CH'} && \text{by (0)} \\ &= (h_{K'R'} \star h_{R'R_x}) \star h_{R_x H'} && \text{by commutativity of } K'C'CH'R_xR' \end{align*} $$

By (1) and the monicity of $h_{R_x H'}$, we deduce:

$$h_{K'C'} \star h_{C'K} \star h_{KR_x} = h_{K'R'} \star h_{R'R_x} \qquad (2)$$

Thus, the commutative diagram depicted below holds:

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

By (2) and the universal mapping property of the pushout $\square K'C'XR'$, there exists a unique morphism $h_{XR_x}$ such that

$$h_{C'X} \star h_{XR_x} = h_{C'K} \star h_{KR_x} \qquad (3)$$

$$h_{R'X} \star h_{XR_x} = h_{R'R_x} \qquad (4)$$

Subsequently, we have

$$h_{C'X} \star (h_{XR_x} \star h_{R_x H'}) = h_{C'C} \star h_{CH'} \qquad (5)$$

$$h_{R'X} \star (h_{XR_x} \star h_{R_x H'}) = h_{R'R_x} \star h_{R_x H'} \qquad (6)$$
because

$$
\begin{align*}
& h_{C'X} \star (h_{XR_x} \star h_{R_x H'}) && \text{by associativity} \\
& = (h_{C'X} \star h_{XR_x}) \star h_{R_x H'} && \text{by (3)} \\
& = (h_{C'K} \star h_{KR_x}) \star h_{R_x H'} && \text{by associativity} \\
& = h_{C'K} \star (h_{KR_x} \star h_{R_x H'}) && \text{by commutativity of } \Box KCH'R_x \\
& = (h_{C'K} \star h_{KC}) \star h_{CH'} && \text{by associativity} \\
& = h_{C'C} \star h_{CH'} && \text{by (0)}
\end{align*}
$$

and

$$
\begin{align*}
& h_{R'X} \star (h_{XR_x} \star h_{R_x H'}) && \text{by associativity} \\
& = (h_{R'X} \star h_{XR_x}) \star h_{R_x H'} && \text{by (4)} \\
& = h_{R'R_x} \star h_{R_x H'} && \text{by (4)}
\end{align*}
$$

Furthermore, by assumption, we have

$$
h_{C'X} \star h_{XH'} = h_{C'C} \star h_{CH'} \quad (7)
$$

$$
h_{R'X} \star h_{XH'} = h_{R'R_x} \star h_{R_x H'} \quad (8)
$$

By the universal mapping property of the pushout square □K'C'XR', there
exists a unique morphism ι : X → H' such that

$h_{C'X} \star \iota = h_{C'C} \star h_{CH'}$

$h_{R'X} \star \iota = h_{R'R_x} \star h_{R_x H'}$

Consequently, we confirm $h_{XH'} = h_{XR_x} \star h_{R_x H'}$.

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

**Lemma 49.** Consider the commutative diagram depicted below, where □KCH'Rₓ is a pushout square:

<figure><img src="image_40.png" /></figure>
If $h_{XH'} \in \Psi_{\neg R_x, \neg C}^-$, then there exist arrows $c' \in C'$ and $r' \in R'$ such that

$$ 
\begin{aligned}
h_{C'C}(c') & \notin \mathrm{Im}(h_{KC}), \\
h_{R'R_x}(r') & \notin \mathrm{Im}(h_{KR_x}).
\end{aligned}
 $$

*Proof.* Suppose $h_{XH'} \in \Psi_{\neg R_x, \neg C}$. By symmetry, it suffices to construct an arrow $c' \in C'$ such that $h_{C'C}(c') \notin \mathrm{Im}(h_{KC})$.

By Lemma 48, we have $\mathrm{Im}(h_{C'C}) \setminus \mathrm{Im}(h_{KC}) \neq \emptyset$.

Let $c \in \mathrm{Im}(h_{C'C}) \setminus \mathrm{Im}(h_{KC})$. There exists $c' \in C'$ such that:

$$ h_{C'C}(c') = c \qquad (-1) $$

Suppose $c$ is an arrow. It follows that $c'$ is also an arrow, as $h_{C'C}$ is a graph homomorphism. Thus, the lemma is proven.

Suppose $c$ is a node. It follows that $c'$ is also a node, as $h_{C'C}$ is a graph homomorphism.

*Claim.* $c' \notin \mathrm{Im}(h_{K'C'})$

- Suppose, by contradiction, that $c' \in \mathrm{Im}(h_{K'C'})$. It follows that there exists $k' \in K'$ such that:

$$ h_{K'C'}(k') = c' \qquad (0) $$

We therefore have:

$$ h_{CH'}(c) = h_{R_x H'}((h_{K'R'} \star h_{R'R_x})(k')) \qquad (1) $$

because

$$ =h_{CH'}(h_{C'C}(c')) \qquad \text{by (1)} $$

$$ =h_{CH'}(h_{C'C}(h_{K'C'}(k')))) \qquad \text{by (0)} $$

$$ =(h_{K'C'} \star h_{C'C} \star h_{CH'})(k') \qquad \text{by definition of composition} $$

$$ =(h_{K'R'} \star h_{R'R_x} \star h_{R_x H'})(k') \qquad \text{by commutativity of } K'C'CH'R_xR' $$

$$ =h_{R_x H'}((h_{K'R'} \star h_{R'R_x})(k')) \qquad \text{by definition of composition} $$

By (1) and Lemma 47, there exists $k \in K$ such that the equations $h_{KC}(k) = c$. Therefore, we have $c = h_{KC}(k) \in \mathrm{Im}(h_{KC})$, which contradicts $c \in \mathrm{Im}(h_{C'C}) \setminus \mathrm{Im}(h_{KC})$.

*Claim.* $\mathrm{Im}(h_{K'C'}) \neq \emptyset$

- Suppose, by contradiction, that $\mathrm{Im}(h_{K'C'}) = \emptyset$. We have $K' = \emptyset$. Since $X$ is connected and $\Box K'C'XR'$ is a pushout square, we have $C' = \emptyset$ or $R' = \emptyset$; otherwise, $X$ could not be connected. By symmetry, we suppose $C' = \emptyset$.
Consequently, the monomorphism $h_{R'X}$ is also an isomorphism. Let $h_{XR'} : X \to R'$ be an inverse to $h_{R'X}$. We have:

$$ 
\begin{align*}
& h_{XH'} \\
&= \mathrm{id}_X \star h_{XH'} \\
&= (h_{XR'} \star h_{R'X}) \star h_{XH'} && \text{because } \mathrm{id}_X = h_{XR'} \star h_{R'X} \\
&= h_{XR'} \star (h_{R'X} \star h_{XH'}) && \text{by commutativity of } R'XH'R_x \\
&= h_{XR'} \star (h_{R'R_x} \star h_{R_xH'}) && \text{by associativity} \\
&= (h_{XR'} \star h_{R'R_x}) \star h_{R_xH'}
\end{align*}
$$

which is a contradiction because, by assumption $h_{XH'} \in \Psi_{\neg R_x, \neg C}$, no morphism $h: X \to R_x$ such that $h \star h_{XH'} = h \star h_{R_x H'}$.

*Claim.* For all node $c'' \in \mathrm{Im}(h_{K'C'})$, for all node $c \in C' \setminus \mathrm{Im}(h_{K'C'})$, there exists a path $c' \stackrel{e_1}{\leftarrow} \dots \stackrel{e_n}{\leftarrow} c''$ with $n \ge 1$.

Let $c''$ be a node of $\mathrm{Im}(h_{K'C'})$. By the claim above, there is a path $h_{C'C}(c') \stackrel{h_{C'C}(e_1)}{\leftarrow}$ $\dots \stackrel{h_{C'C}(e_n)}{\leftarrow}$ $h_{C'C}(c'')$ in $C$, since $h_{C'C}$ is a graph homomorphism. We have $h_{C'C}(e_1) \notin \mathrm{Im}(h_{KC})$ because $h_{C'C}(c') = c \notin \mathrm{Im}(h_{KC})$.

□

**Lemma 50.** Consider the commutative diagram, depicted below, where $h_{XH'} \in \Psi_{\neg R_x, \neg C}$:

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

If there are arrows $c' \in C'$ and $r' \in R'$ such that $h_{C'C}(c') \notin h_{KC}(K)$ and $h_{R'R_x}(r') \notin h_{KR_x}(K)$ then

$$ h_{XH'} \star h_{H'G} \in \Psi_{\neg L, \neg C} $$

*Proof.* Suppose there are arrows $c' \in C'$ and $r' \in R'$ such that

$$ h_{R'R_x}(r') \notin \mathrm{Im}(h_{KR_x}) \quad (-1) $$

$$ h_{C'C}(c') \notin \mathrm{Im}(h_{KC}) \quad (0) $$
From (-1) and the assumption on $h_{R_x L}$ (i.e. for all $a \in R_x$, we have $h_{R_x L}(a) \in \mathrm{Im}(h_{KL})$ if and only if $a \in \mathrm{Im}(h_{KR_x})$), we have

$$ (h_{R'R_x} \star h_{R_x L})(r') \notin \mathrm{Im}(h_{KL}) \quad (1) $$

We will show that there is neither a morphism $h_{XC} : X \to C$ such that $h_{XH'} \star h_{H'G} = h_{XC} \star h_{CG}$ nor a morphism $h_{XL} : X \to L$ such that $h_{XH'} \star h_{H'G} = h_{XL} \star h_{LG}$.

Suppose that there exists a morphism $h_{XC} : X \to C$ such that

$$ h_{XH'} \star h_{H'G} = h_{XC} \star h_{CG} \quad (2) $$

We have the commutative diagram depicted below:

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

We have

$$
\begin{align*}
& h_{LG}((h_{R'R_x} \star h_{R_x L})(r')) \\
&= (h_{R'R_x} \star h_{R_x L} \star h_{LG})(r') && \text{by associativity} \\
&= (h_{R'R_x} \star (h_{R_x L} \star h_{LG}))(r') && \text{by commutativity of } \square R_x H'GL \\
&= (h_{R'R_x} \star (h_{R_x H'} \star h_{H'G}))(r') && \text{by associativity} \\
&= ((h_{R'R_x} \star h_{R_x H'}) \star h_{H'G})(r') && \text{by commutativity of } \square R'XH'R_x \\
&= ((h_{R'X} \star h_{XH'}) \star h_{H'G})(r') && \text{by associativity} \\
&= (h_{R'X} \star (h_{XH'} \star h_{H'G}))(r') && \text{by (2)} \\
&= (h_{R'X} \star h_{XC} \star h_{CG})(r') && \text{by associativity} \\
&= h_{CG}((h_{R'X} \star h_{XC})(r'))
\end{align*}
$$

which is a contradiction, by Lemma 47 and (1).

Suppose that there exists a graph homomorphism $h_{XL}$ such that

$$ h_{XH'} \star h_{H'G} = h_{XL} \star h_{LG} \quad (3) $$

We have the commutative diagram depicted below:
<figure><img src="image_43.png" /></figure>

Therefore,

$$
\begin{align*}
h_{CG}(h_{C'C}(c')) &= (h_{C'C} \star h_{CG})(c') \\
&= (h_{C'C} \star (h_{CH'} \star h_{H'G}))(c') && \text{by commutativity of } \trianglelefteqno{\Delta CGH'} \\
&= ((h_{C'C} \star h_{CH'}) \star h_{H'G})(c') && \text{by associativity} \\
&= ((h_{C'X} \star h_{XH'}) \star h_{H'G})(c') && \text{by commutativity of } \squareno{\trianglelefteqno{\square C'CH'X}} \\
&= (h_{C'X} \star (h_{XH'} \star h_{H'G}))(c') && \text{by associativity} \\
&= (h_{C'X} \star (h_{XL} \star h_{LG}))(c') && \text{by (3)} \\
&= (h_{C'X} \star h_{XL} \star h_{LG})(c') && \text{by associativity} \\
&= h_{LG}((h_{C'X} \star h_{XL})(c'))
\end{align*}
$$

which is a contradiction, by Lemma 47 and (0). □

**Lemma 51.** Let $h_{H'G}$ be the unique homomorphism such that $h_{CH'} \star h_{H'G} = h_{CG}$ and $h_{R_x H'} \star h_{H'G} = h_{R_x L} \star h_{LG}$. For all $h_{XH'} \in \Psi_{\neg R_x, \neg C}$, we have $h_{XH'} \star h_{H'G} \in \Psi_{\neg L, \neg C}$.

*Proof.* Let $h_{XH'} \in \Psi_{\neg R_x, \neg C}$. We can construct the commutative diagram depicted below:

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

where $\squareno{KCGL}$ is a pushout square.
There are arrows $c' \in C'$ and $r' \in R'$ such that $h_{C'C}(c') \notin h_{KC}(K)$ and $h_{R'R_x}(r') \notin h_{KR_x}(K)$, by Lemma 49.

Let $h_{H'G}$ be the unique homomorphism such that $h_{CH'} \star h_{H'G} = h_{CG}$ and $h_{R_x H'} \star h_{H'G} = h_{R_x L} \star h_{LG}$, assumed by the universal mapping property of the pushout square $\square KCH'R_x$.

We have $h_{XH'} \star h_{H'G} \in \Psi_{\sim L, \sim C}$ by Lemma 50.

□

**Lemma 52.** Let $h_{H'G}$ be the unique homomorphism such that $h_{CH'} \star h_{H'G} = h_{CG}$ and $h_{R_x H'} \star h_{H'G} = h_{R_x L} \star h_{LG}$.

The morphism $h_{H'G}$ is injective on arrows.

*Proof.* Suppose that $h_{R_x L}$ is injective on arrows. If $H'$ has at most one arrow, then $h_{H'G}$ is injective on arrows. Suppose that $H'$ has at least two distinct arrows. Let $h_1, h_2 \in H'$ be two distinct arrows. Since $\square KCH'R_x$ is a pushout square, there are three cases. We will show that in each case, the inequality $h_{H'G}(h_1) \neq h_{H'G}(h_2)$ holds.

(1) Suppose that there are $c_1, c_2 \in C$ such that $h_{CH'}(c_1) = h_1$ and $h_{CH'}(c_2) = h_2$.

We have $c_1 \neq c_2$ since $h_1 \neq h_2$ and $h_{CH'}$ is a function.

By the monicity of $h_{CG}$, there are $g_1, g_2 \in G$ such that $g_1 \neq g_2$, $h_{CG}(c_1) = g_1$, and $h_{CG}(c_2) = g_2$. Therefore we have

$$
\begin{align*}
h_{H'G}(h_1) &= h_{H'G}(h_{CH'}(c_1)) & \text{by definition of } h_1 \\
&= (h_{CH'} \star h_{H'G})(c_1) & \\
&= h_{CG}(c_1) & \text{by commutativity of } \triangle CGH' \\
&\neq h_{CG}(c_2) & \text{by monicity of } h_{CG} \text{ and } c_1 \neq c_2 \\
&= (h_{CH'} \star h_{H'G})(c_2) & \text{by commutativity of } \triangle CGH' \\
&= h_{H'G}(h_{CH'}(c_2)) & \\
&= h_{H'G}(h_2) & \text{by definition of } h_2
\end{align*}
$$

(2) Suppose that there are $r_1, r_2 \in R_x$ such that $h_{R_x H'}(r_1) = h_1$ and $h_{R_x H'}(r_2) = h_2$.

We have $r_1 \neq r_2$ because $h_1 \neq h_2$ and $h_{R_x H'}$ is a.

The morphism $h_{R_x L} \star h_{LG}$ is injective on arrows as composition of morphisms $h_{R_x L}$ and $h_{LG}$, which are injective on arrows by assumption. There are arrows $g_1, g_2 \in G$ such that $g_1 \neq g_2$ and $(h_{R_x L} \star h_{LG})(r_1) = g_1$ and $(h_{R_x L} \star h_{LG})(r_2) = g_2$, because $h_{R_x L} \star h_{LG}$ is a graph homomorphism. Therefore,

$$
\begin{align*}
h_{H'G}(h_1) &= h_{H'G}(h_{R_x H'}(r_1)) & \text{by definition of } h_1 \\
&= (h_{R_x H'} \star h_{H'G})(r_1) & \\
&= (h_{R_x L} \star h_{LG})(r_1) & \text{by commutativity of } \square R_x H'GL \\
&\neq (h_{R_x L} \star h_{LG})(r_2) & \text{because } h_{R_x L} \star h_{LG} \text{ is injective on arrows and } r_1 \neq r_2 \\
&= (h_{R_x H'} \star h_{H'G})(r_2) & \text{by commutativity of } \square R_x H'GL \\
&= h_{H'G}(h_{R_x H'}(r_2)) & \\
&= h_{H'G}(h_2) & \text{by definition of } h_2
\end{align*}
$$
(3) Otherwise, there are arrows $r \in R_x$ and $c \in C$ such that $h_{CH'}(c) = h_1$ and $h_{R_x H'}(r) = h_2$. We have three cases:

(3.1) If $c \notin \mathrm{Im}(h_{KC})$ then

$$
\begin{align*}
h_{H'G}(h_1) &= h_{H'G}(h_{CH'}(c)) & \text{by definition of } h_1 \\
&= (h_{CH'} \star h_{H'G})(c) & \\
&= h_{CG}(c) & \text{by commutativity of } \trianglelefteqno{\Delta CGH'} \\
&\neq h_{LG}(h_{R_x L}(r)) & \text{by Lemma 47 and } c \notin \mathrm{Im}(h_{KC}) \\
&= (h_{R_x L} \star h_{LG})(r) & \\
&= (h_{R_x H'} \star h_{H'G})(r) & \text{by commutativity of } \squareno{R_x H'GL} \\
&= h_{H'G}(h_{R_x H'}(r)) & \\
&= h_{H'G}(h_2) & \text{by definition of } h_2
\end{align*}
$$

(3.2) Suppose that $r \notin \mathrm{Im}(h_{KR_x})$. Then $h_{R_x L}(r) \notin \mathrm{Im}(h_{KL}) = \mathrm{Im}(h_{KR_x} \star h_{R_x L})$ by the commutativity of $\trianglelefteqno{\Delta KR_x L}$. Therefore,

$$
\begin{align*}
h_{H'G}(h_1) &= h_{H'G}(h_{CH'}(c)) & \text{by definition of } h_1 \\
&= (h_{CH'} \star h_{H'G})(c) & \\
&= h_{CG}(c) & \text{by commutativity of } \trianglelefteqno{\Delta CGH'} \\
&\neq h_{LG}(h_{R_x L}(r)) & \text{by Lemma 47 and } h_{R_x L}(r) \notin \mathrm{Im}(h_{KL}) \\
&= (h_{R_x L} \star h_{LG})(r) & \\
&= (h_{R_x H'} \star h_{H'G})(r) & \text{by commutativity of } \squareno{R_x H'GL} \\
&= h_{H'G}(h_{R_x H'}(r)) & \\
&= h_{H'G}(h_2) & \text{by definition of } h_2
\end{align*}
$$

(3.3) Otherwise, there are $k_1, k_2 \in K$ such that $h_{KC}(k_1) = c$ and $h_{KR_x}(k_2) = r$. We have $k_1 \neq k_2$ because if $k_1 = k_2$, then we would have a contradiction:

$$
\begin{align*}
h_1 &= h_{CH'}(c) & \text{by definition of } h_1 \\
&= h_{CH'}(h_{KC}(k_1)) & \text{by definition of } c \\
&= h_{CH'}(h_{KC}(k_2)) & \text{by } k_1 = b_2 \\
&= (h_{KC} \star h_{CH'})(k_2) & \\
&= (h_{KR_x} \star h_{R_x H'})(k_2) & \\
&= h_{R_x H'}(r) & \text{by definition of } r \\
&= h_2 & \text{by definition of } h_2
\end{align*}
$$
Therefore, we have

$$h_{H'G}(h_1) = h_{H'G}(h_{CH'}(c)) \qquad \text{by definition of } h_1$$

$$= h_{H'G}(h_{CH'}(h_{KC}(k_1))) \qquad \text{by definition of } c$$

$$= (h_{KC} \star h_{CH'} \star h_{H'G})(k_1)$$

$$= (h_{KC} \star (h_{CH'} \star h_{H'G}))(k_1) \qquad \text{by associativity}$$

$$= (h_{KC} \star h_{CG})(k_1) \qquad \text{by commutativity of } \Delta CGH'$$

$$\neq (h_{KC} \star h_{CG})(k_2) \qquad \text{by monicity of } h_{KC} \star h_{CG} \text{ and } k_1 \neq k_2$$

$$= (h_{KL} \star h_{LG})(k_2) \qquad \text{by commutativity of } \square KCGL$$

$$= (h_{KR_x} \star h_{R_x L} \star h_{LG})(k_2) \qquad \text{by commutativity of } \Delta KR_x L$$

$$= (h_{KR_x} \star (h_{R_x L} \star h_{LG}))(k_2) \qquad \text{by associativity}$$

$$= (h_{KR_x} \star (h_{R_x H'} \star h_{H'G}))(k_2) \qquad \text{by commutativity of } \square R_x H'GL$$

$$= (h_{R_x H'} \star h_{H'G})(r) \qquad \text{by definition of } r$$

$$= h_{H'G}(h_{R_x H'}(r))$$

$$= h_{H'G}(h_2) \qquad \text{by definition of } h_2$$

□

**Lemma 53.** Let $h_{H'G}$ be the unique morphism such that $h_{CH'} \star h_{H'G} = h_{CG}$ and $h_{R_x H'} \star h_{H'G} = h_{R_x L} \star h_{LG}$.

$$\text{Let } h_{XH'} \text{ and } h'_{XH'} \in \Psi_{\neg R_x, \neg C}.$$

$$\text{If } h_{XH'} \neq h'_{XH'}, \text{ then } h_{XH'} \star h_{H'G} \neq h'_{XH'} \star h_{H'G}.$$

*Proof.* Suppose $h_{XH'}$ and $h'_{XH'}$ are elements of $\Psi_{\neg R_x, \neg C}$ such that $h_{XH'} \neq h'_{XH'}$.

Since $X$ is connected with at least one arrow, we deduce there exists an arrow $e$ such that $h_{XH'}(e) \neq h'_{XH'}(e)$.

According to Lemma 52, the morphism $h_{H'G}$ is injective on arrows.

Therefore, we have:

$$(h_{XH'} \star h_{H'G})(e) = h_{H'G}(h_{XH'}(e)) \neq h_{H'G}(h'_{XH'}(e)) = (h'_{XH'} \star h_{H'G})(e).$$

**Lemma 54.** Consider the commutative diagram depicted below

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

There is a homomorphism $h_{XH'}$ satisfying $h_{XH'} \star h_{H'H} = h_{XH}$.
Proof. From the commutativity of the diagram, we have

$$h_{K'C'} \star h_{C'C} \star h_{CH'} = h_{K'R'} \star h_{R'R_x} \star h_{R_xH'}$$

Hence, by the universal mapping property of the pushout $\square K'C'XR'$, there is a unique graph homomorphism $h_{XH'}$ such that

$$h_{R'X} \star h_{XH'} = h_{R'R_x} \star h_{R_xH'} \quad (1)$$

$$h_{C'X} \star h_{XH'} = h_{C'C} \star h_{CH'}$$

Thus, the following commutative diagram holds:

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

We have

$$h_{R'X} \star (h_{XH'} \star h_{H'H}) = h_{R'R} \star h_{RH}$$

$$h_{C'X} \star (h_{XH'} \star h_{H'H}) = h_{C'C} \star h_{CH}$$

from

$$h_{R'R} \star h_{RH} = (h_{R'R_x} \star h_{R_xR}) \star h_{RH} \quad \text{by commutativity of } \triangle R'R_xR$$

$$= h_{R'R_x} \star (h_{R_xR} \star h_{RH}) \quad \text{by associativity}$$

$$= h_{R'R_x} \star (h_{R_xH'} \star h_{H'H}) \quad \text{by commutativity of } \square R_xH'H'R$$

$$= (h_{R'R_x} \star h_{R_xH'}) \star h_{H'H} \quad \text{by associativity}$$

$$= (h_{R'X} \star h_{XH'}) \star h_{H'H} \quad \text{by (1)}$$

$$= h_{R'X} \star (h_{XH'} \star h_{H'H}) \quad \text{by associativity}$$

and

$$h_{C'C} \star h_{CH} = h_{C'C} \star (h_{CH'} \star h_{H'H}) \quad \text{by commutativity of } \triangle CH'H$$

$$= (h_{C'C} \star h_{CH'}) \star h_{H'H} \quad \text{by associativity}$$

$$= (h_{C'X} \star h_{XH'}) \star h_{H'H} \quad \text{by commutativity of } \square C'CH'X$$

$$= h_{C'X} \star (h_{XH'} \star h_{H'H}) \quad \text{by associativity}$$

By the commutativity of the diagram, we have

$$h_{C'C} \star h_{CH} = h_{C'X} \star h_{XH}$$

$$h_{R'R} \star h_{RH} = h_{R'X} \star h_{XH}$$
Thus, we conclude $h_{XH} = h_{XH'} \star h_{H'H}$ because, by the universal mapping property, there is a unique morphism $h: X \to H$ such that $h_{C'C} \star h_{CH} = h_{C'X} \star h$ and $h_{R'R} \star h_{RH} = h_{R'X} \star h$.

**Lemma 55.** Consider the commutative diagram depicted below

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

If $h_{XH} \in \Psi_{\neg R, \neg C}$ then $h_{XH'} \in \Psi_{\neg R_x, \neg C}$.

*Proof.* Suppose $h_{XH} \in \Psi_{\neg R, \neg C}$.

By the definition of $\Psi_{\neg R, \neg C}$, we have

$$ \exists h_{XC}.h_{XH} = h_{XC} \star h_{CH} \qquad (1) $$

$$ \exists h_{XR}.h_{XH} = h_{XR} \star h_{RH} \qquad (2) $$

By the definition of $\Psi_{\neg R_x, \neg C}$, we need to show that there is neither $h_{XC}$ such that $h_{XC} \star h_{CH'} = h_{XH'}$ nor $h_{XR_x}$ such that $h_{XR_x} \star h_{R_x H'} = h_{XH'}$.

*Claim.* There is no $h_{XC}: X \to C$ such that $h_{XC} \star h_{CH'} = h_{XH'}$.

- Suppose, by contradiction, that there is a morphism $h_{XC}$ satisfying

$$ h_{XC} \star h_{CH'} = h_{XH'} \qquad (3) $$

Under this assumption, we have:

$$ \begin{align*} h_{XC} \star h_{CH} &= h_{XC} \star (h_{CH'} \star h_{H'H}) && \text{by commutativity of } \Delta CHH' \\ &= (h_{XC} \star h_{CH'}) \star h_{H'H} && \text{by associativity} \\ &= h_{XH'} \star h_{H'H} && \text{by (3)} \\ &= h_{XH} && \text{by commutativity of } \Delta XHH' \end{align*} $$

which contradicts (1).

*Claim.* There is no $h_{XR_x}$ such that $h_{XR_x} \star h_{R_x H'} = h_{XH'}$.

- Suppose, by contradiction, that there is $h_{XR_x}$ such that

$$ h_{XR_x} \star h_{R_x H'} = h_{XH'} \qquad (4) $$
Let $h_{XR} \stackrel{\text{def}}{=} h_{XR_x} \star h_{R_x R}$. Under this assumption, we have:

$$
\begin{align*}
h_{XR} \star h_{RH} &= (h_{XR_x} \star h_{R_x R}) \star h_{RH} && \text{by definition of } h_{XR} \\
&= h_{XR_x} \star (h_{R_x R} \star h_{RH}) && \text{by associativity} \\
&= h_{XR_x} \star (h_{R_x H'} \star h_{H' H}) && \text{by commutativity of } \square R_x H' H R \\
&= (h_{XR_x} \star h_{R_x H'}) \star h_{H' H} && \text{by associativity} \\
&= h_{X H'} \star h_{H' H} && \text{by (4)} \\
&= h_{X H} && \text{by commutativity of } \triangle X H H'
\end{align*}
$$

which contradicts (2).

**Lemma 56.** Let $h_{H'H}$ be the unique homomorphism such that $h_{CH'} \star h_{H'H} = h_{CH}$ and $h_{R_x H'} \star h_{H'H} = h_{R_x R} \star h_{RH}$.

$$
\text{Let } h_{XH} \in \Psi_{\neg R, \neg C}.
$$

There exists a homomorphism $h_{XH'}$ such that $h_{XH} = h_{XH'} \star h_{H'H}$ and $h_{XH'} \in \Psi_{\neg R_x, \neg C}$.

*Proof.* Under the assumption of the lemma, the following commutative diagram
holds

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

where $\square KCHR$, $\square C'CHX$, $\square R'XHR$, and $\square KCH'R_x$ are pushout squares.

By Proposition 46, the pushout square □KCHR is also a pullback square.
Consequently, there exists a morphism from K' to K, making the following
commutative diagram hold:

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

where $\square KCHR$, $\square C'CHX$, $\square R'XHR$, and $\square KCH'R_x$ are pushout squares.
*Claim.* There is a homomorphism $h_{R'R_x} : R' \to R_x$ such that $h_{R'R_x} \star h_{R_x R} = h_{R'R}$.

- We show first that $h_{R'X}$ is not an isomorphism. Suppose, by contradiction, that $h_{R'X}$ is an isomorphism with an inverse $h_{R'X}^{-1}$. We have

$$ 
\begin{align*}
h_{XH} &= (h_{R'X}^{-1} \star h_{R'X}) \star h_{XH} \\
&= h_{R'X}^{-1} \star (h_{R'X} \star h_{XH}) && \text{by associativity} \\
&= h_{R'X}^{-1} \star (h_{R'R} \star h_{RH}) && \text{by commutativity of } \square R'XHR \\
&= (h_{R'X}^{-1} \star h_{R'R}) \star h_{RH} && \text{by associativity}
\end{align*}
$$

which contradicts the assumption $h_{XH} \in \Psi_{\neg R, \neg C}$.

Thus, by Definition 29, if follows that $\mathrm{Im}(h_{R'R}) \subseteq R_x$. Consequently, we can define a morphism $h_{R'R_x} : R' \to R_x$ by letting $h_{R'R_x}(r') \stackrel{\mathrm{def}}{=} h_{R'R}(r')$ for all $r' \in R'$. We have $h_{R'R_x} \star h_{R_x R} = h_{R'R}$ because for all $r \in R'$, we have $h_{R'R_x}(r') = h_{R'R}(r')$, and $h_{R_x R}$ is the canonical inclusion mapping.

By Lemma 54, there is a homomorphism $h_{XH'}$ such that $h_{XH'} \star h_{H'H} = h_{XH}$. Thus, the following commutative diagram holds:

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

We conclude that $h_{XH'} \in \Psi_{\neg R_x, \neg C}$ by Lemma 55.

**Lemma 57.** Let $h_{H'H}$ be the unique morphism such that $h_{CH'} \star h_{H'H} = h_{CH}$ and $h_{R_x H'} \star h_{H'H} = h_{R_x R} \star h_{RH}$.

Let $h_{XH}, h'_{XH} \in \Psi_{\neg R, \neg C}$ such that $h_{XH} \neq h'_{XH}$.

Then there exist morphisms $h_{XH'}$ and $h'_{XH'}$ such that:

- $h_{XH} = h_{XH'} \star h_{H'H}$

- $h'_{XH} = h'_{XH'} \star h_{H'H}$

- $h_{XH'} \in \Psi_{\neg R_x, \neg C}$

- $h'_{XH'} \in \Psi_{\neg R_x, \neg C}$

- $h_{XH'} \neq h'_{XH'}$

*Proof.* By Lemma 56, there exist homomorphisms $h_{XH'}$ and $h'_{XH'}$ such that:

- $h_{XH} = h_{XH'} \star h_{H'H}$

- $h'_{XH} = h'_{XH'} \star h_{H'H}$
$$-h_{XH'} \in \Psi_{\neg R_x, \neg C}$$

$$-h'_{XH'} \in \Psi_{\neg R_x, \neg C}$$

Since $h_{XH} \neq h'_{XH}$ and both factor through $h_{H'H}$, it follows that $h_{XH'} \neq h'_{XH'}$. Hence, the homomorphisms $h_{XH'}$ and $h'_{XH'}$ satisfy all the conditions.