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

HAL
open science

# Termination of Injective DPO Graph Rewriting Systems using Subgraph Counting

Qi Qiu

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

## To cite this version:

Qi Qiu. Termination of Injective DPO Graph Rewriting Systems using Subgraph Counting. 18th International Conference on Graph Transformation (ICGT 2025), Jun 2025, Koblenz, Germany. 10.1007/978-3-031-94706-3_1. hal-04955684

HAL Id: hal-04955684

https://hal.science/hal-04955684v1

Submitted on 19 Feb 2025

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Termination of Injective DPO Graph Rewriting Systems using Subgraph Counting

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 present a machine-checkable sufficient condition for relative termination of double-pushout graph rewriting systems with injective rules on edge-labeled multigraphs. Our method defines a graph's weight as the sum of weights of occurrences of a set of graphs within it. By ensuring (1) every rewriting step using rules in a set A of rules strictly decreases the host graph's weight, and (2) every rewriting step using rules in a set B of rules never increases it, we guarantee that rules in the set A can be applied only finitely many times in any rewriting sequence with rules in the union of A and B. Our method resolves termination cases that prior interpretation-based methods cannot. We also propose an implementation of our technique <fnref n="1" />.

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

## 1 Introduction

Distributed systems play a crucial role in improving performance, scalability, and efficiency in modern computing[Hei+10]. Ensuring their correctness is vital but challenging due to the inherent complexity of these systems [LSP82].

While interactive theorem proving [HUW14; Mar15] offers a promising approach to formally verifying properties of distributed systems [Har11; Pot+19; Cou+16], it requires proficiency in proof assistants, making the process both demanding and time-consuming. Automatic methods that generate certificates verifiable by proof assistants provide a practical alternative [CTC24; Con+03].

In this paper, we present a machine-checkable sufficient condition for relative termination [Ges90] of double-pushout (DPO) graph rewriting systems with injective rules [EPS73; Cor+97]. DPO graph rewriting provides an intuitive yet formal framework for modeling distributed systems, enabling rigorous analysis and automated verification of their properties. Relative termination ensures that, given two rule sets $\mathcal{A}$ and $\mathcal{B}$, rules in $\mathcal{A}$ can only be applied finitely many times in any sequence of rule applications from $\mathcal{A} \cup \mathcal{B}$.

Our method works as follows. Let $\mathcal{X}$ denote a set of graphs. We assign weights (natural numbers) to occurrences of graphs in $\mathcal{X}$, and the weight of a graph $G$

<footnote n="1">¹ The source code is available at https://anonymous.4open.science/r/icgt25-32AE</footnote>
is defined as the sum of the weights of all occurrences of graphs in $\mathcal{X}$ within $G$. Let $\mathcal{A}$ and $\mathcal{B}$ be sets of injective DPO rewriting rules. Our technique requires that, for every graph $X$ in $\mathcal{X}$, and for every rewriting step $G \Rightarrow H$ using a rule from $\mathcal{A}$ or $\mathcal{B}$, there exists an injective mapping from the set of occurrences of $X$ (those neither fully contained in $R$ nor fully contained in the context) in the result graph $H$ to the set of such occurrences in the host graph $G$. Suppose the following conditions hold: (i) For every rule in $\mathcal{A}$, the left-hand-side graph's weight is strictly greater than the right-hand-side graph's weight; (ii) For every rule in $\mathcal{B}$, the left-hand-side graph's weight is greater than or equal to the right-hand-side graph's weight. Under these conditions, rewriting steps using rules in $\mathcal{A}$ strictly decrease the weights of the host graphs, while rewriting steps using rules in $\mathcal{B}$ do not increase them. Consequently, the rewriting rules in $\mathcal{A}$ can only be applied finitely many times: since the weight of a finite graph is a natural number and strictly decreases with each rewriting step using a rule in $\mathcal{A}$, the process must terminate after finitely many iterations.

Our method proves termination for systems such as the one described in Example 47, whereas prior interpretation-based approaches presented in [ZKB14; BKZ14; Bru+15; EO24; OE24] cannot. Additionally, we provide an implementation of our technique<fnref n="2" />.

The remainder of this paper is organized as follows. § 2 recalls some essential preliminary definitions. § 3 presents a sufficient condition for termination of DPO graph rewriting systems with injective rules and injective matches. § 4 extends the technique to systems with non-injective matches. § 5 illustrates the method with some examples. § 6 compares our approach with some existing methods. Finally, § 7 concludes with remarks and future research directions. The missing proofs and definitions can be found in the appendix.

## 2 Preliminaries

We recall some definitions related to the double-pushout approach to edge-labeled directed multigraphs rewriting and relative termination. For more detailed information, we refer the reader to [Kön+18; Ehr+97] for the double-pushout approach to edge-labeled multigraphs rewriting, [Pie91; BW90] for category theory concepts, and [Ges90] for relative termination.

### 2.1 Graphs

**Definition 1 (Unlabeled graph [BW90]).** An unlabeled graph $G$ consists of a collection of nodes (also called objects) and a collection of edges equipped with a source (or domain) node and a target (or codomain) node.

For an unlabeled graph $G$, we denote by $G_0$ its collection of nodes, $G_1$ its collection of edges, $\text{dom}: G_1 \to G_0$ the domain function, and $\text{cod}: G_1 \to G_0$ the codomain function. An unlabeled graph is **finite** if $G_0$ and $G_1$ are both finite sets. By $a: s \to t$, we denote the edge $a$ from $s$ to $t$.

<footnote n="2">² The source code is available at https://anonymous.4open.science/r/icgt25-32AE</footnote>
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 graphs).** Let $G$ and $H$ be unlabeled graphs. A homomorphism of unlabeled graphs $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 edge $a$ from $s$ to $t$ in $G$, the image $h_1(a)$ is an edge from $h_0(s)$ to $h_0(t)$ in $H$.

**Definition 3 (Labeled graph [Kön+18]).** Let $\Sigma$ be a finite set of labels. A labeled graph is an ordered pair $(G, \lambda)$ where $G$ is an unlabeled graph and $\lambda: G_1 \to \Sigma$ is an edge-labeling function. It is called finite if its underlying unlabeled graph is finite.

By $a: s \stackrel{l}{\to} t$, we denote the arrow $a$ labeled by $l$ from $s$ to $t$. Unless otherwise specified, the term 'graph' will refer to labeled graphs. A homomorphism of labeled graphs is a homomorphism of unlabeled graphs that preserves the labels assigned to the edges.

**Definition 4 (Homomorphism of labeled graphs [Kön+18]).** Let $(G, \lambda)$ and $(H, \lambda')$ be labeled graphs. A homomorphism of labeled graphs $h: (G, \lambda) \to (H, \lambda')$ is a homomorphism of unlabeled graphs such that for each edge $a$ in $G$, we have $\lambda = \lambda' \circ h_1$.

## 2.2 Pushout

**Definition 5 (Category [Pie91; BW90]).** A category is an unlabeled graph $C$ together with a total function $u: C_0 \to C_1$ and a partial function $\star: C_1 \times C_1 \to C_1$ such that (i) for all edges $f: X \to Y$ and $g: Y \to Z$, the edge $f \star g: X \to Z$ is defined; (ii) for every node $X$, $u(X)$ is an edge from $X$ to $X$; (iii) for every $f: X \to Y$, we have $u(X) \star f = f = f \star u(Y)$; (iv) for all edges $f$, $g$ and $h$, we have $(f \star g) \star h = f \star (g \star h)$ whenever either side is defined. Edges are called **morphisms**. The function $\star$ is called **composition**. For all $X \in C_0$, the edge $u(X)$ is denoted $\text{id}_X$ and is called the **identity** of the object $X$.

**Notation 6** The composition of morphisms $f: X \to Y$ and $g: Y \to Z$ is written in diagrammatic order as $f \star g$, rather than in functional order $g \circ f$.

**Definition 7 (Monomorphism [Pie91; BW90]).** A morphism $f: X \to Y$ is **monic** (or a **monomorphism**) if for all morphisms $g$ and $h$, if $g \star f = h \star f$, then $g = h$. A monomorphism is denoted by $f: X \to Y$.

*Example 8.* Labeled graphs and their homomorphisms form a category, referred to as **Graph**. Its objects are labeled graphs, its morphisms are graph homomorphisms, and the monomorphisms are injective homomorphisms.

**Definition 9 (Span [Löw10]).** A pair $(\alpha: A \to B, \beta: A \to C)$ of morphisms with a common domain is called a **span**, denoted by $B \stackrel{\alpha}{\rightleftharpoons} A \to C$.
**Definition 10 (Cospan).** A pair $(\beta' : B \to D, \alpha' : C \to D)$ of morphisms with a common codomain is called a **cospan**, denoted by $B \xrightarrow{\beta'} D \stackrel{\alpha'}{\hookrightarrow} C$.

**Definition 11 (Diagram [BW90]).** Let $G$ be an unlabeled graph. A **diagram** (in $C$ of shape $G$) is a homomorphism of unlabeled graphs $h : G \to C$ where $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 \cdots \star h(s_{n-1}) = h(t_1) \star h(t_2) \star \cdots \star h(t_{m-1})$ holds.

**Definition 12 (Pushout [BW90]).**

A **pushout** of a span $B \stackrel{\alpha}{\hookrightarrow} A \xrightarrow{\beta} C$, as shown on the right, is defined as a cospan $B \xrightarrow{\beta'} D \stackrel{\alpha'}{\hookrightarrow} C$ such that $\alpha \star \beta' = \beta \star \alpha'$, and for every cospan $B \xrightarrow{\gamma'} E \stackrel{\gamma}{\hookrightarrow} 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 of the pushout**.

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

**Definition 13 (Pullback [Pie91]).**

A **pullback** of a cospan $B \xrightarrow{\beta'} D \stackrel{\alpha'}{\hookrightarrow} C$, as shown on the right, is defined as a span $B \stackrel{\alpha}{\hookrightarrow} A \xrightarrow{\beta} C$ such that $\alpha \star \beta' = \beta \star \alpha'$, and for every span $B \xrightarrow{\gamma'} 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 of the pullback**.

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

**Notation 14** When the context makes it clear, a morphism $h : A \to B$ will be denoted by $h_{AB}$, and diagrams will be referred to by their nodes, as is standard in geometry. For example, the diagram involving morphisms $\alpha, \beta, \alpha'$, $\beta'$ in Definition 12 will be denoted by $ACDB$ or $ABDC$.

*Remark 15.* We work within the category **Graph**. The terms homomorphism and morphism will be used interchangeably; the same applies to monic and injective, and to injective homomorphism and monomorphism.
## 2.3 DPO Rewriting

**Definition 16 (DPO rewriting rule [Ehr+97]).** A DPO rewriting rule $\rho$ is a span $L \stackrel{l}{\leftarrow} K \xrightarrow{r} R$, where $K$ is the *interface*, $L$ is the *left-hand-side graph*, denoted `lhs($\rho$)`, and $R$ is the *right-hand-side graph*, denoted `rhs($\rho$)`. The rule is *left-monic* if the morphism $l$ is monic, *right-monic* if the morphism $r$ is monic, *monic* if it is left- and right-monic. A match of the rule in an graph $G$ is a morphism $m: L \to G$.

**Definition 17 (DPO Rewriting step [EO24]).**

A DPO diagram $\delta$ is a diagram as shown on the right. This diagram $\delta$ is a witness for the *rewriting step* from $G$ to $H$ using the rule $\rho$ and match $m$, denoted $G \Rightarrow_{\rho}^{m} H$ or $G \Rightarrow_{\rho}^{\Delta} H$. We denote left($\Delta$) and right($\Delta$) the pushout squares KLGC and KRHC, respectively.

$$ \begin{array}{ccc} L & \stackrel{l}{\leftarrow} & K \xrightarrow{r} R \\ m \downarrow & \searrow & PO \downarrow \\ G & \stackrel{l'}{\leftarrow} & C \xrightarrow{r'} H \end{array} $$

**Definition 18 (DPO rewriting framework [EO24]).** A DPO rewriting framework $\mathfrak{F}$ is a mapping of DPO rewriting rules to classes of DPO diagrams such that, for every rule $\rho$, $\mathfrak{F}(\rho)$ is a class of DPO diagrams with top-span $\rho$.

The DPO rewriting relation $\Rightarrow_{\rho, \mathfrak{F}}$ induced by a DPO rewriting rule $\rho$ in $\mathfrak{F}$ is defined as follows: $G \Rightarrow_{\rho, \mathfrak{F}} H$ iff $G \Rightarrow_{\rho}^{\Delta} H$ for some $\Delta \in \mathfrak{F}(\rho)$. The DPO rewriting relation $\Rightarrow_{\mathcal{R}, \mathfrak{F}}$ induced by a set $\mathcal{R}$ of DPO rewriting rules in $\mathfrak{F}$ is given by: $G \Rightarrow_{\mathcal{R}, \mathfrak{F}} H$ iff $G \Rightarrow_{\rho, \mathfrak{F}} H$ for some $\rho \in \mathcal{R}$. When $\mathfrak{F}$ is clear from the context, we suppress $\mathfrak{F}$ and write $\Rightarrow_{\rho}$ and $\Rightarrow_{\mathcal{R}}$.

Let $\mathfrak{F}$ denote the DPO rewriting framework that associates any rule with the class of all DPO diagrams with the rule as the top span. Similarly, let $\mathfrak{M}$ denote the DPO rewriting framework that associates any rule with the class of all DPO diagrams having monic matches and the rule as the top span.

## 2.4 Relative Termination

**Definition 19 (Rewriting sequence).** Let $\mathcal{R}$ be a set of DPO rewriting rules and $\mathfrak{F}$ a DPO rewriting framework. A $(\mathcal{R}, \mathfrak{F})$-rewriting sequence is a finite sequence $s_0, s_1, \dots, s_m$ of objects such that $s_n \Rightarrow_{\mathcal{R}, \mathfrak{F}} s_{n+1}$ for each $0 \le n \le m-1$, or an infinite sequence $s_0, s_1, \dots$ of objects such that $s_n \Rightarrow_{\mathcal{R}, \mathfrak{F}} s_{n+1}$ for each $n \in \mathbb{N}$.

**Definition 20 (Relative termination [Klo87; Ges90]).** Let $\mathcal{A}$ and $\mathcal{B}$ be sets of rewriting rules. Let $\mathfrak{F}$ be a DPO rewriting framework. We say that $\Rightarrow_{\mathcal{A}, \mathfrak{F}}$ is *terminating relative to* $\Rightarrow_{\mathcal{B}, \mathfrak{F}}$ if any infinite $(\mathcal{A} \cup \mathcal{B}, \mathfrak{F})$-rewriting sequence has only a finite number of rewriting steps with rules in $\mathcal{A}$.

# 3 A Termination Criterion

We present a method for termination analysis of DPO graph rewriting systems with injective rules and injective matches. Building on the interpretation method
framework [BN98], we first define the weight of a graph in § 3.1. Using this definition, we outline the general approach and identify the key challenge in § 3.2, and introduce the concept of non-increasing rules in § 3.3. A solution to the challenge is then proposed in § 3.4, culminating in our termination criterion in § 3.5.

## 3.1 Measuring graphs with ruler-Graphs

Analogous to measuring physical objects with rulers, we measure graphs using ruler-graphs—special graphs that act as reference structures. A ruler-graph measures a graph $G$, and provides a measurement of $G$ relative to that ruler-graph. To aggregate measurements across multiple ruler-graphs, we assign weights to their measurements via weight functions. The weight of a graph is defined as the sum of the weighted measurements obtained from all ruler-graphs.

**Definition 21 (Ruler-graph).** A *ruler-graph* is a graph.

**Definition 22 (Measurement).** Let $X$ be a ruler-graph and $G$ a graph. The *measurement of* $G$ with respect to $X$, denoted $m_X(G)$, is $m_X(G) = |\text{Mono}(X, G)|$.

**Definition 23 (Weight function).** A *weight function* for a set of ruler-graphs $\mathcal{X}$ is a map $s_{\mathcal{X}}: \mathcal{X} \to \mathbb{N}$ assigning a weight in $\mathbb{N}$ to each ruler-graph.

**Definition 24 (Graph weight).** Let $\mathcal{X}$ be a set of ruler-graphs, $s_{\mathcal{X}}$ a weight function, and $G$ a graph. The *weight of graph* $G$ relative to $s_{\mathcal{X}}$, denoted $w_{s_{\mathcal{X}}}(G)$ (or simply $w(G)$ when $s_{\mathcal{X}}$ is clear from context), is defined as:

$$w_{s_{\mathcal{X}}}(G) = \sum_{X \in \mathcal{X}} s_{\mathcal{X}}(X) \cdot m_X(G).$$

*Remark 25.* This work focuses on deriving sufficient conditions for termination, deferring the construction of ruler-graphs to future work.

## 3.2 General idea and key challenge

For the remainder of this section, we assume: a set $\mathcal{R} = \mathcal{A} \cup \mathcal{B}$ of injective DPO rewriting rules, a set $\mathcal{X}$ of ruler-graphs, and a weight function $s_{\mathcal{X}}$. Let $\rho = (L \leftarrow K \xrightarrow{r} R)$ denote a rule in $\mathcal{R}$ and $X \in \mathcal{X}$.

The rewriting relation $\Rightarrow_{\mathcal{A},\mathfrak{M}}$ is terminating relative to $\Rightarrow_{\mathcal{B},\mathfrak{M}}$ if the following hold: (i) for all $G \Rightarrow_{\mathcal{A},\mathfrak{M}} H$, $w_{s_{\mathcal{X}}}(G) > w_{s_{\mathcal{X}}}(H)$, and (ii) for all $G \Rightarrow_{\mathcal{B},\mathfrak{M}} H$, $w_{s_{\mathcal{X}}}(G) \ge w_{s_{\mathcal{X}}}(H)$. However, directly verifying all rewriting steps is infeasible due to their potential infiniteness. Thus, we aim to provide a rule-based sufficient condition for termination.

**Notation 26** The disjoint union of two sets $S$ and $S'$ will be denoted by $S \uplus S'$. Let $X, A, B, G$ be graphs, and let $\alpha: A \to G$ and $\beta: B \to G$ be morphisms. We
define the following sets of monomorphisms of X in G:

$$ \mathrm{Mono}(X, G, \alpha) = \{\iota: X \to G \mid \exists\beta: X \to A. \iota = \beta \star \alpha\}, $$

$$ \mathrm{Mono}(X, G, \neg\alpha) = \{\iota: X \to G \mid \neg\beta: X \to A. \iota = \beta \star \alpha\}, $$

$$ \mathrm{Mono}(X, G, \neg\alpha, \beta) = \left\{ \iota: X \to G \;\middle|\; \left( \begin{array}{@{}l@{}} \neg\beta: X \to A. \iota = \zeta \star \alpha \\ \land (\exists\zeta: X \to B. \iota = \zeta \star \beta) \end{array} \right) \right\}, $$

$$ \mathrm{Mono}(X, G, \neg\alpha, \neg\beta) = \left\{ \iota: X \to G \;\middle|\; \left( \begin{array}{@{}l@{}} \neg\beta: X \to A. \iota = \zeta \star \alpha \\ \land (\neg\beta: X \to B. \iota = \zeta \star \beta) \end{array} \right) \right\}. $$

Consider a DPO diagram (illustrated on the right) defining a rewriting step $G \Rightarrow_{\rho, \mathfrak{M}} H$. The sets of monomorphisms from X to G and H can be decomposed into the following disjoint unions:

$$ \begin{array}{ccccl} & & L & \leftarrow & K \xrightarrow{r} R \\ & & \searrow & & \searrow \\ m' & \leftarrow & l' & & m' \\ & & \searrow & & \searrow \\ G & \leftarrow & C & \xrightarrow{r'} & H \end{array} $$

$$ \mathrm{Mono}(X, G) = \mathrm{Mono}(X, G, l') \uplus \mathrm{Mono}(X, G, \neg l', m) \uplus \mathrm{Mono}(X, G, \neg l', \neg m) $$

$$ \mathrm{Mono}(X, H) = \mathrm{Mono}(X, H, r') \uplus \mathrm{Mono}(X, H, \neg r', m') \uplus \mathrm{Mono}(X, H, \neg r', \neg m') $$

Thus, we have:

$$ |\mathrm{Mono}(X, G)| = |\mathrm{Mono}(X, G, l')| + |\mathrm{Mono}(X, G, \neg l', m)| + |\mathrm{Mono}(X, G, \neg l', \neg m)| $$

$$ |\mathrm{Mono}(X, H)| = |\mathrm{Mono}(X, H, r')| + |\mathrm{Mono}(X, H, \neg r', m')| + |\mathrm{Mono}(X, H, \neg r', \neg m')| $$

Using the following Lemma 27, we derive:

$$ |\mathrm{Hom}(X, G)| = |\mathrm{Mono}(X, C)| + |\mathrm{Mono}(X, L, \neg l)| + |\mathrm{Mono}(X, G, \neg l', \neg m)| $$

$$ |\mathrm{Mono}(X, H)| = |\mathrm{Mono}(X, C)| + |\mathrm{Mono}(X, R, \neg r)| + |\mathrm{Mono}(X, H, \neg r', \neg m')| $$

**Lemma 27.**

Let X be a ruler-graph. For a pushout square as shown on the right, we have

$$ \begin{array}{c} |\mathrm{Mono}(X, B)| = |\mathrm{Mono}(X, D, \beta')| \\ |\mathrm{Mono}(X, C, \neg\beta)| = |\mathrm{Mono}(X, D, \neg\beta', \alpha')| \end{array} $$

$$ \begin{array}{ccc} C & \stackrel{\beta}{\rightleftarrows} & A \\ \alpha' & \searrow & \searrow \\ D & \rightleftarrows & B \end{array} $$

*Proof.* See the Appendix, § C.

Therefore, we obtain:

$$ |\mathrm{Mono}(X, G)| - |\mathrm{Mono}(X, H)| = |\mathrm{Mono}(X, L, \neg l)| - |\mathrm{Mono}(X, R, \neg r)| + |\mathrm{Mono}(X, G, \neg l', \neg m)| - |\mathrm{Mono}(X, H, \neg r', \neg m')| $$

By Lemma 28, this simplifies to:

$$ |\mathrm{Mono}(X, G)| - |\mathrm{Mono}(X, H)| = |\mathrm{Mono}(X, L)| - |\mathrm{Mono}(X, R)| + |\mathrm{Mono}(X, G, \neg l', \neg m)| - |\mathrm{Mono}(X, H, \neg r', \neg m')| $$
**Lemma 28.** Let X be a graph. Let $L \stackrel{l}{\leftarrow} K \xrightarrow{r} R$ be an injective DPO graph rewriting rule. We have

$$| \mathrm{Mono}(X, L, \neg l) | - | \mathrm{Mono}(X, R, \neg r) | = | \mathrm{Mono}(X, L) | - | \mathrm{Mono}(X, R) |$$

*Proof.* See the Appendix, Equation C.

Consequently, the weight difference satisfies:

$$\begin{align*}
& w_{s_X}(G) - w_{s_X}(H) \\
&\stackrel{\text{def}}{=} \sum_{X \in \mathcal{X}} s_X(X) * m_X(G) - \sum_{X \in \mathcal{X}} s_X(X) * m_X(H) \\
&\stackrel{\text{def}}{=} \sum_{X \in \mathcal{X}} s_X(X) * |\mathrm{Mono}(X, G)| - \sum_{X \in \mathcal{X}} s_X(X) * |\mathrm{Mono}(X, H)| \\
&= \sum_{X \in \mathcal{X}} s_X(X) * (|\mathrm{Mono}(X, G)| - |\mathrm{Mono}(X, H)|) \\
&= \sum_{X \in \mathcal{X}} s_X(X) * (|\mathrm{Mono}(X, L)| - |\mathrm{Mono}(X, R)|) + \\
&\qquad \sum_{X \in \mathcal{X}} s_X(X) * (|\mathrm{Mono}(X, G, \neg l', \neg m)| - |\mathrm{Mono}(X, H, \neg r', \neg m')|)
\end{align*}$$

Since $\sum_{X \in \mathcal{X}} s_X(X) * (|\mathrm{Mono}(X, L)| - |\mathrm{Mono}(X, R)|)$ can be precisely computed, the key challenge is to establish a lower bound for

$$\sum_{X \in \mathcal{X}} s_X(X) * (|\mathrm{Mono}(X, G, \neg l', \neg m)| - |\mathrm{Mono}(X, H, \neg r', \neg m')|)$$

### 3.3 Non-increasing rules

The DPO diagram defining $G \Rightarrow_{\rho} H$ with injective match $m$ can be viewed, up to graph renaming, as a DPO diagram in the category of sets where all morphisms are inclusion functions. The corresponding DPO diagram is illustrated on the right.

In this visualization, $L', R', C', K$ are mutually disjoint sets with $L' \uplus K = L$, $R' \uplus K = R$, $C' \uplus K = C$ and $G = L \cup C$ and $H = R \cup C'$. Thus, any subgraph of $H$ (resp. $G$) can be considered as a union of subgraphs of $C$ and $R$ (resp. $L$).

**Definition 29.** Consider a rewriting step defined by the DPO diagram above. Let X be a ruler-graph and G a graph. An X-occurrence in G is a subgraph of G isomorphic to X. An X-occurrence x implicitly created by the rewriting step is an X-occurrence in H which is included neither in R nor in C. Let $R' = x \cap R$, $C' = x \cap C$ and $h_{R'L} : R' \to L$ a monomorphism preserving interface elements. The corresponding X-occurrence relative to $h_{R'L}$ of x is the X-occurrence in G defined by $h_{R'L}(R') \cup C'$. An X-occurrence x implicitly destroyed by the rewriting step is an X-occurrence in G which is included neither in L nor in C.

<figure><img src="image_7.png" /></figure>
We define the set $D(R, X)$ of all subgraphs of $R$ which can form an $X$-occurrence in the result graph which is included neither in $R$ nor in $C$.

**Definition 30.** Let $X$ be a graph and $L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R$ an injective DPO rewriting rule. The set $D(R, X)$ consists of all subgraphs $R' \subseteq R$ satisfying the following conditions:

- $R'$ is not a subgraph of $r(K)$,

- $R'$ is not isomorphic to $X$,

- a diagram as shown on the right where $h_{K'K}: K' \rightarrow K$ and $h_{R'R}: R' \rightarrow R$ are inclusion functions can be constructed.

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

**Notation 31** We use the notation from [OE23a, Example 9] to visualize edge-labeled graph homomorphisms. Labeled graphs are enclosed in boxes with their names displayed in the top-left corner. Nodes and edges are assigned subsets of $\mathbb{N}$ as identifiers, and these identifiers are chosen such that: (i) Each node or edge $y$ in the codomain graph is assigned the union of the identifiers of all nodes or edges in the domain graph that are mapped to $y$; (ii) The graph homomorphism is uniquely determined by this assignment.

To further improve readability, we represent sets by listing their elements. Additionally, we omit identifiers when doing so does not cause confusion. This is illustrated in the following representation of a homomorphism $h: G \rightarrow H$.

<figure><img src="image_9.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. Edge identifiers are omitted.

**Example 32.** Consider the injective DPO rule from [BKZ14, Example 6]:

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

Let $X$ be $\bullet \xrightarrow{a} \bullet \xrightarrow{a} \bullet$. The set $D(R, X)$ contains only $\circled{1}^a \circled{4}$ and $\circled{5}^a \circled{2}$.

**Example 33.** Let $X$ be the graph $\bullet \rightarrow \bullet \rightarrow \bullet$. Consider the following rule.

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

The set $D(R, X)$ contains a unique element: $\circled{2} \rightarrow \circled{3}$. The subgraph $\circled{2} \rightarrow \circled{1}$, denote as $R'$, cannot belong to $D(R, X)$. This is because it is a subgraph of $r(K)$.
**Definition 34 (Non-increasing rule).**

Let $\rho = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R)$ be a rule and $X$ a ruler-graph. The rule $\rho$ is $X$-non-increasing if the following four conditions hold: (1) for all $R' \in D(R, X)$ there exists an $h_{R'L}: R' \rightarrow L$ such that the diagram shown on the right holds,

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

(2) For all node or arrow $r'$ in $R'$, if $r' \notin \text{Im}(r)$ then $h_{R'L}(r') \notin \text{Im}(l)$,

(3) For all $R', R'' \in D(R, X)$, for all edges $x \in R'$ and $y \in R''$, if $x \neq y$, then $h_{R'L}(x) \neq h_{R''L}(y)$,

(4) If $X$ has isolated nodes, then for all $R', R'' \in D(R, X)$ and nodes $x \in R'$, $y \in R''$, if $x \neq y$, then $h_{R'L}(x) \neq h_{R''L}(y)$.

Intuitively, a rule $\rho$ is $X$-non-increasing if, for any rewriting step using $\rho$, there exists an injective mapping from the set of $X$-occurrences implicitly created by the step to the set of $X$-occurrences implicitly destroyed by the step. This will be proved in Lemma 40.

*Example 35.* Consider the rule presented in Example 32. Let $X$ be $\bullet \xrightarrow{a} \bullet \xrightarrow{a} \bullet$. By Example 32, the set $D(R, X)$ contains only two elements: $R': \textcircled{1}^a \textcircled{4}$ and $R'': \textcircled{5}^a \textcircled{2}$. The rule is $X$-non-increasing because the following diagrams hold and $h_{R'L}$ and $h_{R''L}$ satisfy all conditions in Definition 34:

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

To illustrate the $X$-non-increasing property, consider the rewriting step defined by the DPO diagram below. Whenever $R'$ (resp. $R''$) forms an $X$-occurrence that is included neither in $R$ nor $C$ with a subgraph $C' \subseteq C$, the graph $h_{R'L}(R')$ (resp. $h_{R''L}(R'')$) forms a $X$-occurrence in $G$ with $C'$. Furthermore, distinct $X$-occurrences created in $H$ have distinct corresponding $X$-occurrences in $G$.
<figure><img src="image_14.png" /></figure>

The second condition guarantees that any X-occurrence implicitly created by the rewriting step has its corresponding X-occurrence not included in the context (Consequently, its corresponding X-occurrence is implicitly destroyed by the rewriting step). Counterexamples are provided in Example 36 and Example 37.

*Example 36.* Let $X$ be the graph $\bullet \rightarrow \bullet \rightarrow \bullet$. The following rewriting rule is not $X$-non-increasing.

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

As shown in Example 33, $D(R, X)$ contains exactly one element $R'$: $\overset{\circ}{2} \rightarrow \overset{\circ}{3}$. The unique monomorphism $h_{R'L}: R' \rightarrow L$ fails the second condition of Definition 34. For any rewriting step using this rule, the corresponding $X$-occurrence relative to $h_{R'L}$ of any $X$-occurrence created by the rewriting step is included in the context.

*Example 37.* Let $X$ be the graph $\bullet \rightarrow \bullet$. The following rewriting rule is not $X$-non-increasing.

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

The set $D(R, X)$ contains $R'$: $\overset{\circ}{1} \quad \overset{\circ}{3}$. Despite the existence of a unique monomorphism $h_{R'L}: R' \rightarrow L$ preserving interface elements, this rule fails the second condition of Definition 34. For any rewriting step using this rule, the corresponding $X$-occurrence relative to $h_{R'L}$ of any $X$-occurrence created by the rewriting step is included in the context.

The third and fourth conditions ensure that distinct $X$-occurrences implicitly created have distinct corresponding $X$-occurrences. Counterexamples for these conditions are given in Example 38 and Example 39.

*Example 38.* Let $X$ be the graph $\bullet \rightarrow \bullet \rightarrow \bullet$. The following rewriting rule is not $X$-non-increasing.

<figure><img src="image_17.png" /></figure>
The set $D(R, X)$ contains exactly two elements $R'$: $\textcircled{2}$ and $R''$: $\textcircled{3}$. Despite unique monomorphisms $h_{R'L}: R' \to L$ and $h_{R''L}: R'' \to L$ preserving interface elements, they fail the third condition of Definition 34. For any rewriting step using this rule, $X$-occurrences implicitly created by the rewriting rule with the same subgraph of the context have the same corresponding $X$-occurrence.

*Example 39.* Let $X$ be the graph $\bullet \to \bullet$ $\bullet$, which has an isolated node. The following rewriting rule is not $X$-non-increasing.

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

The set $D(R, X)$ contains exactly two elements $R'$: $\textcircled{2}$ and $R''$: $\textcircled{3}$. There are unique monomorphisms $h_{R'L}: R' \to L$ and $h_{R''L}: R'' \to L$ preserving interface elements, but they fail the fourth condition of Definition 34. For any rewriting step using this rule, $X$-occurrences created by the rewriting rule with the same subgraph of the context have the same corresponding $X$-occurrence.

## 3.4 Solution to the key challenge

The following lemma ensures that if $\rho$ is $X$-non-increasing, then, for any rewriting step using $\rho$, the cardinality of the set of $X$-occurrences implicitly destroyed by the rewriting step is at least as large as the cardinality of the set of $X$-occurrences implicitly created by the rewriting step.

**Lemma 40.**

Let $X$ be a ruler-graph and $\rho = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R)$ an injective DPO rewriting rule. Suppose that $\rho$ is $X$-non-increasing. For every rewriting step induced by the DPO diagram (shown on the right), we have

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

$$| \text{Mono}(X, G, \neg m, \neg l') | \ge | \text{Mono}(X, H, \neg m', \neg r') |$$

*Proof.* See the Appendix, Section C.

## 3.5 Termination criterion

**Lemma 41 (Decreasing step).** Let $\rho = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R)$ be an injective DPO rewriting rule, $\mathcal{X}$ a set of ruler-graphs, $s_{\mathcal{X}}: \mathcal{X} \to \mathbb{N}$ a weight function, and $G \Rightarrow_{\rho, \mathfrak{M}} H$ a rewriting step. If $\rho$ is $X$-non-increasing for every ruler-graph $X \in \mathcal{X}$, then $w_{s_{\mathcal{X}}}(G) - w_{s_{\mathcal{X}}}(H) \ge w_{s_{\mathcal{X}}}(L) - w_{s_{\mathcal{X}}}(R)$.

*Proof.* See the Appendix, Section C.

**Theorem 42 (Termination).** Let $\mathcal{A}$ and $\mathcal{B}$ be sets of injective DPO rewriting rules, $\mathcal{X}$ a set of ruler-graphs and $s_{\mathcal{X}}$ a weight function. If the following hold:
1. for every $\rho \in A \cup B$ and for every $X \in \mathcal{X}$, the rule $\rho$ is $X$-non-increasing,

2. for every $\rho \in A$, we have $w_{s_X}(\text{lhs}(\rho)) > w_{s_X}(\text{rhs}(\rho))$,

3. for every $\rho \in B$, we have $w_{s_X}(\text{lhs}(\rho)) \ge w_{s_X}(\text{rhs}(\rho))$.

Then $\Rightarrow_{A,M}$ is terminating relative to $\Rightarrow_{B,M}$.

*Proof.* See the Appendix, Section C.

# 4 Extension to non-injective matches

The technique presented in § 3 can be extended to non-injective matches.

**Definition 43 (Quotient Rule [HMP01]).**

Given a rule $\rho = L \leftarrow K \rightarrow R$, a rule $\rho' = (L' \leftarrow K' \rightarrow R')$ is called a **quotient rule** of $\rho$ if there exists a DPO diagram (shown on the right) where all vertical graph morphisms are surjective. The set of quotient rules of $\rho$ is denoted by $Q(\rho)$, and for a rule set $A$, we write $Q(A) = \bigcup_{\rho \in A} Q(\rho)$.

$$ \begin{tikzcd} L \arrow[r, "L'"] & K \arrow[r, "K'"] \arrow[d, "PO"] & R \arrow[d, "PO"] \\ & & \arrow[dl, "L'"] \arrow[dr, "K'"] \arrow[dl, "PO"] \arrow[dr, "R'"] \end{tikzcd} $$

**Lemma 44 (Quotient Lemma [HMP01]).** Let $\rho$ be a DPO rewriting rule. For any graphs $G$ and $H$, $G \Rightarrow_{p,\mathfrak{F}} H$ if and only if $G \Rightarrow_{Q(p),\mathfrak{M}} H$.

**Corollary 45.** Let $A$ and $B$ be sets of injective DPO rewriting rules. The rewriting relation $\Rightarrow_{A,\mathfrak{F}}$ is terminating relative to $\Rightarrow_{B,\mathfrak{F}}$ if $\Rightarrow_{Q(A),\mathfrak{M}}$ is terminating relative to $\Rightarrow_{Q(B),\mathfrak{M}}$.

# 5 Examples

Our criterion is easier to check than existing interpretation-based methods for the following example.

*Example 46.* Consider the rewriting rule in Example 32. Let $X$ be the graph
* $\bullet \xrightarrow{a} \bullet \xrightarrow{a} \bullet$ with weight 1 and $\mathcal{X} = \{X\}$. The rule is $X$-non-increasing by Example 35. Since $w(L) = 1 > 0 = w(R)$, it terminates by Theorem 42.

We consider an example for which the techniques from [BKZ14; Bru+15; EO24; Det18; OE24] fail.

*Example 47.* The rewriting rule illustrated below is a variant of a rewriting rule presented in [Det18, Example 6], obtained by removing all edges in the interface.

<figure><img src="image_20.png" /></figure>
Let $X$ be the graph $\bullet \xrightarrow{s} \bullet \xleftarrow{s} \bullet$ with weight 1 and $\mathcal{X} = \{X\}$. The set $D(R, X)$ has a unique element $R'$: $\xrightarrow{\circ s \circ} \xrightarrow{\circ}$. The rule is $X$-non-increasing with the unique monomorphism $h_{R'L}$ which preserves the interface elements. Since $w(L) = 1 > 0 = w(R)$, the rule terminates by Theorem 42.

We present an example where $\mathcal{X}$ is not a singleton.

*Example 48.* Consider the rewriting rules presented in [OE24, Example 5.6] illustrated below:

$$ \rho = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
  % L
  \node[draw, circle, fill, inner sep=1.2pt] (a1) at (0,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (a2) at (2,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (b1) at (0,1.5) {};
  \node[draw, circle, fill, inner sep=1.2pt] (b2) at (2,1.5) {};
  \node[above=0.2cm of a1] {1};
  \node[above=0.2cm of a2] {2};
  \node[left=0.5cm of a1] {a};
  \node[right=0.5cm of a2] {a};
  \node[above=0.2cm of b1] {3};
  \node[above=0.2cm of b2] {4};
  \node[right=0.5cm of b1] {b};
  \node[left=0.5cm of b2] {b};
  \node[right=0.5cm of b1] {5};
  \node[right=0.5cm of b2] {b};
\end{tikzpicture}
\quad
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
  % K
  \node[draw, circle, fill, inner sep=1.2pt] (k1) at (0,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (k2) at (2,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (l1) at (0,1.5) {};
  \node[draw, circle, fill, inner sep=1.2pt] (l2) at (2,1.5) {};
  \node[above=0.2cm of k1] {1};
  \node[above=0.2cm of k2] {2};
  \node[left=0.5cm of k1] {a};
  \node[right=0.5cm of k2] {a};
  \node[above=0.2cm of l1] {3};
  \node[above=0.2cm of l2] {4};
  \node[right=0.5cm of l1] {b};
  \node[left=0.5cm of l2] {b};
\end{tikzpicture}
\quad
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
  % R
  \node[draw, circle, fill, inner sep=1.2pt] (r1) at (0,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r2) at (2,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r3) at (0,1.5) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r4) at (2,1.5) {};
  \node[above=0.2cm of r1] {1};
  \node[above=0.2cm of r2] {2};
  \node[right=0.5cm of r1] {a};
  \node[left=0.5cm of r2] {b};
  \node[above=0.2cm of r3] {3};
  \node[right=0.5cm of r4] {b};
\end{tikzpicture} $$
$$ \tau = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
  % L
  \node[draw, circle, fill, inner sep=1.2pt] (l1) at (0,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (l2) at (2,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r1) at (0,1.5) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r2) at (2,1.5) {};
  \node[above=0.2cm of l1] {1};
  \node[above=0.2cm of l2] {2};
  \node[left=0.5cm of l1] {b};
  \node[right=0.5cm of l2] {b};
  \node[above=0.2cm of r1] {3};
  \node[right=0.5cm of r2] {b};
\end{tikzpicture}
\quad
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
  % K
  \node[draw, circle, fill, inner sep=1.2pt] (k1) at (0,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (k2) at (2,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (l1) at (0,1.5) {};
  \node[draw, circle, fill, inner sep=1.2pt] (l2) at (2,1.5) {};
  \node[above=0.2cm of k1] {1};
  \node[above=0.2cm of k2] {2};
  \node[left=0.5cm of k1] {a};
  \node[right=0.5cm of k2] {a};
  \node[above=0.2cm of l1] {3};
  \node[right=0.5cm of l2] {b};
\end{tikzpicture}
\quad
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
  % R
  \node[draw, circle, fill, inner sep=1.2pt] (r1) at (0,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r2) at (2,0) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r3) at (0,1.5) {};
  \node[draw, circle, fill, inner sep=1.2pt] (r4) at (2,1.5) {};
  \node[above=0.2cm of r1] {1};
  \node[above=0.2cm of r2] {2};
  \node[right=0.5cm of r1] {a};
  \node[left=0.5cm of r2] {b};
  \node[above=0.2cm of r3] {3};
  \node[right=0.5cm of r4] {b};
\end{tikzpicture} $$

Let $X$ be $\bullet \not\to a$ with weight 5, let $Y$ be $\bullet \not\to b$ with weight 3 and $\mathcal{X} = \{X, Y\}$. The rules $\rho$ and $\tau$ are both $X$- and $Y$-non-increasing with $D(\text{rhs}(\rho), X) = D(\text{rhs}(\rho), Y) = D(\text{rhs}(\tau), X) = D(\text{rhs}(\tau), Y) = \emptyset$. We have $w(\text{lhs}(\rho)) = 10 > 9 = w(\text{rhs}(\rho))$ and $w(\text{lhs}(\tau)) = 6 > 5 = w(\text{rhs}(\tau))$. Thus, this rewriting system terminates by Theorem 42.

*Example 49 (Limitation).* Our method fails to prove termination for the rewriting rule in [EO24, Example D.3], because our approach cannot take into account antipatterns (see [OE24, Remark 6.2]).

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

# 6 Related work

The subgraph-counting method in [OE24] by Overbeek and Endrullis is designed for the PBPO+ [OER23]—a rewriting formalism capable of simulating left-injective DPO rewriting. It can prove termination for systems like [OE24, Examples 5.2, 5.7, 5.9] and [Det18, Example 6], which lie beyond the scope of our technique. Additionally, this method can be applied for many categories.

However, it is very closely related to our work in the setting where they are both defined. Both methods weight objects by summing weighted morphisms targeting them, and, for both methods, the key challenge lies in estimating weights for morphisms whose images partially overlap with the rewriting context.

The two methods employ distinct strategies to overcome this challenge. The subgraph-counting method relies on type-morphisms (see [OE23b, p. 9, remark 4.11, Lemma 4.23]), whereas our approach requires injective mappings from (i)
<table><caption>Table 1: Applicability of termination techniques to DPO rewriting examples. The symbol ✓ indicates termination can be proved by the technique, ✗ indicates it cannot be proved, and — denotes irrelevance or out-of-scope cases.</caption><thead><tr><th colspan="2">Techniques</th><th>Forward closure [Plu95]</th><th>Modular criterion [Det18]</th><th>Type graph [BKZ14]</th><th>Type graph [Bru+15]</th><th>Type graph [EO24]</th><th>Subgraph counting [OE24]</th><th>Our method</th></tr></thead><tbody><tr><td rowspan="2">[Plu95]</td><td>Example 3.8</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td></tr><tr><td>Example 4.1</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>✗</td></tr><tr><td rowspan="4">[Det18]</td><td>Example 3</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td></tr><tr><td>Example 4</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✗</td></tr><tr><td>Example 5</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td></tr><tr><td>Example 6</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td rowspan="4">[BKZ14]</td><td>Example 1</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>✗</td></tr><tr><td>Example 5</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>✗</td></tr><tr><td>Example 4 and 6</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>✓</td></tr><tr><td>Routing Protocol</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td><td>✗</td></tr><tr><td rowspan="4">[Bru+15]</td><td>Example 2</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>✓</td></tr><tr><td>Example 4</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>✓</td></tr><tr><td>Example 5</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>✗</td></tr><tr><td>Example 6</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>✗</td></tr><tr><td rowspan="8">[EO24]</td><td>Example 6.2</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>✓</td><td>✓</td></tr><tr><td>Example 6.3</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>✗</td><td>✓</td><td>✓</td></tr><tr><td>Example 6.4</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td></tr><tr><td>Example 6.5</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td></tr><tr><td>Example D.1</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>✓</td><td>✓</td></tr><tr><td>Example D.2</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>✗</td><td>✗</td></tr><tr><td>Example D.3</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>✗</td><td>✗</td></tr><tr><td>Example D.4</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td><td>-</td></tr><tr><td rowspan="6">[OE24]</td><td>Example 5.2</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td></tr><tr><td>Example 5.3</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Example 5.5</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Example 5.6</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Example 5.7</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>-</td><td>-</td></tr><tr><td>Example 5.8</td><td>-</td><td>-</td><td>-</td><td>-</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Current paper</td><td>Example 47</td><td>✓</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td><td>✓</td></tr></tbody></table>

subgraph occurrences partially overlapping the rewriting context in the result graph to (ii) those in the host graph.

Consequently, their method suffers from discrete interface, as mentioned in [OE24, Example 5.5]. For instance, it proves termination for [OE24, Example 5.5] but fails for [OE24, Example 6.3], where the rules differ only by a discrete interface. Similarly, it fails to prove termination for Example 47, but if an edge
labeled by “s” from node 1 to node 3 is added, then it succeeds. However, their method handles [Plu95, Example 4.1], which our method cannot.

The type graph method, which weighs an object by summing the weights of morphisms from the object to a type graph, was initially introduced by Zantema et al. [ZKB14] for cycle-rewriting systems. This method has since been generalized to edge-labeled multigraphs by Bruggink et al. [BKZ14] for DPO rewriting with monic matches and injective rules, later extended to DPO rewriting in general by Bruggink et al. [Bru+15], and further adapted to more categories and different DPO variants by Endrullis et al. [EO23]. These methods are not directly comparable with our technique in general. On the one hand, the termination of Example 47 can be proved by our method but not by the type graph methods due to the existence of a surjection from the output graph to the input graph as explained in [EO24, Example D.4]. On the other hand, our method cannot prove the termination of [BKZ14, Example 1, 5, 6 and Ad-hoc Routing Protocol], nor [Bru+15, Example 5, 6], because our method cannot take into account antipatterns (see [OE24, Remark 6.2]), nor [EO24, Examples D2 and D3].

Plump [Plu95] introduced a necessary and sufficient termination condition for left-injective DPO hypergraph rewriting via forward closure, though verifying this condition is undecidable. While this method proves termination of Example 47, our approach succeeds on [Plu95, Example 3.8] but fails in proving termination of [Plu95, Example 4.1].

Plump [Det18] later proposed a modular critical pair-based strategy for left-injective DPO hypergraph rewriting with monic matches. Our method complements this: while modularity reduces global complexity, each subsystem requires individual termination proofs. For example, the measure based on the indegree proposed in [Det18] cannot prove the termination of Example 47 due to the additional loops. Specifically, if the context graph is identical to the interface graph then we have $3^k < 2^k + 2^k + 3^k$ for all $k \in \mathbb{N}$. In contrast, our method succeeds.

Levendovszky et al. [LPE07] propose a termination criterion for DPO rewriting (monic matches, injective rules, negative application condition), though automated verification is hard as explained in [LPE07, §6].

Bottoni et al. [Bot+05] propose a termination criterion for DPO/SPO rewriting on high-level replacement units. Their method imposes a strongly constrained measuring function and the only concrete measuring function proposed are node-counting and edge-counting.

Bottoni et al. [BP10] presents a criterion for termination of DPO rewriting with monic matches, injective rules and negative application conditions, based on the construction of a labeled transition system.

A comparative analysis of termination techniques for DPO graph rewriting systems, drawn from prior work [Plu95; Det18; BKZ14; Bru+15; EO24; OE24], is summarized in Table 1. Our approach successfully proves termination for 14 of these systems.
# 7 Conclusion and future work

We have presented a machine-checkable sufficient condition for relative termination of DPO systems with injective rules on edge-labeled multigraphs. This method resolves cases where prior interpretation-based techniques [ZKB14; BKZ14; Bru+15; EO24; OE24] fail (e.g., Example 47) and, unlike the subgraph-counting approach in [OE24], avoids limitations arising from discrete interfaces. The method has been implemented in an OCaml tool <fnref n="3" />.

An interesting direction for future work is to extend our method to DPO systems with negative application conditions and to take antipatterns into account.

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

# References

[BKZ14] 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.

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

[Bot+05] P. Bottoni et al. "Termination of High-Level Replacement Units with Application to Model Transformation". In: *Electronic Notes in Theoretical Computer Science* 127.4 (2005). Proceedings of the Workshop on Visual Languages and Formal Methods (VLFM 2004), pp. 71–86. ISSN: 1571-0661. DOI: https://doi.org/10.1016/j.entcs.2004.08.048.

[BP10] Paola Bottoni and Francesco Parisi Presicce. "A Termination Criterion for Graph Transformations with Negative Application Conditions". In: *Electronic Communications of the EASST* 30 (2010). DOI: 10.14279/tuj.eceasst.30.419.

[Bru+15] H.J.S. Bruggink et al. "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.

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

[Con+03] E. Contejean et al. "Proving Termination of Rewriting with CiME". In: *Extended Abstracts of the 6th International Workshop on Termination, WST'03*. 2003, pp. 71–73.

[Cor+97] A. Corradini et al. "Algebraic Approaches to Graph Transformation - Part I: Basic Concepts and Double Pushout Approach". In: *Handbook of Graph Grammars*. 1997.

<footnote n="3">³ The source code is available at https://anonymous.4open.science/r/icgt25-32AE</footnote>
[Cou+16] P. Courtieu et al. "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.

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

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

[Ehr+97] H. Ehrig et al. "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.

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

[EO24] J. Endrullis and R. Overbeek. "Generalized Weighted Type Graphs for Termination of Graph Transformation Systems". In: *Graph Transformation*. Ed. by R. Harmer and J. Kosiol. Cham: Springer Nature Switzerland, 2024, pp. 39-58. ISBN: 978-3-031-64285-2. DOI: 10.1007/978-3-031-64285-2_3.

[EPS73] H. Ehrig, M. Pfender, and H. J. Schneider. "Graph-grammars: An algebraic approach". In: *14th Annu. Symp. Switching Automata Theory (SWAT)*. IEEE, 1973, pp. 167-180.

[Ges90] A. Geser. "Relative Termination". In: *1990*.

[Har11] J. Harrison. "Formal Verification". In: *Software and Systems Safety*. IOS Press, 2011, pp. 103-157.

[Hei+10] G. Heiser et al. "The Road to Trustworthy Systems". In: *Proceedings of the Fifth ACM Workshop on Scalable Trusted Computing*. 2010, pp. 3-10.

[HMP01] A. Habel, J. Müller, and D. Plump. "Double-pushout graph transformation revisited". In: *Math. Struct. Comput. Sci.* 11.5 (2001), pp. 637-688.

[HUW14] 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.

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

[Kön+18] B. König et al. "A Tutorial on Graph Transformation". In: *Graph Transformation, Specifications, and Nets: In Memory of Hartmut Ehrig* (2018), pp. 83-104.
[Löw10] M. Löwe. "Graph Rewriting in Span-Categories". In: *Graph Transformations*. Ed. by H. Ehrig et al. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010.

[LPE07] T. Levendovszky, U. Prange, and H. Ehrig. "Termination Criteria for DPO Transformations with Injective Matches". In: *Electronic Notes in Theoretical Computer Science* 175.4 (2007). Proceedings of the Workshop on Graph Transformation for Concurrency and Verification (GT-VC 2006), pp. 87–100. ISSN: 1571-0661. DOI: https://doi.org/10.1016/j.entcs.2007.04.019.

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

[LSP82] 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.

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

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

[OE23b] 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.

[OE24] R. Overbeek and J. Endrullis. "Termination of Graph Transformation Systems Using Weighted Subgraph Counting". In: *Logical Methods in Computer Science* Volume 20, Issue 4, 12 (2024). ISSN: 1860-5974. DOI: 10.46298/lmcs-20(4:12)2024. URL: https://lmcs.episciences.org/12700.

[OER23] 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.

[Pie91] B. C. Pierce. *Basic category theory for computer scientists*. MIT Press, 1991.

[Plu95] D. Plump. "On Termination of Graph Rewriting". In: *Graph-Theoretic Concepts in Computer Science*. Ed. by M. Nagl. Berlin, Heidelberg: Springer Berlin Heidelberg, 1995, pp. 88–100. DOI: 10.1007/3-540-60618-1_68.

[Pot+19] M. Potop-Butucaru et al. "Formal Methods for Mobile Robots". In: *Distributed Computing by Mobile Entities: Current Research in Moving and Computing* (2019), pp. 278–313.

[ZKB14] 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 Pullback, Adhesive Category and VK-square

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

**Definition 51 (Van Kampen Square [LS04, Definition 2]).** A van Kampen (VK) square (i) is a pushout square which satisfies the following condition: given a commutative cube (ii) of which (i) forms the bottom face and the back faces are pullbacks, the front faces are pullbacks if and only if the top face is a pushout.

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

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

**Definition 52 (Adhesive category [LS04, Definition 5]).** A category *C* is said to be *adhesive* if

- *C* has pushouts along monomorphisms, and

- *C* has pullbacks, and

- pushouts along monomorphisms are VK squares.

**Proposition 53 ([LS04, p.8]).** The category *Graph* of directed labeled multigraphs is adhesive.

## B Auxiliary lemmas

**Lemma 54.** Consider the following commutative diagram in *Graph* where KCHR is a pushout.
<figure><img src="image_24.png" /></figure>

The square $K'C'XR'$ is a pushout.

**Proof.** **Graph** is adhesive by Proposition 53. By Definition 52, pushouts along monomorphisms are VK squares. The square $KCHR$ is a pushout along monomorphisms. Hence $KCHR$ is VK square. By Definition 51, the square $K'C'XR'$ is pushout if the squares $C'CHX$ and $R'XHR$ are pullbacks. By assumption, the squares $C'CHX$ and $R'XHR$ are pullbacks. Therefore, $K'C'XR'$ is pushout.

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

$$ \begin{array}{ccc} A & \to & B \\ \bigwedge & & \mathrm{PO} \\ C & \to & D \end{array} $$

The following hold

1. 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$.

2. For all $b \in B \setminus h_{AB}(A)$ and $c \in C$, we have $\beta'(b) \neq \alpha'(c)$.

**Proof.** Let $b \in B$ and $c \in C$ such that $h_{BD}(b) = h_{CD}(c)$.

There are two cases: if $b$ and $c$ are two nodes then let $S$ be the singleton graph with unique node $u$, otherwise—$b$ and $c$ must be two edges—let let $S$ be the graph with two distinct nodes and a unique edge $u$.

Define morphisms $h_{SB}: S \to B$ and $h_{SC}: S \to C$ such that $h_{SB}(u) = b$ and $h_{SC}(u) = c$. We have $h_{SB} \circ h_{BD} = h_{SC} \circ h_{CD}$. The pushout square $ACDB$ is also a pullback square by Proposition 50, and the universal property of the pullback guarantees the existence of a unique morphism $h_{SA}: S \to A$ such that $h_{SA} \circ h_{AB} = h_{SB}$ and $h_{SA} \circ h_{AC} = h_{SC}$. Let $a = h_{SA}(u)$. Then $a \in A$, and by composition:

$$ - h_{AB}(a) = (h_{SA} \circ h_{AB})(u) = h_{SB}(u) = b $$

$$ - h_{AC}(a) = (h_{SA} \circ h_{AC})(u) = h_{SC}(u) = c $$

The second assertion is a direct consequence of the first. Suppose, for contradiction, there exist $b \in B \setminus h_{AB}(A)$ and $c \in C$ such that $h_{BD}(b) = h_{CD}(c)$. Since the first assertion holds, there must exist $a \in A$ with $h_{AB}(a) = b$ and $h_{AC}(a) = c$. However, this contradicts the assumption that $b \notin h_{AB}(A)$. $\square$
**Lemma 56.** Consider the following commutative diagram in Graph.

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

The square $K'KCC'$ is pullback square.

*Proof.* Let $K \leftarrow A \to C'$ be a span such that

$$h_{AK} \star h_{KC} = h_{AC'} \star h_{C'C} \quad (1)$$

We show first that there exists a morphism $h_{AK'}: A \to K'$ such that

$$h_{AK'} \star h_{K'C'} = h_{AC'}$$

$$h_{AK'} \star h_{K'K} = h_{AK}$$

From (1), we obtain

$$h_{AK} \star h_{KC} \star h_{CH} = h_{AC'} \star h_{C'C} \star h_{CH} \quad (2)$$

From (2) and commutativity of $C'CHX$ and $KCHR$, we deduce

$$(h_{AK} \star h_{KR}) \star h_{RH} = (h_{AC'} \star h_{C'X}) \star h_{XH} \quad (3)$$

Since (3) holds and $R'XHR$ is a pullback square, there exists a unique morphism $h_{AR'}: A \to R'$ such that

$$h_{AR'} \star h_{R'R} = h_{AK} \star h_{KR} \quad (4)$$

$$h_{AR'} \star h_{R'X} = h_{AC'} \star h_{C'X} \quad (5)$$

Since (5) holds and $K'C'XR'$ is a pullback square, there exists a unique morphism $h_{AK'}: A \to K'$ such that

$$h_{AK'} \star h_{K'C'} = h_{AC'} \quad (6)$$

$$h_{AK'} \star h_{K'R'} = h_{AR'} \quad (7)$$

We have $h_{AK'} \star h_{K'C'} = h_{AC'}$ by (6), and $h_{AK'} \star h_{K'K} = h_{AK}$ because $h_{KR}$ is injective and the following holds:

$$(h_{AK'} \star h_{K'K}) \star h_{KR} = h_{AK} \star h_{K'R'} \star h_{R'R} \quad \text{by commutativity of } K'KRR'$$

$$= h_{AR'} \star h_{R'R} \quad \text{by (7)}$$

$$= h_{AK} \star h_{KR} \quad \text{by (4)}$$
Now, we show the unicity of such a morphism from A to K'.

Let $h'_{AK'}: A \to K'$ be a morphism such that

$$h'_{AK'} \star h_{K'C'} = h_{AC'}$$

$$h'_{AK'} \star h_{K'K} = h_{AK}$$

From $h_{AK'} \star h_{K'C'} = h_{AC'}$, $h'_{AK'} \star h_{K'C'} = h_{AC'}$ and injectivity of $h_{K'C'}$, we deduce $h_{AK'} = h_{AK'}$.

□

**Lemma 57.** Consider the following commutative diagram in Graph.

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

There exists a unique monomorphism $h_{XG}: X \to G$ such that $h_{C'C} \star h_{CG} = h_{C'X} \star h_{XG}$ and $h_{R'L} \star h_{LG} = h_{R'X} \star h_{XG}$.

*Proof.* There exists a unique morphisms $h_{XG}: X \to G$, because $K'C'XR'$ is a pushout square and $h_{K'C'} \star h_{C'C} \star h_{CG} = h_{K'R'} \star h_{R'L} \star h_{LG}$. Therefore, the following commutative diagram holds

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

It remains to show that $h_{XG}$ is injective.

Let $x_1, x_2$ be two elements in the graph X such that $x_1 \neq x_2$. Since $K'R'XC'$ is a pushout square, there are 4 possible cases:

1. there are $c_1, c_2 \in C'$ such that $h_{C'X}(c_1) = x_1$ and $h_{C'X}(c_2) = x_2$;

2. there are $r_1, r_2 \in R'$ such that $h_{R'X}(r_1) = x_1$ and $h_{R'X}(r_2) = x_2$;
3. there are $r' \in R'$ and $c' \in C'$ such that $h_{C'X}(c') = x_1$ and $h_{R'X}(r') = x_2$;

4. there are $r' \in R'$ and $c' \in C'$ such that $h_{C'X}(c') = x_2$ and $h_{R'X}(r') = x_1$;

Since the second and fourth cases are symmetric to the first and third case, respectively, it suffices to show that in the first and third cases, we have $h_{XG}(x_1) \neq h_{XG}(x_2)$.

Case (1) Suppose that there are $c_1, c_2 \in C'$ such that $h_{C'X}(c_1) = x_1$ and $h_{C'X}(c_2) = x_2$.

We have $c_1 \neq c_2$ since $x_1 \neq x_2$ and $h_{C'X}$ is injective.

Therefore we have

$$ \begin{align*} h_{XG}(x_1) &= h_{XG}(h_{C'X}(c_1)) & \text{by definition of } c_1 \\ &= (h_{C'X} \star h_{XG})(c_1) \\ &= (h_{C'C} \star h_{CG})(c_1) & \text{by commutativity of } C'CGX \\ \neq (h_{C'C} \star h_{CG})(c_2) & \text{by injectivity of } h_{C'C} \star h_{CG} \text{ and } c_1 \neq c_2 \\ &= (h_{C'X} \star h_{XG})(c_2) & \text{by commutativity of } C'CGX \\ &= h_{XG}(h_{C'X}(c_2)) \\ &= h_{XG}(x_2) & \text{by definition of } c_2 \end{align*} $$

Case (3) Suppose that there are $r' \in R'$ and $c' \in C'$ such that $h_{C'X}(c') = x_1$ and $h_{R'X}(r') = x_2$.

We have three cases:

(3.1) Suppose that $h_{C'C}(c') \notin \text{Im}(h_{KC})$. We have

$$ \begin{align*} h_{XG}(x_1) &= h_{XG}(h_{C'X}(c')) & \text{by definition of } c' \\ &= (h_{C'X} \star h_{XG})(c') \\ &= (h_{C'C} \star h_{CG})(c') & \text{by commutativity of } C'CGX \\ &= h_{CG}(h_{C'C}(c')) \\ \neq h_{LG}(h_{R'L}(r')) & \text{by Lemma 55 and } h_{C'C}(c') \notin \text{Im}(h_{KC}) \\ &= (h_{R'L} \star h_{LG})(r') \\ &= (h_{R'X} \star h_{XG})(r') & \text{by commutativity of } R'XGL \\ &= h_{XG}(h_{R'X}(r')) \\ &= h_{XG}(x_2) & \text{by definition of } r' \end{align*} $$

(3.2) Suppose $h_{R'L}(r') \notin \text{Im}(h_{KL})$. This case is symmetric to the previous case.

(3.3) Suppose that there are $k_1, k_2 \in K$ such that $h_{KC}(k_1) = h_{C'C}(c')$ and $h_{KL}(k_2) = h_{R'L}(r')$.

We cannot have $k_1 = k_2$.

Suppose, by contradiction, that we have

$$ k_1 = k_2 \tag{8} $$
Since $K'C'CK$ is also a pullback square by Proposition 50 and $h_{KC}(k_1) = h_{C'C}(c')$ and $h_{C'C}(c') = h_{C'C}(c')$, there is $k' \in K'$ such that $h_{K'K}(k') = k_1$ and $h_{K'C'}(k') = c'$.

We have $h_{K'R'}(k') = r'$ because $h_{R'L}$ is injective, $h_{R'L}(r') = h_{R'L}(r')$ and

$$ \begin{align*} & h_{R'L}(h_{K'R'}(k')) \\ &= (h_{K'R'} \star h_{R'L})(k') \\ &= (h_{K'K} \star h_{KL})(k') \qquad \text{by commutativity of } K'R'LK \\ &= (h_{KL})(h_{K'K}(k')) \\ &= (h_{KL})(k_1) \\ &= (h_{KL})(k_2) \qquad \text{by assumption (8)} \end{align*} $$

Therefore, we have the contradiction:

$$ \begin{align*} x_1 &= h_{C'X}(c') && \text{by definition of } c' \\ &= h_{C'X}(h_{K'C'}(k')) && \text{by definition of } k' \\ &= (h_{K'C'} \star h_{C'X})(k') && \text{by definition of } k' \\ &= (h_{K'R'} \star h_{R'X})(k') && \text{by the commutativity of } K'C'XR' \\ &= h_{R'X}(h_{K'R'}(k')) \\ &= h_{R'X}(r') && \text{by definition of } r' \\ &= x_2 && \text{by definition of } x_2 \end{align*} $$

Thus, the following inequality holds

$$ k_1 \neq k_2 \qquad (9) $$

$$ \begin{align*} h_{XG}(x_1) &= h_{XG}(h_{C'X}(c')) && \text{by definition of } c' \\ &= (h_{C'X} \star h_{XG})(c') && \text{by definition of } c' \\ &= (h_{C'C} \star h_{CG})(c') && \text{by commutativity of } C'CGX \\ &= (h_{CG})(h_{KC}(k_1)) && \text{by definition of } k_1 \\ &= (h_{KC} \star h_{CG})(k_1) \\ &\neq (h_{KC} \star h_{CG})(k_2) && \text{by injectivity of } h_{KC} \star h_{CG} \text{ and (9)} \\ &= (h_{KL} \star h_{LG})(k_2) && \text{by commutativity of } KLGC \\ &= h_{LG}(h_{KL}(k_2)) \\ &= h_{LG}(h_{R'L}(r')) && \text{by the definition of } k_2 \\ &= (h_{R'L} \star h_{LG})(r') && \text{by definition of } r' \\ &= (h_{R'X} \star h_{XG})(r') && \text{by commutativity of } R'XLG \\ &= h_{XG}(h_{R'X}(r')) \\ &= h_{XG}(x_2) && \text{by definition of } r' \end{align*} $$
**Lemma 58.** Let $X$ be a graph. Let $\rho = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R)$ be an injective DPO rewriting rule. Let $G \Rightarrow_{\rho, \mathcal{M}} H$ be a rewriting step defined by the following DPO diagram:

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

Let $h'_{XH}, h''_{XH} : X \to H$ be monomorphisms. In the category **Graph**, we can construct the following commutative diagram

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

where

- $K'R'XC'$ is pushout and pullback;

- $K''R''XC''$ is pushout and pullback;

- $K'KCC'$ is pullback;

- $K''KCC''$ is pullback;

- $h'_{XG} : X \to G$ is the unique morphism such that $h_{C'C} \star h_{CG} = h_{C'X} \star h'_{XG}$ and $h_{R'L} \star h_{LG} = h_{R'X} \star h'_{XG}$;

- $h''_{XG} : X \to G$ is the unique morphism such that $h_{C''C} \star h_{CG} = h_{C''X} \star h''_{XG}$ and $h_{R''L} \star h_{LG} = h_{R''X} \star h''_{XG}$.

By Lemma 57, there exist $h'_{XG}, h''_{XG} : X \to G$ such that

- $h'_{XG} : X \to G$ is the unique morphism such that $h_{C'C} \star h_{CG} = h_{C'X} \star h'_{XG}$ and $h_{R'L} \star h_{LG} = h_{R'X} \star h'_{XG}$;

- $h''_{XG} : X \to G$ is the unique morphism such that $h_{C''C} \star h_{CG} = h_{C''X} \star h''_{XG}$ and $h_{R''L} \star h_{LG} = h_{R''X} \star h''_{XG}$.

We have the following commutative diagram
<figure><img src="image_30.png" /></figure>

where

- K'R'XC'' is pushout and pullback;

- K''R''XC'' is pushout and pullback;

- K'KCC' is pullback;

- K''KCC'' is pullback;

If $\rho$ is X-non-increasing and $h'_{XH} \neq h''_{XH}$ then $h'_{XG} \neq h''_{XG}$.

*Proof.* Suppose that $\rho$ is X-non-increasing and $h'_{XH} \neq h''_{XH}$. We are going to show $h'_{XG} \neq h''_{XG}$.

From $h'_{XH} \neq h''_{XH}$, we deduce there exists an element $x \in X$ such that $h_{XH}(x) \neq h''_{XH}(x)$. We can suppose that

$$x \text{ is either an isolated nodes or an edge.} \tag{10}$$

because otherwise $x$ would be a non-isolated node and we can take an incident edge of $x$.

Since K'R'XC' and K''R''XC'' are pushouts, there are 4 possible cases:

1. there are $c' \in C'$, $c'' \in C''$ such that $h_{C'X}(c') = h_{C'X}(c'') = x$;

2. there are $r' \in R'$, $r'' \in R''$ such that $h_{R'X}(r') = h_{R'X}(r'') = x$

3. there are arrows $r' \in R'$ and $c'' \in C''$ such that

$$h_{C''X}(c'') = x$$

$$h_{R'X}(r') = x$$

$$\mathfrak{h}c' \in C'.h_{C'X}(c') = x$$

$$\mathfrak{h}r'' \in R''.h_{R''X}(r'') = x$$

4. there are arrows $r'' \in R''$ and $c' \in C'$ such that

$$h_{C'X}(c') = x$$

$$h_{R''X}(r'') = x$$

$$\mathfrak{h}c'' \in C''.h_{C''X}(c'') = x$$

$$\mathfrak{h}r' \in R'.h_{R'X}(r') = x$$
We are going to show that in each case we have $h'_{XG}(x) \neq h''_{XG}(x)$. Since the fourth case is symmetric to the third case, it suffices to analyse the first three cases.

(1) Suppose that there are $c' \in C'$, $c'' \in C''$ such that $h_{C'X}(c') = h_{C'X}(c'') = x$. Suppose, by contradiction, that the following equality holds

$$h_{C'C}(c') = h_{C''C}(c'') \quad (11)$$

we have the following contradiction:

$$
\begin{align*}
& h'_{XH}(x) \\
&=h'_{XH}(h_{C'X}(c')) \\
&=(h_{C'X} \star h'_{XH})(c') \\
&=(h_{C'C} \star h_{CH})(c') && \text{By commutativity of } C'XHC \\
&=h_{CH}(h_{C'C}(c')) \\
&=h_{CH}(h_{C''C}(c'')) && \text{by (11)} \\
&=(h_{C''C} \star h_{CH})(c'') \\
&=(h_{C''X} \star h''_{XH})(c'') && \text{By commutativity of } C''CHX \\
&=h''_{XH}(h_{C''X}(c'')) \\
&=h''_{XH}(x)
\end{align*}
$$

Therefore, we have

$$h_{C'C}(c') \neq h_{C''C}(c'') \quad (12)$$

$$
\begin{align*}
h'_{XG}(x) &= h'_{XG}(h_{C'X}(c')) && \text{by definition of } c' \\
&= (h_{C'X} \star h'_{XG})(c') \\
&= (h_{C'C} \star h_{CG})(c') && \text{by commutativity of } C'CGX \\
&= h_{CG}(h_{C'C}(c')) \\
&\neq h_{CG}(h_{C''C}(c'')) && \text{by (12) and the injectivity of } h_{CG} \\
&= (h_{C''C} \star h_{CG})(c'') \\
&= (h_{C''X} \star h''_{XG})(c'') && \text{by commutativity of } C''CGX \\
&= h''_{XG}(h_{C''X}(c'')) \\
&= h''_{XG}(x) && \text{by definition of } c''
\end{align*}
$$

(2) Suppose that there are $r' \in R'$, $r'' \in R''$ such that $h_{R'X}(r') = h_{R'X}(r'') = x$. We have

$$h_{R'R}(r') \neq h_{R''R}(r'') \quad (13)$$
by an argument analogous to the argument for $h_{C'C}(c') \neq h_{C''C}(c'')$ in the
previous case. Since $\rho$ is $X$-non-increasing, (13) and (10) hold, we have

$$
h_{R'L}(r') \neq h_{R''L}(r'') \quad (14)
$$

Hence, the following inequality holds

$$
\begin{align*}
h'_{XG}(x) &= h'_{XG}(h_{R'X}(r')) && \text{by definition of } r' \\
&= (h_{R'X} \star h'_{XG})(r') && \\
&= (h_{R'L} \star h_{LG})(r') && \text{by commutativity of } R'XGL \\
&= h_{LG}(h_{R'L}(r')) && \\
&\neq h_{LG}(h_{R''L}(r'')) && \text{By injectivity of } h_{LG} \text{ and (14)} \\
&= (h_{R''L} \star h_{LG})(r'') && \\
&= (h_{R''X} \star h''_{XG})(r'') && \text{by commutativity of } R''XGL \\
&= h''_{XG}(h_{R''X}(r'')) && \\
&= h''_{XG}(x) && \text{by definition of } r''
\end{align*}
$$

(3) Suppose, that there are arrows $r' \in R'$ and $c'' \in C''$ such that

$$
\begin{align*}
h_{C''X}(c'') &= x \\
h_{R'X}(r') &= x \\
\mathcal{J}c' \in C'.h_{C'X}(c') &= x \\
\mathcal{J}r'' \in R''.h_{R''X}(r'') &= x \tag{15}
\end{align*}
$$

Suppose, by contradiction, that we have

$$
h_{C''C}(c'') \in \mathrm{Im}(h_{KC}) \qquad (16)
$$

Then, there are $k_2 \in K$ such that $h_{KC}(k_2) = h_{C''C}(c'')$.

There is $k'' \in K''$ such that $h_{K''K}(k'') = k_2$ and $h_{K''C''}(k'') = c''$ because
$K''C''CK$ is a pullback square and $h_{KC}(k_2) = h_{C''C}(c'')$.

We have $h_{K''R''}(k'') \in R''$ and

$$
\begin{align*}
& h_{R''X}(h_{K''R''}(k'')) \\
&=(h_{K''R''} \star h_{R''X})(k'') \\
&=(h_{K''C''} \star h_{C''X})(k'') && \text{by commutativity of } K''R''XC'' \\
&=h_{C''X}(h_{K''C''}(k'')) \\
&=h_{C''X}(c'') \\
&=x
\end{align*}
$$

which contradicts the assumption (15).
Thus, the following holds

$$h_{C''C}(c'') \notin \mathrm{Im}(h_{KC}) \qquad (17)$$

We deduce

$$
\begin{align*}
h'_{XG}(x) &= h'_{XG}(h_{C''X}(c'')) && \text{by definition of } c'' \\
&= (h_{C''X} \star h'_{XG})(c'') && \\
&= (h_{C''C} \star h_{CG})(c'') && \text{by commutativity of } C''CGX \\
&= h_{CG}(h_{C''C}(c'')) \\
&\neq h_{LG}(h_{R'L}(r')) && \text{by Lemma 55 and the assumption (17)} \\
&= (h_{R'L} \star h_{LG})(r') \\
&= (h_{R'X} \star h''_{XG})(r') && \text{by commutativity of } R'XGL \\
&= h''_{XG}(h_{R'X}(r')) \\
&= h''_{XG}(x) && \text{by definition of } r'
\end{align*}
$$

## C Proofs of Lemma 27, Lemma 28, Lemma 40 and Lemma 41

### Lemma 27

Let $X$ be a graph. For a pushout square as shown on the right, we have

$$ \begin{array}{ccc} | \mathrm{Mono}(X, B) | = | \mathrm{Mono}(X, D, \beta') | & & \\ | \mathrm{Mono}(X, C, \neg \beta) | = | \mathrm{Mono}(X, D, \neg \beta', \alpha') | & & \end{array} $$

$$ \begin{array}{ccc} C \stackrel{\beta}{\rightleftarrows} A & & \\ \llcorner \alpha' \quad \downarrow \alpha & & \\ D \stackrel{\beta'}{\rightleftarrows} B & & \end{array} $$

$$ \textit{Proof. Claim.} \quad |\mathrm{Mono}(X, B)| = |\mathrm{Mono}(X, D, \beta')| $$

- The inclusion $\mathrm{Mono}(X, B) \star \beta' \subseteq \mathrm{Mono}(X, D, \beta')$ holds by definition of $\mathrm{Mono}(X, B)$ and $\mathrm{Mono}(X, D, \beta')$. In fact, if $\iota \in \mathrm{Mono}(X, B) \star \beta'$, then there is a monomorphism $\zeta : X \to B$ satisfying $\iota = \zeta \star \beta'$. Since $\zeta \star \beta'$ is also a monomorphism, $\iota$ is also an element of $\mathrm{Mono}(X, D, \beta')$.

- The inclusion $\mathrm{Mono}(X, B) \star \beta' \supseteq \mathrm{Mono}(X, D, \beta')$ holds by definition of $\mathrm{Mono}(X, B)$ and $\mathrm{Mono}(X, D, \beta')$. Suppose $\iota \in \mathrm{Mono}(X, D, \beta')$. There is a monomorphism $\zeta : X \to B$ satisfying $\iota = \zeta \star \beta'$. It follows that $\iota = \zeta \star \beta' \in \mathrm{Mono}(X, B) \star \beta'$.

- Hence, we have $\mathrm{Mono}(X, B) \star \beta' = \mathrm{Mono}(X, D, \beta')$.

- $|\mathrm{Mono}(X, B)| \le |\mathrm{Mono}(X, D, \beta')|$ follows by the injectivity of $\beta'$.

$$ \textit{Claim.} \quad |\mathrm{Mono}(X, C, \neg \beta)| = |\mathrm{Mono}(X, D, \neg \beta', \alpha')| $$

- The inclusion $\mathrm{Mono}(X, C, \neg \beta) \star \alpha' \subseteq \mathrm{Mono}(X, D, \neg \beta', \alpha')$ can be justified as follows: Suppose $\eta \star \alpha' \in \mathrm{Mono}(X, C, \neg \beta) \star \alpha'$. Since $\eta \star \alpha'$ is a monomorphism, it suffices to show that there is no $\zeta : X \to B$ such that $\eta \star \alpha' = \zeta \star \beta'$. Suppose, by contradiction, that such a $\zeta$ exists, then the following commutative diagram holds:
<figure><img src="image_31.png" /></figure>

The pushout square $\Box ABDC$ is also a pullback square, by Proposition 50. The universal property of the pullback provides a morphism $\gamma : X \to A$ such that $\eta = \gamma \star \beta$. $\gamma$ is a monomorphism, because $\eta = \gamma \star \beta$ and $\eta$ is a monomorphism. Therefore, the existence of $\gamma$ contradicts the assumption that $\eta \in \mathrm{Mono}(X, C, \neg\beta)$. Thus, $\iota$ is also an element of $\mathrm{Mono}(X, D, \neg\beta', \alpha')$.

- The inclusion $\mathrm{Mono}(X, C, \neg\beta) \star \alpha' \supseteq \mathrm{Mono}(X, D, \neg\beta', \alpha')$ can be justified as follows. Suppose that $\iota : X \to D$ is an element of $\mathrm{Mono}(X, D, \neg\beta', \alpha')$. According to the definition of $\mathrm{Mono}(X, D, \neg\beta', \alpha')$, there exists $\eta : X \to C$ making

$$ \iota = \eta \star \alpha' \qquad (18) $$

We show that $\eta$ is an element of $\mathrm{Mono}(X, C, \neg\beta)$ by contradiction. Suppose that there is a monomorphism $\zeta : X \to A$ such that

$$ \eta = \zeta \star \beta \qquad (19) $$

and observe:

$$ \iota \stackrel{\mathrm{def}}{=} \eta \star \alpha' \qquad \text{by (18)} $$

$$ \stackrel{\mathrm{def}}{=} (\zeta \star \beta) \star \alpha' \qquad \text{by (19)} $$

$$ = \zeta \star (\beta \star \alpha') \qquad \text{by associativity} $$

$$ = \zeta \star (\alpha \star \beta') \qquad \text{by commutativity of } ABDC $$

$$ = (\zeta \star \alpha) \star \beta' $$

There is a contradiction because no such factorization of $\iota$ should exist as $\iota \in \mathrm{Mono}(X, D, \neg\beta', \alpha')$.

- We conclude by the monicity of $\alpha'$.

**Lemma 28** Let $X$ be a graph. Let $L \stackrel{l}{\leftarrow} K \xrightarrow{r} R$ be an injective DPO graph rewriting rule. We have

$$ | \mathrm{Mono}(X, L, \neg l) | - | \mathrm{Mono}(X, R, \neg r) | = | \mathrm{Mono}(X, L) | - | \mathrm{Mono}(X, R) | $$

$$ \textit{Proof. Claim.} \quad | \mathrm{Mono}(X, L, l) | = | \mathrm{Mono}(X, R, r) | $$

- We prove $|\mathrm{Mono}(X, L, l)| \le |\mathrm{Mono}(X, R, r)|$ by constructing an injection from $\mathrm{Mono}(X, L, l)$ to $\mathrm{Mono}(X, R, r)$. Let $h \in \mathrm{Mono}(X, L, l)$. By definition, we have $h = g \star l$ for some $g : X \to K$. Thus, $g \star r \in \mathrm{Mono}(X, L, r)$. Let $h' \in \mathrm{Mono}(X, L, l)$ such that $h \ne h'$. We have $h' = g' \star l$ for some $g' : X \to K$. We have $g \ne g'$ because otherwise we would have $h = g \star l = g' \star l = h'$. From the monicity of $r$, we conclude $g \star r \ne g' \star r$.
- Analogously, we can prove $|\text{Mono}(X, L, l)| \ge |\text{Mono}(X, R, r)|$ by constructing an injection from $\text{Mono}(X, R, r)$ to $\text{Mono}(X, L, l)$.

Hence, the following equality holds

$$ 
\begin{align*}
& |\text{Mono}(X, L, \neg l)| - |\text{Mono}(X, R, \neg r)| \\
&= |\text{Mono}(X, L) \setminus \text{Mono}(X, L, l)| - |\text{Mono}(X, R) \setminus \text{Mono}(X, R, r)| \\
&= (|\text{Mono}(X, L)| - |\text{Mono}(X, L, l)|) - (|\text{Mono}(X, R)| - |\text{Mono}(X, R, r)|) \\
&= (|\text{Mono}(X, L)| - |\text{Mono}(X, R)|) - (|\text{Mono}(X, L, l)| - |\text{Mono}(X, R, r)|) \\
&= |\text{Mono}(X, L)| - |\text{Mono}(X, R)|
\end{align*}
$$

**Lemma 40**

Let $X$ be a ruler-graph and $\rho = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R)$ an injective DPO rewriting rule. Suppose that $\rho$ is $X$-non-increasing. For every rewriting step induced by the DPO diagram (shown on the right), we have

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

$$ |\text{Mono}(X, G, \neg m, \neg l')| \ge |\text{Mono}(X, H, \neg m', \neg r')| $$

*Proof.* We are going to show that for two arbitrary distinct monomorphisms $h'_{XH}, h''_{XH} \in \text{Mono}(X, H, \neg m, \neg r')$, there are two distinct monomorphisms $h'_{XG}, h''_{XG} \in \text{Mono}(X, G, \neg m, \neg l')$.

Let $h'_{XH} \in \text{Mono}(X, H, \neg m, \neg r')$ be a monomorphism. In the category **Graph**, we can construct the following commutative diagram

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

$KCHR$ is also pullback, by Proposition 50, because it is pushout. Therefore, since $KCHR$ is also pullback and $h_{K'C'} \star h_{C'C} \star h_{CH} = h_{K'R'} \star h_{R'R} \star h_{R'R}$ holds, there exists $h_{K'K} : K' \to K$ such that

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

$$ h_{K'R'} \star h_{R'R} = h_{K'K} \star h_{KR} \qquad (21) $$

The square $K'KCC'$ and $K'R'RK$ are pullbacks, by Lemma 56. Hence, the following commutative diagram holds
<figure><img src="image_34.png" /></figure>

Since the rule is by assumption X-non-increasing, there is a morphism $h_{R'L}$ such that $K'KLR'$ is commutative.

$K'C'XR'$ is a pushout by Lemma 54.

Thus, the following commutative diagram holds

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

By Lemma 57, there is a unique monomorphism $h'_{XG} : X \to G$ such that $h_{C'X} \star h'_{XG} = h_{C'C} \star h_{CG}$ and $h_{R'X} \star h'_{XG} = h_{R'L} \star h_{LG}$.

The monomorphism $h'_{XG}$ is in the set $\text{Mono}(X, G, \neg m, \neg l')$, by $h'_{XH} \in \text{Mono}(X, H, \neg m', \neg r')$ and Definition 34. Intuitively, $h'_{XH} \in \text{Mono}(X, H, \neg m', \neg r')$ implies that some elements in X are mapped onto $h_{RH}(R) \setminus (r \star h_{RH})(K)$. By the first assumption of Definition 34, these elements are mapped onto $h_{LG}(L) \setminus (l \star h_{LG})(K)$.

The monomorphism $h'_{XG}$ belongs to the set $\text{Mono}(X, G, \neg m, \neg l')$, because of $h'_{XH} \in \text{Mono}(X, H, \neg m', \neg r')$ and Definition 34. Intuitively, $h'_{XH} \in \text{Mono}(X, H, \neg m', \neg r')$ implies that certain elements of X are mapped into $h_{RH}(R) \setminus (r \star h_{RH})(K)$. By the second assumption of Definition 34, these elements are also mapped into $h_{LG}(L) \setminus (l \star h_{LG})(K)$.

Let $h''_{XH} : X \to H$ be a monomorphism such that

$$h'_{XH} \neq h''_{XH} \qquad (22)$$

In the category **Graph**, we can construct the following commutative diagram:
<figure><img src="image_36.png" /></figure>

Analogously, there exists a unique monomorphism $h''_{XG}: X \to G$ such that
$h_{C''X} \star h''_{XG} = h_{C''C} \star h_{CG}$ and $h_{R''X} \star h''_{XG} = h_{R''L} \star h_{LG}$.

By (22) and Lemma 58, we have $h_{XG} \neq h'_{XG}$.

**Lemma 41** [Decreasing step] Let $\rho = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\rightarrow} R)$ be an injective DPO rewriting rule, $\mathcal{X}$ a set of ruler-graphs, $s_{\mathcal{X}}: \mathcal{X} \to \mathbb{N}$ a weight function, and $G \Rightarrow_{\rho, \mathbb{N}} H$ a rewriting step. If $\rho$ is $X$-non-increasing for every ruler-graph $X \in \mathcal{X}$, then:

$$w_{s_{\mathcal{X}}}(G) - w_{s_{\mathcal{X}}}(H) \geq w_{s_{\mathcal{X}}}(L) - w_{s_{\mathcal{X}}}(R)$$

*Proof.* Let the following diagram be the witness diagram of the rewriting step

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

Let $X \in \mathcal{X}$.

We have

$$
\begin{align*}
& |\text{Mono}(X, G)| \\
&= |\text{Mono}(X, G, l') \uplus \text{Mono}(X, G, \neg l', m) \uplus \text{Mono}(X, G, \neg l', \neg m)| \\
&= |\text{Mono}(X, G, l')| + |\text{Mono}(X, G, \neg l', m)| + |\text{Mono}(X, G, \neg l', \neg m)| \\
&= |\text{Mono}(X, C)| + |\text{Mono}(X, L, \neg l)| + |\text{Mono}(X, G, \neg l', \neg m)| \quad \text{by Lemma 27}
\end{align*}
$$

and

$$
\begin{align*}
& |\text{Mono}(X, H)| \\
&= |\text{Mono}(X, H, r') \uplus \text{Mono}(X, H, \neg r', m') \uplus \text{Mono}(X, H, \neg r', \neg m')| \\
&= |\text{Mono}(X, H, r')| + |\text{Mono}(X, H, \neg r', m')| + |\text{Mono}(X, H, \neg r', \neg m')| \\
&= |\text{Mono}(X, C)| + |\text{Mono}(X, R, \neg r)| + |\text{Mono}(X, H, \neg r', \neg m')| \quad \text{by Lemma 27}
\end{align*}
$$
Therefore, the following inequality holds

$$
\begin{align*}
& |\text{Mono}(X, G)| - |\text{Mono}(X, H)| \\
& = (|\text{Mono}(X, L, \neg l)| - |\text{Mono}(X, R, \neg r)|) + (|\text{Mono}(X, G, \neg l', \neg m)| - |\text{Mono}(X, H, \neg r', \neg m')|) \\
& \geq |\text{Mono}(X, L, \neg l)| - |\text{Mono}(X, R, \neg r)| && \text{by Lemma 40} \\
& = |\text{Mono}(X, L)| - |\text{Mono}(X, R)| && \text{by Lemma 28}
\end{align*}
$$

Thus, the following inequality holds

$$
\begin{align*}
w_{s_X}(G) - w_{s_X}(H) \\
&= \sum_{X \in \mathcal{X}} w(X) * |\text{Mono}(X, G)| - \sum_{X \in \mathcal{X}} w(X) * |\text{Mono}(X, H)| \\
&= \sum_{X \in \mathcal{X}} w(X) * (|\text{Mono}(X, G)| - |\text{Mono}(X, H)|) \\
&\geq \sum_{X \in \mathcal{X}} w(X) * (|\text{Mono}(X, L)| - |\text{Mono}(X, R)|) \\
&= \sum_{X \in \mathcal{X}} w(X) * |\text{Mono}(X, L)| - \sum_{X \in \mathcal{X}} w(X) * |\text{Mono}(X, R)| \\
&= w_{s_X}(L) - w_{s_X}(R)
\end{align*}
$$

□

**Theorem 42** [Termination] Let $\mathcal{A}$ and $\mathcal{B}$ be sets of injective DPO rewriting rules, $\mathcal{X}$ a set of ruler-graphs and $s_{\mathcal{X}}$ a weight function. If the following hold

1. $\rho$ is $X$-non-increasing for every rule $\rho \in \mathcal{A} \cup \mathcal{B}$ and for every ruler-graph $X \in \mathcal{X}$,

2. $w_{s_X}(lhs(\rho)) > w_{s_X}(rhs(\rho))$ for every rule $\rho \in \mathcal{A}$,

3. $w_{s_X}(lhs(\rho)) \geq w_{s_X}(rhs(\rho))$ for every rule $\rho \in \mathcal{B}$.

Then $\Rightarrow_{\mathcal{A}, \mathcal{M}}$ is terminating relative to $\Rightarrow_{\mathcal{B}, \mathcal{M}}$.

*Proof.* By assumption (1) and Lemma 41, the inequality $w_{s_X}(G) - w_{s_X}(H) \ge w_{s_X}(lhs(\rho)) - w_{s_X}(rhs(\rho))$ holds for all rules $\rho \in \mathcal{A} \cup \mathcal{B}$ and for all rewriting steps $G \Rightarrow_{\rho, \mathcal{M}} H$.

From assumptions (2) and (3), we deduce

- $w_{s_X}(G) > w_{s_X}(H)$ for every rule $\rho \in \mathcal{A}$;

- $w_{s_X}(G) \geq w_{s_X}(H)$ for every rule $\rho \in \mathcal{B}$.

Since $w_{s_X}(G) \in \mathbb{N}$ for all graph $G$. Every rewriting sequence can only have a finite number of rewriting steps using rules in $\mathcal{A}$.
## D Additional Examples

*Example 59.* Consider the following rewriting rule presented in [EO24, Example 6.2].

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

*Example 60.* Consider a rewriting rule given by Overbeek and Endrullis in [OE24, Example 5.2] depicted in the bottom span of the following diagram

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

*Example 61.* Consider the rewriting rules presented in [OE24, Example 5.3] that can be depicted as the bottom spans of

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

Let $X$ be $\bullet \rightarrow \bullet$. We have $|\text{Mono}(X, L)| = 1 > 0 = |\text{Mono}(X, R)|$ for both rules. Thus, this rewriting system terminates by Theorem 42.

*Example 62.* Consider the following commutative diagram

<figure><img src="image_41.png" /></figure>
The bottom span of the diagram is a rewriting rule presented in [OE24, Example 5.5]. Its termination in the DPO rewriting framework with monic matches can be proved by our approach using the same argument for Example 72.

*Example 63.* Consider the DPO rewriting system with monic matches presented in [OE24, Example 5.6] with $\rho$ replaced by $\rho'$ as depicted by the span

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

Its termination is not in the scope of our method due to its non-node-injective left-hand side morphism.

*Example 64.* Example 5.7 has conditions on the host graph, which cannot be modeled by DPO rewriting rules.

*Example 65.* The POPO+ rewriting system presented in [OE24, Example 5.7] cannot be modeled by DPO rewriting rules due to the application condition on the context.

*Example 66.* Consider the DPO rewriting system presented in [OE24, Example 5.8], [Det18, Example 3] and [Plu95, Example 3.8]. It rewriting rules are depicted by the bottom spans of the following diagram

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

Let $X$ be $\bullet \xrightarrow{a} \bullet \xrightarrow{b} \bullet$

For both rules, $R_X$ is

$R_X$

We have $|\text{Mono}(X, L)| = 1 > 0 = |\text{Mono}(X, R)|$ for $\rho$, and $|\text{Mono}(X, L)| = 0 = 0 = |\text{Mono}(X, R)|$ for $\tau$, therefore $\rho$ is eliminated.

Let $Y$ be $\bullet \xrightarrow{c} \bullet$. For $\tau$, we have

$R_X$

and $|\text{Mono}(Y, L)| = 1 > 0 = |\text{Mono}(Y, R)|$.

Thus, this rewriting systems terminates by Theorem 42.
*Example 67.* Our method cannot prove the termination of the DPO rewriting system with monic matches presented in [Det18, Example 4]. The rewriting rule are depicted below

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

The rule $r_3$ can be eliminated by considering monomorphisms from $\bullet \xrightarrow{B} \bullet$,
then The rule $r_4$ can be eliminated by considering monomorphisms from $\bullet \xrightarrow{R} \bullet$.

But our method cannot eliminate $r_1$ and $r_2$. However, combined with the technique proposed by Plump in [Det18], we can prove the termination of this rewriting system: $\{r_1\}$ and $\{r_2\}$ are both terminating, and their union is termination by [Det18].

*Example 68.* Our method cannot prove the termination of the DPO rewriting system with monic matches presented in [Bru+15, Example 5].

*Example 69.* Our method cannot prove the termination of the DPO rewriting system with monic matches presented in [Bru+15, Example 6].

*Example 70.* The DPO rewriting system with monic matches presented in [Det18, Example 6] is not in the scope of our method due to the non-injective rule.

*Example 71.* The rewriting rule illustrated below is from [Det18, Example 6].

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

Its termination can be proved by our method.
*Example 72.* Consider the rule presented in [EO24, Example 6.3] illustrated in the bottom span of the following diagram:

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

Let $X$ be the graph $\bullet \stackrel{\leftarrow}{\hookrightarrow} \bullet$ and $\mathcal{X} = \{X\}$. Let $s_X$ be the weight function associating the weight of 1 to $X$. There is only one element $(x) \to (y)$ in $D(X, R)$. Since $w_{s_X}(L) = 1 > 0 = w_{s_X}(R)$, the rule terminates by Theorem 42.