Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations

This work was supported by JSPS KAKENHI Grant Number JP21K13828.

Yoshiki Nakamura
Tokyo Institute of Technology

Email<EMAIL_ADDRESS>
We study the decidability and complexity of equational theories of the existential calculus of relations with transitive closure (ECoR*) and its fragments,
where ECoR* is the positive calculus of relations with transitive closure extended with complements of term variables and constants.
We give characterizations of these equational theories by using edge saturations and we show that the equational theory is
1) coNP-complete for ECoR* without transitive closure;
2) in coNEXP for ECoR* without intersection and PSPACE-complete for two smaller fragments;
3) $\Pi_{1}^{0}$-complete for ECoR*.
The second result gives PSPACE-upper bounds for some extensions of Kleene algebra, including Kleene algebra with top w.r.t. binary relations.

relation algebra, Kleene algebra, complexity

m m#1 ·#2
m m#1 †#2
m m#1 ∪#2
m m#1 ∩#2

§ INTRODUCTION

The calculus of relations (CoR, for short) <cit.> is an algebraic system on binary relations.
As binary relations appear everywhere in computer science, CoR and relation algebras (including their transitive closure extensions) can be applied to various areas, such as databases and program development and verification.
However, the equational theory of CoR is undecidable <cit.>.
The undecidability holds even over the signature $\set{\cdot, \cup, \bl^{-}}$
of composition ($\cdot$), union ($\cup$), and complement ($\bl^{-}$) <cit.>, moreover even when the number of term variables is one <cit.>.

One approach to avoid the undecidability of the equational theory of CoR is to consider its positive fragments, by excluding complements.
The terms of the positive calculus of relations ($\PCoR$, for short) <cit.>
is the set of terms over the signature $\set{\cdot, \cup, \bl^{\smile}, \bot, \top, \const{I}, \cap}$
of composition ($\cdot$), union ($\cup$), converse ($\bl^{\smile}$), the empty relation ($\bot$), the universal relation ($\top$), the identity relation ($\const{I}$), and intersection ($\cap$).
The equational theory of $\PCoR$ is decidable <cit.>.

This decidability result also holds when adding the reflexive transitive operator, thus arriving at Kleene allegory terms <cit.>.

Then, it is natural to ask about the decidability and complexity of $\PCoR$ when the complement operator is added in restricted ways (cf. e.g., antidomain <cit.> and tests in Kleene algebra with tests (KAT) <cit.>) to extend the expressive power of $\PCoR$ without drastically increasing the complexity.
In this paper, inspired by the negations of atomic programs in the context of propositional dynamic logic (PDL) <cit.>,
we consider existential calculi of relations—positive calculi of relations extended with complements of term variables and constants (i.e., the complement operator only applies to term variables or constants)—and study the decidability and complexity of their equational theories.

We denote by $\PCoRTC$ the $\PCoR$ with the reflexive transitive closure operator ($\bl^{*}$).
We denote by $\ECoR$ (resp. $\ECoRTC$) the $\PCoR$ (resp. $\PCoRTC$) with complements of term variables and constants.
For example, whereas $(a \cdot a)^{-}$ and $(a^{*})^{-}$ are not $\ECoR$ terms, $\ECoR$ contains terms such as:

2*$a^{-}$                                          2*$\left(\begin{array}{l}
\mbox{there is \emph{not} an ($a$-labeled) edge} \\
\mbox{from the source to the target}
\end{array}\right)$

2*$ (a \cdot a) \cap a^{-} \cap \const{I}^{-}$     2*$\left(\begin{array}{l}
\mbox{the distance from the source} \\
\mbox{to the target is two}
\end{array}\right)$

They are not expressible in $\PCoR$ because they are not preserved under homomorphisms; thus, $\ECoR$ is strictly more expressive than $\PCoR$.
More precisely, w.r.t.  binary relations,
while $\PCoR$ has the same expressive power as the three-variable fragment of existential positive logic with equality <cit.>,
$\ECoR$ has the same expressive power as the three-variable fragment of existential logic with equality <cit.>[
$\ECoR$ has the same expressive power as the level $\Sigma_1^{\CoR}$ of the dot-dagger alternation hierarchy <cit.><cit.> of $\CoR$, because every $\ECoR$ term is a $\Sigma_1^{\CoR}$ term,
and conversely, every $\Sigma_1^{\CoR}$ term has an equivalent $\ECoR$ term by pushing complement and projection deeper into the term to the extent possible.
Here, $\Sigma_1^{\CoR}$ has the same expressive power as the three-variable fragment of existential logic (i.e., the level $\Sigma_1$ of the quantifier alternation hierarchy of first-order logic) <cit.>.].
(The name “existential calculi of relations” comes from this fact.)

On the equational theory of $\ECoRTC$, while it subsumes that of $\PCoRTC$ (including axioms of Kleene algebra and allegory <cit.>),
some non-trivial valid (in)equations are as follows: (see <Ref> for the proofs):

\begin{align}
\label{equation: I- top 0}      \top            & = a \cup a^{-}                               \\
\label{equation: I- top}              a b a^{-} & \le \const{I}^{-} a^{-} \cup a \const{I}^{-}
\end{align}

\begin{align}
\label{equation: I- ID}               a                & \le \const{I}^{-} \cup a a \\
\label{equation: I- De Morgan}        a^{\smile} a^{-} & \le \const{I}^{-}
\end{align}

§.§ Contribution and related work

We show that the equational theory is

1) coNP-complete for $\ECoR$ (<Ref>);

2) in coNEXP for $\ECoR$ without $\cap$ (<Ref>);
PSPACE-complete for $\ECoR$ without $\cap$ such that $\const{I}^{-}$ does not occur (<Ref>)
and for $\ECoR$ without $\cap$ such that $a^{-}$ does not occur for any term variable $a$ (<Ref>);

3) $\Pi_{1}^{0}$-complete for $\ECoRTC$ (<Ref>).

<Ref> summarizes our results and related results.
<ref> gives PSPACE-upper bounds for some

Complexity of the equational theory (w.r.t. binary relations) over $\sig \cup \sig'$
where $\sig \subseteq \set{\cdot, \cup, \bl^{\smile}, \cap, \bl^{*}, \bot, \top, \const{I}} = \sig_{\mathrm{PCoR*}}$ and $\sig' \subseteq \set{a^{-}, \const{I}^{-}, \bl^{-}}$.
Here, $a^{-}$, $\const{I}^{-}$, $\bl^{-}$ denote the complements of term variables, those of constants, and the (full) complement.

[height=1.2]$\sig$    $\sig'$                                                                  $\emptyset$
$\set{\const{I}^{-}}$                                                                                $\set{a^{-}}$                                                                        $\set{a^{-},\const{I}^{-}}$                                   $\set{\bl^{-}}$

2*$\set{\cdot, \cup} \subseteq \sig \subseteq \sig_{\mathrm{PCoR*}} \setminus \set{{\bl^{*}}}$         coNP-c
3|c|coNP-c                                                                                $\Sigma_{1}^{0}$-c

(<cit.>, <cit.>, <cit.>)          3|c|(<Ref>)       (<cit.>)

2*$\set{\cdot, \cup, \bl^{*}} \subseteq \sig \subseteq \sig_{\mathrm{PCoR*}} \setminus \set{\cap}$     PSPACE-c                                                                             PSPACE-c                                                      PSPACE-c                                                  in coNEXP

(<cit.>, <cit.>, <Ref>)     (<Ref>)                             (<Ref>)                         (<Ref>)     $\Pi_{1}^{1}$-c

2*$\set{\cdot, \cup, \cap, \bl^{*}} \subseteq \sig  \subseteq \sig_{\mathrm{PCoR*}}$                   EXPSPACE-c                                                                           EXPSPACE-hard                                                 2|c|$\Pi_1^{0}$-c

(<cit.>, <cit.>)

<cit.>                                                      2|c|(<Ref>)

On the lower bound, the validity problem for PDL with intersection and negation of atomic programs, which is $\Pi_{1}^{1}$-complete <cit.>, is recursively reducible to the equational theory over the signature $\set{\cup, \cdot, \bl^*, \bl^-}$ by the standard translation from modal logics to $\CoR$ <cit.> while eliminating the identity using a fresh variable preserving the validity <cit.>.
extensions of Kleene algebra (KA) w.r.t. binary relations, as $\ECoR$ without $\cap$ includes KA terms (i.e., terms over the signature $\set{\cdot, \cup, \bl^{*}, \bot, \const{I}}$).
Notably, it includes KA with converse ($\smile$) <cit.> and KA with top ($\top$) <cit.> w.r.t. binary relations; thus, the result gives a positive answer to a question posed by Pous and Wagemaker <cit.> as follows:
the equational theory of KA with top w.r.t. binary relations is still in PSPACE.[Very recently, this result is also given in <cit.>.]
Additionally, <ref> negatively answers a question posed by Nakamura <cit.> as follows:
the equational theory of Kleene allegories with complements of term variables (w.r.t. binary relations) is undecidable.

To show them,
we give a graph theoretical characterization of the equational theory of $\ECoRTC$ (<Ref>).
The characterization using graph languages and graph homomorphisms is based on that for $\PCoRTC$, by Brunet and Pous <cit.><cit.>,
but the identical characterization fails for $\ECoRTC$.

Nevertheless, we can extend such a characterization even for $\ECoRTC$, by extending their graph languages, using edge saturations (cf. saturations of graphs <cit.>; in our saturation, the vertex set is fixed).
Using this graph characterization, we can show the upper bounds of <ref> and <ref>.

For the upper bound of <ref>: the equational theory of $\ECoRTC$ without intersection,
we refine the graph characterization above by using path graphs with some additional information, called saturable paths (<Ref>).
This notion is inspired by Hintikka-trees for Boolean modal logics <cit.> and PDL with the negation of atomic programs <cit.>,

where we consider paths instead of infinite trees and introduce the converse and the difference relation $\const{I}^{-}$.
This characterization gives the coNEXP upper bound for the equational theory of $\ECoRTC$ without intersection.
Moreover, for some fragments, we can give word automata using saturable paths, which shows that
the equational theory of $\ECoRTC$ without intersection is decidable in PSPACE if $\const{I}^{-}$ does not occur (<Ref>)
or if $a^{-}$ does not occur (for any term variable $a$) (<Ref>).
(Our automata construction cannot apply to the full case (<Ref>).)

For the lower bounds, <ref> and <ref> are immediate from the results known in regular expressions <cit.>.
For <ref>, we give a reduction from the universality problem for context-free grammars (<Ref>), via KA with hypotheses <cit.> of the form $\term \le a$ (where $\term$ is a term and $a$ is a term variable) w.r.t. binary relations.

§.§ Outline

<Ref> briefly gives basic definitions.
<Ref> defines $\ECoRTC$ (<Ref>) and recalls known results w.r.t. word and graph languages for smaller fragments of $\ECoRTC$ (<Ref>).
In <Ref>, we give a graph theoretical characterization for $\ECoRTC$, using edge saturations.
By using this, we prove <ref> and the upper bound of <ref>.
In <Ref>, we introduce saturable paths, which refine the characterization of graph saturations, for $\ECoRTC$ without intersection.
Moreover, we give automata using saturable paths for two smaller fragments.
By using them, we prove <ref>.
In <Ref>, we prove the lower bound of <ref>.
<Ref> concludes this paper.

§ PRELIMINARIES

We write $\nat$ for the set of all non-negative integers.
For $l, r \in \nat$, we write $[l, r]$ for the set $\{i \in \nat \mid l \le i \le r\}$.
For $n \in \nat$, we write $[n]$ for $[1, n]$.
For a set $A$, we write $\card(A)$ for the cardinality of $A$ and $\wp(A)$ for the power set of $A$.

§.§ Graphs

For $k \in \nat$, a $k$-pointed graph $\graph$ over a set $A$ is a tuple $\tuple{|\graph|, \set{a^{\graph}}_{a \in A}, \pt{1}^{\graph}, \dots, k^{\graph}}$, where

* $|\graph|$ is a non-empty set of vertices;

* $\aterm^{\graph} \subseteq |\graph|^2$ is a binary relation for each $\aterm \in A$ ($\tuple{x, y} \in \aterm^{\graph}$ denotes that there is an $\aterm$-labeled edge from $x$ to $y$);

* $\pt{1}^{\graph}, \dots, k^{\graph} \in |\graph|$ are the vertices pointed by $\pt{1}, \dots, k$.

We say that $2$-pointed graphs are graphs, here; we mainly use them.
For $2$-pointed graph $\graph$, we say that $\lv^{\graph}$ and $\rv^{\graph}$ are the source and target, respectively.

A (graph) homomorphism from a graph $\graph[1]$ to a graph $\graph[2]$ is a map $h$ from $|\graph[1]|$ to $|\graph[2]|$ such that

* $\tuple{h(\lv^{\graph[1]}), h(\rv^{\graph[1]})} = \tuple{\lv^{\graph[2]}, \rv^{\graph[2]}}$;

* $\tuple{h(x), h(y)} \in a^{H}$ for every $a \in A$ and $\tuple{x, y} \in a^{G}$.

In particular, we say that $h$ is isomorphism if $h$ is bijective and $\tuple{h(x), h(y)} \not \in a^{\graph[2]}$ for every $a \in A$ and $\tuple{x, y} \not\in a^{\graph[1]}$.
We write $h \colon \graph[1] \homo \graph[2]$ if $h$ is a homomorphism from $\graph[1]$ to $\graph[2]$
and write $\graph[1] \homo \graph[2]$ if $h \colon \graph[1] \homo \graph[2]$ for some $h$.
The relation $\homo$ is a preorder.
We display graphs in a standard way,
where the node having an ingoing (resp. outgoing) unlabeled arrow denotes the source (resp. the target).
For example, the following are two connected graphs, and dotted arrows induce a homomorphism between them:
$\begin{tikzpicture}[baseline = -2.2ex]
\graph[grow right = 1.2cm, branch down = 1.2ex, nodes={mynode}]{
{0/{}[draw, circle], 2/{}[draw, circle, xshift = 1.5em]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
0 ->["$a$"] 1;
2 ->["$b$", out = 0, in = -135] 1;
l -> 0; 1 -> r;
\node[below = 3ex of 0, draw, circle, mynode](0'){};
\node[below = 3ex of 1, draw, circle, mynode](1'){};
\node[left = .5em of 0'](l'){};
\node[right = .5em of 1'](r'){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
0' ->["$a$", bend left = 15] 1';
0' ->["$b$", bend right = 15] 1';
l' -> 0'; 1' -> r';
\path (0) edge [homoarrow,->] (0');
\path (2) edge [homoarrow,->, out=-90, in=45] (0');
\path (1) edge [homoarrow,->] (1');
\end{tikzpicture}$.

§ EXISTENTIAL CALCULI OF RELATIONS

§.§ The existential calculus of relations with transitive closure (): syntax and semantics

§.§.§ Syntax

We fix a finite set $\SIG$ of variables.
The set of $\ECoRTC$ terms over $\SIG$ is defined as follows:[For simplicity, in the term set, the converse only applies to terms of the form $a$ or $a^{-}$ and $\bot^{-}$ and $\top^{-}$ does not occur, but we can give a polynomial-time transformation to the term set (<Ref>) by taking the converse normal form
and that $\models_{\REL} \bot^{-} = \top$ and $\models_{\REL} \top^{-} = \bot$ hold.
Thus, our complexity upper bounds hold (<Ref>) even if we exclude these restrictions.]

\begin{align*}
\ECoRTC \ni \term[1], \term[2], \term[3] & ::= \aterm \mid \aterm^{-} \mid \aterm^{\smile} \mid (\aterm^{-})^{\smile} \mid \const{I} \mid \const{I}^{-} \mid \bot \mid \top   \\
& \mid \term[1] \cdot \term[2] \mid \term[1] \cup \term[2] \mid \term[1] \cap \term[2] \mid \term[1]^{*} \tag*{($\aterm \in \SIG$).}
\end{align*}

We use parentheses in ambiguous situations.
We often abbreviate $t \cdot s$ to $t s$.
For $n \in \nat$, we write $\term^{n}$ for $\begin{cases}
\term \cdot \term^{n-1} & (n \ge 1) \\
\const{I}               & (n = 0)
\end{cases}$.

Let $\sig_{\ECoRTC} \defeq \set{\cdot, \cup, \bl^{\smile}, \cap, \bl^{*}, \const{\bot}, \const{\top}, \const{I}} \cup \set{a^{-}, \const{I}^{-}}$.
Here, “$\bl^{\smile}$” only applies to $a$ or $a^{-}$ (for simplicity)
and we use “$a^{-}$” to denote the complement of term variables and “$\const{I}^{-}$” to denote the complement of constants (the important complemented constant is only $\const{I}^{-}$ in this setting).

For $\sig \subseteq \sig_{\ECoRTC}$,
we write $\Termset_{\sig}$ for the set of all terms $\term$ in $\ECoRTC$ s.t. every operator occurring in $\term$ matches one of $\sig$.
We use the following acronyms for some signatures (recall the acronyms in <Ref>; here, extended KA ($\ExKA$) terms are used to denote $\ECoRTC$ terms without $\cap$, in this paper):

$\sig_{\mathop{acronym}}$     operator set

${\ECoRTC}$                   ${\set{\cdot, \cup, \bl^{\smile}, \cap, \bl^{*}, \bot, \top, \const{I}, a^{-}, \const{I}^{-}}}$

${\ECoR}$                     $\sig_{\ECoRTC} \setminus \set{\bl^{*}}$

${\ExKA}$                     $\sig_{\ECoRTC} \setminus \set{\cap} \quad (= \sig_{\KA} \cup \set{\bl^{\smile}, \top, a^{-}, \const{I}^{-}})$

${\PCoRTC}$                   $\sig_{\ECoRTC} \setminus \set{a^{-}, \const{I}^{-}}$

${\PCoR}$                     $\sig_{\PCoRTC} \setminus \set{\bl^{*}}$

${\KA}$                       $\sig_{\PCoRTC} \setminus \set{\bl^{\smile}, \cap, \top} \quad (= \set{\cdot, \cup, \bl^{*}, \bot, \const{I}})$

Let $\SIG_{\const{I}} \defeq \SIG \cup \set{\const{I}}$ and let

\begin{align*}
\SIG^{(-)} & \defeq \set{a, a^{-} \mid a \in \SIG}; & \SIG_{\const{I}}^{(-)} & \defeq \set{a, a^{-} \mid a \in \SIG_{\const{I}}}.
\end{align*}

For each term $\term \in \SIG_{\const{I}}^{(-)} \cup \set{\bot, \top}$, $\comnf{\term}$ denotes the following term, where $a \in \SIG$:

\begin{align*}
\comnf{a} & \defeq a^{-}; & \comnf{a^{-}} & \defeq a; & \comnf{\const{I}} & \defeq \const{I}^{-}; & \comnf{\const{I}^{-}} & \defeq \const{I}; & \comnf{\bot} & \defeq \top; & \comnf{\top} & \defeq \bot \tag*{.}
\end{align*}

An equation $\term[1] = \term[2]$ is a pair of terms.
An inequation $\term[1] \le \term[2]$ is an abbreviation of the equation $\term[1] \cup \term[2] = \term[2]$.[Note that $\jump{\term[1]}_{\model} \subseteq \jump{\term[2]}_{\model} \Longleftrightarrow \jump{\term[1] \cup \term[2]}_{\model} = \jump{\term[2]}_{\model}$.]

The size $\len{\term}$ of a term $\term$ is the number of symbols occurring in $\term$.
Also, let $\len{\term[1] = \term[2]} \defeq \len{\term[1]} + \len{\term[2]}$.

§.§.§ Relational semantics

For binary relations $R, Q$ on a set $W$, the relational converse $R^{\smile}$, the relational composition $R \cdot Q$, the $n$-th iteration $R^{n}$ (where $n \in \nat$), and the reflexive transitive closure $R^*$ are defined by:

\begin{align*}
R^{\smile} & \defeq \set{\tuple{y, x} \mid \tuple{x, y} \in R}                                                                 \\
R \cdot Q  & \defeq \set{\tuple{x, z} \mid \exists y \in W.\ \tuple{x, y} \in R \ \land \ \tuple{y, z} \in Q}\span \span       \\
R^n        & \defeq \begin{cases}
R \cdot R^{n-1}                 & (n \ge 1) \\
\set{\tuple{x, x} \mid x \in W} & (n = 0)
\end{cases};                                                      & R^* & \defeq \bigcup_{n \in \nat} R^n.
\end{align*}

We say that $\graph$ is a $k$-pointed structure if
$\graph$ is a $k$-pointed graph over $\SIG_{\const{I}}^{(-)}$ such that

* $\const{I}^{\graph[1]} = \set{\tuple{x, x} \mid x \in |\graph[1]|}$;

* $\comnf{a}^{\graph[1]} = |\graph[1]|^2 \setminus a^{\graph[1]}$ for $a \in \SIG_{\const{I}}$.[$a^{\graph[1]}$ is redundant for each $a \in \SIG_{\const{I}}^{(-)} \setminus \SIG$ because it is determined by the other relations. However, this definition is compatible with the later.]

We say that $0$-pointed structures are structures.
We use $\model$ and $\ppmodel$ to denote $0$- and $2$-pointed structures, respectively.
For a structure $\model$ and two vertices $x, y \in |\model|$,
we write ${\model}[x, y]$ for the $2$-pointed structure $\tuple{|\model|, \set{a^{\model}}_{a \in \SIG_{\const{I}}^{(-)}}, x, y}$.

The binary relation $\jump{\term}_{\model} \subseteq |\model|^2$ of an $\ECoRTC$ term $\term$ on a structure $\model$ is defined as follows (where $a \in \SIG$):

a_                           a^
a^-_                       (a^-)^

_                        ∅
⊤_                        ||^2

[1] ∪[2]_      [1]_ ∪[2]_
[1] ∩[2]_      [1]_ ∩[2]_

I_                   I^
I^-_               (I^-)^

[1] ·[2]_     [1]_ ·[2]_

[1]^*_                ⋃_n ∈ [1]^n_
^⌣_              _^⌣.

We write $\models_{\REL} \term[1] = \term[2]$ if $\jump{\term[1]}_{\model} = \jump{\term[2]}_{\model}$ for every structure $\model$.
The equational theory over $\sig$ w.r.t. binary relations is defined as the set of all pairs $\term[1] = \term[2]$ of terms in $\Termset_{\sig}$ s.t. $\models_{\REL} \term[1] = \term[2]$.

Based on $\jump{\bl}_{\model}$, we define the following notations:

\begin{align*}
{\model}[x, y] \models \term         & \defiff \tuple{x, y} \in \jump{\term}_{\model}                                  \\
\ppmodel \models \term[1] = \term[2] & \defiff (\ppmodel \models \term[1]) \leftrightarrow (\ppmodel \models \term[2]) \\
\model \models \term[1] = \term[2]   & \defiff \jump{\term[1]}_{\model} = \jump{\term[2]}_{\model}.
\end{align*}

(Note that $\model \models \term[1] = \term[2] \iff \forall x, y \in |\model|.\  {\model}[x,y] \models \term[1] = \term[2]$.)

§.§ KA terms w.r.t. binary relations and word languages

For a set $X$, we write $X^*$ for the set of all finite sequences (i.e., words) over $X$.
We write $\const{I}$ for the empty word.
We write $w v$ for the concatenation of words $w$ and $v$.
For set $L, K \subseteq \SIG^*$, the composition $L \cdot K$ is defined by:

\[L \cdot K \defeq \set{w v \mid w \in L \ \land \  v \in K}.\]

The (word) language $\lang{\term} \subseteq \SIG^*$ of a KA term $\term$ is defined by:

a                           a

[1] ∪[2]      [1] ∪[2]

I                   I

[1] ·[2]     [1] ·[2]

[1]^*                ⋃_n ∈ [1]^n.

Interestingly, for KA terms, it is well-known that the equational theory w.r.t. binary relations coincides with that under the (single) word language interpretation (see, e.g., <cit.>):
for every KA terms $\term[1], \term[2]$, we have

\begin{equation}
\label{equation: rel and lang}
{} \models_{\REL} \term[1] \le \term[2] \quad \iff \quad \lang{\term[1]} \subseteq \lang{\term[2]}. \tag{$\dagger$}
\end{equation}

The following follows from (<ref>) and the known results in regular expressions <cit.> (<cit.>, for precise constructions):

The equational theory of $\Termset_{\set{\cdot, \cup}}$ (w.r.t. binary relations) is coNP-complete.

The equational theory of $\Termset_{\set{\cdot, \cup, \bl^{*}}}$ (w.r.t. binary relations) is PSPACE-complete.

They can show the lower bounds of <Ref>.

The equivalence (<ref>) breaks if we add $\cap$, $\bl^{\smile}$, or $\top$ by a standard word language interpretation <cit.>.
Note that (<ref>) also breaks if we add $a^{-}$ or $\const{I}^{-}$ with $\lang{a^{-}} \defeq \SIG^* \setminus \set{a}$
and $\lang{\const{I}^{-}} \defeq \SIG^* \setminus \set{\const{I}}$, respectively.
For example, $\models_{\REL} \top a \top b \top = \top b \top a \top$ holds <cit.>, but their languages are not the same.
Here, $\top$ abbreviates the term $c \cup \comnf{c}$ (cf. <Ref>) where $c$ is any.
Conversely, for example, $\lang{a^{-}} = \lang{\const{I} \cup (\SIG \setminus \set{a}) \cup (\SIG \cdot \SIG \cdot \SIG^*)}$ holds,
but such an equation does not hold in relational semantics (where a finite set $L = \set{\term[1]_1, \dots, \term[1]_n}$ of terms abbreviates the term $\term[1]_1 \cup \dots \cup \term[1]_n$, here).

§.§  and graph languages

Recall <Ref>.
Using graph languages rather than word languages, we can give a characterization of the equational theory w.r.t. binary relations for more general terms (e.g., <cit.>).
We use the following three operations on graphs,
series-composition ($\cdot$), parallel-composition ($\cap$), and converse ($\bl^{\smile}$):

\begin{align*}
G \cdot H
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {c/{}[draw, circle]}
-!- {t1/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of t1](t1l){}; \path (t1) edge[earrow, ->] (t1l);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 ->["$G$"] c;
c ->["$H$"] t1;
\end{tikzpicture}
& G \cap H
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {t1/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of t1](t1l){}; \path (t1) edge[earrow, ->] (t1l);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 ->["$G$", bend left = 25] t1;
s1 ->["$H$", bend right = 25] t1;
\end{tikzpicture} \\
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {t1/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of t1](t1l){}; \path (t1) edge[earrow, ->] (t1l);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
t1 ->["$G$"] s1;
\end{tikzpicture}.
\end{align*}

The following is inspired by <cit.>, <cit.> for $\PCoRTC$, where we extend the definition of $a^{-}$ and $\const{I}^{-}$ for $\ECoRTC$.

The graph language $\glang(t)$ of an $\ECoRTC$ term $t$ is a set of graphs over $\SIG_{\const{I}}^{(-)}$, defined by:

\begin{align*}
\glang(a)                               & \defeq \set{
\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 ->["$a$"] 1;
l -> 0; 1 -> r;
\end{tikzpicture}
}  \mbox{ where $a \in \Sigma^{(-)}$}                   \span\span                                                                                \\
\glang(\bot)                            & \defeq \emptyset                                                                                &
\glang(\top)                            & \defeq \set{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 1 -> r;
\end{tikzpicture}}                                 \\
\glang(\term[1] \cup \term[2])          & \defeq \glang(\term[1]) \cup \glang(\term[2])                                                                                \\
& \hspace{1.5em} \glang(\term[1] \cap \term[2])  \defeq
\set{G \cap H \mid G \in \glang(\term[1]) \ \land \  H \in \glang(\term[2])}                                                                                \span \span            \\
\glang(\const{I})                       & \defeq \set{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 0](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 0 -> r;
\end{tikzpicture}}                                 &
\glang(\const{I}^{-})                   & \defeq \set{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, font = \scriptsize, opacity = 1](a1){$\comnf{\const{I}}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 -- a1 -> 1;
l -> 0; 1 -> r;
\end{tikzpicture}} \\
\glang(\term[1] \cdot \term[2])         & \defeq \set{G \cdot H \mid G \in \glang(\term[1]) \ \land \  H \in \glang(\term[2])}                        \span \span                  \\
\glang(\term[1]^{*})                    & \defeq
\bigcup_{n \in \nat} \glang(\term[1]^n) &
\glang(\term[1]^{\smile})               & \defeq \set{ G^{\smile} \mid G \in \glang(\term[1])}.
\end{align*}

For a graph $G$ over $\SIG_{\const{I}}^{(-)}$, the binary relation $\jump{G}_{\model} \subseteq |\model|^2$ on a structure $\model$ is defined by:

\[\tuple{x, y} \in \jump{G}_{\model} \quad \defiff \quad (G \homo {\model}[x, y]).\]

($\graph[1] \homo \graph[2]$ denotes that there is a homomorphism from $\graph[1]$ to $\graph[2]$.)
For each graph language $\glang$, let

\[\jump{\glang}_{\model} \defeq \bigcup_{G \in \glang} \jump{G}_{\model}.\]

Based on $\jump{G}_{\model}$ and $\jump{\glang}_{\model}$, we use $\models$ (<Ref>) also for graphs and graph languages.
Note that:

\begin{align*}
\ppmodel \models G & \iff G \homo \ppmodel; & \ppmodel \models \glang & \iff \exists G \in \glang. G \homo \ppmodel.
\end{align*}

The graph languages above characterize the relational semantics and the equational theory for $\PCoRTC$, as follows
(<Ref> is shown by induction on $\term$ and <Ref> is shown by using <Ref>; see the full version <cit.><Ref>, for more details):

For every structure $\model$ and  term $\term$,

\[\jump{\term}_{\model} = \jump{\glang(\term)}_{\model}.\]

For every $\PCoRTC$ terms $\term[1], \term[2]$, we have

\[{} \models_{\REL} \term[1] \le \term[2] \iff \forall G \in \glang(\term[1]). \exists H \in \glang(\term[2]).\  H \homo G. \]

We can prove ${} \models_{\REL} a \cap b \le a \cap (\top b)$ by the homomorphism $\begin{tikzpicture}[baseline = -1.ex]
\graph[grow right = 1.2cm, branch down = 1.2ex, nodes={mynode}]{
{0/{}[draw, circle], 2/{}[draw, circle, xshift = 1.5em]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
0 ->["$a$"] 1;
2 ->["$b$", out = 0, in = -135] 1;
l -> 0; 1 -> r;
\end{tikzpicture} \homo \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
0 ->["$a$", bend left = 20] 1;
0 ->["$b$", bend right = 20] 1;
l -> 0; 1 -> r;
\end{tikzpicture}$. Here,

\begin{align*}
\mathcal{G}(a \cap b)        & = \set{\hspace{-.1em}\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
0 ->["$a$", bend left = 20] 1;
0 ->["$b$", bend right = 20] 1;
l -> 0; 1 -> r;
\end{tikzpicture}\hspace{-.1em}}; & \hspace{-.8em}
\mathcal{G}(a \cap (\top b)) & = \set{\hspace{-.1em}\begin{tikzpicture}[baseline = -1.ex]
\graph[grow right = 1.2cm, branch down = 1.2ex, nodes={mynode}]{
{0/{}[draw, circle], 2/{}[draw, circle, xshift = 1.5em]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
0 ->["$a$"] 1;
2 ->["$b$", out = 0, in = -135] 1;
l -> 0; 1 -> r;
\end{tikzpicture}\hspace{-.1em}}.
\end{align*}

§ GRAPH CHARACTERIZATION FOR

We consider extending <Ref> for $\ECoRTC$.
We can straightforwardly extend <Ref>.

For every structure $\model$ and $\ECoRTC$ term $\term$,
we have $\jump{t}_{\model} = \jump{\glang(t)}_{\model}$.

Similar to <Ref> (see the full version <cit.><Ref>).

However, we cannot extend <Ref>, immediately.

${} \models_{\REL} \top \le a \cup \comnf{a}$ holds (cf. <Ref>), but the right-hand side formula of <Ref> fails because
there does not exist any homomorphism from any graphs in $\glang(a \cup \comnf{a})$:

\begin{align*}
\glang(a \cup \comnf{a}) & = \quad \set{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5,inner sep = 1.5pt, font = \scriptsize, opacity = 1](a1){$a$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 -- a1 -> 1;
l -> 0; 1 -> r;
\end{tikzpicture}, \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt,font = \scriptsize, opacity = 1](a1){$\comnf{a}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 -- a1 -> 1;
l -> 0; 1 -> r;
\end{tikzpicture}} \\
\glang(\top)             & \ni \qquad \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 1 -> r;
\end{tikzpicture}.
\end{align*}

(The same problem occurs even without $\top$; consider ${} \models_{\REL} b \cup \comnf{b} \le a \cup \comnf{a}$ where $b \neq a$.)

To avoid the problem above, we consider modifying the graph languages using edge saturations.

§.§ Edge-saturated graphs and 2-pointed structures

For a binary relation $R$, we write $\eqcl{R}$ for the equivalence closure of $R$ (the minimal equivalence relation subsuming $R$).

For a graph $\graph$ over $\SIG_{\const{I}}^{(-)}$, we write $\graph^{\Quo}$ for the quotient graph[Precisely, $\graph^{\Quo}$ is the graph over $\SIG_{\const{I}}^{(-)}$, defined by
$|\graph^{\Quo}| = \set{\gquo{x}{\graph} \mid x \in \graph}$;
$a^{\graph^{\Quo}} = \set{\tuple{X, Y} \in |\graph^{\Quo}|^2 \mid \exists x \in X.\ \exists y \in Y.\   \tuple{x, y} \in a^{\graph}}$ for $a \in \SIG_{\const{I}}^{(-)}$;
$\tuple{\lv^{\graph^{\Quo}}, \rv^{\graph^{\Quo}}} = \tuple{\gquo{\lv^{\graph}}{\graph}, \gquo{\rv^{\graph}}{\graph}}$.] of $G$ w.r.t. the equivalence relation $\eqcl{(\const{I}^{G})}$;
e.g., if $G = \begin{tikzpicture}[baseline = -1.5ex]
\graph[grow right = 1.8cm, branch down = 2ex, nodes={mysmallnode, font=\scriptsize}]{
{0/{$0$}[draw, circle], 2/{$2$}[draw, circle, xshift = 2.2em]}-!-{1/{$1$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5,  inner sep = 1.5pt, font = \scriptsize, opacity = 1](a1){$a$}(1);
\path (2) edge [bend right= 15, draw = white, opacity = 0] node[pos= 0.4,  inner sep = 1.5pt, font = \scriptsize, opacity = 1](a2){$b$}(1);
\path (0) edge [bend right = 15, draw = white, opacity = 0] node[pos= 0.6,  inner sep = 1.5pt, font = \scriptsize, opacity = 1](a3){$\const{I}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
{0,2} -- {a1,a2} -> 1;
{2} --[bend left = 10] {a3} ->[bend left = 10] 0;
l -> 0; 1 -> r;
\end{tikzpicture}$, $G^{\Quo} = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.5cm, branch down = 2ex, nodes={mysmallnode, font=\tiny, minimum width=.7cm}]{
{0/{$\set{0,2}$}[draw, circle]}-!-{1/{$\set{1}$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5,  inner sep = 1.5pt, font = \scriptsize, opacity = 1](a1){$a$}(1);
\path (0) edge [bend right = 25, draw = white, opacity = 0] node[pos= 0.5,  inner sep = 1.5pt, font = \scriptsize, opacity = 1](a2){$b$}(1);
\node[right = .5em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 10] I00 ->[bend left = 10] 0;
{0} --[bend left = 10] {a1} ->[bend left = 10] 1;
{0} --[bend right = 10] {a2} ->[bend right = 10] 1;
l -> 0; 1 -> r;
\end{tikzpicture}$.
We use $\gquo{x}{\graph}$ to denote the quotient set of a vertex $x \in |\graph|$ w.r.t.  the equivalence relation $\eqcl{(\const{I}^{\graph})}$.

Let $\graph$ be a graph over $\SIG_{\const{I}}^{(-)}$.
We say that $G$ is consistent if for every $a \in \SIG_{\const{I}}$,  the following holds:

($a$-consistent) $(\eqcl{(\const{I}^{G})} \cdot a^{G} \cdot \eqcl{(\const{I}^{G})}) \cap (\eqcl{(\const{I}^{G})} \cdot \comnf{a}^{G} \cdot \eqcl{(\const{I}^{G})}) = \emptyset$.

We say that $G$ is (consistently) edge-saturated if $G$ is consistent and the following hold:

($a$-saturated)  $a^{G} \cup \comnf{a}^{G} = |G|^2$, for every $a \in \SIG_{\const{I}}$;

(I-equivalence) $\const{I}^{G}$ is an equivalence relation.

Each edge-saturated graph induces a $2$-pointed structure:

If a graph $G$ over $\SIG_{\const{I}}^{(-)}$ is edge-saturated, then $G^{\Quo}$ is a $2$-pointed structure.

$\const{I}^{G^{\Quo}}$ is the identity relation because $\const{I}^{G}$ is an equivalence relation <ref>.
For $a \in \SIG_{\const{I}}$, $\bar{a}^{G^{\Quo}} = |G^{\Quo}|^2 \setminus a^{G^{\Quo}}$ holds because
$a^{G^{\Quo}} \cup \bar{a}^{G^{\Quo}} = |G^{\Quo}|^2$ <ref>
and $a^{G^{\Quo}} \cap \bar{a}^{G^{\Quo}} = \emptyset$ <ref>.
Thus, $G^{\Quo}$ is a $2$-pointed structure.

§.§ Graph characterization via edge saturations

For graphs $\graph[1], \graph[2]$ over $\SIG_{\const{I}}^{(-)}$,
we say that $\graph[2]$ is an edge-extension of $\graph[1]$, if $|\graph[2]| = |\graph[1]|$ and $a^{\graph[2]} \supseteq a^{\graph[1]}$ for every $a \in \SIG_{\const{I}}^{(-)}$.
We say that $\graph[2]$ is an (edge-)saturation of $\graph[1]$ if
$\graph[2]$ is an edge-extension of $\graph[1]$ and is edge-saturated.

Let $\Fill(\graph[1])$ be the set of all saturations of $\graph[1]$.

For a graph language $\glang$,
let $\Fill(\glang) \defeq \bigcup_{\graph \in \glang} \Fill(\graph)$ and $\Quo(\glang) \defeq \set{\graph^{\Quo} \mid \graph \in \glang}$.
We abbreviate $\Quo \circ \Fill$ to $\QuoFill$.

When $\SIG = \set{a}$,
$\QuoFill(\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = .7cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 1 -> r;
\end{tikzpicture})$ is the set:

\[\left\{ \hspace{-.1em}\begin{tikzpicture}[remember picture, baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mynode}]{
{C0/{}[draw, circle]}
\node[left = .5em of C0](l){};
\node[right = .5em of C0](r){};
\node[below left = 2ex and .0em of C0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$\comnf{a}$};
\node[below right = 2ex and .0em of C0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
C0 --[bend left = 10] a00 ->[bend left = 10] C0;
C0 --[bend left = 10] I00 ->[bend left = 10] C0;
l -> C0; C0 -> r;
\end{tikzpicture},
\begin{tikzpicture}[remember picture, baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mynode}]{
{C0/{}[draw, circle]}
\node[left = .5em of C0](l){};
\node[right = .5em of C0](r){};
\node[below left = 2ex and .0em of C0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$a$};
\node[below right = 2ex and .0em of C0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
C0 --[bend left = 10] a00 ->[bend left = 10] C0;
C0 --[bend left = 10] I00 ->[bend left = 10] C0;
l -> C0; C0 -> r;
\end{tikzpicture},
\begin{tikzpicture}[remember picture, baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mynode}]{
{D0/{}[draw, circle]}-!-{D1/{}[draw, circle]}
\node[left = .5em of D0](l){};
\node[right = .5em of D1](r){};
\node[below left = 2ex and .0em of D0, inner sep = .5pt, font = \scriptsize, opacity = 1](a00){$\comnf{a}$};
\node[below left = 2ex and .0em of D1, inner sep = .5pt, font = \scriptsize, opacity = 1](a11){$\comnf{a}$};
\path (D0) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$\comnf{a}$}(D1);
\path (D1) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(D0);
\node[below right = 2ex and .0em of D0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[below right = 2ex and .0em of D1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (D0) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(D1);
\path (D1) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](I10){$\comnf{\const{I}}$}(D0);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
D0 --[bend left = 10] a00 ->[bend left = 10] D0;
D0 --[bend left = 10] a01 ->[bend left = 10] D1;
D1 --[bend left = 10] a10 ->[bend left = 10] D0;
D1 --[bend left = 10] a11 ->[bend left = 10] D1;
D0 --[bend left = 10] I00 ->[bend left = 10] D0;
D0 --[bend left = 10] I01 ->[bend left = 10] D1;
D1 --[bend left = 10] I10 ->[bend left = 10] D0;
D1 --[bend left = 10] I11 ->[bend left = 10] D1;
l -> D0; D1 -> r;
\end{tikzpicture}, \dots, \begin{tikzpicture}[remember picture, baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mynode}]{
{E0/{}[draw, circle]}-!-{E1/{}[draw, circle]}
\node[left = .5em of E0](l){};
\node[right = .5em of E1](r){};
\node[below left = 2ex and .0em of E0, inner sep = .5pt, font = \scriptsize, opacity = 1](a00){$\comnf{a}$};
\node[below left = 2ex and .0em of E1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a11){$a$};
\path (E0) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a01){$a$}(E1);
\path (E1) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(E0);
\node[below right = 2ex and .0em of E0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[below right = 2ex and .0em of E1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (E0) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(E1);
\path (E1) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](I10){$\comnf{\const{I}}$}(E0);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
E0 --[bend left = 10] a00 ->[bend left = 10] E0;
E0 --[bend left = 10] a01 ->[bend left = 10] E1;
E1 --[bend left = 10] a10 ->[bend left = 10] E0;
E1 --[bend left = 10] a11 ->[bend left = 10] E1;
E0 --[bend left = 10] I00 ->[bend left = 10] E0;
E0 --[bend left = 10] I01 ->[bend left = 10] E1;
E1 --[bend left = 10] I10 ->[bend left = 10] E0;
E1 --[bend left = 10] I11 ->[bend left = 10] E1;
l -> E0; E1 -> r;
\end{tikzpicture}, \dots \right\}.\]

$\QuoFill(\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = .7cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 1 -> r;
\end{tikzpicture})$ has $18$ graphs up to isomorphism (the sum of patterns ($2^{1 \times 1} = 2$) when the two vertices are connected with $\const{I}$ and patterns ($2^{2 \times 2} = 16$) otherwise).
For every $G$ in $\QuoFill(\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = .7cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 1 -> r;
\end{tikzpicture})$,
there exists a homomorphism to $G$ from [baseline = -.5ex]
[grow right = 1cm, branch down = 6ex, nodes=mynode]
0/[draw, circle]-!-1/[draw, circle]
[left = .5em of 0](l);
[right = .5em of 1](r);
(0) edge [draw = white, opacity = 0] node[pos= 0.5,inner sep = 1.5pt, font = , opacity = 1](a1)$a$(1);
[use existing nodes, edges=color=black, pos = .5, earrow, edge quotes=fill=white, inner sep=1pt,font= ]
0 – a1 -> 1;
l -> 0; 1 -> r;
or [baseline = -.5ex]
[grow right = 1cm, branch down = 6ex, nodes=mynode]
0/[draw, circle]-!-1/[draw, circle]
[left = .5em of 0](l);
[right = .5em of 1](r);
(0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt,font = , opacity = 1](a1)$\comnf{a}$(1);
[use existing nodes, edges=color=black, pos = .5, earrow, edge quotes=fill=white, inner sep=1pt,font= ]
0 – a1 -> 1;
l -> 0; 1 -> r;
, as $G$ is edge-saturated:

\begin{align*}
\glang(a \cup \comnf{a}) & = \hspace{.2em} \left\{\begin{tikzpicture}[baseline = -.5ex, remember picture]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{X0/{}[draw, circle]}-!-{X1/{}[draw, circle]}
\node[left = .5em of X0](l){};
\node[right = .5em of X1](r){};
\path (X0) edge [draw = white, opacity = 0] node[pos= 0.5,inner sep = 1.5pt, font = \scriptsize, opacity = 1](a1){$\comnf{a}$}(X1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
X0 -- a1 -> X1;
l -> X0; X1 -> r;
\end{tikzpicture}\right.
\hspace{.15em} , \hspace{.15em}
\left.\begin{tikzpicture}[baseline = -.5ex, remember picture]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{Y0/{}[draw, circle]}-!-{Y1/{}[draw, circle]}
\node[left = .5em of Y0](l){};
\node[right = .5em of Y1](r){};
\path (Y0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt,font = \scriptsize, opacity = 1](a1){$a$}(Y1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
Y0 -- a1 -> Y1;
l -> Y0; Y1 -> r;
\end{tikzpicture}\right\}                                                                   \\
\QuoFill(\glang(\top))   & = \hspace{.2em} \left\{\begin{tikzpicture}[baseline = -.5ex, remember picture]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{C0/{}[draw, circle]}
\node[left = .5em of C0](l){};
\node[right = .5em of C0](r){};
\node[below left = 2ex and .0em of C0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$\comnf{a}$};
\node[below right = 2ex and .0em of C0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
C0 --[bend left = 10] a00 ->[bend left = 10] C0;
C0 --[bend left = 10] I00 ->[bend left = 10] C0;
l -> C0; C0 -> r;
\end{tikzpicture},
\begin{tikzpicture}[baseline = -.5ex, remember picture]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{C20/{}[draw, circle]}
\node[left = .5em of C20](l){};
\node[right = .5em of C20](r){};
\node[below left = 2ex and .0em of C20, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$a$};
\node[below right = 2ex and .0em of C20, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
C20 --[bend left = 10] a00 ->[bend left = 10] C20;
C20 --[bend left = 10] I00 ->[bend left = 10] C20;
l -> C20; C20 -> r;
\end{tikzpicture}
\dots,
\begin{tikzpicture}[baseline = -.5ex, remember picture]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mynode}]{
{E0/{}[draw, circle]}-!-{E1/{}[draw, circle]}
\node[left = .5em of E0](l){};
\node[right = .5em of E1](r){};
\node[below left = 2ex and .0em of E0, inner sep = .5pt, font = \scriptsize, opacity = 1](a00){$\comnf{a}$};
\node[below left = 2ex and .0em of E1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a11){$a$};
\path (E0) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a01){$a$}(E1);
\path (E1) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(E0);
\node[below right = 2ex and .0em of E0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[below right = 2ex and .0em of E1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (E0) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(E1);
\path (E1) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](I10){$\comnf{\const{I}}$}(E0);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
E0 --[bend left = 10] a00 ->[bend left = 10] E0;
E0 --[bend left = 10] a01 ->[bend left = 10] E1;
E1 --[bend left = 10] a10 ->[bend left = 10] E0;
E1 --[bend left = 10] a11 ->[bend left = 10] E1;
E0 --[bend left = 10] I00 ->[bend left = 10] E0;
E0 --[bend left = 10] I01 ->[bend left = 10] E1;
E1 --[bend left = 10] I10 ->[bend left = 10] E0;
E1 --[bend left = 10] I11 ->[bend left = 10] E1;
l -> E0; E1 -> r;
\end{tikzpicture}, \dots \right\}. %
\begin{tikzpicture}[remember picture, overlay]
\path (X0) edge [homoarrow,->] (C0);
\path (X1) edge [homoarrow,->] (C0);
\path (Y0) edge [homoarrow,->] (C20);
\path (Y1) edge [homoarrow,->] (C20);
\path (Y0) edge [homoarrow,->] (E0);
\path (Y1) edge [homoarrow,->] (E1);
\end{tikzpicture}
\end{align*}

As above, by using $\QuoFill(\glang(\top))$ instead of $\glang(\top)$, we can avoid the problem in <Ref>.
Using $\QuoFill$, we can strengthen <Ref> (<cit.>, <cit.>), for $\ECoRTC$, as <Ref>.
We first show the following:

For any graph $\graph$ over $\SIG_{\const{I}}^{(-)}$,
$\jump{\graph}_{\model} = \jump{\QuoFill(\graph)}_{\model}$.

We prove that for any $\graph$, both $\jump{\graph}_{\model} = \jump{\Fill(\graph)}_{\model}$ and $\jump{\graph}_{\model} = \jump{\graph^{\Quo}}_{\model}$, respectively.

For $\jump{\graph}_{\model} = \jump{\Fill(\graph)}_{\model}$:
If $\graph[2] \in \Fill(\graph)$ and $h \colon \graph[2] \homo {\model}[x_0, y_0]$,
then $h \colon \graph \homo {\model}[x_0, y_0]$ because $\graph[2]$ is a saturation of $\graph$.
If $h \colon \graph \homo {\model}[x_0, y_0]$,
let $\graph[2]$ be the saturation of $\graph[1]$ s.t. $a^{H} = \set{\tuple{x,y} \mid \tuple{h(x), h(y)} \in a^{\model}}$ for $a \in \SIG_{\const{I}}^{(-)}$.
Then $h \colon \graph[2] \homo {\model}[x_0,y_0]$.
Here, $\graph[2]$ is an edge-extension of $\graph[1]$ because $\tuple{x, y} \in a^{\graph[1]} \Longrightarrow \tuple{h(x), h(y)} \in a^{\model} \Longrightarrow \tuple{x, y} \in a^{\graph[2]}$;
$\graph[2]$ is edge-saturated because $\model$ is edge-saturated; thus, $\graph[2]$ is indeed a saturation of $\graph[1]$.
For example, from the homomorphism for $\graph[1] \homo {\model}[x_0, y_0]$, by filling non-existing edges in $\graph[1]$ so that they map to edges of ${\model}$,
we can construct the saturation $\graph[2]$ of $\graph[1]$ s.t. $\graph[2] \homo {\model}[x_0, y_0]$, as follows:

\begin{align*}
& \graph[1] = \hspace{-.5em} \begin{tikzpicture}[remember picture, baseline = -1.ex]
\graph[grow right = 1cm, branch down = 1.5ex, nodes={mynode}]{
{1X0/{}[draw, circle]}-!-{/,1X2/{}[draw, circle]}-!-{1X1/{}[draw, circle]}
\node[left = .5em of 1X0](1Xl){};
\node[right = .5em of 1X1](1Xr){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
1X0 ->["$a$"] 1X1;
1X1 ->["$a$"] 1X2;
1X0 ->["$\const{I}$", bend right = 35] 1X2;
1Xl -> 1X0; 1X1 -> 1Xr;
\end{tikzpicture} \hspace{4em} \graph[2] =\hspace{-.5em} \begin{tikzpicture}[remember picture, baseline = -1.ex]
\graph[grow right = 1cm, branch down = 1.5ex, nodes={mynode}]{
{2X0/{}[draw, circle]}-!-{/,2X2/{}[draw, circle]}-!-{2X1/{}[draw, circle]}
\node[left = .5em of 2X0](2Xl){};
\node[right = .5em of 2X1](2Xr){};
\node[below right = 2ex and .0em of 2X0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](2XI00){$\const{I}$};
\node[below left = 2ex and .0em of 2X0, inner sep = .5pt, font = \scriptsize, opacity = 1](2Xa00){$a$};
\node[below right = 2ex and .0em of 2X1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](2XI11){$\const{I}$};
\node[below left = 2ex and .0em of 2X1, inner sep = .5pt, font = \scriptsize, opacity = 1](2Xa11){$a$};
\node[below right = 2ex and .0em of 2X2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](2XI22){$\const{I}$};
\node[below left = 2ex and .0em of 2X2, inner sep = .5pt, font = \scriptsize, opacity = 1](2Xa22){$a$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1.pt,font= \scriptsize}]{
2X0 <->["$a$"] 2X1;
2X1 <->["$a$"] 2X2;
2X0 <->["$a$"] 2X2;
2X0 <->["$\const{I}$", bend left = 20] 2X1;
2X2 <->["$\const{I}$", bend right = 35] 2X1;
2X0 <->["$\const{I}$", bend right = 35] 2X2;
2X0 --[bend left = 10] 2Xa00 ->[bend left = 10] 2X0;
2X0 --[bend left = 10] 2XI00 ->[bend left = 10] 2X0;
2X1 --[bend left = 10] 2Xa11 ->[bend left = 10] 2X1;
2X1 --[bend left = 10] 2XI11 ->[bend left = 10] 2X1;
2X2 --[bend left = 10] 2Xa22 ->[bend left = 10] 2X2;
2X2 --[bend left = 10] 2XI22 ->[bend left = 10] 2X2;
2Xl -> 2X0; 2X1 -> 2Xr;
\end{tikzpicture}     \\[-2ex]
& \hspace{6em} {\model}[x_0, y_0] = \hspace{-.5em}\begin{tikzpicture}[remember picture, baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mynode, inner sep = 1.5pt}]{
{4X0/{}[draw, circle]}-!-{4X1/{}[draw, circle]}
\node[above left = .1ex and .5em of 4X0](4Xl){};
\node[below left = .1ex and .5em of 4X0](4Xr){};
\node[below left = 2ex and .0em of 4X0, inner sep = .5pt, font = \scriptsize, opacity = 1](4Xa00){$a$};
\node[below left = 2ex and .0em of 4X1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](4Xa11){$\comnf{a}$};
\path (4X0) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](4Xa01){$a$}(4X1);
\path (4X1) edge [draw = white, opacity = 0, bend left = 18] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](4Xa10){$\comnf{a}$}(4X0);
\node[below right = 2ex and .0em of 4X0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](4XI00){$\const{I}$};
\node[below right = 2ex and .0em of 4X1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](4XI11){$\const{I}$};
\path (4X0) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](4XI01){$\comnf{\const{I}}$}(4X1);
\path (4X1) edge [draw = white, opacity = 0, bend left = 80] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](4XI10){$\comnf{\const{I}}$}(4X0);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
4X0 --[bend left = 10] 4Xa00 ->[bend left = 10] 4X0;
4X0 --[bend left = 10] 4Xa01 ->[bend left = 10] 4X1;
4X1 --[bend left = 10] 4Xa10 ->[bend left = 10] 4X0;
4X1 --[bend left = 10] 4Xa11 ->[bend left = 10] 4X1;
4X0 --[bend left = 10] 4XI00 ->[bend left = 10] 4X0;
4X0 --[bend left = 10] 4XI01 ->[bend left = 10] 4X1;
4X1 --[bend left = 10] 4XI10 ->[bend left = 10] 4X0;
4X1 --[bend left = 10] 4XI11 ->[bend left = 10] 4X1;
4Xl -> 4X0; 4X0 -> 4Xr;
\end{tikzpicture}.
\begin{tikzpicture}[remember picture, overlay]
\path (1X0) edge [homoarrow,->] (4X0);
\path (1X1) edge [homoarrow,->] (4X0);
\path (1X2) edge [homoarrow,->] (4X0);
\path (2X0) edge [homoarrow,->] (4X0);
\path (2X1) edge [homoarrow,->] (4X0);
\path (2X2) edge [homoarrow,->] (4X0);
\end{tikzpicture}
\end{align*}

For $\jump{\graph}_{\model} = \jump{\graph^{\Quo}}_{\model}$:
If $\graph[1]^{\Quo} \homo {\model}[x_0, y_0]$,
then $\graph[1] \homo {\model}[x_0,y_0]$ because $\graph[1] \homo \graph[1]^{\Quo}$ by the quotient map (with transitivity of $\homo$).
If $h \colon \graph \homo {\model}[x_0, y_0]$,
then $h \circ g \colon \graph[1]^{\Quo} \homo {\model}[x_0, y_0]$, where $g$ is a section of the quotient map from $\graph[1]$ to $\graph[1]^{\Quo}$ (a map $g$ s.t. $g(X) \in X$ for $X \in |\graph[1]^{\Quo}|$).
Hence, $\jump{\graph}_{\model} = \jump{\Fill(\graph)}_{\model} = \jump{\QuoFill(\graph)}_{\model}$.

For every $\ECoRTC$ terms $\term[1], \term[2]$,

\begin{equation*}
{} \models_{\REL} \term[1] \le \term[2] \iff \forall G \in \QuoFill(\glang(\term[1])). \exists H \in \glang(\term[2]).\ H \homo G.
\end{equation*}

By the following formula transformation:

\begin{align*}
& {} \models_{\REL} \term[1] \le \term[2]  \iff \forall \model.\  \jump{\term[1]}_{\model} \subseteq \jump{\term[2]}_{\model} \tag{Def.\ of $\models_{\REL}$}                                                 \\
& \iff \forall \model.\  \jump{\QuoFill(\glang(\term[1]))}_{\model} \subseteq \jump{\glang(\term[2])}_{\model} \tag{\Cref{proposition: semantics for graphs ECoR,lemma: graph characterization ECoR QuoFill}} \\
& \iff \forall \model. \forall G \in \QuoFill(\glang(\term[1])).\ \jump{G}_{\model} \subseteq \jump{\glang(\term[2])}_{\model}  \tag{Def.\ of $\jump{}$}                                                      \\
& \iff \forall G \in \QuoFill(\glang(\term[1])).\forall \model. \  \jump{G}_{\model} \subseteq \jump{\glang(\term[2])}_{\model}                                                                               \\
& \iff \forall G \in \QuoFill(\glang(\term[1])).\forall \ppmodel.                                                                                \\
& \quad (G \homo \ppmodel) \mbox{ implies } (\exists H \in \glang(\term[2]).\  H \homo \ppmodel) \tag{Def.\ of $\jump{}$}                                                                                \\
\label{tag: heart} & \iff \forall G \in \QuoFill(\glang(\term[1])). \exists H \in \glang(\term[2]).\ H \homo G. \tag{$\heartsuit$}
\end{align*}

Here, for (<ref>),
Let $H \in \glang(\term[2])$ be such that $H \homo G$.
Then for any $2$-pointed structure $\ppmodel$ s.t. $G \homo \ppmodel$,
we have $H \homo \ppmodel$ by transitivity of $\homo$.
By letting $\ppmodel = G$.
Note that $G$ is a $2$-pointed structure since $G \in \QuoFill(\glang(\term[1]))$ (<Ref>).

We should use $\QuoFill$, rather than $\Fill$.
Consider $\models_{\REL} \top \le \const{I} \cup \comnf{\const{I}}$.
Then there does not exist any homomorphism
from any graphs in $\glang(\const{I} \cup \comnf{\const{I}}) =  \set{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 0](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 0 -> r;
\end{tikzpicture}, \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt,font = \scriptsize, opacity = 1](a1){$\comnf{\const{I}}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 -- a1 -> 1;
l -> 0; 1 -> r;
\end{tikzpicture}}$ to the graph $\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0, bend left] node[pos= 0.5,inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$\const{I}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left] node[pos= 0.5,inner sep = 1.5pt, font = \scriptsize, opacity = 1](a10){$\const{I}$}(0);
\node[above = 2ex of 0,inner sep = 1.5pt, font = \scriptsize,](a00){$\const{I}$};
\node[above = 2ex of 1,inner sep = 1.5pt, font = \scriptsize,](a11){$\const{I}$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 15] a00 ->[bend left = 15] 0;
0 -- a01 -> 1;
1 -- a10 -> 0;
1 --[bend left = 15] a11 ->[bend left = 15] 1;
l -> 0; 1 -> r;
\end{tikzpicture} \in \Fill(\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = .7cm, branch down = 6ex, nodes={mynode}]{
{0/{}[draw, circle]}-!-{1/{}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
l -> 0; 1 -> r;
\end{tikzpicture})$.

§.§ Bounded model property

<Ref> gives an upper bound for the equational theories of existential calculi of relations.
Note that the model checking problem of $\ECoRTC$ is decidable in polynomial time.

The following problem is decidable in $\mathcal{O}(\len{t} \times \card(|\ppstruc|)^{\omega})$ time:
given a finite $2$-pointed structure $\ppstruc$ and an $\ECoRTC$ term $\term[1]$, does $\ppstruc \models \term[1]$ hold?
Here, $\omega$ is the matrix multiplication exponent.

Let $\ppmodel = {\model}[x, y]$.
For $\term[2] \in \mathrm{Sub}(\term)$,
let $f_{\term[2]} \colon |\model| \times |\model| \to \set{\const{true}, \const{false}}$ be such that
$f_{\term[2]}(x, y) = \const{true}$ iff $\tuple{x, y} \in \jump{\term[2]}_{\model}$.
Here, $\mathrm{Sub}(\term[1])$ denotes the set of all sub-terms of $\term[1]$.
Then the function tables of $\set{f_{\term[2]}}_{\term[2] \in \mathrm{Sub}(\term[1])}$ can be calculated by a simple dynamic programming on $\term[2]$,
where for the case $\term[2] = \term[3]^*$,
we use the algorithm for the transitive closure of boolean matrix <cit.>.

For every $\ECoRTC$ terms $\term[1]$, $\term[2]$,
we have:
${} \not\models_{\REL} \term[1] \le \term[2]$ $\iff$
there exists a $2$-pointed structure $\ppmodel \in \QuoFill(\glang(\term[1]))$ such that $\ppmodel \not\models \term[1] \le \term[2]$.

$\Longleftarrow$: Trivial.
Let $\ppmodel = {\model}[x, y] \in \QuoFill(\glang(\term[1]))$ be a $2$-pointed structure such that $\forall H \in \glang(\term[2])$, $H \not\homo \ppmodel$ (<Ref>).
Then $\tuple{x, y} \in \jump{\QuoFill(\glang(\term[1]))}_{\model}$ because $\QuoFill(\glang(\term[1])) \ni \ppmodel \homo {\model}[x, y]$ ($\homo$ is reflexive).
$\tuple{x,y} \not\in \jump{\glang(\term[2])}_{\model}$ because $\forall H \in \glang(\term[2]).\ H \not\homo \ppmodel$ (Def. of $\jump{}_{\model}$).
Thus $\tuple{x, y} \in \jump{\term[1]}_{\model}$ and $\tuple{x, y} \not\in \jump{\term[2]}_{\model}$ (<Ref>).
Hence $\ppstruc \not\models \term[1] \le \term[2]$.

The equational theory of $\ECoRTC$ is in $\Pi_{1}^{0}$.

Since $\not\models_{\REL} \term[1] = \term[2]$ if and only if $(\not\models_{\REL} \term[1] \le \term[2]) \lor (\not\models_{\REL} \term[2] \le \term[1])$,
it suffices to show that the following problem is in $\Sigma_{1}^{0}$:
given $\ECoRTC$ terms $\term[1], \term[2]$, does $\not\models_{\REL} \term[1] \le \term[2]$ hold?
This follows from <Ref> with <Ref>.
Note that for every $G \in \QuoFill(\glang(\term[1]))$, $\#(|G|)$ is always finite,
and that we can easily enumerate the graphs in $\QuoFill(\glang(\term[1]))$.

Particularly for $\ECoR$ (not $\ECoRTC$), graphs of each term $\term[1]$ have a linear number of vertices in the size $\len{\term[1]}$.

For every $\ECoR$ term $\term[1]$ and $G \in \QuoFill(\glang(\term[1]))$, we have $\card(|G|) \le 1 + \len{\term[1]}$.

By easy induction on $\term[1]$, we have: for every $H \in \glang(\term[1])$, $\card(|H|) \le 1 + \len{\term[1]}$.
Also $\#(|G|) \le \#(|H|)$ is clear for every $G \in \QuoFill(H)$.

The equational theory of $\ECoR$ is coNP-complete.

For hardness: By <ref>, as $\ECoR$ subsumes $\Termset_{\set{\cdot, \cup}}$.
For upper bound:
Similarly for <ref>,
we show that the following problem is in NP: given $\ECoR$ terms $\term[1], \term[2]$, does $\not\models_{\REL} \term[1] \le \term[2]$ hold?
By <Ref>, we can give the following algorithm:

* Take a graph $H \in \glang(\term[1])$ non-deterministically according to the definition of $\glang$;
then take a graph $G \in \Fill(H)$, non-deterministically ($G$ is a graph in $\Fill(\glang(\term[1]))$).

* Return $\const{true}$ if $G^{\Quo} \not\models \term[1] \le \term[2]$; $\const{false}$ otherwise.

Then $\not\models_{\REL} \term[1] \le \term[2]$ if some execution returns $\const{true}$; $\models_{\REL}  \term[1] \le \term[2]$ otherwise.
Here, $G^{\Quo} \not\models \term[1] \le \term[2]$ can be decided in polynomial time by
<Ref> with $\#(|G^{\Quo}|) \le 1 + \len{\term[1]}$ (<Ref>).

§ SATURABLE PATHS: SATURATIONS FROM A PATH GRAPH FOR INTERSECTION-FREE FRAGMENTS

In this section, we refine the graph characterization of edge-saturations (in the previous section) for $\ECoRTC$ without intersection ($\ExKA$, for short; <Ref>) by using saturable paths.

Using this characterization, we can show the decidability of the equational theory (<Ref>) and give an automata construction for two smaller fragments (<Ref>).

§.§ NFAs as terms

A non-deterministic finite automaton with epsilon translations $\empt$ (NFA, for short) $\automaton = \tuple{|\automaton|, \set{a^{\automaton}}_{a \in A}, \lv^{\automaton}, \rv^{\automaton}}$ over a set $A$ (with $A$ containing a designated element $\empt$) is a graph over $A$.
The transition relation $\delta_{w}^{\automaton}$ of a word $w = a_1 \dots a_n \in (A \setminus \set{\empt})^*$ is defined by:

\[\delta_{w}^{\automaton} \defeq (\empt^{\automaton})^* \cdot a_1^{\automaton} \cdot (\empt^{\automaton})^* \cdot \ldots \cdot (\empt^{\automaton})^* \cdot a_n^{\automaton} \cdot (\empt^{\automaton})^*.\]

For notational simplicity, for $x \in |\automaton|$ and $X \subseteq |\automaton|$,
let $\delta_{w}^{\automaton}(x) \defeq \set{y \mid \tuple{x, y} \in \delta_{w}^{\automaton}}$ and $\delta_{w}^{\automaton}(X) \defeq \bigcup_{x \in X} \delta_{w}^{\automaton}(x)$.
The language $\lang{\automaton}$ of $\automaton$ is defined by:

\[\lang{\automaton} \defeq \set{w \in (A \setminus \set{\empt})^* \mid \tgt^{\automaton} \in \delta_{w}^{\automaton}(\src^{\automaton})}.\]

Let $\SIG_{\const{I}}^{(-, \smile)} \defeq \set{a, a^{\smile} \mid a \in \SIG^{(-)}} \cup \set{\const{I}, \const{I}^{-}}$.
Similarly for $\comnf{\term}$,
for each $\term \in \SIG_{\const{I}}^{(-, \smile)} \cup \set{\bot, \top}$,
$\widebreve{\term}$ denotes the following term, where $a \in \SIG^{(-)}$:

\begin{align*}
\widebreve{a} & \defeq a^{\smile} & \widebreve{a^{\smile}} & \defeq a & \widebreve{\const{I}} & \defeq \const{I} & \widebreve{\const{I}^{-}} & \defeq \const{I}^{-} & \widebreve{\top} & \defeq \top & \widebreve{\bot} & \defeq \bot.
\end{align*}

In the following, we always consider NFAs over the set $\AutSIG$ (where $\const{I}$ is used as epsilon transitions).

For an NFA $\automaton$ over $\AutSIG$,
the binary relation $\jump{\automaton}_{\struc} \subseteq |\automaton|^2$ is defined by:

\[\jump{\automaton}_{\struc} \defeq \bigcup_{w \in \lang{\automaton}} \jump{w}_{\struc}.\]

Naturally, we can give a construction from $\ExKA$ terms to NFAs using Thompson's construction <cit.>, as follows:

The NFA $\automaton_t$ of an $\ExKA$ term $\term$ is defined by:

\begin{align*}
\automaton_{a}
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {sm/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of sm](sml){}; \path (sm) edge[earrow, ->] (sml);
\path (s1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau1){$a$}(sm);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 -- tau1 -> sm;
\end{tikzpicture}        \mbox{($a \in \WordSIG$)}                       &
\automaton_{\const{I}}
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {sm/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of sm](sml){}; \path (sm) edge[earrow, ->] (sml);
\path (s1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau1){$\empt$}(sm);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 -- tau1 -> sm;
\end{tikzpicture}                   \\
\automaton_{\term[1] \cup \term[2]}
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {s2/{}[draw, circle, above = .5ex], s3/{}[draw, circle, above = .5ex]}
-!- {t2/{}[draw, circle, above = .5ex], t3/{}[draw, circle, above = .5ex]}
-!- {t1/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of t1](t1l){}; \path (t1) edge[earrow, ->] (t1l);
\path (s1) edge [draw = white, opacity = 0, bend left = 10] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau12){$\empt$}(s2);
\path (s1) edge [draw = white, opacity = 0, bend right = 10] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau13){$\empt$}(s3);
\path (t2) edge [draw = white, opacity = 0, bend left = 10] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau21){$\empt$}(t1);
\path (t3) edge [draw = white, opacity = 0, bend right = 10] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau31){$\empt$}(t1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 -- {tau12, tau13} -> {s2, s3}; {t2, t3} -- {tau21, tau31} -> t1;
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s2 ->["$\automaton_{t}$"] t2;
s3 ->["$\automaton_{s}$"] t3;
\end{tikzpicture} &
\automaton_{\bot}
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {sm/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of sm](sml){}; \path (sm) edge[earrow, ->] (sml);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
\end{tikzpicture}                                                       \\
\automaton_{\term[1] \cdot \term[2]}
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {c1/{}[draw, circle]}
-!- {c2/{}[draw, circle]}
-!- {t1/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of t1](t1l){}; \path (t1) edge[earrow, ->] (t1l);
\path (c1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau1){$\empt$}(c2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
c1 -- {tau1} -> c2;
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 ->["$\automaton_{t}$"] c1;
c2 ->["$\automaton_{s}$"] t1;
\end{tikzpicture}                   & \automaton_{\top}
& \defeq \automaton_{a \cup \comnf{a}}                                                                                \\
\automaton_{\term[1]^{*}}
& \defeq \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mynode, font = \scriptsize}]{
{s1/{}[draw, circle]}
-!- {c1/{}[draw, circle]}
-!- {c2/{}[draw, circle]}
-!- {t1/{}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of t1](t1l){}; \path (t1) edge[earrow, ->] (t1l);
\path (s1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau1){$\empt$}(c1);
\path (c2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau2){$\empt$}(t1);
\path (c2) edge [draw = white, opacity = 0, bend left = 60] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau3){$\empt$}(c1);
\path (s1) edge [draw = white, opacity = 0, bend left = 20] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau4){$\empt$}(t1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 -- {tau1} -> c1;
c2 -- {tau2} -> t1;
c2 --[bend left = 15] {tau3} ->[bend left = 15] c1;
s1 --[bend left = 5] {tau4} ->[bend left = 5] t1;
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
c1 ->["$\automaton_{t}$"] c2;
\end{tikzpicture}.
\end{align*}

For every structure $\struc$ and $\ExKA$ term $\term$, we have $\jump{\term}_{\struc} = \jump{\automaton_{\term}}_{\struc}$.

Let $\term[2]$ be the term $\term$ in which each $\top$ has been replaced with $a \cup \comnf{a}$.
Then, $\jump{\term[2]}_{\model} = \jump{\term}_{\model}$ holds by <Ref>
and $\automaton_{\term[2]}$ coincides with $\automaton_{\term}$ (by <Ref>).
By viewing $\term[2]$ as the regular expression over $\WordSIG$, we have $\lang{\term[2]} = \lang{\automaton_{\term[2]}}$ <cit.>.
By straightforward induction on $\term[2]$ using the distributivity, $\jump{\term[2]}_{\struc} = \bigcup_{w \in \lang{\term[2]}} \jump{w}_{\struc}$ (<Ref>).
Thus $\jump{\term}_{\struc} = \jump{\term[2]}_{\struc} = \bigcup_{w \in \lang{\term[2]}} \jump{w}_{\struc} = \bigcup_{w \in \lang{\automaton_{\term[2]}}} \jump{w}_{\struc} = \jump{\automaton_{\term[2]}}_{\struc} = \jump{\automaton_{\term}}_{\struc}$.

Thanks to the above proposition, we work directly with NFAs rather than terms in the sequel.

§.§ Saturable paths

For a word $w \in (\WordSIG)^*$,
we use $\graph(w)$ to denote the unique graph in $\glang(w)$ (<Ref>), up to isomorphism.
Here, each vertex in $\graph(w)$ is indexed by a number in $[0, n]$, from the left to the right,
where $w = a_1 \dots a_n$.
For example,

\[\graph(\comnf{\const{I}} a^{\smile} \comnf{a}) =  \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mysmallnode, font = \scriptsize}]{
{s1/{$0$}[draw, circle]}
-!- {c1/{$1$}[draw, circle]}
-!- {c2/{$2$}[draw, circle]}
-!- {t1/{$3$}[draw, circle]}
\node[left = 4pt of s1](s1l){} edge[earrow, ->] (s1);
\node[right = 4pt of t1](t1l){}; \path (t1) edge[earrow, ->] (t1l);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
s1 ->["$\comnf{\const{I}}$"] c1;
c2 ->["$a$"] c1;
c2 ->["$\comnf{a}$"] t1;
\end{tikzpicture}.\]

For each $w$, $G(w)$ is a path graph (by forgetting labels and directions of edges).

Recall $\jump{\automaton}_{\model}$ in <Ref>.
Based on $\jump{\automaton}_{\model}$, we use $\models$ (<Ref>) also for automata.
Note that:

\begin{align*}
\ppmodel \models \automaton & \iff \exists w \in \lang{\automaton}.\ \ppmodel \models w \tag{Def.\ of $\jump{\automaton}_{\model}$}           \\
& \iff \exists w \in \lang{\automaton}.\ G(w) \homo \ppmodel. \tag{\Cref{proposition: semantics for graphs ECoR}}
\end{align*}

In this subsection, we consider the following saturability problem:
given an NFA $\automaton[1]$ and a word $w$, is there a saturation $\graph[2]$ of $\graph(w)$ such that $\graph[2]^{\Quo} \not\models \automaton[1]$? (Recall $\graph[2]^{\Quo}$ (<Ref>).)
This problem can apply to the equational theory (<Ref>).
For this problem, we introduce saturable paths.

Let $\SIG = \set{a}$.
Let $\automaton[1]$ be the NFA obtained from the term $\comnf{a} \cdot \comnf{a} \cdot \comnf{a}^*$ and $w = \comnf{a}$:

\begin{align*}
\automaton[1] & = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.25cm, branch down = 2.5ex, nodes={mysmallnode, font = \scriptsize}]{
{1/{$\mathtt{A}$}[draw, circle]}
-!- {2/{$\mathtt{B}$}[draw, circle]}
-!- {3/{$\mathtt{C}$}[draw, circle]}
\node[left = 4pt of 1](l){} edge[earrow, ->] (1);
\node[right = 4pt of 3](r){}; \path (3) edge[earrow, ->] (r);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](tau1){$\comnf{a}$}(2);
\path (2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau2){$\comnf{a}$}(3);
\node[above = 1.5ex of 3, inner sep = 1.pt,  font= \scriptsize, opacity = 1](tau3){$\comnf{a}$};
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
1 -- {tau1} -> 2;
2 -- {tau2} -> 3;
3 --[bend left = 20] {tau3} ->[bend left = 20] 3;
\end{tikzpicture} &
G(w)          & = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.25cm, branch down = 2.5ex, nodes={mysmallnode, font = \scriptsize}]{
{1/{$0$}[draw, circle]}
-!- {2/{$1$}[draw, circle]}
\node[left = 4pt of 1](l){} edge[earrow, ->] (1);
\node[right = 4pt of 2](r){}; \path (2) edge[earrow, ->] (r);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau1){$\comnf{a}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
1 -- {tau1} -> 2;
\end{tikzpicture}.
\end{align*}

Let us consider constructing a saturation $\graph[2]$ of $\graph(w)$ such that $\graph[2]^{\Quo} \not\models \automaton[1]$.
In this case, the following $\textcolor{blue}{\graph[2]_1}$ is the unique solution ($\textcolor{red}{\graph[2]_2}, \textcolor{red}{\graph[2]_3}, \textcolor{red}{\graph[2]_4}$ are not the solution because $\mathtt{C} \in U_1$):

\begin{align*}
\textcolor{blue}{\graph[2]_1} & = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.5cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\node[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$a$};
\node[above left = 2ex and .0em of 1, inner sep = .5pt, font = \scriptsize, opacity = 1](a11){$a$};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$\comnf{a}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$a$}(0);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 10] a00 ->[bend left = 10] 0;
1 --[bend left = 10] a11 ->[bend left = 10] 1;
0 -- a01 -> 1;
1 --[bend left = 15] a10 ->[bend left = 15] 0;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
\node[below = .5ex of 0, font = \scriptsize]{($\mathtt{A}$)};
\node[below = .5ex of 1, font = \scriptsize]{($\mathtt{B}$)};
\end{tikzpicture} &
\textcolor{red}{\graph[2]_2}  & = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.5cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\node[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$a$};
\node[above left = 2ex and .0em of 1, inner sep = .5pt, font = \scriptsize, opacity = 1](a11){$a$};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$\comnf{a}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(0);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 10] a00 ->[bend left = 10] 0;
1 --[bend left = 10] a11 ->[bend left = 10] 1;
0 -- a01 -> 1;
1 --[bend left = 15] a10 ->[bend left = 15] 0;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
\node[below = .5ex of 0, font = \scriptsize]{($\mathtt{A}, \mathtt{C}$)};
\node[below = .5ex of 1, font = \scriptsize]{($\mathtt{B}, \textcolor{red}{\mathtt{C}}$)};
\end{tikzpicture} \\
\textcolor{red}{\graph[2]_3}  & = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.5cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\node[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$\comnf{a}$};
\node[above left = 2ex and .0em of 1, inner sep = .5pt, font = \scriptsize, opacity = 1](a11){$a$};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$\comnf{a}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$a$}(0);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 10] a00 ->[bend left = 10] 0;
1 --[bend left = 10] a11 ->[bend left = 10] 1;
0 -- a01 -> 1;
1 --[bend left = 15] a10 ->[bend left = 15] 0;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
\node[below = .5ex of 0, font = \scriptsize]{($\mathtt{A}, \mathtt{B}, \mathtt{C}$)};
\node[below = .5ex of 1, font = \scriptsize]{($\mathtt{B}, \textcolor{red}{\mathtt{C}}$)};
\end{tikzpicture} &
\textcolor{red}{\graph[2]_4}  & = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.5cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\node[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$a$};
\node[above left = 2ex and .0em of 1, inner sep = .5pt, font = \scriptsize, opacity = 1](a11){$\comnf{a}$};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$\comnf{a}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$a$}(0);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 10] a00 ->[bend left = 10] 0;
1 --[bend left = 10] a11 ->[bend left = 10] 1;
0 -- a01 -> 1;
1 --[bend left = 15] a10 ->[bend left = 15] 0;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
\node[below = .5ex of 0, font = \scriptsize]{($\mathtt{A}$)};
\node[below = .5ex of 1, font = \scriptsize]{($\mathtt{B}, \textcolor{red}{\mathtt{C}}$)};
\end{tikzpicture}.
\end{align*}

Here the states under each vertex denote that they are reachable from the state $\mathtt{A}$ on the vertex $0$;
more precisely, each set $U_{i} \subseteq |\automaton|$ (where $i \in |G(w)|$) is defined by:

\begin{align*}
z \in U_{i} & \defiff \exists v \in \lang{{\automaton}[\bl, z]}.\  G(v) \homo \graph[2]^{\Quo}[\bl, \gquo{i}{\graph[2]}].
\end{align*}

Here, ${\automaton}[\bl, z]$ denotes the graph $\automaton$ in which $\rv^{\automaton}$ has been replaced with $z$ (similarly for $\graph[2]^{\Quo}[\bl, \gquo{i}{\graph[2]}]$).
By definition, $\graph[2]^{\Quo} \not\models \automaton$ (iff $\lnot (\exists v \in \lang{{\automaton}}.\  G(v) \homo \graph[2]^{\Quo})$) iff $\rv^{\automaton[1]} \not\in U_{\rv^{\graph[2]}}$.
For example, in $\textcolor{red}{\graph[2]_2}$, $\mathtt{C} \in U_{1}$ because $G(\comnf{a} \; \comnf{a} \;  \comnf{a}) \homo \graph[2]_2^{\Quo}$ holds by:

\begin{align*}
& \begin{tikzpicture}[baseline = -.5ex, remember picture]
\graph[grow right = 1.25cm, branch down = 2.5ex, nodes={mynode, font = \scriptsize}]{
{L1/{}[draw, circle]}
-!- {L2/{}[draw, circle]}
-!- {L3/{}[draw, circle]}
-!- {L4/{}[draw, circle]}
\node[left = 4pt of L1](Ll){} edge[earrow, ->] (L1);
\node[right = 4pt of L4](Lr){}; \path (L4) edge[earrow, ->] (Lr);
\path (L1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](Ltau1){$\comnf{a}$}(L2);
\path (L2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](Ltau2){$\comnf{a}$}(L3);
\path (L3) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](Ltau3){$\comnf{a}$}(L4);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
L1 -- {Ltau1} -> L2;
L2 -- {Ltau2} -> L3;
L3 -- {Ltau3} -> L4;
\node[below = .5ex of L1, font = \scriptsize]{($\mathtt{A}$)};
\node[below = .5ex of L2, font = \scriptsize]{($\mathtt{B}$)};
\node[below = .5ex of L3, font = \scriptsize]{($\mathtt{C}$)};
\node[below = .5ex of L4, font = \scriptsize]{($\mathtt{C}$)};
\end{tikzpicture}
\quad
\begin{tikzpicture}[baseline = -.5ex, remember picture]
\graph[grow right = 1.5cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{R0/{$0$}[draw, circle]}-!-{R1/{$1$}[draw, circle]}
\node[left = .5em of R0](Rl){};
\node[right = .5em of R1](Rr){};
\node[above left = 2ex and .0em of R0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](Ra00){$a$};
\node[above left = 2ex and .0em of R1, inner sep = .5pt, font = \scriptsize, opacity = 1](Ra11){$a$};
\path (R0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](Ra01){$\comnf{a}$}(R1);
\path (R1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](Ra10){$\comnf{a}$}(R0);
\node[above right = 2ex and .0em of R0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](RI00){$\const{I}$};
\node[above right = 2ex and .0em of R1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](RI11){$\const{I}$};
\path (R0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](RI01){$\comnf{\const{I}}$}(R1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
R0 --[bend left = 10] Ra00 ->[bend left = 10] R0;
R1 --[bend left = 10] Ra11 ->[bend left = 10] R1;
R0 -- Ra01 -> R1;
R1 --[bend left = 15] Ra10 ->[bend left = 15] R0;
R0 --[bend left = 10] RI00 ->[bend left = 10] R0;
R1 --[bend left = 10] RI11 ->[bend left = 10] R1;
R0 <-[bend left = 10] RI01 ->[bend left = 10] R1;
Rl -> R0; R1 -> Rr;
\node[below = 3ex of R0]{};
\end{tikzpicture}.
\begin{tikzpicture}[remember picture, overlay]
\path (L1.north) edge [homoarrow,->, bend left = 10] (R0.north west);
\path (L2.south) edge [homoarrow,->, bend right = 10] (R1.south);
\path (L3.north) edge [homoarrow,->, bend left = 15] (R0.north west);
\path (L4.south) edge [homoarrow,->, bend right = 15] (R1.south);
\end{tikzpicture}
\end{align*}

In contrast, in $\graph[2]_1$, because $\mathtt{C} \not\in U_1$ (i.e., $\forall v \in [\automaton].\  \graph(v) \not\homo \graph[2]_{1}^{\Quo}$) holds, we have $\graph[2]_1^{\Quo} \not\models \automaton$.

Consider the following $P$, which is the graph $G(w)$ with an equivalence relation $\const{I}$, its complement $\comnf{\const{I}}$, and $\set{U_{i}}_{i \in |G(w)|}$:

\begin{align*}
P & = \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.5cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 1](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$\comnf{a}$}(1);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 -- a01 -> 1;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
\node[below = .5ex of 0, font = \scriptsize]{$\mathtt{A}$};
\node[below = .5ex of 1, font = \scriptsize]{$\mathtt{B}$};
\end{tikzpicture}.
\end{align*}

Using only the data of $P$, we can show the existence of a saturation of $G(w)$.
For each pair $\tuple{i, j}$ of vertices,
if ($\delta_{a}^{\automaton[1]}(U_{i}) \subseteq U_{j}$ and $\delta_{\widebreve{a}}^{\automaton[1]}(U_{j}) \subseteq U_{i}$) or
($\delta_{\comnf{a}}^{\automaton[1]}(U_{i}) \subseteq U_{j}$ and $\delta_{\widebreve{\comnf{a}}}^{\automaton[1]}(U_{j}) \subseteq U_{i}$) holds (cf. <ref> in <Ref>),
then we add either the $a$- or $\comnf{a}$-labeled edge, according to this condition;
for example, for the pair $\tuple{1, 0}$,
since $\delta_{a}^{\automaton[1]}(U_1) = \emptyset \subseteq U_0$ and $\delta_{\widebreve{a}}^{\automaton[1]}(U_0) = \emptyset \subseteq U_1$ hold,
we add the edge for $\tuple{1, 0} \in a^{\graph[2]}$ (we cannot add the edge for $\tuple{1, 0} \in \comnf{a}^{\graph[2]}$ because $\delta_{\comnf{a}}^{\automaton[1]}(U_1) = \set{\mathtt{C}} \not\subseteq U_0$).
Note that $\set{U_{i}}_{x \in |G(w)|}$ is invariant when we add edges in this strategy.
By adding such edges as much as possible, we can give a saturation of $G(w)$ from $P$ preserving $\set{U_{i}}_{x \in |G(w)|}$ (cf. <Ref>); finally, $H_1$ is obtained, as follows (from the left to the right):

.85[baseline = -.5ex]
[grow right = 1.5cm, branch down = 6ex, nodes=mysmallnode, font = ]
0/$0$[draw, circle]-!-1/$1$[draw, circle]
[left = .5em of 0](l);
[right = .5em of 1](r);

(0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = , opacity = 1](a01)$\comnf{a}$(1);

[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = , opacity = 1](I00)$\const{I}$;
[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = , opacity = 1](I11)$\const{I}$;
(0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = , opacity = 1](I01)$\comnf{\const{I}}$(1);
[use existing nodes, edges=color=black, pos = .5, earrow, edge quotes=fill=white, inner sep=1pt,font= ]

0 – a01 -> 1;

0 –[bend left = 10] I00 ->[bend left = 10] 0;
1 –[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
[below = .5ex of 0, font = ]($\mathtt{A}$);
[below = .5ex of 1, font = ]($\mathtt{B}$);

[baseline = -.5ex]
[grow right = 1.5cm, branch down = 6ex, nodes=mysmallnode, font = ]
0/$0$[draw, circle]-!-1/$1$[draw, circle]
[left = .5em of 0](l);
[right = .5em of 1](r);

(0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = , opacity = 1](a01)$\comnf{a}$(1);
(1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = , opacity = 1](a10)$a$(0);
[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = , opacity = 1](I00)$\const{I}$;
[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = , opacity = 1](I11)$\const{I}$;
(0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = , opacity = 1](I01)$\comnf{\const{I}}$(1);
[use existing nodes, edges=color=black, pos = .5, earrow, edge quotes=fill=white, inner sep=1pt,font= ]

0 – a01 -> 1;
1 –[bend left = 15, line width = 1.2pt] a10 ->[bend left = 15, line width = 1.2pt] 0;
0 –[bend left = 10] I00 ->[bend left = 10] 0;
1 –[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
[below = .5ex of 0, font = ]($\mathtt{A}$);
[below = .5ex of 1, font = ]($\mathtt{B}$);

[baseline = -.5ex]
[grow right = 1.5cm, branch down = 6ex, nodes=mysmallnode, font = ]
0/$0$[draw, circle]-!-1/$1$[draw, circle]
[left = .5em of 0](l);
[right = .5em of 1](r);
[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = , opacity = 1](a00)$a$;

(0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = , opacity = 1](a01)$\comnf{a}$(1);
(1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = , opacity = 1](a10)$a$(0);
[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = , opacity = 1](I00)$\const{I}$;
[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = , opacity = 1](I11)$\const{I}$;
(0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = , opacity = 1](I01)$\comnf{\const{I}}$(1);
[use existing nodes, edges=color=black, pos = .5, earrow, edge quotes=fill=white, inner sep=1pt,font= ]
0 –[bend left = 10, line width = 1.2pt] a00 ->[bend left = 10, line width = 1.2pt] 0;

0 – a01 -> 1;
1 –[bend left = 15] a10 ->[bend left = 15] 0;
0 –[bend left = 10] I00 ->[bend left = 10] 0;
1 –[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
[below = .5ex of 0, font = ]($\mathtt{A}$);
[below = .5ex of 1, font = ]($\mathtt{B}$);

[baseline = -.5ex]
[grow right = 1.5cm, branch down = 6ex, nodes=mysmallnode, font = ]
0/$0$[draw, circle]-!-1/$1$[draw, circle]
[left = .5em of 0](l);
[right = .5em of 1](r);
[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = , opacity = 1](a00)$a$;
[above left = 2ex and .0em of 1, inner sep = .5pt, font = , opacity = 1](a11)$a$;
(0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = , opacity = 1](a01)$\comnf{a}$(1);
(1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = , opacity = 1](a10)$a$(0);
[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = , opacity = 1](I00)$\const{I}$;
[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = , opacity = 1](I11)$\const{I}$;
(0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = , opacity = 1](I01)$\comnf{\const{I}}$(1);
[use existing nodes, edges=color=black, pos = .5, earrow, edge quotes=fill=white, inner sep=1pt,font= ]
0 –[bend left = 10] a00 ->[bend left = 10] 0;
1 –[bend left = 10, line width = 1.2pt] a11 ->[bend left = 10, line width = 1.2pt] 1;
0 – a01 -> 1;
1 –[bend left = 15] a10 ->[bend left = 15] 0;
0 –[bend left = 10] I00 ->[bend left = 10] 0;
1 –[bend left = 10] I11 ->[bend left = 10] 1;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
l -> 0; 1 -> r;
[below = .5ex of 0, font = ]($\mathtt{A}$);
[below = .5ex of 1, font = ]($\mathtt{B}$);

[another example with $\bl^{\smile}$ and $\comnf{\const{I}}$]
Let $\SIG = \set{a}$.
Let $\automaton[1]$ be the NFA obtained from $\comnf{\const{I}} \cdot (\widebreve{a} \cdot \widebreve{\comnf{a}})^*$ and $w = a \comnf{a}$:

\begin{align*}
\automaton[1] & = \scalebox{.85}{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mysmallnode, font = \scriptsize}]{
{1/{$\mathtt{A}$}[draw, circle]}
-!- {2/{$\mathtt{B}$}[draw, circle]}
-!- {3/{$\mathtt{C}$}[draw, circle]}
-!- {4/{$\mathtt{D}$}[draw, circle]}
\node[left = 4pt of 1](l){} edge[earrow, ->] (1);
\node[right = 4pt of 4](r){}; \path (4) edge[earrow, ->] (r);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](tau1){$\comnf{\const{I}}$}(2);
\path (2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau2){$\widebreve{a}$}(3);
\path (3) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau3){$\widebreve{\comnf{a}}$}(4);
\path (2) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](g){$\empt$}(4);
\path (4) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](b){$\empt$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
1 -- {tau1} -> 2;
2 -- {tau2} -> 3;
3 -- {tau3} -> 4;
2 --[bend left = 15] {g} ->[bend left = 15] 4;
4 --[bend left = 15] {b} ->[bend left = 15] 2;
\end{tikzpicture}} &
G(w)          & = \scalebox{.85}{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 2.5ex, nodes={mysmallnode, font = \scriptsize}]{
{1/{$0$}[draw, circle]}
-!- {2/{$1$}[draw, circle]}
-!- {3/{$2$}[draw, circle]}
\node[left = 4pt of 1](l){} edge[earrow, ->] (1);
\node[right = 4pt of 3](r){}; \path (3) edge[earrow, ->] (r);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau1){$a$}(2);
\path (2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau2){$\comnf{a}$}(3);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
1 -- {tau1} -> 2;
2 -- {tau2} -> 3;
\end{tikzpicture}}.
\end{align*}

Let us consider constructing a saturation $\graph[2]$ of $\graph(w)$ such that $\graph[2]^{\Quo} \not\models \automaton[1]$.
Then, the following $\graph[2]$ is a solution (note that $\mathtt{D} \not\in U_2$; thus, $\graph[2]^{\Quo} \not\models \automaton$)
and the following $P$ is the corresponding saturable path:

\begin{align*}
\textcolor{blue}{\graph[2]} & = \hspace{-.4em} \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}-!-{2/{$2$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 2](r){};
\node[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$a$};
\node[above left = 2ex and .0em of 1, inner sep = .5pt, font = \scriptsize, opacity = 1](a11){$\comnf{a}$};
\node[above left = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a22){$a$};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$a$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(0);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a12){$\comnf{a}$}(2);
\path (2) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a21){$a$}(1);
\path (0) edge [draw = white, opacity = 0, bend right = 30] node[pos= 0.4, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a02){$a$}(2);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\node[above right = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I22){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I12){$\comnf{\const{I}}$}(2);
\path (0) edge [draw = white, opacity = 0, bend right = 45] node[pos= 0.6, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I02){$\const{I}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 10] a00 ->[bend left = 10] 0;
1 --[bend left = 10] a11 ->[bend left = 10] 1;
2 --[bend left = 10] a22 ->[bend left = 10] 2;
0 --[] a01 ->[] 1;
1 --[bend left = 15] a10 ->[bend left = 15] 0;
1 --[] a12 ->[] 2;
2 --[bend left = 15] a21 ->[bend left = 15] 1;
0.south east <-[bend right = 10] a02 ->[bend right = 10] 2.south west;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
2 --[bend left = 10] I22 ->[bend left = 10] 2;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
1 <-[bend left = 10] I12 ->[bend left = 10] 2;
0.south <-[bend right = 10] I02 ->[bend right = 10] 2.south;
l -> 0; 2 -> r;
\node[below = 2.5ex of 0,  font = \scriptsize]{($\mathtt{A,C}$)};
\node[below = 2.5ex of 1,  font = \scriptsize]{($\mathtt{B,D}$)};
\node[below = 2.5ex of 2,  font = \scriptsize]{($\mathtt{A,C}$)};
\end{tikzpicture}  &
P                           & = \hspace{-.4em}  \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}-!-{2/{$2$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 2](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5,  inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$a$}(1);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5,  inner sep = .5pt, font = \scriptsize, opacity = 1](a12){$\comnf{a}$}(2);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\node[above right = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I22){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5,  inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5,  inner sep = .5pt, font = \scriptsize, opacity = 1](I12){$\comnf{\const{I}}$}(2);
\path (0) edge [draw = white, opacity = 0, bend right = 45] node[pos= 0.6,  inner sep = 1.5pt, font = \scriptsize, opacity = 1](I02){$\const{I}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[] a01 ->[] 1;
1 --[] a12 ->[] 2;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
2 --[bend left = 10] I22 ->[bend left = 10] 2;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
1 <-[bend left = 10] I12 ->[bend left = 10] 2;
0.south <-[bend right = 10] I02 ->[bend right = 10] 2.south;
l -> 0; 2 -> r;
\node[below = 2.5ex of 0,  font = \scriptsize]{$\mathtt{A,C}$};
\node[below = 2.5ex of 1,  font = \scriptsize]{$\mathtt{B,D}$};
\node[below = 2.5ex of 2,  font = \scriptsize]{$\mathtt{A,C}$};
\end{tikzpicture}.
\end{align*}

(See <Ref> for an example when there is no saturation.)

Inspired by $\set{U_{i}}_{i \in |G(w)|}$ above, for characterizing the saturability problem, we define saturable paths;
they are path graphs with additional data (an equivalence relation $\const{I}$, its complement $\comnf{\const{I}}$, and $\set{U_{i}}_{i \in |G(w)|}$) for taking saturations appropriately.
For graphs $\graph[1], \graph[2]$ over $\SIG_{\const{I}}^{(-)}$,
we say that $\graph[2]$ is an $\const{I}$-saturation of $\graph[1]$ if
$\graph[2]$ is an edge-extension of $\graph[1]$ such that

* for every $a \in \SIG^{(-)}$, $a^{\graph[2]} = a^{\graph[1]}$;

* $\const{I}^{\graph[2]}$ is an equivalence relation and $\comnf{\const{I}}^{\graph[2]} = |\graph[2]|^2 \setminus \const{I}^{\graph[2]}$;

* $\graph[2]$ is consistent.

(By definition, $\graph[2]$ is uniquely determined from $\const{I}^{\graph[2]}$, if exists.)

For an NFA $\automaton$ over $\AutSIG$ and a word $w$ over $\WordSIG$,
consider a pair $P = \tuple{G, \set{U_{i}}_{i \in |G|}}$ of

* $G$ an $\const{I}$-saturation of $G(w)$;

* $U_i \subseteq |\automaton|$ for each $i \in |\graph|$.

For $a \in \SIG_{\const{I}}^{(-, \smile)}$, let

\[\Con_{a}^{\automaton}(U, U')  \defeq (\delta_{a}^{\automaton}(U) \subseteq U' \land \delta_{\widebreve{a}}^{\automaton}(U') \subseteq U).\]

Then we say that $P$ is a saturable path for $\not\models_{\REL} w \le \automaton$ if the following three hold:

(P-s-t) $\lv^{\automaton} \in U_{\lv^{G}}$ and $\rv^{\automaton} \not\in U_{\rv^{G}}$;

(P-Con) for all $a \in \SIG_{\const{I}}^{(-)}$ and $\tuple{i, j} \in a^{G}$, $\Con_{a}^{\automaton}(U_{i}, U_{j})$;

(P-Sat)  for all $a \in \SIG_{\const{I}}$ and $\tuple{i, j} \in |G|^2$,

$\Con_{a}^{\automaton}(U_{i}, U_{j}) \lor \Con_{\comnf{a}}^{\automaton}(U_{i}, U_{j})$.

Saturable paths can characterize the saturability problem, as <Ref>.
We first show the following:

For every saturable path $P = \tuple{G, \set{U_{i}}_{i \in |G|}}$ for $\not\models_{\REL} w \le \automaton$,
there is a saturation $H$ of $G$ such that

(P-Con') for all $a \in \SIG_{\const{I}}^{(-)}$ and $\tuple{i, j} \in a^{\graph[2]}$, $\Con_{a}^{\automaton}(U_{i}, U_{j})$.

Starting from $\graph[2] = G$, we add edges labeled with $a \in \SIG^{(-)}$ while preserving <ref>, by repeating the following:

* If $\tuple{i, j} \in (\const{I}^{\graph[2]} \cdot a^{\graph[2]} \cdot \const{I}^{\graph[2]}) \setminus a^{\graph[2]}$ for some $a \in \SIG^{(-)}$ and $i, j \in |\graph[2]|$,
we add the edge to $\graph[2]$.
Then, $\Con_{a}^{\automaton[1]}(U_{i}, U_{j})$ holds as follows.
Let $i', j'$ be s.t.  $\tuple{i, i'} \in \const{I}^{\graph[2]}$, $\tuple{i', j'} \in a^{\graph[2]}$, and $\tuple{j', j} \in \const{I}^{\graph[2]}$.
For every $z \in |\automaton|$,
we have

\begin{align*}
z \in U_{i'} & \Longrightarrow z \in \delta_{\const{I}}^{\automaton}(U_{i}) \tag{$U_{i'} \subseteq \delta_{\const{I}}^{\automaton}(U_{i})$ \ref{definition: Hintikka: consistent 2}} \\
& \Longrightarrow z \in U_i \tag{$\delta_{\const{I}}^{\automaton} = (\const{I}^{\automaton})^*$ is reflexive}                                                           \\
& \dots \Longrightarrow z \in U_{i'}. \tag*{($\const{I}^{\graph[2]}$ is symmetric)}
\end{align*}

Thus $U_{i} = U_{i'}$.
In the same way, $U_{j} = U_{j'}$.
Hence $\Con_{a}^{\automaton[1]}(U_{i}, U_{j})$ is derived from $\Con_{a}^{\automaton[1]}(U_{i'}, U_{j'})$.

* Otherwise, since $\graph[2]$ is not edge-saturated, $\tuple{i, j} \not\in a^{\graph[2]} \cup \comnf{a}^{\graph[2]}$ for some $a \in \SIG$ and $i, j \in |\graph[2]|$.
If $\Con_{a}^{\automaton[1]}(U_{i}, U_{j})$ holds, then we add the edge for $\tuple{i, j} \in a^{\graph[2]}$ to $\graph[2]$.
Otherwise, since $\Con_{\comnf{a}}^{\automaton[1]}(U_{i}, U_{j})$ holds by <ref>,
we add the edge for $\tuple{i, j} \in \comnf{a}^{\graph[2]}$ to $\graph[2]$.

Then $\graph[2]$ is a saturation of $G$, as follows.
For <ref>:
Because $G$ is an $\const{I}$-saturation.
For <ref>: Clear.
For <ref>:
By that $G$ is consistent and $(\const{I}^{\graph[2]} \cdot a^{\graph[2]} \cdot \const{I}^{\graph[2]}) \cap (\const{I}^{\graph[2]} \cdot \comnf{a}^{\graph[2]} \cdot \const{I}^{\graph[2]}) = \emptyset$ is preserved (by the construction of $\graph[2]$).

[of <Ref>]
Recall $\automaton$, $w$, and the saturable path $P = \tuple{G, \set{U_{i}}_{i \in |G|}}$ in <Ref>.

\begin{align*}
G                                                                                & = \hspace{-.6em}
\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}-!-{2/{$2$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 2](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$a$}(1);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a12){$\comnf{a}$}(2);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\node[above right = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I22){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I12){$\comnf{\const{I}}$}(2);
\path (0) edge [draw = white, opacity = 0, bend right = 45] node[pos= 0.6, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I02){$\const{I}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[] a01 ->[] 1;
1 --[] a12 ->[] 2;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
2 --[bend left = 10] I22 ->[bend left = 10] 2;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
1 <-[bend left = 10] I12 ->[bend left = 10] 2;
0.south <-[bend right = 10] I02 ->[bend right = 10] 2.south;
l -> 0; 2 -> r;
\end{tikzpicture} &
G'                                                                                & = \hspace{-.6em} \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}-!-{2/{$2$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 2](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$a$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(0);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a12){$\comnf{a}$}(2);
\path (2) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a21){$a$}(1);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\node[above right = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I22){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I12){$\comnf{\const{I}}$}(2);
\path (0) edge [draw = white, opacity = 0, bend right = 45] node[pos= 0.6, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I02){$\const{I}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[] a01 ->[] 1;
1 --[bend left = 15, line width = 1.2pt] a10 ->[bend left = 15, line width = 1.2pt] 0;
1 --[] a12 ->[] 2;
2 --[bend left = 15, line width = 1.2pt] a21 ->[bend left = 15, line width = 1.2pt] 1;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
2 --[bend left = 10] I22 ->[bend left = 10] 2;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
1 <-[bend left = 10] I12 ->[bend left = 10] 2;
0.south <-[bend right = 10] I02 ->[bend right = 10] 2.south;
l -> 0; 2 -> r;
\end{tikzpicture}
\\
G''                                                                                & = \hspace{-.6em} \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}-!-{2/{$2$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 2](r){};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$a$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(0);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a12){$\comnf{a}$}(2);
\path (2) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a21){$a$}(1);
\path (0) edge [draw = white, opacity = 0, bend right = 30] node[pos= 0.4, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a02){$a$}(2);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\node[above right = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I22){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I12){$\comnf{\const{I}}$}(2);
\path (0) edge [draw = white, opacity = 0, bend right = 45] node[pos= 0.6, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I02){$\const{I}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[] a01 ->[] 1;
1 --[bend left = 15] a10 ->[bend left = 15] 0;
1 --[] a12 ->[] 2;
2 --[bend left = 15] a21 ->[bend left = 15] 1;
0.south east <-[bend right = 10, line width = 1.2pt] a02 ->[bend right = 10, line width = 1.2pt] 2.south west;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
2 --[bend left = 10] I22 ->[bend left = 10] 2;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
1 <-[bend left = 10] I12 ->[bend left = 10] 2;
0.south <-[bend right = 10] I02 ->[bend right = 10] 2.south;
l -> 0; 2 -> r;
\end{tikzpicture}
\textcolor{blue}{H}                                                                                & = \hspace{-.6em} \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}-!-{2/{$2$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 2](r){};
\node[above left = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a00){$a$};
\node[above left = 2ex and .0em of 1, inner sep = .5pt, font = \scriptsize, opacity = 1](a11){$\comnf{a}$};
\node[above left = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a22){$a$};
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$a$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a10){$\comnf{a}$}(0);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a12){$\comnf{a}$}(2);
\path (2) edge [draw = white, opacity = 0, bend left = 25] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a21){$a$}(1);
\path (0) edge [draw = white, opacity = 0, bend right = 30] node[pos= 0.4, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a02){$a$}(2);
\node[above right = 2ex and .0em of 0, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I00){$\const{I}$};
\node[above right = 2ex and .0em of 1, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I11){$\const{I}$};
\node[above right = 2ex and .0em of 2, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I22){$\const{I}$};
\path (0) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I01){$\comnf{\const{I}}$}(1);
\path (1) edge [draw = white, opacity = 0, bend left = 65] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](I12){$\comnf{\const{I}}$}(2);
\path (0) edge [draw = white, opacity = 0, bend right = 45] node[pos= 0.6, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I02){$\const{I}$}(2);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
0 --[bend left = 10, line width = 1.2pt] a00 ->[bend left = 10, line width = 1.2pt] 0;
1 --[bend left = 10, line width = 1.2pt] a11 ->[bend left = 10, line width = 1.2pt] 1;
2 --[bend left = 10, line width = 1.2pt] a22 ->[bend left = 10, line width = 1.2pt] 2;
0 --[] a01 ->[] 1;
1 --[bend left = 15] a10 ->[bend left = 15] 0;
1 --[] a12 ->[] 2;
2 --[bend left = 15] a21 ->[bend left = 15] 1;
0.south east <-[bend right = 10] a02 ->[bend right = 10] 2.south west;
0 --[bend left = 10] I00 ->[bend left = 10] 0;
1 --[bend left = 10] I11 ->[bend left = 10] 1;
2 --[bend left = 10] I22 ->[bend left = 10] 2;
0 <-[bend left = 10] I01 ->[bend left = 10] 1;
1 <-[bend left = 10] I12 ->[bend left = 10] 2;
0.south <-[bend right = 10] I02 ->[bend right = 10] 2.south;
l -> 0; 2 -> r;
\end{tikzpicture}
\end{align*}

First, we add the $a$-labeled edge for $\tuple{2, 1}$ because $\tuple{2, 1} \in (\const{I}^{G} \cdot a^{G} \cdot \const{I}^{G})$; similarly, we add the $\comnf{a}$-labeled edge for $\tuple{1, 0}$ (let $G'$ be the graph).
Second, we consider adding an $a$- or $\comnf{a}$-labeled edge for $\tuple{0, 2}$.
Then, because $\Con_{a}^{\automaton}(\set{\mathtt{A,C}}, \set{\mathtt{A,C}})$, we add an $a$-labeled edge for $\tuple{0, 2}$ (note that $\lnot \Con_{\comnf{a}}^{\automaton}(\set{\mathtt{A,C}}, \set{\mathtt{A,C}})$ because $\delta_{\widebreve{\comnf{a}}}^{\automaton}(\set{\mathtt{A, C}}) = \set{\mathtt{D}} \not\subseteq \set{\mathtt{A, C}}$); we also add an $a$-labeled edge for $\tuple{2, 0}$ because $\tuple{2, 0}, \tuple{0, 2} \in \const{I}^{G'}$ (let $G''$ be the graph).
By adding the other edges similarly, the saturation $\textcolor{blue}{\graph[2]}$ of $G(w)$ can be obtained.

For an NFA $\automaton$ over $\AutSIG$ and a word $w$ over $\WordSIG$,
the following are equivalent:

* There is a saturation $\graph[2]$ of $G(w)$ such that $\graph[2]^{\Quo} \not\models w \le \automaton$.

* There is a saturable path $P$ for $\not\models_{\REL} w \le \automaton$.

Let $P = \tuple{G, \set{U_{i}}_{i \in |G|}}$.
Let $\graph[2]$ be the saturation of $G$ (<Ref>).
Then $\graph[2]^{\Quo} \not\models w \le \automaton[1]$ holds as follows.
For $\graph[2]^{\Quo} \models w$:
Because $G(w) \homo \graph[2] \homo \graph[2]^{\Quo}$ (cf. <Ref>).
For $\graph[2]^{\Quo} \not\models \automaton[1]$:
Assume that $\graph[2]^{\Quo} \models \automaton[1]$.

Then there is a word $\aterm[1]_1 \dots \aterm[1]_m \in \lang{\automaton[1]}$ such that $
\graph(\aterm[1]_1 \dots \aterm[1]_m) \homo \graph[2]^{\Quo}$.
By $\aterm[1]_1 \dots \aterm[1]_m \in \lang{\automaton[1]}$, there are $z_0, \dots, z_m \in |\automaton[1]|$ such that
$\tuple{z_0, z_m} = \tuple{\lv^{\automaton[1]}, \rv^{\automaton[1]}}$ and for $k \in [m]$, $z_k \in \delta_{\aterm[1]_{k}}^{\automaton[1]}(z_{k-1})$.
By $\graph(\aterm[1]_1 \dots \aterm[1]_m) \homo \graph[2]^{\Quo}$, there are $l_0, \dots, l_m \in |\graph[2]|$ such that
$\tuple{l_0, l_{m}} = \tuple{\lv^{\graph[2]}, \rv^{\graph[2]}}$ and for $k \in [m]$, $\tuple{l_{k-1}, l_{k}} \in \aterm[1]_k^{\graph[2]}$.

For every $k \in [0, m]$, $z_k \in U_{l_{k}}$.

By induction on $k$.
Case $k = 0$:
By $\src^{\automaton[1]} \in \tset[3]_{\lv^{\graph[2]}}$ <ref>.
Case $k \ge 1$:
We have

\begin{align*}
z_k \in \delta_{\aterm[1]_k}^{\automaton[1]}(z_{k-1})
& \subseteq \delta_{\aterm[1]_k}^{\automaton[1]}(\tset[3]_{l_{k-1}}) \tag{By $z_{k-1} \in \tset[3]_{l_{k-1}}$ (IH)}                              \\
& \subseteq \tset[3]_{l_{k}}. \tag*{(By $\tuple{l_{k-1}, l_{k}} \in \aterm[1]_k^{\graph[2]}$ \ref{definition: Hintikka: consistent 2}) \qedhere}
\end{align*}

Since $z_m \in \tset[3]_{l_{m}}$ contradicts $\tgt^{\automaton[1]} \not\in \tset[3]_{\rv^{\graph[2]}}$ <ref>,
$\graph[2]^{\Quo} \not\models \automaton[1]$.

We define $P = \tuple{G, \set{U_{i}}_{i \in |G|}}$ as follows:

* $G$ is the edge extension of $G(w)$ such that
$a^{G} = a^{\graph[2]}$ for $a \in \set{\const{I}, \comnf{\const{I}}}$ and $a^{G} = a^{G(w)}$ for $a \in \SIG^{(-)}$;

* each set $U_{i} \subseteq |\automaton|$ is defined by:

\begin{align*}
z \in U_{i} & \defiff \exists v \in \lang{{\automaton}[\bl, z]}.\  G(v) \homo {\graph[2]^{\Quo}}[\bl, \gquo{i}{\graph[2]}].
\end{align*}

Here, ${\automaton}[\bl, z]$ denotes the graph $\automaton$ in which $\rv^{\automaton}$ has been replaced with $z$ (similarly for $\graph[2]^{\Quo}[\bl, \gquo{i}{\graph[2]}]$).

Then $P$ is a saturable path for $\not\models_{\REL} w \le \automaton$, as follows.

Let $a \in \SIG_{\const{I}}^{(-, \smile)}$.
If $G(a) \homo {\graph[2]^{\Quo}}[[i]_{\graph[2]}, [j]_{\graph[2]}]$, then
$\Con_{a}^{\automaton[1]}(U_{i}, U_{j})$.
(Here, ${\graph[2]^{\Quo}}[[i]_{\graph[2]}, [j]_{\graph[2]}]$ denotes the graph ${\graph[2]^{\Quo}}$ in which $\lv^{{\graph[2]^{\Quo}}}$ and $\rv^{{\graph[2]^{\Quo}}}$ have been replaced with $[i]_{\graph[2]}$ and $[j]_{\graph[2]}$, respectively.)

Let $z \in U_{i}$.
By definition,
there is $v \in \lang{\automaton[1][\bl, z]}$ such that $G(v) \homo {\graph[2]^{\Quo}}[\bl, \gquo{i}{\graph[2]}]$.
Combining with $G(a) \homo {\graph[2]^{\Quo}}[\gquo{i}{\graph[2]}, \gquo{j}{\graph[2]}]$ yields $G(va) \homo {\graph[2]^{\Quo}}[\bl, \gquo{j}{\graph[2]}]$.
Thus, for every $z' \in \delta_{a}^{\automaton[1]}(z)$, $z' \in U_{j}$.
Hence $\delta_{a}^{\automaton[1]}(U_{i}) \subseteq U_{j}$.
Similarly by $G(\widebreve{a}) \homo {\graph[2]^{\Quo}}[\gquo{j}{\graph[2]}, \gquo{i}{\graph[2]}]$, $\delta_{\widebreve{a}}^{\automaton[1]}(U_{j}) \subseteq U_{i}$.

For <ref>:
$\lv^{\automaton[1]} \in U_{\lv^{G}}$ is shown by considering $v = \const{I}$.
$\rv^{\automaton[1]} \not\in U_{\rv^{G}}$ is because $\graph[2]^{\Quo} \not\models \automaton[1]$.
For <ref>:
Let $\tuple{i, j} \in a^{G}$.
Because $G(a) \homo {\graph[2]^{\Quo}}[\gquo{i}{\graph[2]},\gquo{j}{\graph[2]}]$ (since $\graph[2]$ is a saturation of $G$),
we have $\Con_{a}^{\automaton[1]}(U_{i}, U_{j})$ (the sub-lemma).
For <ref>:
For every $a \in \SIG$ and $i, j \in |G|$,

because either $G(a) \homo {\graph[2]^{\Quo}}[[i]_{\graph[2]}, [j]_{\graph[2]}]$ or $G(\comnf{a}) \homo {\graph[2]^{\Quo}}[[i]_{\graph[2]}, [j]_{\graph[2]}]$ always holds,
we have $\Con_{a}^{\automaton[1]}(U_{i}, U_{j}) \lor \Con_{\comnf{a}}^{\automaton[1]}(U_{i}, U_{j})$ (the sub-lemma).

For two NFAs $\automaton[1], \automaton[2]$ over $\AutSIG$, TFAE:

* $\not\models_{\REL} \automaton[1] \le \automaton[2]$.

* $\exists w \in \lang{\automaton[1]}.\ $ there is a saturable path for $\not\models_{\REL} w \le \automaton[2]$.

We have

\begin{align*}
& \not\models_{\REL} \automaton[1] \le \automaton[2]                                                                                \\
& \iff \exists w \in \lang{\automaton[1]}. \exists \graph[2] \in \Fill(G(w)).\ \graph[2]^{\Quo} \not\models \automaton[1] \le \automaton[2] \tag{\Cref{lemma: bounded model property for ECoRTC}}                                                      \\
& \iff \exists w \in \lang{\automaton[1]}. \exists \graph[2] \in \Fill(G(w)).\ \graph[2]^{\Quo} \not\models w \le \automaton[2] \tag{Because $\graph[2]^{\Quo} \models w$ and $\graph[2]^{\Quo} \models \automaton[1]$ by $\graph[2] \in \Fill(G(w))$} \\
& \iff \exists w \in \lang{\automaton[1]}.\ \mbox{there is a saturable path for $\not\models_{\REL} w \le \automaton[2]$}. \tag*{(\Cref{lemma: Hintikka}) \qedhere}
\end{align*}

§.§ Exponential-size model property

The characterization by saturable paths (<Ref>) gives another bounded model property for $\ExKA$ terms (cf. <Ref>) as follows.
The following proof is an analogy of the well-known pumping lemma from automata theory.

For every NFAs $\automaton[1], \automaton[2]$ over $\AutSIG$,
if ${} \not\models_{\REL} \automaton[1] \le \automaton[2]$, then
there is a $2$-pointed structure $\ppstruc$ of size $\#(|\ppstruc|) \le \#(|\automaton[1]|) \times 2^{\#(|\automaton[2]|)}$
such that $\ppstruc \not\models_{\REL} \automaton[1] \le \automaton[2]$.