Miguel Landry

Foko Sindjoung

Pascale Minet
email: pascale.minet@inria.fr

Wireless Link Quality Prediction in IoT Networks

Keywords: Machine learning, link quality estimation, wireless network, TSCH

est destinée au dépôt

I. MOTIVATIONS

Internet of Things (IoT) is a network consisting of interconnected devices called objects, that are able to monitor their surrounding environment, produce data from the sensed information and communicate with each other without any external intervention. A specific node, called a sink, is usually in charge of gathering data and analyzing them in order to take decisions. All the IoT objects, except the sink, are subject to multiple constraints including reduced energy, limited processing capacity and reduced memory size. All these constraints make data gathering a challenge. IoT networks are used in many domains of our everyday life: health care, precision agriculture, security, process control, predictive maintenance, environment monitoring...

In this work, we are interested in studying the quality of wireless links in an IoT network. Using links of bad quality would incur re-transmissions wasting node energy which decreases network lifetime. In addition, re-transmissions increase delivery latency. Furthermore, re-transmissions may be unable to mask the unreliability of wireless links and message losses are observed. Therefore, the Quality of Experience (QoE) perceived by the user is reduced. Our objective is to use some link quality metrics to predict the link quality using machine learning methods. The expected benefit of using link quality prediction being to anticipate link breakages and route changes before loosing packets. It should result in a better QoE provided by the network.

Link quality estimation is more complex in IoT networks which may consist of a large number of deployed objects, and whose transmitters/receivers are designed to consume the least possible energy. Aguayo et al. [START_REF] Aguayo | Link-level Measurements from an 802.11b mesh network[END_REF] showed that such transmitters/receivers are more exposed to external interference and noises, which result in a quality degradation of wireless communication links. In that context, link quality estimation is used to enable sensors to choose the best path for delivering their data to the sink by anticipating link breakages. Efficient link quality estimation that provides a fine grain classification of links are usually based on several link quality metrics [START_REF] Kirubasri | A Study on Hardware and Software Link Quality Metrics for Wireless Multimedia Sensor Networks[END_REF].

Multiple Machine Learning techniques exist. We can distinguish linear ones (e.g. Logistic regression, Linear Support Vector Machine) from non-linear ones (e.g. Support Vector Machine, Random Forest). The aim of this paper is to choose which one is the best one to predict wireless link quality.

II. STATE OF THE ART

In this section, we will first present a brief overview of link quality metrics described in the literature, then we will focus on machine learning techniques that can be used to make predictions in a wireless network.

A. Link quality metrics in IoT

A good link quality metric should ensure stability and accuracy for the used learning technique. The existing metrics we know generally ensure either stability or accuracy, depending on their types, but rarely both.

To estimate the link quality in IoT, we distinguish two types of metrics: hardware-based metrics and software-based metrics. Hardware-based metrics obtain their data directly from the objects (without prior processing). The main hardware-based metrics are [START_REF] Kirubasri | A Study on Hardware and Software Link Quality Metrics for Wireless Multimedia Sensor Networks[END_REF], [START_REF] Baccour | Radio link quality estimation in wireless sensor networks: a survey[END_REF]:

1) Received Signal Strength Indicator (RSSI): most radio transmitters/receivers have an RSSI register, which provides information on the signal strength of the received packet. When there is no transmission, the register gives a background noise. 2) Link Quality Indicator (LQI): This is a proposal of the IEEE 502.15 standard. Its evaluation is specific to the vendor.

LQI can be considered as a measure based on the first eight symbols of the received signal

3) Signal to Noise ratio (SNR): this is given by the difference between the actually received signal (without noise) and the background noise. The accuracy provided by hardware-based metrics is not sufficient because of two main factors: only packets whose transmission succeed are considered and the evaluation does not consider the whole received packet, but only its first symbols.

The software-based metrics are obtained by computation and they can be classified into three categories [START_REF] Baccour | Radio link quality estimation in wireless sensor networks: a survey[END_REF]: 1) Packet Delivery Ratio (PDR): also known as PRR (Packet Reception Ratio) or PSR (Packet Success Ratio), it is obtained by computing the ratio of the number of packets successfully received over the number of transmitted packets. 2) Required Number of Packet Transmission (RNP): this is an emitter-based metric that counts the average number of transmission/re-transmissions required before successful packet reception. It can be computed as the number of packets transmitted and re-transmitted during an observation period, divided by the number of packets received successfully, minus one. 3) Score: some link quality metrics provide link estimations that do not refer to physical phenomena (such as receiving or re-transmitting packets), but instead provide a score or label that is set in a certain rank. There are several ones: Fuzzy Link Quality Estimator (F-LQE), MetricMap, CSI, ... Whatever the metric used to estimate the link quality, some network properties must be preserved, since link quality estimation aims to improve the quality of service provided by the network. So it is important to keep in mind that good link quality estimators for IoT network should contribute to an increase in network throughput, a decrease in packet delivery latency and a higher route stability for data gathering. Therefore, they should improve the user QoE.

B. Machine learning techniques

Machine Learning (ML) is an application of artificial intelligence that provides systems the ability to automatically learn and improve from experience without being explicitly programmed [START_REF]What is machine learning? a definition[END_REF]. Multiple machine learning techniques exist. We distinguish two categories: linear models and non-linear models. In this paper, we will use the Linear Regression model (LR), the Linear Support Vertor Machine (Linear SVM) model, the SVM model and the Random Forest (RF) model. All are well-known models frequently used for classification tasks. LR and Linear SVM are linear models while SVM and RF are non-linear models.

III. PRESENTATION OF THE DATA SET

The data set used in this paper is collected from a Time-Slotted Channel Hopping (TSCH) network. TSCH is a multichannel time-slotted medium access scheme for lower-power and reliable wireless networking solutions in Low-Power Lossy Networks (LLNs) [START_REF] Alexandros | Impact of guard time length on ieee 802.15.4e tsch energy consumption[END_REF]. It has been designed to meet the requirements of industrial applications in terms of latency, reliability and network lifetime. To reduce latency, TSCH takes advantage on the one hand of a multichannel scheme to increase parallelism in transmissions, and on the other hand, of scheduled transmissions to avoid collisions. Furthermore,it implements a channel hopping scheme to mitigate noise and interference, and consequently to enable high reliability [START_REF] Chang | Adaptative synchronization in multi-hop tsch networks[END_REF].

A. How traces have been collected?

Our data set is provided by Mercator [START_REF] Brun-Laguna | Moving Beyond Testbeds? Lessons (We) Learned about Connectivity[END_REF], a combination of firmware and software specifically designed to collect connectivity data sets in testbeds. The same firmware runs on each node in the testbed; a software, running on a computer connected to the testbed, drives the experiment. The firmware allows the software to control the radio of the node, by sending commands to its serial port. The software can send a command to a node to either transmit a frame (specifying the frequency to transmit on), or switch the remote node to receive mode (on a particular frequency). In the receive mode, the node issues a notification to the software each time it receives a frame.

Mercator acts on the Grenoble testbed1 consisting of 50 nodes operating on 16 channels. The test duration is about 48 hours. Collected data are timestamped. On the beginning of the experiment, the first node transmits a burst of 100 frames on the first channel, while all other nodes are in receive mode. Then, this node does the same on all the other channels. After transmitting on all channels, the next node takes over and does the same. This process takes place until all nodes have transmitted.

Measurements are done in transactions. A transaction starts from the transmission of the first frame on the first channel by the first node, to the transmission of the hundredth frame on the last channel by the last node. Each transaction is run in 2 hours 30 minutes and 58 seconds. The data set used has a total of 19 transactions.A frame sent by node A is counted as received by node B if and only if B sends an acknowledgment.

B. Which features have been measured?

The collected data include 108659 measurements of the Packet Delivery Ratio (PDR) and the Average Received Strengh Indicator (RSSI).

Let A be the sender and B the receiver on a given channel for a transaction t.

P DR t (A → B) = N um.

of acks sent by B N um. of f rames sent by A

Therefore, the PDR of a node for a transaction t, on a given channel is between 0 and 1 (P DR t (A B ) ∈ [0, 1]: 0 if no acknowledgment is sent by B and 1 if B sends 100 acknowledgments.

RSSI avgt (A → B) = N um. of f rames sent by A i=1 rssi i N um.

of f rames sent by A

Where rssi i represents the RSSI of the i th frame received by B on the channel considered. The RSSI values are less than 0 in all the cases. The data set is pre-processed as follows: if no frame is received by B, the corresponding RSSI will be set to the lowest value of collected RSSIs minus one.

Since the PDR values are expressed as a ratio, they have no unit, whereas the average RSSI values are given in dBm. In the following, we write PDR to designate P DR t (A → B) and RSSI to designate RSSI avgt (A → B).

C. Statistical elements of the data set

The PDR and RSSI statistical elements are summarized in Table I. This table shows that we can use machine learning in our context, since the size of data (population) is important. We also note that there is a significant variation on both PDR and RSSI when we look at their min and max values. So, since ML models need data from different classes to make accurate predictions, we can expect to have fine predictions when using these metrics. IV. HOW TO PREDICT Machine learning models need to train themselves before being able to predict with a good accuracy. The data set used for predictions is split in two sets: a test set and a training set. The training set consists of labeled data used to train the ML model and increase prediction accuracy, whereas the test set contain data that the trained ML model may have never seen before, and which are used to measure how robust its predictions are. In our experiments, the split ratio is 75% for the training set and 25% for the validation set, as usual [START_REF] Venkatesh | What is training data, really[END_REF].

Since the wireless network considered operates on 16 channels and the quality of a wireless link depends on the channel considered as shown by Figures 1 and5, we predict the quality of any link on each of the 16 channels, independently.

For each link and each channel, we split the data set into a training set and a test set; we then train the model over the training set and predict the link quality on the channel considered for the samples in the test set. By comparing the predicted set with the real set, the confusion matrix is computed by evaluating the true-positive, the true-negative, the false-positive and the false-negative for the link and channel considered. The confusion matrix for the link is obtained by summing the confusion matrices obtained for that link on all the 16 channels. As usual, the accuracy of the link prediction is equal to the sum of the number of true-positive and the number of true-negative, divided by the total number of samples considered for this link.

We then compute the confusion matrix for all links by summing the confusion matrices obtained for each link and evaluate the accuracy of the ML technique as previously. Programs written for our experiments are available online2 .

V. COMPARISON OF ML TECHNIQUES USING RSSI RSSI is a simple hardware metric able to provide a quick and accurate estimate of whether a link is of good quality or not, according to the power of signal received by a node [START_REF] Baccour | Radio link quality estimation in wireless sensor networks: a survey[END_REF]. Fig. 1 depicts the evolution of RSSI values on a network link (Link 1 ). There is no signal in channel 22, while the majority of channels have constant RSSI values. Moreover, the signal on channel 21 is of short duration compared to the simulation duration. We also notice that Link 1 has very low RSSI values, close to the minimum.

A. Definition of classes for the prediction using RSSI

Since the PDR value of a link has a direct impact on link performance (e.g. number of retransmissions), we draw the waterfall plot [START_REF] Brun-Laguna | Moving Beyond Testbeds? Lessons (We) Learned about Connectivity[END_REF] in Fig. 2, which depicts the pairs (PDR, RSSI) for all the samples in the data set. We compute the median RSSI value associated with the PDR values of 0.75 and 0.3 considered as good and bad values, respectively to deduce the RSSI thresholds associated with each class, leading to the RSSI values of -85 dBm and -87 dBm, respectively. Hence, we define three classes for prediction using the RSSI feature:

• A link is considered as Good if its RSSI value is greater than or equal to -85 dBm;

• If the RSSI is less than or equal to -87 dBm, we consider the link as Bad;

• Otherwise (-87 < RSSI < -85 dBm), we consider the link as Intermediate.

B. Results of predictions based on RSSI over Link 1

Fig. 3 depicts the confusion matrices applied to the RSSI feature and obtained with LR, Linear SVM, SVM and RF, respectively. These confusion matrices correspond to the prediction on Link 1 (Fig. 1). For this link, the Random Forest (RF) classifier has the highest prediction accuracy, followed by SVM classifier, Logistic Regression and Linear SVM, respectively. Notice that SVM is too optimistic by classifying 24% of intermediate links as good ones.

C. Prediction based on RSSI over all the links

To obtain a more general result for the RSSI feature, we make prediction over all the network links according to the principle given in Section IV. The corresponding confusion matrices depicted in Fig 4 show that RF has the highest accuracy (99.5%), followed by SVM (98.4%), Logistic Regression (96.4%) and Linear SVM (95.5%) respectively. Unlike Random Forest which classifies practically all the links in their respective classes, Linear Regression classifies up to 11.8% of good links as intermediate and 0.3% of good links as bad ones, which can prevent the use of good links. More penalizing for network performance, the Linear SVM classifies 11% of bad links as intermediate and 5.2% as good (this last case can strongly impact packet delivery since worse links are classified as good).

Thereby, we conclude that the Random Forest classifier is the suited model to use when predicting link quality in a TSCH network using the RSSI feature.

However, the RSSI metric is only measured for successfully received packets. Therefore, when a radio link suffers from excessive packet losses, the RSSI metric may overestimate the link quality by not considering the information of lost packets [START_REF] Baccour | Radio link quality estimation in wireless sensor networks: a survey[END_REF], [START_REF] Fonseca | Four bit wireless link estimation[END_REF], [START_REF] Gomez | Impact of lqi-based routing metrics on the performance of a one-to-one routing protocol for ieee 802.15.4 multihop networks[END_REF].

VI. COMPARISON OF ML TECHNIQUES USING PDR

Re-transmissions of packet in the network significantly decrease the node energy and consequently the network lifetime. PDR enables to determine the average number of packets that need to be re-transmitted to reach their destination. Still considering Link 1 used before, Fig 5 presents the evolution of PDR over time on all the channels.

With regard to the evolution of PDR values over the sixteen channels of Link 1 (Fig 5), many channels (13, 14, 15, 24) move permanently from lower to higher values. Channel 22 does not have any PDR value while channel 21 just has PDR values for a short period. The other channels have either good or Bad PDR values.

A. Definition of classes for prediction using PDR

We define tree classes of link quality for PDR feature:

• A link is of Good quality if its PDR is greater than or equal to 0.75; • If the PDR is less than or equal to 0.3, we consider the link is of Bad quality;

• Otherwise (0.3 < P DR < 0.75), we consider that it is a link of Intermediate quality. As shown in Fig. 6, the Random Forest classifier has the highest accuracy followed by Logistic Regression, SVM and Linear SVM classifier, respectively.

B. Predictions based on PDR for

C. Prediction based on PDR over all the links

Results of prediction over all the links, and based on PDR metric are presented in Fig 7 .  The Random Forest classifier outperforms the other models with an accuracy of 99.3%. It is followed by Linear SVM (96.9%), SVM (96.4%) and Logistic Regression (95.3%), respectively.

Linear regression classifies up to 14.8% of good links as intermediate and 0.3% as bad ones, which can prevent the use of good links. Linear SVM classifies 8.2% of good links as bad and 4% of bad link as good (this prevents the use of good links whereas bad links can be used, leading to a decrease in QoE).

The Random Forest classifier is then recommended to use when making prediction using the PDR feature in TSCH networks. Although it has the best accuracy, Random Forest classifier predicts 2.8% of good links as bad and 0.9% of bad links as good. This eventually decreases the QoE offered by the network.

We believe that compared to the predictions based on RSSI, the predictions based on PDR are more reliable since PDR considers all the packets sent on the link, whereas RSSI only considers successfully received packets. It would also be interesting to investigate the predictions based on both PDR and RSSI to take advantages of both metrics. By doing so, we would be able to solve one of the challenges pointed by Baccour et al. [START_REF] Baccour | Radio link quality estimation in wireless sensor networks: a survey[END_REF], which said that predicting link quality is to find an optimal trade-off between the stability of the link quality estimator and the ability to cope with link quality dynamics.

VII. IMPROVED PREDICTION USING BOTH PDR AND RSSI

To have an efficient link quality estimation which provides fine grain classification of links, we jointly use the PDR and RSSI metrics. The goal is to study whether combining these two metrics, a software metric and a hardware metric, may provide a more accurate prediction. However, as the PDR metric takes into account all the sent packets and not only the received ones as RSSI does, the PDR metric is considered as the first criterion.

A. Definition of classes using PDR and RSSI

The classes we define for the prediction using the two metrics are given in Table II.

C. Prediction based on PDR and RSSI over all the links

Prediction on all the links using both PDR and RSSI has also been done, and results are presented in Fig 9.

With PDR+RSSI, RF has the highest accuracy (98.3%), followed by Logistic Regression (96.1%), SVM (95.8%) and linear SVM (94%), respectively.

From all the results presented in this paper, we conclude that among the ML techniques tested, RF provides the best accuracy, whatever the metric used. The question is now, which is the best metric to use with RF? RF with PDR predicts 2.8% of Good links as Bad whereas RF with PDR+RSSI predicts only 0.1% of Good links as Bad and does not predict any Bad link as Good. Such prediction errors may significantly decrease the QoE of the network, since Good links will not be used, while Bad links predicted Good will be used. Furthermore, Fig. 10 depicts the percentage of links per class. It shows that PDR+RSSI recognizes the highest number of Good links and the highest number of Bad links. That is why it is preferred, even if the accuracy of RF wih PDR (99.3%) is greater than the one using both PDR and RSSI (98.3%).

VIII. CONCLUSION

In this paper, we propose to predict link quality in TSCH networks supporting IoT applications. We studied two link quality estimators: a hardware one, RSSI, and a software one, PDR. We compared the accuracy provided by different machine learning techniques, namely Logistic Regression, Linear Support Vector Machine, Support Vector Machine and Random Forest classifier. Whatever the link quality estimator used, RSSI, PDR or both, the Random Forest (RF) classifier model outperforms the other models.

Since using Bad links that have been predicted Good strongly penalizes network performance in terms of end-to-end latency, end-to-end reliability and network lifetime, the joint use of PDR and RSSI improves the accuracy of link quality prediction. Hence, we recommend to use the Random Forest classifier applied on both PDR and RSSI metrics. As a further work, we plan to use the link quality prediction presented in this paper to improve the clustering protocol of motes in an IoT network.

Fig. 1 :

 1 Fig. 1: RSSI evolution over time for Link 1 .

Fig. 2 :

 2 Fig. 2: Values of RSSI and PDR for the data set considered.

Fig. 3 :

 3 Fig. 3: Confusion matrix with RSSI on Link 1 .

Fig. 4 :

 4 Fig. 4: Confusion matrix with RSSI on all the Links.

Fig. 5 :

 5 Fig. 5: PDR evolution over time of Link 1 .

Link 1 Fig 6 Fig. 6 :

 166 Fig 6 presents the confusion matrices resulting from the prediction using LR, Linear SVM, SVM and RF on Link 1 .

Fig. 7 :

 7 Fig. 7: Confusion matrix with PDR on all the Links.

Fig. 8 :

 8 Fig. 8: Confusion matrix with PDR and RSSI on Link 1 .

Fig. 9 :

 9 Fig. 9: Confusion matrix with PDR and RSSI on all the Links.

Fig. 10 :

 10 Fig. 10: Percentage of links per class.

TABLE I :

 I PDR and RSSI statistical elements.

TABLE II :

 II Classes defined using both PDR and RSSI. A link is of Good quality if its PDR is greater than or equal to 0.75;• if its PDR is less than or equal to 0.3, the link is considered as being of Bad quality; It is also Bad if its RSSI is less than or equal to -87. This last case is the only difference with the classification based on PDR only. and its PDR is between 0.3 and 0.75. • Otherwise, the link is considered as being of Intermediate quality.B. Predictions based on both PDR and RSSI for Link 1Results of predictions using LR, Linear SVM, SVM and RF are shown in Fig8for Link 1 . The accuracy of RF is the highest. It is followed by SVM, Linear SVM and Logistic Regression, respectively.

•

https://www.iot-lab.info/deployment/grenoble/

https://github.com/miguelfoko/LinkQuality


Christian Doczkal

Damien Pous

Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq *

Keywords: Graphs, Treewidth, Algebra, Rewriting, Coq ACM Reference

The labeled multigraphs of treewidth at most two can be described using a simple term language over which isomorphism of the denoted graphs can be finitely axiomatized. We formally verify soundness and completeness of such an axiomatization using Coq and the mathematical components library. The completeness proof is based on a normalizing and confluent rewrite system on term-labeled graphs. While for most of the development a dependently typed representation of graphs based on finite types of vertices and edges is most convenient, we switch to a graph representation employing a fixed type of vertices shared among all graphs for establishing confluence of the rewrite system. The completeness result is then obtained by transferring confluence from the fixed-type setting to the dependently typed setting.

CCS Concepts • Theory of computation → Equational logic and rewriting; Type theory; • Mathematics of computing → Graph theory.

Introduction

In graph theory, the notion of treewidth [START_REF] Diestel | Graph Theory[END_REF] of a graph measures how close a graph is to a forest. In particular, the graphs of treewidth at most one are just the forests. Among the open problems related to treewidth, there is the question of finding finite axiomatisations of isomorphism for graphs of a given treewidth [5, page 118]. This question was recently answered positively for multi-graphs of treewidth at most two [START_REF] Cosme | K 4 -free graphs as a free algebra[END_REF], in the following way. A 2pdom-algebra is an algebra over the following signature, subject to eleven equational axioms:

Σ = {• 2 , ∥ 2 , (_ • ) 1 , dom 1 , 1 0 }
Graphs form an algebra for this signature, and a term u over this signature makes it possible to denote a graph g(u). For instance, the graphs of (a A first important result is that Σ-terms make it possible to denote precisely the class of connected graphs of treewidth at most two. That the graph of a term is connected and has treewidth at most two is relatively easy; the converse direction-every connected graph of treewidth at most two can be represented by a term-is much harder [START_REF] Cosme | K 4 -free graphs as a free algebra[END_REF]. This result was recently formalized in Coq [START_REF] Doczkal | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs[END_REF], by going through the well-known characterization of treewidth at most two graphs as those excluding K 4 as a minor [START_REF] James | Topology of series-parallel networks[END_REF].

We also have that graphs modulo isomorphism form a 2pdom-algebra: the eleven axioms of 2pdom-algebra (Fig. 1 below) are all valid in the algebra of graphs. While a pen and paper proof is relatively easy, formalizing it in a proof assistant is non-trivial: it requires proper tools for combining graphs (to get the algebra of graphs) and for reasoning about graphs obtained by nested quotients and disjoint unions (to get the laws). This was also formalized in Coq [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF].

As a consequence, for all terms u, v which can be proved equal using the 2pdom-axioms, g(u) and g(v) are isomorphic. The converse implication also holds: 2pdom-axioms are complete w.r.t. graph isomorphisms, so that (connected, treewidth at most two) graphs actually form the free 2pdomalgebra. Formalizing this completeness theorem in Coq is the main contribution of the present paper.

This theorem is difficult because it must translate a rather global notion (an isomorphism between two graphs) into a sequence of local reasoning steps (an equational proof from 2pdom-axioms). The result was first proved in [START_REF] Cosme | K 4 -free graphs as a free algebra[END_REF]. We hoped to formalize this proof in Coq [START_REF] Doczkal | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs[END_REF] until we realized an alternative proof could be used [START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF]. The alternative proof is much easier from the graph-theoretical point of view: it does not require a precise analysis of the structure of treewidth at most two graphs. Instead, it relies on a graph rewrite system that is terminating and confluent up to 2pdom-equivalence. By using Newman's lemma to prove confluence via local confluence, the starting global isomorphism is only analyzed locally in the proof. This is the proof we follow in the present formalization [START_REF] Doczkal | Coq formalization accompanying this paper[END_REF]; we give a more precise sketch of it in Section 3. That this proof is simpler does not mean it is easy to formalize in a proof assistant: it involves both local and global operations on graphs, and the local confluence proof, which is already long on paper, requires good abstractions to avoid getting lost in the details.

x ∥ (y ∥ z) = (x ∥ y) ∥ z x ∥ y = y ∥ x 1 ∥ 1 = 1 x • (y • z) = (x • y) • z x • 1 = x x •• = x (x ∥ y) • = x • ∥ y • (x • y) • = y • • x • dom(x ∥ y) = 1 ∥ x•y • dom(x • y) = dom(x • dom(y)) dom(x) • (y ∥ z) = dom(x)•y ∥ z
In order to define the rewrite system and prove most of the required results about it (Sections 4 to 7), we need to slightly generalize the letter-labeled graphs from [START_REF] Doczkal | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs[END_REF][START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF] to allow for a uniform treatment of both letter-labeled graphs (used in the statement) and 2pdom-labeled graphs (used for the rewrite system). However, even the generalized representation turned out to be inappropriate for getting a formal proof of local confluence. We circumvent this difficulty by using a second representation for graphs and rewrite steps for this part of the proof. This second representation makes it possible to prove local confluence in a natural way, as with pen and paper, by organizing case distinctions as most appropriate and using 'without-loss-of-generality' reasoning to factor out similar cases (Section 8). We then establish correspondence between our two representations (Section 9), allowing us to transfer local confluence from the second representation to the first and wrap everything together.

2pdom-Algebras

We first recall the definition and basic properties of 2pdomalgebra [START_REF] Cosme | K 4 -free graphs as a free algebra[END_REF][START_REF] Pous | Allegories: decidability and graph homomorphisms[END_REF]. We consider the signature from the introduction for terms and algebras. We sometimes omit the • symbol and we assign priorities so that the expression (x • (y • )) ∥ z can be written just as xy • ∥ z. Definition 2.1. A 2pdom-algebra is a Σ-algebra satisfying the axioms from Fig. 1. Definition 2.2. An element x of a 2pdom-algebra is called a test if x ∥ 1 = x. We let α, β, . . . range over such tests.

G • H := G H G ∥ H := G H G • := G dom(G) := G 1 := a := a Figure 2. Graph operations.
Note that 1 is a test, as well as dom(x), for all x.

Lemma 2.3. For all tests α, β in a 2pdom-algebra, we have

α • = α α β = α ∥ β = βα
We deduce from the second equation that α β is a test, and that tests with • and 1 form a commutative monoid.

We fix an alphabet A and let a, b, . . . range over the letters in A. We let u, v . . . range over Σ-terms with variables in A, which we call terms in the sequel. For terms u and v, we write u ≡ v when the equation is derivable from the axioms of 2pdom-algebras (equivalently, when the equation universally holds in all 2pdom-algebras). Terms quotiented by this relation form the free 2pdom-algebra over A.

Sketch of Completeness Proof

We now sketch the completeness proof from [START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF], delegating most of the formal definitions to the subsequent sections.

We consider directed multigraphs with two designated vertices respectively called input and output, and edges labeled in A. We just call them graphs. Examples of such graphs were given in Section 1, where inputs and outputs were depicted using unlabeled ingoing and outgoing arrows.

Graphs form a 2pdom-algebra by considering the operations in Fig. 2. The binary operations (•) and ( ∥ ) respectively correspond to series and parallel composition, converse (_ • ) just exchanges input and output, and domain (dom) relocates the output to the input. Proposition 3.1 (Soundness). Graphs form a 2pdom-algebra.

By interpreting a letter a ∈ A as the graph a in Fig. 2, we can associate a graph g(u) to every term u (cf. rest of Fig. 2).

Note that the parallel composition of a graph with the graph 1 merges the input and output of the former graph. For instance, the graph a ∥ 1 consists of a single vertex with a self-loop labeled with a. We have that a term u is a test if and only if the input and output of g(u) coincide [8, Lemma 10].

By Proposition 3.1, g(u) and g(v) are isomorphic whenever u ≡ v. A formal proof of this soundness result is described in [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF]. We slightly generalize it in the present work (Proposition 5.2 below), but our main contribution is a formal proof that the converse implication also holds: the axioms of 2pdom-algebra are complete w.r.t. graph isomorphism: Theorem 3.2 (Completeness). For all terms u, v such that g(u) and g(v) are isomorphic, we have u ≡ v.

As explained in the introduction, the key idea in the proof from [START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF] consists in using a graph rewrite system. This system is not used to obtain canonical normal forms. Instead, it makes it possible to recover various terms denoting a given graph, and its confluence makes it possible to relate those terms via the axioms.

The rewrite system works on a generalization of the previous graphs, where vertices are labeled with tests and edges are labeled by terms rather than letters. Its main rules are the following ones:

u v α → uαv u α β → α dom(u β ) u v → u ∥ v
(The circular vertices, i.e., those that are removed, must be distinct from input and output and must not have other incident edges.) Its behavior is reminiscent from the stateremoval algorithm used to construct a regular expression from an automaton: vertices and edges are removed until we obtain a small graph, from which we can read back a term.

For instance, we have the following sequence of rewrite steps, which witnesses the fact that a•dom(b)•c ∥ d is a term denoting the starting graph. Note that the rewrite system is non-deterministic: one of the most trivial examples is that we could also obtain the term d ∥ a•dom(b)•c from the above graph. It is however confluent modulo a generalized notion of isomorphism where labels are compared using the relation ≡. Proving this property is one of the key steps of the completeness proof.

Also note that there are terms which cannot be reached via the rewrite system. Consider for instance, the reduction below, which gives us the term (dom(a)•dom(b))•c for the first graph: All in all, the completeness proof is obtained by combining the following three key properties:

(i) for all u, u ≡ u ↓ (ii) for all u, g(u) → * g ′ (u ↓ ), where for a normalized term v, g ′ (v) is the small irreducible graph labeled with v.

(iii) → is confluent modulo generalized isomorphism
The first one is a syntactic property proved by induction on u, whose formalization requires some work but does not raise any problem (induction and equational reasoning have very good support in proof assistants).

The second one, reducibility, is also proved by induction on u, but requires much more work: we have to prove that rewrite steps are preserved under the various algebraic operations, and that there are enough rewrite rules to effectively reduce every graph of a term into a small irreducible graph.

To prove the third property, we use Newman's lemma to reduce confluence to local confluence. We then have to analyze all critical pairs and show that they can all be joined modulo isomorphism and 2pdom axioms. This is the most delicate step for the formalization: we have to analyze many cases, and in each case we need to produce appropriate rewrite steps and isomorphisms.

Once we have proved those three properties, completeness is obtained as follows.

Proof of Theorem 3.2. Starting from two terms such that g(u) and g(v) are isomorphic, we know by reducibility (ii) that g(u) → * g ′ (u ↓ ) and g(v) → * g ′ (v ↓ ). Since the graphs g ′ (u ↓ ) and g ′ (v ↓ ) are irreducible, we deduce by confluence (iii) that they are isomorphic (modulo the axioms), from which we deduce u ↓ ≡ v ↓ . We conclude that u ≡ v by transitivity, using (i) twice. □

Packaged Labeled Multigraphs

We now describe the formalization of labeled multigraphs. As explained above, we need two kinds of graphs: graphs with unlabeled vertices and edges labeled in A for the overall completeness result, as well as graphs with test-labeled vertices and term-labeled edges as an intermediate data-structure.

In order to share code and define the various operations on those two classes of graphs at once, we introduce the following abstraction for labels, which we explain below: Definition 4. We usually omit the indices on equivalence relations, if they can be inferred from the context. We use setoids for labels since we want to instantiate these labels with tests and terms, compared modulo the axioms of 2pdom-algebra.

We require a commutative monoid on vertex labels because one of the most crucial operations in our development is that of forming vertex-quotients of graphs (i.e., collapsing the vertices of a graph with respect to some equivalence relation): collapsed vertices get labeled with the composition in the monoid of their initial labels.

The last requirement is motivated as follows. In order to express the rewrite system succinctly and to enable more opportunities to reason by symmetry, it is convenient to consider a notion of isomorphism on term-labeled graphs where edges can be flipped, using the converse operation to update the label: an edge from x to y labeled with u can be seen as an edge from y to x labeled with u • . In contrast, such an operation should not be allowed on letter-labeled graphs (there is no converse operation on the alphabet).

Using the relation ≡ ′ e makes it possible to capture those two cases. We will define isomorphisms such that a u labeled edge from x to y can be mapped to a v labeled edge from y to x provided u ≡ ′ e v. The requirements on this relation ensure that we obtain an equivalence relation on graphs when doing so. The two label structures below capture the two aforementioned cases. Definition 4.2 (The alphabet A as a label structure). The trivial monoid (on the single element type unit), together with the discrete setoid on A (i.e., with Leibniz equality), and the empty relation on A for ≡ ′ , form a label structure. Definition 4.3 (2pdom-algebras as label structures). For every 2pdom-algebra X , we have a label structure with X as edge-labels, tests as vertex-labels, and x ≡ ′ e y := x ≡ y • . We fix a label structure L with setoids (L v , ≡) and (L e , ≡) for the rest of this section and the following one. We write x : G to denote that x is a vertex of G.

4.4 (Graph). An (L-labeled directed multi-) graph is a structure G = ⟨V , E, p, l v , l e ⟩, where • V is a finite type of vertices • E is a finite type of edges • p : B → E → V is
Note that self-loops are allowed, as well as parallel edges with the same label. Representing the source and target functions for edges using a single function allows us to avoid code duplication at several places: this pieces of information are often handled in a uniform way.

In order to define sequential and parallel composition (cf. Fig. 2), we rely, as in [START_REF] Doczkal | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs[END_REF][START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF], on the following two operations: disjoint union and (vertex-)quotients.

Definition 4.5. Let G=⟨V , E, p, l v , l e ⟩ and G ′ =⟨V ′ , E ′ , p ′ , l v ′ , l e ′ ⟩. The disjoint union of G and G ′ , is the graph G + G ′ := ⟨V + V ′ , E + E ′ , p + p ′ , l v + l v ′ , l e + l e ′ ⟩ Here, f + f ′ (for f ∈ {p, l v , l e }) is the pointwise lifting of f and f ′ to the sum type E + E ′ or V + V ′ with results in V + V ′ , L v , or L e ).
In order to define quotients on graphs we exploit that finite types are closed under taking quotients. If ≈ : X → X → B is a boolean equivalence relation on some finite type X , the quotient [START_REF] Cohen | Pragmatic Quotient Types in Coq[END_REF] of X with respect to ≈, written X /≈ , is a finite type as well. The type X /≈ comes with functions π : X → X /≈ and π : X /≈ → X such that π (π x) = x for all x : X /≈ and π (π x) ≈ x for all x : X . Definition 4.6. Let G=⟨V , E, p, l v , l e ⟩ and let ≈ :

G → G → B be an equivalence relation. The quotient of G modulo ≈, written G /≈ , is the graph ⟨V /≈ , E, λbe. π (p b e), l v ′ , l e ⟩
where l v ′ := λx .

(y:V |π y=x ) l v y gathers in every equivalence class (i.e., every vertex of the new graph) all the vertex labels of the vertices in the class.

In addition to those global operations for the algebra of graphs, we need the following local operations to define the rewrite system: Definition 4.7. Let G be a graph and let x, y : G, α, β : L v , and u : L e . We write:

• 1 α for the edge-free graph with one α-labeled vertex.

• 2

β α := 1 α + 1 β (a graph with only two vertices). • G ∔ α := G + 1 α (G with an additional vertex). • G ∔ [x, u,
y] for G with an additional u-labeled edge from x to y.

• u

β α := 2 β α ∔ [in l * , u, in r * ]
(a graph with a single edge between two distinct vertices).

• G[x ← α] for G where x is labeled with α ⊗ l v x (i.e, α is combined with the existing label of x).

Note that for all these graph operations (both the local ones and the global ones), working in Coq with a representation of graphs closely following Definition 4.4 is extremely convenient: it is compact, and all basic invariants are nicely enforced via (dependent) types. Moreover, the mathematical components library [18] provides all the required infrastructure for taking disjoint unions and quotients on finite types.

Given b : B, we define u

≡ [b] v to be u ≡ v if is b = false, and u ≡ ′ v if b = true.
This allows us to define isomorphisms as follows:

Definition 4.8. Let F =⟨V , E, p, l v , l e ⟩ and G=⟨V ′ , E ′ , p ′ , l v ′ , l e ′ ⟩ be graphs. A homomorphism from F to G consists of three functions h v : V → V ′ , h e : E → E ′ , and h d : E → B such that 1. for all e : E, b : B, p ′ b (h e e) = h v (p (h d e ⊕ b) e).
2. for all y : V ′ , l v ′ y ≡ (x |h v x =y) l v x; 3. for all e : E, l e ′ (h e e) ≡ [h d e] l e e. An isomorphism is a homomorphism where h v and h e are bijections. In this case, the second condition simplifies to l v ′ (h v x) ≡ l v x for all x : V . We denote the type of isomorphisms between graphs F and G by F ≃ G.

Intuitively, the h d predicate in a homomorphism indicates whether the homomorphism flips a given edge or not. If an edge e is flipped, the vertex component h v should map the source of e to the target of h e e and vice versa, whence the use of a boolean xor operation in the first requirement. Accordingly, the labels of the two edges should be related by ≡ ′ rather than ≡ when an edge is flipped (third requirement).

Note that the notion of isomorphism depends on the label structure. When the label structure L is the one from Definition 4.2, h d must be the constantly false function (because of the third condition), and the second condition vanishes since all vertices are labeled with the unique value of type unit; therefore, we recover in this case a standard definition of non-edge-flipping isomorphism on edge-labeled multigraphs [START_REF] Doczkal | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs[END_REF][START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF]. Fact 4.9. Graph isomorphism is an equivalence relation.

We remark that Definition 4.8 formalizes the computational notion of isomorphism rather the property of two graphs being isomorphic. This is crucial for a compositional treatment of isomorphisms. To see this, consider the graph expression F ∔ [x, u, y] and the operation of replacing F with an isomorphic graph G. This requires to also replace the vertices x and y with their respective images under the vertex component of the isomorphism. This approach is thus required in order to state (and prove) the two congruence properties below. (In the following, when an isomorphism h : F ≃ G appears as a function, it is to be taken as the underlying vertex component h v .) Lemma 4.10. Let F, G be graphs and let h :

F ≃ G. • F ∔ [x, u, y] ≃ G ∔ [h x, u, h y] • F [x ← α] ≃ G[h x ← α]
Concretely in Coq, formalizing the isomorphisms in such a computational way requires us • to place the definition in Type rather than Prop,

• to express that functions are bijective using explicit inverses (here we build on a small library where we encapsulate computational bijections between types), • to make sure that whenever we define an isomorphism, we make it either transparent so that its computational content is immediately available, via reduction, or we prove appropriate equations about it before making it opaque for reduction. Like in [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF], we prove the following properties about the global operations of union and quotient: Lemma 4.11 (Generalization of [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF]Lem. 6.6]). For all multigraphs F, F ′ , G, G ′ , H , we have: is its restriction to F , and for all x : G there exists y : F with in r x ≈ in l y.

1. F + G ≃ G + F and F + (G + H ) ≃ (F + G) + H . 2. If F ≃ G and F ′ ≃ G ′ , then F + F ′ ≃ G + G ′ . 3. If ≈, ≈ ′ are two pointwise equivalent equivalence rela- tions on (the vertices) of F , then F /≈ ≃ F /≈ ′ . 4. If F ≃ G then F /≈ ≃ G /≈ ′ ,
These lemmas allow us to extrude quotients out of unions and to simplify quotients [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF]. The generalization to vertexlabeled graphs requires us to verify that vertex labels are collected in a consistent way by the quotient operation (Definition 4.6). While we use ssreflect notations for the 'bigops' operation appearing in this definition, we have to reprove various laws since we only have a monoid structure up to a setoid equality. The generalization to edge-flipping isomorphisms is harmless: the concrete isomorphisms (the first, third, and last three items) do not use this opportunity, and the remaining congruence properties just forward this piece of information.

In addition, we prove a series of basic isomorphisms about interactions between the various operations. We list a few of them below. Together with Lemma 4.11 these properties allow us to reason algebraically and compositionally when we have to prove isomorphisms between graphs. The situation is however not as satisfactory as with standard equational reasoning: the type dependency in congruence lemmas (e.g., Lemma 4.10) prevents us from using standard tools like 'setoid rewriting' so that we generally have to apply these congruence lemmas manually. Lemma 4.12. For all graphs F, G, we have

• F ∔ [x, u, y] ≃ F ∔ [y, v, x] whenever u ≡ ′ v, • F ∔ [x, u, y] ∔ [z, v, t] ≃ F ∔ [z, v, t] ∔ [x, u, y], • F ∔ [x, u, y][z ← α] ≃ F [z ← α] ∔ [x, u, y], • F ∔ [x, u, y] + G ≃ (F + G) ∔ [in l x, u, in l y], • (F ∔ [x, u, y]) /≈ ≃ F /≈ ∔ [πx, u, πy].
We also prove the following lemma, allowing us to provide an explicit representation for a given quotient graph. We shall see in Section 7 that this makes it possible to prove some concrete isomorphisms by reasoning globally at places where the compositional approach is less convenient. Lemma 4.13. Let G and H be graphs and let ⟨h v , h e , h d ⟩ be a homomorphism from G to H with h v surjective and h e bijective. Then G /≈ ≃ H , where ≈ is the kernel of h v (i.e., x ≈ y iff h v x = h v y).

The 2pdom-Algebra of Graphs

In order to obtain a Σ-algebra, we need to work with twopointed graphs: The notions of homomorphism and isomorphism are extended accordingly: on 2p-graphs, they should map the input to the input, and likewise for the outputs. We write F ≃ 2 G when two 2p-graphs F and G are isomorphic. The local operations are extended to 2p-graphs in the obvious way, and we overload the notations for these operations.

We can now give a formal definition for the Σ-operations on 2p-graphs (Fig. 3, where R eqv is the equivalence closure of a binary relation R). This is the same definition as in [START_REF] Doczkal | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs[END_REF][START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF] except that it is generalized to graphs over an arbitrary label structure; the way vertex labels are handled is completely hidden in the definition of the quotient operation on graphs (Definition 4.6). Accordingly, since we have generalized [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF]Lem. 6.6] to L-labeled graphs (Lemma 4.11), the formal proof [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF] of Proposition 3.1 smoothly scales into a proof of the following generalization: Proposition 5.2. For every label structure L, 2p-graphs over L form a 2pdom-algebra.

We finally define the function g interpreting terms into graphs. There are actually two such functions: • the one from Theorem 3.2, which interprets a term as a letter-labeled graph, i.e., a graph over the label structure from Definition 4.2. This is the unique Σhomomorphism g A such that g A (a) = a * * for all letters a ∈ A, where * : unit is the only allowed vertex-label.

⟨G, ι, o⟩ • ⟨G ′ , ι ′ , o ′ ⟩ := ⟨(G + G ′ ) /≈ , π (in l ι), π (in r o ′ )⟩ where ≈ := {(in l o, in r ι ′ )} eqv ⟨G, ι, o⟩ ∥ ⟨G ′ , ι ′ , o ′ ⟩ := ⟨(G + G ′ ) /≈ , π (in l ι), π (in r o ′ )⟩ where ≈ := {(in l ι, in r ι ′ ), (in l o, in r o ′ )} eqv
• the one used in the reducibility statement for the rewrite system, which produces a term-labeled graph, i.e., a graph over the label structure from Definition 4.3 applied to the 2pdom-algebra of terms. This is the unique Σ-homomorphism g T such that g T (a) = â1 1 for all letters a ∈ A, where 1 is the term 1 seen as a test, and â is the letter a seen as a term. Since we proved that both algebras of graphs are 2pdomalgebras (Proposition 5.2), we get that u ≡ v entails g(u) ≃ 2 g(v) for both functions. However, the completeness proof we sketched in Section 3 only gives us a proof of completeness with respect to g T . To get completeness with respect to g A , we build on the following lemma:

Lemma 5.3. If g A (u) ≃ 2 g A (v) then g T (u) ≃ 2 g T (v).
Proof. Follows from relabelings between two label structures being Σ-homomorphisms and preserving isomorphisms. □ We only work with g T in the sequel; we abbreviate it as g.

Rewrite System

We now present the graph rewrite system we use to establish completeness of the axioms in Fig. 1. The rewrite system rewrites 2p-graphs labeled with elements of an arbitrary 2pdom-algebra X1 which we fix in this section.

An informal description the rules is given in Fig. 4. A key intuition about these rules, which does not need to be formalized, is the following. First observe that if X is itself an algebra of 'basic' graphs, so that we have graphs labeled with basic graphs, then one can expand a graph into a basic graph by 'replacing' the edges and vertices by their labels. (In fact, the construction of the previous section is a monad in the category of 2pdom-algebras, where multiplication is given by expansion.) The key intuition is that isomorphisms and rewrite rules preserve expansions: if F ≃ 2 G or F → G then the expansions of F and G are isomorphic (as basic graphs) 2 . This is consistent with the analogy given in Section 3 about state-removal procedures for extracting regular expressions out of finite automata: there, the automata are rewritten through local operations that preserve the overall language.

(V0) α → (V1) u α β → α dom(u β ) (V2) u v α → uαv (E1) u α → α (u ∥ 1) (E2) u v → u ∥ v
It is important here that we work modulo edge-flipping isomorphisms. For instance, the following step is an instance of rule (V2) modulo such isomorphisms:

u v α → u • αv
If we were not doing so, we would need two variants of rule (V2) (the one above and the symmetric one), as well as a variant of rule (V1) and a variant of rule (E2). We would thus move from five to nine cases in each case analysis on steps, and from 15 to 45 cases in the local confluence proof. Alternatively, we could add a rule to flip an arbitrary edge. But such a rule is not terminating so that it would prevent us from using Newman's lemma for proving confluence. (All other rules remove either an edge or a vertex, so that the system we use is obviously terminating.) Remark 6.1. Rule (V0) deserves some explanation, as it is not included in [START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF]. Note that graphs of the shape д(u) are always connected and that the rewrite system never disconnects connected graphs. Consequently, rule (V0) will never apply when starting from the graph of a term. We include the rule because it makes the rewrite system confluent also on possibly disconnected graphs, without changing its behavior on the connected graphs we care about. This allows us to avoid talking about connectivity, at the cost of five easy additional cases in the confluence proof.

Unlike for the construction of the 2pdom-algebra of graphs, which mainly uses global operations on graphs, the rewrite system is defined using various local operations. There are at least two fundamentally different ways to formalize this rewrite system: a subtractive version and an additive one. Assume an operation G \ x that removes a vertex x : G (and any incident edges) from the graph G. Then rule (V0) can be expressed as rewriting G to G \ z, provided that z {ι, o} and that z has no incident edges. Alternatively, this rule can be expressed as rewriting G ∔ α to G. Note that the latter formulation does not require any side condition: the fact that the new vertex is isolated and distinct from input and output is implicit in definition of G ∔ α. This makes the additive formulation rather appealing, especially with the graph representation employed so far. Indeed, the subtractive formulation not only requires explicit side conditions, but also an operation for deleting vertices, which is painful to account for with this representation: deleting z : G from G is only possible if z is neither input nor output, so that vertex deletion on 2p-graphs must take a proof of this fact as additional argument. 3Recall from Section 3 that the two most important properties of the rewrite system are:

(ii) Reducibility of g(u) to a small irreducible graph;

(iii) Confluence up to isomorphism. It turns out that (ii) can be proved with reasonable effort using an additive formulation of the rewrite system and the packaged representation of graphs. However, as we will argue in Section 8, a subtractive formulation is much more convenient for (iii) and requires us to temporarily use a second representation of graphs.

We now give the formal definition of the rewrite system we use to prove the reducibility property. The rules are given in Fig. 5. Recall that G ∔ α is defined as the disjoint union of G and the single-vertex graph 1 α whose only vertex is * . Hence, its vertices are in l x for x : G and in r * .

Note that, by design, the rules to not yield a graph property (i.e., steps are not preserved under isomorphisms). Thus, we need to close under both isomorphism and transitivity in order to obtain a well-behaved rewrite system. We do so through the following inductive definition:

F ≃ 2 G F ⇒ G F ≃ 2 F ′ F ′ → G G ⇒ H F ⇒ H
Since ≃ 2 is reflexive and transitive, so is ⇒.

To obtain reducibility in the following section, we need to show that rewrite steps are preserved by the Σ-operations on 2p-graphs: Since the operations are already known to preserve isomorphisms (part of Proposition 5.2), it suffices by induction on the rewrite sequence to prove the lemma when G → G ′ . The last item is straightforward since converse and domain do not modify the (non-pointed) graph of their argument. It moreover suffices to do only one side of the first two items since parallel composition is commutative, and since we can use converse to swap the arguments of sequential compositions (again, by Proposition 5.2).

Lemma 6.2 (Preservation of steps). If G ⇒ G ′ , then 1. G ∥ H ⇒ G ′ ∥ H and H ∥ G ⇒ H ∥ G ′ , 2. G • H ⇒ G ′ • H and H • G ⇒ H • G ′ , 3. G • ⇒ G ′• and dom(G) ⇒ dom(G ′ ). (V0) G∔α → G (V1) G∔α∔[in l x, u, in r * ] → G[x ← dom(uα)] (E1) G∔[x, u, x] → G[x ← u ∥ 1] (V2) G∔α∔[in l x, u, in r * ]∔[in r * , v, in l y] → G∔[x, uαv, y] (E2) G∔[x, u, y]∔[x, v, y] → G∔[x, u ∥ v, y]
Since both parallel and sequential composition are defined as a quotient of a disjoint union, we factorize most of the work by proving the following technical lemma: Lemma 6.3. Let G, G ′ , H be 2p-graphs and let ≈ be an equivalence relation on the vertices of G + H such that vertices of G which are neither input nor output are not equivalent to any other vertex. Let ≈ ′ be the equivalence relation mimicking

≈ on G ′ + H . If G → G ′ , then ⟨(G + H ) /≈ , π in l ι G , π in r o H ⟩ ⇒ ⟨(G ′ + H ) /≈ ′, π in l ι G ′, π in r o H ⟩.
Proof. The lemma intuitively holds because every vertex that can potentially be removed in G by the given rewrite step to G ′ cannot be the input or the output. Since the quotient touches at most the input and output of G, such a vertex can still be removed in

⟨(G + H ) /≈ , π in l ι G , π in r o H ⟩.
In practice, this lemma is proved compositionally: after a case analysis on the rule used to derive G → G ′ , we use the commutation properties established between the local operations and the global ones (Lemma 4.12) in order to rewrite ⟨(G + H ) /≈ , π in l ι G , π in r o H ⟩ into an isomorphic graph for which the same rewrite rule syntactically applies, and we prove that the resulting graph is isomorphic to the expected one by using the commutation properties again. □

Note that the use of ⇒ in the lemma above is solely to allow for isomorphism steps around a single proper step; this pattern is occurs at several places in our development

Reducibility

We work in this section with the 2pdom-algebra of terms over A, and with 2p-graphs labeled using this algebra.

To get a formal reducibility statement, we need to define the normalization function discussed in Section 3, as well as the function g ′ from normal terms to graphs.

A normal term is either a test (α), or a triple (α, u, β) where u is intuitively not a test, although we do not need to keep track of this information. We obtain irreducible graphs from normal terms by setting g ′ (α) := 1 α and g ′ (α, u, β) := u β α .

We recover a term from a normal term by setting ⌊(α)⌋ := α and ⌊(α, u, β)⌋ := αuβ.

The role of the normalization function _ ↓ is to recursively compute a term whose shape matches the shape of terms obtained from irreducible graphs. It is defined as the unique Σ-homomorphism such that a ↓ = (1, a, 1), after having defined the following Σ-algebra on normal terms:

(α, u, β) • (γ , v, δ ) := (α, uβγv, δ ) (α, u, β) • (γ ) := (α, u, βγ ) (γ ) • (α, u, β) := (γ α, u, β) (α) • (β) := (α β) (α, u, β) ∥ (γ , v, δ ) := (αγ , u ∥ v, βδ ) (α, u, β) ∥ (γ ) := (αuβ ∥ γ ) (γ ) ∥ (α, u, β) := (γ ∥ αuβ) (α) ∥ (β) := (α β) (α, u, β) • := (β, u • , α) (α) • := (α) dom((α, u, β)) := (αdom(uβ))
dom((α)) := (α)

1 := (1)
As explained in Section 3, this syntactic normalization function is valid w.r.t. 2pdom axioms. Proposition 7.1 (Normalization). For all terms u, ⌊u ↓ ⌋ ≡ u.

Proof. This amounts to proving that the above equations defining the Σ-algebra on normal terms are all derivable from 2pdom axioms after applying ⌊_⌋ on both sides. □ Formalizing reducibility is more challenging: Proposition 7.2 (Reducibility). For all terms u, we have g(u) ⇒ g ′ (u ↓ ).

Proof. We proceed by induction on u. In each case, we obtain reduction sequences by induction, which we can combine using the preservation lemma; then it suffices to do a case analysis on the shape of the normal terms, and to perform a last rewrite step if necessary. Suppose for instance that u = v ∥ w. By induction we get reduction sequences g(v) ⇒ g ′ (v ↓ ) and g(w) ⇒ g ′ (w ↓ ), from which we deduce by Lemma 6.2 that g(u) = g(v) ∥ g(w) ⇒ g ′ (v ↓ ) ∥ g ′ (w ↓ ). Then there are three cases to consider:

• either both v ↓ and w ↓ are tests, say (α) and (β), so that u ↓ = (α β). In this case it suffices to check that

g ′ (v ↓ ) ∥ g ′ (w ↓ ) = 1 α ∥ 1 β ≃ 2 1 α β = g ′ (u ↓ ) • or none of them is a test: v ↓ = (α, v ′ , β), w ↓ = (γ , w ′ , δ ), u ↓ = (αγ , v ′ ∥ w ′ , βδ
), and we check that

g ′ (v ↓ ) ∥ g ′ (w ↓ ) = v ′ β α ∥ w ′δ γ ≃ 2 2 β δ αγ ∔ [in l * , v ′ , in r * ] ∔ [in l * , w ′ , in r * ] → 2 β δ αγ ∔ [in l * , v ′ ∥ w ′ , in r * ] (E2) = (v ′ ∥ w ′ ) β δ αγ = g ′ (u ↓ )
• or one of them is a test and the other is not, say v ↓ = (α, v ′ , β) and w ↓ = (γ ), so that u ↓ = (αv ′ β ∥ γ ). There we have

g ′ (v ↓ ) ∥ g ′ (w ↓ ) = v ′ β α ∥ 1 γ ≃ 2 1 α βγ ∔ [ * , v ′ , * ] → 1 α βγ (v ′ ∥ 1) (E0) ≃ 2 1 αv ′ β ∥ γ = g ′ (u ↓ )
The last isomorphism comes from the law α βγ (v ′ ∥ 1) ≡ αv ′ β ∥ γ , which is indeed derivable.

In those three cases for parallel composition, the first isomorphism we have to provide is between the graph g ′ (v ↓ ) ∥ g ′ (w ↓ ), which is a quotient of a graph with two to four vertices, and a concrete graph with one or two vertices. We could prove those isomorphisms compositionally, but it turned out to be more convenient to prove them using Lemma 4.13, by providing surjective homomorphisms explicitly.

The other Σ-operations are handled similarly, domain and converse of course being simpler. □

Confluence

We use Newman's lemma to prove confluence of ⇒ via local confluence of the single step relation →: every strongly normalizing and locally confluent relation is confluent. The rewriting relation is strongly normalizing since the number of vertices plus the number of edges decreases along each step. Since we work modulo isomorphisms and our single step relation is not a graph property, the appropriate local confluence property is the following one:

Proposition 8.1 (Local confluence modulo isomorphisms). If F ′ ← F ≃ 2 G → G ′ , then there exists H such that F ′ , G ′ ⇒ H .
Thanks to the inductive definition we used for ⇒, we easily formalize the required variant of Newman's lemma to deduce confluence of ⇒.

Formalizing the above local confluence lemma however turns out to be extremely tedious using packaged graphs and our additive definition of the rewrite rules. To see why, consider one of the simplest cases, the interaction of two instances of the (V1) rule. Our assumptions in this case are:

• F ∔ α ∔ [in l x, u, in r * ] ≃ 2 G ∔ β ∔ [in l y, v, in r * ] • F ∔ α ∔ [in l x, u, in r * ] → F [x ← dom(uα)] • G ∔ β ∔ [in l y, v, in r * ] → G[y ← dom(vα)]
In order to close this pair, we first have to check whether the isomorphism maps in r * to in r * (in which case the two instances are the same). Otherwise, we need to trace the vertex removed on the right through the isomorphism in order to expand F accordingly and vice versa. Moreover, one needs to exhibit an isomorphism between the untouched parts of F and G. This happens in a dependently typed setting and our attempts to carry out these constructions failed due to circular dependencies between the involved statements. Moreover, even if this problem could be solved, it would not lead to a natural proof of local confluence: the vertices of interest each have two names (in F and in G), keeping track of their correspondences rapidly grows out of hands, and we cannot organize case distinctions in the most efficient way. Instead, we prove local confluence using an alternative representation of both graphs and the step relation. As it comes to graphs, we employ open graphs: graphs where both vertices and edges are just natural numbers. Although such a formal representation is commonplace [START_REF] Chen | Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle[END_REF][START_REF] Guéneau | Formal Proof and Analysis of an Incremental Cycle Detection Algorithm[END_REF][START_REF] Lammich | Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL[END_REF][START_REF] Noschinski | A Graph Library for Isabelle[END_REF][START_REF] Abhishek | Towards a Constructive Formalization of Perfect Graph Theorems[END_REF], we are not aware of any work where a correspondence with a packaged representation was established and exploited. For the step relation, we employ a subtractive characterization such that single steps can be performed independently from the concrete shape of the considered graph. Definition 8.2 (Open graph). We fix two copies V and E of the countably infinite type N of natural numbers and call them vertices and edges respectively. An (open) pre-graph is a tuple

U = ⟨V U , E U , p U , l v U , l e U , ι U , o U ⟩ where • V U is a finite set of vertices • E U is a finite set of edges • p U : B → E → V
• ι U , o U ∈ V U .
We let O, U , V . . . range over open pre-graphs. The separation into pre-graphs and well-formedness is crucial here. It allows us to separate the task of proving that a graph has the desired shape from proving that it is actually a graph.

In Coq, we use the finmap library [START_REF] Cohen | A finset and finmap library[END_REF] to represent finite sets over the countable types V and E. Moreover, we turn the well-formedness predicate into a class, allowing it to be inferred it automatically in many situations.

We then define operations corresponding to those defined on 2p-graphs. In the case of open graphs, where edges and vertices are external, the operations adding vertices and edges take the edge to be added as additional argument. That is, we have the following operations:

• U ∔ [x, α] denotes U with vertex x labeled with α • U ∔ [e, x, u, y] denotes U with e u-labeled edge from x to y. • U [x ← a] denotes U where x is labeled with a ⊗l v U x.

• U \ x denotes U with x and all edges incident to x removed. • U -E denotes U with all the edges in E removed.

All these operations are easily defined as operations on pregraphs. They yield graphs under the expected side conditions (e.g., adding an edge requires that the vertices are part of the graph and deleting a vertex requires that the deleted vertex is distinct from input and output). In particular, vertex deletion, which we will use extensively below, is a benign operation on open graphs. In contrast, the quotient and disjoint union operations we extensively used in the previous sections would be painful to deal with on open graphs.

We have the following notion of strong equivalence: two pre-graphs are strongly equivalent if they only differ by their labels, up to the setoid relations on L v and L e . 1. ≡ is an equivalence relation on pre-graphs 2

. U [x ← α][y ← β] ≡ U [y ← β][x ← α] 3. U \ x \ y = U \ y \ x 4. U ∔ [e, x, u, y] \ z ≡ (U \ z) ∔ [e, x, u, y] if z {x, y} and e E U 5. U ∔ [e, x, u, y] \ y ≡ U \ y 6. U ∔ [x, a] \ x ≡ U if U is well-formed and x V U . 7. U [x ← α] ≡ V [x ← β] if U ≡ V and α ≡ β 8. U ∔ [e, x, u, y] ≡ V ∔ [e, x, v, y] if U ≡ V and u ≡ v
Note that most of these equivalences hold irrespective of whether the graph G is well-formed or not. A notable exception is [START_REF] Diestel | Graph Theory[END_REF], where the addition of x to a graph that is not well-formed could turn a formerly "dangling" edge into one that is incident to x and would therefore be removed by the deletion of x. That the last two items hold is extremely convenient as it allows us to use 'setoid rewriting', something we cannot use for isomorphisms on packaged graphs due to the dependency between the replaced graphs and their vertices (cf. Lemma 4.10).

(V0) z ∈ V U I U (z) = ∅ z IO U U → U \ z (V1) I U (z) = {e} arc U e x u z x z z IO U U → U [x ← dom(u • l v U z)] \ z (V2) I U (z) = {e 1 , e 2 } e 1 e 2 z {x, y} z IO U arc U e 1 x u z arc U e 2 z v y U → U \ z ∔ [max(e 1 , e 2 ), x, u • l v U z • v, y] (E1) arc U e x _ x U → (U -{e})[x ← l e U e] (
We now turn to the definition of the step relation. We want steps to be preserved under isomorphism so that the local confluence property can be stated using a single graph as a left-hand side of two reduction steps. This forces us to handle the edge-flipping behavior in the definition of the rules. To this end, we define a predicate expressing whether an edge can, up to reversal, be seen as a given edge, and then use this predicate in the definition of the step relation. We moreover write I G (x) for the set of edges incident to x in G. The rules of our subtractive variant of the step relation are given in Fig. 6. We use a max operation on edges (natural numbers) in rules (V2) and (E2): by doing so, the name of the edge which is kept depends only on the edges being removed and not on the order in which the edges are matched. This is convenient in that it allows us to close localconfluence critical pairs using strong equivalences rather than isomorphisms. We define the multi-step rewrite relation ⇒ as the least transitive relation containing strong equivalence, single steps, but also the relation that flips a single edge in a graph. This is fine since we reason modulo edge-flipping isomorphisms on packaged graphs; doing so makes it possible to use symmetry reasoning in the analysis of the critical pairs. Now we have everything in place to prove local confluence Putting everything together as explained at the end of Section 3, we obtain a formal proof Theorem 3.2. Formalizing this proof required us to setup several tools for reasoning about graphs and isomorphisms, under two distinct representations: the packaged representation, which is convenient for constructing and combining graphs, and the open representation, which is convenient for subtractive operations.

The formalization has a moderate size (2700/3900 lines of specification/proofs); large parts of it consist in general infrastructure and lemmas about labeled directed multigraphs, which should be reusable and has been integrated with [START_REF] Doczkal | Graph Theory in Coq: Minors, Treewidth, and Isomorphisms[END_REF].

We leave four main directions for future work. First, for the sake of simplicity, the structures we require in addition to those in the mathematical components library [18] (e.g., setoids, labels, graphs) are defined using "telescopes" rather than following the packaged classes design employed in [18]. This causes some minor efficiency problems that can be alleviated by using primitive projections for the records involved. Nevertheless, we plan to rework the concrete implementation of these structures. This should improve efficiency while at the same time giving us the opportunity to provide a library with more fine-grained abstractions.

Second, 2pdom-algebras form a fragment of 2p-algebras, where a neutral element for parallel composition is added, allowing one to denote all graphs of treewidth at most twonot just the connected ones. Soundness and completeness of 2p-algebra is established in [START_REF] Cosme | K 4 -free graphs as a free algebra[END_REF][START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF], each time by building on completeness of 2pdom-algebra. We plan to explore a more direct approach: we believe that the present formal proof could be extended to deal directly with this more general case, just by modifying the rewrite system and the shape of the normal terms. We would also like to study smaller fragments. For instance, is it still possible to axiomatize graph isomorphism in absence of the converse operation? Third, by combining our completeness proof for 2pdomalgebra with the extraction function from treewidth at most two connected graphs to terms [START_REF] Cosme | K 4 -free graphs as a free algebra[END_REF] formalized in [START_REF] Doczkal | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs[END_REF], we could obtain a formal proof that such graphs form the free 2pdomalgebra. The rewrite system we used here makes it possible to define another extraction function [START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF], whose informal description is much easier. Formalizing this approach however seems challenging: it requires to study the expansion function (cf. [START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF]) we alluded to at the beginning of Section 6, which is a global and deeply dependently typed operation.

Fourth, completeness of 2pdom-algebra has been recently used to obtain that the equational theory of allegories [START_REF] Freyd | Categories, Allegories[END_REF] is decidable [START_REF] Pous | Allegories: decidability and graph homomorphisms[END_REF]. This decidability proof involves more graph theory than the present one: it exploits the fact that the graphs of treewidth at most two are precisely those excluding K 4 as a minor, and it requires a long analysis of the possible homomorphisms occurring within such graphs. Formalizing this proof seems rather challenging but not out of reach, thanks to the library we have developed so far.

  •b • ) ∥ c and (a•dom(b)•c) ∥ d are:

Figure 1 .

 1 Figure 1. Axioms of 2pdom-algebras.

  would give us (dom(b)•dom(a))•c; but no reduction would give us dom(a)•(dom(b)•c), which is also a term denoting the same graph. To deal with this issue, we use a syntactic normalization function u → u ↓ in order to isolate the tests occurring on both sides of a term. (Normalized terms are not canonical, though: the normalization function is far from equating all provably equal terms.)

Definition

  a function where p false e indicates the source of the edge e and p true e indicates the target of the edge e • l v : V → L v indicates the label of each vertex • l e : E → L e indicates the label of each edge

  where ≈ ′ is the equivalence relation on G induced through the given isomorphism by a given equivalence relation ≈ on F . 5. F + G /≈ ≃ (F + G) /≈ ′ where ≈ is an equivalence relation on G and ≈ ′ is its extension to F + G (leaving all vertices of F in singleton classes). 6. F /≈ /≈ ′ ≃ F /≈ ′′ , with ≈ an equivalence relation on F , ≈ ′ an equivalence relation on F /≈ , and ≈ ′′ the equivalence relation on F obtained by composing ≈ and ≈ ′ . 7. (F + G) /≈ ≃ F /≈ ′ when G has no edge and all vertices labeled with 1, ≈ is an equivalence relation on F + G, ≈ ′

Definition 5 . 1 .

 51 A two-pointed graph (or 2p-graph for short) is a structure ⟨G, ι, o⟩ where G is a graph and ι : G and o : G are two vertices called input and output respectively.

Figure 3 .

 3 Figure 3. Σ-operations on 2p-graphs.

Figure 4 .

 4 Figure 4. Rewrite rules for term-labeled graphs. The square vertices may have additional incident edges. The circular vertices (i.e., those that are removed) must be distinct from input and output and must not have other incident edges.

Figure 5 .

 5 Figure 5. Additive presentation of the rewrite system.

  indicates the source and target of edges • l v U : V → L v indicates the labels of vertices • l e U : E → L e indicates the labels of edges • ι U and o U indicate the input and the output A pre-graph is well-formed (i.e, an open graph) if the following conditions hold: • p U b e ∈ V U for all b : B and e ∈ E U .

Definition 8 . 3 (

 83 Strong equivalence). Let O and U be pregraphs. We call O and U strongly equivalent, written O ≡ U , if the following conditions are satisfied 1. V O = V U and E O = E U . 2. the functions p O and p U agree on V O 3. l v O x ≡ l v U x for all x ∈ V O 4. l e O e ≡ l e U e for all e ∈ E O 5. ι O = ι U and o O = o U In other words, strong equivalences correspond to nonedge flipping isomorphisms which are the identity on both vertices and edges. This relation enjoys a number of useful properties, of which we list only a few: Lemma 8.4.

E2) arc U e 1 x u y arc U e 2 x v y e 1 e 2 UFigure 6 .

 26 Figure 6. Open step relation.

  arc U e x u y := e ∈ E U ∧ ∃b. p U b e = x ∧ p U (¬b) e = y ∧ l e U e ≡ [b] u

Through the label structure from Definition 4.3.

The only exception to this intuition is the rule (V0), which is used in a special way in the present development; see Remark 6.1 below.

Another possibility would be to do nothing if the passed vertex is the input or the output. However, this would make the type of vertices of G \ z dependent on the value of z and therefore would not solve the problem.

This is the finite type of pairs of elements x : V and proofs of x ∈ V U .

* This work has been funded by the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157), and was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon and UCA JEDI , within the programs "Investissements d'Avenir" ANR-11-IDEX-0007 and ANR-15-IDEX-01, respectively. , New Orleans, LA, USA

Proposition 8.5. Let O, U , V be open graphs such that U ← O → V . Then there exist graphs U ′ and V ′ such that U ⇒ U ′ , V ⇒ V ′ and U ′ ≡ V ′ .

Since ⇒ is closed under strong equivalence, the statement is equivalent to the one where U ′ is syntactically equal to V ′ . We prefer this formulation because it matches the way we prove the lemma.

Proof. The proof boils down to a case distinction between all the possible pairs of rules that could have been applied to obtain U ← O → V . We can reduce the number of cases by assuming, without loss of generality, that the rule applied on the left has a lower index (with respect to the textual order in Fig. 6). In Coq, this is realized by defining the relation → as a relation in Type and defining a function numbering the rules. There are still fifteen cases left, and each of them comes with its own case distinctions. We discuss only some illustrative cases below.

• Consider an interaction of the rule (V1) with arc O e x u z and rule (V2) with arc O e 1 x ′ u ′ z ′ and arc O e 2 z ′ v ′ y ′ . We have z z ′ due to the different number of incident edges. If z {x ′ , y ′ } the instances are independent, so assume z ∈ {x ′ , y ′ }. Without loss of generality, we can assume z = x ′ , for otherwise we exchange the roles of x ′ and y ′ as well as e 1 and e 2 , setting u ′ := v ′• and v ′ := u ′• and flipping the edge introduced through the application of (V2). Hence, e 2 = e, z ′ = x, and v ′ = u, exhibiting the situation below:

After applying rule (V1) on both sides and using the equivalences from Lemma 8.4, it suffices to show dom(uαvβ) ≡ dom(uαdom(vβ)). • Rules (V2) and (E2) can interact as follows:

This pair can be joined by applying rule (E1) in the left and rule (V1) on the right, yielding the derivable equation uαv

• Rule (V1) can interact with itself as follows:

This pair can be joined by applying Rule (V0) on both sides, not requiring any equation. □

Note that we need to allow edge-flips in the definition of ⇒ in order to factor the proof by reasoning without loss of generality in the first case discussed in the proof. This is important: we use this pattern thirteen times in the full proof, which is 500 lines long. We remark that the last case mentioned above does not arise in [START_REF] Doczkal | Treewidth-two graphs as a free algebra[END_REF] where the graphs are assumed to be connected.

Transferring Local Confluence

Proposition 8.5 proves local confluence, but not using the representation employed in the rest of the formalization. In this section, we outline what is needed in order to transfer this result and obtain a proof of Proposition 8.1.

We first need translation functions between the two representations of graphs. We start with the translation from open graphs to packaged graphs. Definition 9.1 (Packing). Let U be an open graph. We define the packing of U , written pack U , to be the 2p-graph whose finite type of vertices is the finite type of elements of V U (also denoted by V U 4 ) and likewise for edges. The remaining components are obtained by casting the components of U to the appropriate types (e.g., p : B → E U → V U for the endpoints of edges).

Since finite sets over countable types coerce to finite types in Coq, this packing operation is easy to define.

For the converse translation, from packaged graphs to open graphs, the main issue is in embedding the finite types of edges and vertices of a given packaged graph into the generic vertex and edge types. For these, we employ two generic injections

Both of these come only with partial inverses in general, since T may be empty. This is never the case for the vertex type of 2p-graphs however, which must contain input and output, so that we get:

The functions are defined such that proj v (inj v v) = v whenever v is a vertex (of some 2p-graph) and proj e (inj e e) = Some e whenever e is an edge. The operation of opening a packaged graph can then be defined as follows

• l e ′ e := if proj e e is Some e ′ then l e e ′ else 1

At this point, we can prove:

In order to relate the two variants of the step relation, we need a proper notion of isomorphism on open graphs. This is obtained by reusing isomorphisms on packaged graphs via the packing operation. Note that we define isomorphism as a relation between pre-graphs; this relation is a partial equivalence relation (PER) rather than an equivalence relation due to the wellformedness requirement.

As expected, strong equivalences give rise to isomorphisms. Fact 9.5. O ≃ 2 U whenever O ≡ U and O is well-formed.

Note that, given O ≡ U , well-formedness of O implies well-formedness of U , allowing us to have only one wellformedness assumption. This is convenient when showing that a complex graph expression is isomorphic to an expression known to be well-formed. Now that we have a proper notion of isomorphisms on open graphs, we can show that the open step relation commutes with them. Lemma 9.6. If U → U ′ and U ≃ 2 V , then there exists some

This property is relatively easy to prove because it deals exclusively with open graphs. All we need to do is establish a number of lemmas showing that incidence of edges and the arc predicate are preserved under isomorphisms. As with isomorphisms of packaged graphs, this requires viewing isomorphisms as functions from vertices to vertices.

We then need to prove that (additive) packaged steps and (subtractive) open steps actually match. To prove that packaged steps give rise to open steps we first establish a number of commutation properties about the opening operation: Fact 9.7. We have

Proof. By case analysis on F → F ′ . We sketch the case for the (V1) rule, the other cases are similar. That is, we need to find a graph

By Lemma 9.6, we can also make isomorphism steps before making an actual step. We pick a fresh vertex z and a fresh edge e and then use Fact 9.7 to push the opening operation down to the graph G. Thus (1) reduces to showing:

The side conditions of rule (V1) are then easily established. Applying the rule (V1) determines U ′ to be

For the converse direction (reflecting open steps with packaged steps), we need to be able to trace vertices through the packing operation. For this, we define a function

Recall that the vertex type of pack U is the set of vertices of U . Hence, this amounts to pairing vertices x with proofs of x ∈ U if possible and otherwise returning a default vertex. Fact 9.9. We have

when e E U Lemma 9.10.

Proof. By induction on the given sequence, since strong equivalence and edge-flips are both contained in isomorphism, it suffices to prove the lemma in the case of a single rewrite step. We proceed by case analysis on this step. We again sketch the case for (V1), the other cases are similar. We have I G (z) = {e}, arc U e x u z, z x, and z {ι U , o U } and we need to show

where α := l v U z. In order to apply the (V1) rule for →, we need to expand U . Without loss of generality, e is an edge from x to z; if not, we apply an isomorphism that reverses e in U and reestablish all assumptions. Now it suffices to show

and apply rule (V1). Finally, the isomorphism (3) is established by extruding the packing operation on the right. During this process, we can choose the vertex and edge to be added (Fact 9.9) and we choose x and e respectively.