By <Ref>, there are a word $w = a_1 \dots a_n \in \lang{\automaton[1]}$ and a saturable path $P = \tuple{G, \set{U_{i}}_{i \in [0, n]}}$ for $\not\models_{\REL} w \le \automaton[2]$.
Without loss of generality, we can assume that $n$ is the minimum among such words.
Since $w \in \lang{\automaton[1]}$, let $\set{s_{i}}_{i \in [0, n]}$ be such that
$\tuple{s_0, s_{n}} = \tuple{\src^{\automaton[1]}, \tgt^{\automaton[1]}}$ and $s_x \in \delta_{a_i}^{\automaton[1]}(s_{i-1})$ for $i \in [n]$.
Assume that $n+1 > \#(|\automaton[1]|) \times 2^{\#(|\automaton[2]|)}$.
By the pigeonhole principle, there are $0 \le x < y \le n$ s.t. $\tuple{\term[2]_x, U_x} = \tuple{\term[2]_y, U_y}$.
Let $w' \defeq a_1 \dots a_x a_{y + 1} \dots a_n$.
Let $P'$ be the $P$ in which
the source of the edge for $\tuple{y, y+1} \in a_{y+1}^{G}$ has been replaced with $x$
and the vertices between $x+1$ and $y$ are removed:

\begin{align*}
P  & = \begin{tikzpicture}[baseline = -.5ex]
\node[mynode, draw, circle](L1){};
\node[mynode, draw, circle, right = 1.8cm of L1, line width = 1.pt](L2){};
\node[mynode, draw = gray!80, circle, right = 1.8cm of L2, text = gray!80](L3){};
\node[mynode, draw, circle, right = 1cm of L3, line width = 1.pt](L4){};
\node[mynode, draw, circle, right = 1.8cm of L4](L5){};
\node[left = 4pt of L1](Ll){} edge[earrow, ->] (L1);
\node[right = 4pt of L5](Lr){}; \path (L5) edge[earrow, ->] (Lr);
\path (L1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](Ltau1){$a_1 \dots a_x$}(L2);
\path (L2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1, text = gray!80](Ltau2){$a_{x+1} \dots a_{y}$}(L3);
\path (L3) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](Ltau3){$a_{y+1}$}(L4);
\path (L4) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](Ltau4){$a_{y+2} \dots a_{n}$}(L5);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
L1 --[] {Ltau1} ->[] L2;
L2 --[ color = gray!80] {Ltau2} ->[, color = gray!80] L3;
L3 --[] {Ltau3} ->[] L4;
L4 --[] {Ltau4} ->[] L5;
\node[below = .5ex of L1, font = \scriptsize]{$U_{0}$};
\node[below = .5ex of Ltau1, font = \scriptsize]{$\dots$};
\node[below = .5ex of L2, font = \scriptsize]{$U_{x}$};
\node[below = .5ex of L3, font = \scriptsize, text = gray!80]{$U_{y}$};
\node[below = .5ex of L4, font = \scriptsize]{$U_{y+1}$};
\node[below = .5ex of Ltau4, font = \scriptsize]{$\dots$};
\node[below = .5ex of L5, font = \scriptsize]{$U_{n}$};
\end{tikzpicture} \\
P' & =\begin{tikzpicture}[baseline = -.5ex]
\node[mynode, draw, circle](L1){};
\node[mynode, draw, circle, right = 1.8cm of L1, line width = 1.pt](L2){};
\node[mynode, draw, circle, right = 1cm of L2, line width = 1.pt](L4){};
\node[mynode, draw, circle, right = 1.8cm of L4](L5){};
\node[left = 4pt of L1](Ll){} edge[earrow, ->] (L1);
\node[right = 4pt of L5](Lr){}; \path (L5) edge[earrow, ->] (Lr);
\path (L1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](Ltau1){$a_1 \dots a_x$}(L2);
\path (L2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](Ltau3){$a_{y+1}$}(L4);
\path (L4) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](Ltau4){$a_{y+2} \dots a_{n}$}(L5);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
L1 --[] {Ltau1} ->[] L2;
L2 --[] {Ltau3} ->[] L4;
L4 --[] {Ltau4} ->[] L5;
\node[below = .5ex of L1, font = \scriptsize]{$U_{0}$};
\node[below = .5ex of Ltau1, font = \scriptsize]{$\dots$};
\node[below = .5ex of L2, font = \scriptsize]{$U_{x}$};
\node[below = .5ex of L4, font = \scriptsize]{$U_{y+1}$};
\node[below = .5ex of Ltau4, font = \scriptsize]{$\dots$};
\node[below = .5ex of L5, font = \scriptsize]{$U_{n}$};
\end{tikzpicture}
\end{align*}

($\const{I}$- or $\comnf{\const{I}}$-labeled edges and some intermediate vertices are omitted, for simplicity.)
Here, when $\tuple{x, y+1} \in \const{I}^{G}$ and $a_{y+1} = \comnf{\const{I}}$, the graph of $P'$ is not consistent; so, we replace the label $\const{I}$ with the label $\comnf{\const{I}}$ for every pair $\tuple{i, j}$ s.t. ${i \neq j} \land \Con_{\comnf{\const{I}}}^{\automaton[2]}(U_{i}, U_{j})$.
($i \neq j$ is for the reflexivity of the relation of $\const{I}$ and $\Con_{\comnf{\const{I}}}^{\automaton[2]}(U_{i}, U_{j})$ is for preserving <ref>).
Then, $w' \in [\automaton]$ holds by $s_x = s_y$ and $P'$ is an saturable path for $\not\models_{\REL} w' \le \automaton[2]$ because
each condition for $P'$ is shown by that for $P$ (with $U_{x} = U_{y}$) and that $P'$ is (almost) a “subgraph” of $P$ (see the full version <cit.><Ref>, for more details).
However, this contradicts that $n$ is the minimum.
Thus, $\#(|G|) = n + 1 \le \#(|\automaton[1]|) \times 2^{\#(|\automaton[2]|)}$.
Finally, $\ppstruc = \graph[2]^{\Quo}$ is the desired $2$-pointed structure, where $\graph[2]$ is the saturation of $G$ obtained from <Ref>.

The equational theory of $\ExKA$ terms (w.r.t. binary relations) is decidable in coNEXP.

Similarly for <ref>,
it suffices to show that the following problem is in NEXP: given $\ExKA$ terms $\term[1], \term[2]$, does $\not\models_{\REL} \term[1] \le \term[2]$ hold?
By <Ref> (with <Ref>), we can give the following algorithm:

* Take a $2$-pointed structure $\ppstruc$ of size $\#(|\ppstruc|) \le \#(|\automaton_{\term[1]}|) \times 2^{\#(|\automaton_{\term[2]}|)}$, non-deterministically.
Here, $\automaton_{\term[1]}$ and $\automaton_{\term[2]}$ are the NFAs obtained from $\term[1]$ and $\term[2]$, respectively (<Ref>).

* Return $\const{true}$, if $\ppstruc \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, $\ppstruc \not\models \term[1] \le \term[2]$ can be decided in exponential time (<Ref>).

§.§ From saturable paths to word automata

For some cases, for an NFA $\automaton$, we can construct an NFA $\AH{\automaton}$ such that:
for every word $w$ over $\WordSIG$, TFAE:

* $w \in \lang{\AH{\automaton}}$;

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

To this end, first, let

\[\fml(\mathcal{U}, U) \defeq \bigwedge \begin{cases}
U \times (|\automaton| \setminus U) \times U \times (|\automaton| \setminus U) \subseteq \mathcal{U} \\
\forall \tuple{t_1, t_2, t_3, t_4} \in \mathcal{U}. \forall a \in \SIG_{\const{I}}.                  \\
\quad  \bigvee \begin{cases}
\delta_a^{\automaton}(t_1) \subseteq U \land  t_2 \not\in \delta_{\widebreve{a}}^{\automaton}(U) \\
\delta_{\comnf{a}}^{\automaton}(t_3) \subseteq U \land t_4 \not\in \delta_{\widebreve{\comnf{a}}}^{\automaton}(U)
\end{cases}
\end{cases}\]

and we show the following lemma:

Let $\automaton$ be an NFA over $\AutSIG$ and $w = a_1 \dots a_n$ be a word over $\WordSIG$.
Recall the formula of <ref>:

\begin{align*}
& \forall \tuple{i, j} \in [0, n]^2.\forall a \in \SIG_{\const{I}}.  \bigvee \left\{\begin{aligned}
\delta_{a}^{\automaton}(U_{i}) \subseteq U_{j} \land \delta_{\widebreve{a}}^{\automaton}(U_{j}) \subseteq U_{i} \\
\delta_{\comnf{a}}^{\automaton}(U_{i}) \subseteq U_{j} \land \delta_{\widebreve{\comnf{a}}}^{\automaton}(U_{j}) \subseteq U_{i}
\end{aligned}\right.
\end{align*}

This formula is equivalent to the following formula:[This transformation is also used for the automata construction in <cit.> (roughly speaking, the $\mathcal{U}$ corresponds to the “$P$” in <cit.>), but is a bit more complicated due to converse.]

\begin{align*}
& \exists \mathcal{U} \subseteq |\automaton|^4. \forall i \in [0, n].\ \fml(\mathcal{U}, U_{i}).
\end{align*}

We have

\begin{align*}
& \delta_{a}^{\automaton}(U_{i}) \subseteq U_{j} \ \land \  \delta_{\widebreve{a}}^{\automaton}(U_{j}) \subseteq U_{i}                                                                             \\
& \Leftrightarrow \delta_{a}^{\automaton}(U_{i}) \subseteq U_{j} \ \land \  |\automaton| \setminus U_{i} \subseteq |\automaton|  \setminus \delta_{\widebreve{a}}^{\automaton}(U_{j})              \\
& \Leftrightarrow (\forall t_1 \in U_{i}. \delta_a^{\automaton}(t_1) \subseteq U_{j}) \land (\forall t_2 \in |\automaton| \setminus U_{i}. t_2 \not\in \delta_{\widebreve{a}}^{\automaton}(U_{j})) \\
& \Leftrightarrow \forall t_1 \in U_{i}. \forall t_2 \in |\automaton| \setminus U_{i}.\  \delta_a^{\automaton}(t_1) \subseteq U_{j} \land t_2 \not\in \delta_{\widebreve{a}}^{\automaton}(U_{j}).
\end{align*}

Thus by letting

\begin{align*}
\xi(U) & \defeq \bigvee \left\{\begin{aligned}
\delta_a^{\automaton}(t_1) \subseteq U \land  t_2 \not\in \delta_{\widebreve{a}}^{\automaton}(U) \\
\delta_{\comnf{a}}^{\automaton}(t_3) \subseteq U \land t_4 \not\in \delta_{\widebreve{\comnf{a}}}^{\automaton}(U)
\end{aligned}\right.; \\
\nu(U) & \defeq U \times (|\automaton| \setminus U) \times U \times (|\automaton| \setminus U),
\end{align*}

we have

\begin{align*}
& \forall \tuple{i, j} \in [0, n]^2.\forall a \in \SIG_{\const{I}}.  \bigvee \left\{\begin{aligned}
\delta_{a}^{\automaton}(U_{i}) \subseteq U_{j} \land \delta_{\widebreve{a}}^{\automaton}(U_{j}) \subseteq U_{i} \\
\delta_{\comnf{a}}^{\automaton}(U_{i}) \subseteq U_{j} \land \delta_{\widebreve{\comnf{a}}}^{\automaton}(U_{j}) \subseteq U_{i}
\end{aligned}\right. \\
& \Leftrightarrow \forall \tuple{i, j} \in [0, n]^2. \forall a \in \SIG_{\const{I}}. \forall \tuple{t_1, t_2, t_3, t_4} \in \nu(U_{i}).\  \xi(U_{j})                                                                               \\
& \Leftrightarrow \forall \tuple{t_1, t_2, t_3, t_4} \in \bigcup_{i = 0}^{n} \nu(U_{i}).\   \forall a \in \SIG_{\const{I}}. \forall i \in [0, n].\  \xi(U_{i})                                                                     \\
& \Leftrightarrow \exists \mathcal{U}  \subseteq |\automaton|^4.\  \bigcup_{i = 0}^{n} \nu(U_{i}) \subseteq \mathcal{U} \quad \land {}                                                                                \\
\label{tag: diamond} & \qquad \quad \forall \tuple{t_1, t_2, t_3, t_4} \in \mathcal{U}. \forall a \in \SIG_{\const{I}}.  \forall i \in [0, n].\  \xi(U_{i}) \tag{$\diamondsuit$}
\\
& \Leftrightarrow  \exists \mathcal{U}  \subseteq |\automaton|^4. \forall i \in [0, n].\  \nu(U_{i}) \subseteq \mathcal{U} \quad \land {}                                                                                \\
& \qquad \quad \forall \tuple{t_1, t_2, t_3, t_4} \in \mathcal{U}. \forall a \in \SIG_{\const{I}}.\  \xi(U_{i})                                                                                \\
& \Leftrightarrow  \exists \mathcal{U} \subseteq |\automaton|^4. \forall i \in [0, n].\ \fml(\mathcal{U}, U_{i}).
\end{align*}

Here, for (<ref>),
By letting $\mathcal{U} = \bigcup_{i = 0}^{n} \nu(U_{i})$.
Because the formula $\forall \tuple{t_1, t_2, t_3, t_4} \in \mathcal{U}'. \forall a \in \SIG_{\const{I}}.  \forall i \in [0, n].\  \xi(U_{i})$ holds for any $\mathcal{U}' \subseteq \mathcal{U}$
and $\bigcup_{i = 0}^{n} \nu(U_{i}) \subseteq \mathcal{U}$.

By using the formula of <Ref> for <ref>,
we can check the condition <ref> pointwisely (without considering pairs of $[0,n]^2$).
Using this, we give the following NFAs construction:

For an NFA $\automaton$ over $\AutSIG$, let $\AH{\automaton}$ be the NFA over $\AutSIG$ defined by:

* $|\AH{\automaton}| \defeq \set{\blacktriangleright, \blacktriangleleft} \cup \set{\tuple{\mathcal{U}, U} \in \wp(|\automaton|^4) \times \wp(|\automaton|) \mid \fml(\mathcal{U}, \tset[3]) \land \delta_{\const{I}}^{\automaton}(\tset[3]) \subseteq \tset[3]}$;

* $\const{I}^{\AH{\automaton}}$ is the minimal set such that

* for all $\tuple{\mathcal{U}, U} \in |\AH{\automaton}|$ s.t.  $\src^{\automaton} \in U$, $\tuple{\blacktriangleright, \tuple{\mathcal{U}, U}} \in \const{I}^{\AH{\automaton}}$;

* for all $\tuple{\mathcal{U}, U} \in |\AH{\automaton}|$ s.t.  $\tgt^{\automaton} \not\in U$, $\tuple{\tuple{\mathcal{U}, \tset[3]}, \blacktriangleleft} \in  \const{I}^{\AH{\automaton}}$;

* for each $a \in \AutSIG$, $a^{\AH{\automaton}}$ is the minimal set such that for every $\tuple{\mathcal{U}, U}, \tuple{\mathcal{U}, U'} \in |\AH{\automaton}|$ s.t.  $\Con_{a}^{\automaton}(\tset[3], \tset[3]')$,
$\tuple{\tuple{\mathcal{U}, \tset[3]}, \tuple{\mathcal{U}, \tset[3]'}} \in a^{\AH{\automaton}}$ holds;

* $\src^{\AH{\automaton}} = {\blacktriangleright}$ and $\tgt^{\AH{\automaton}} = {\blacktriangleleft}$.

(Here, $\blacktriangleright$ and $\blacktriangleleft$ are two fresh symbols.
$\mathcal{U}$ is introduced for <ref>, cf. <Ref>.
Note that $\mathcal{U}$ is invariant in transitions.)

For example, when $|\automaton[1]| = \set{\mathtt{A}, \mathtt{B}}$ and
$\tuple{\lv^{\automaton[1]}, \rv^{\automaton[1]}} = \tuple{\mathtt{A},\mathtt{B}}$,
the NFA $\AH{\automaton[1]}$ is of the following form,
where the existence of each dashed state $\tuple{\mathcal{U}_1, U}$ depends on whether $\fml(\mathcal{U}_1, U) \land \delta_{\const{I}}^{\automaton[1]}(U) \subseteq U$ holds
and the existence of the $a$-labeled edge on each dashed edge from $\tuple{\mathcal{U}_1, U}$ to $\tuple{\mathcal{U}_1, U'}$ depend on whether $\Con_{a}^{\automaton[1]}(U, U')$ holds:

\begin{align*}
\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.5cm, branch down = 4.5ex, nodes={ font = \scriptsize}]{
{,/,1/{$\blacktriangleright$}[mysmallnode, draw, circle, yshift = -1ex, xshift = -1em]}
-!- {/,u12/{$\mathcal{U}_1,\set{\mathtt{A},\mathtt{B}}$}[mysmallnode, draw, circle, yshift=3ex, minimum width=2.5em ,dashed],/, }
-!- {/, u2/{$\mathcal{U}_1,\set{\mathtt{B}}$}[mysmallnode, draw, circle, yshift = -0.5ex, minimum width=2.5em ,dashed],/,  u1/{$\mathcal{U}_1,\set{\mathtt{A}}$}[mysmallnode, draw, circle, yshift=0ex, minimum width=2.5em ,dashed],/{$\vdots$ (for $\mathcal{U}_2, \mathcal{U}_3, \dots$)}[yshift = -1ex, xshift = 2.5em]}
-!- {/,u0/{$\mathcal{U}_1,\emptyset$}[mysmallnode, draw, circle, yshift=3ex, minimum width=2.5em ,dashed],/}
-!- {,/,4/{$\blacktriangleleft$}[mysmallnode, draw, circle, yshift = -1ex, xshift = 1em]}
\node[left = 4pt of 1](l){} edge[earrow, ->] (1);
\node[right = 4pt of 4](r){}; \path (4) edge[earrow, ->] (r);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
1 ->["$\const{I}$"] {u1,u12};
{u1,u0} ->["$\const{I}$"] {4};
{u0,u1,u2,u12} <->[color = gray, dashed, complete bipartite] {u0,u1,u2,u12};
\node[fit=(u0)(u1)(u12)(u2), draw, dotted]{};
\end{tikzpicture}.
\end{align*}

Using this transformation, $\AH{\automaton}$ satisfies the following:

For every NFA $\automaton$ over $\AutSIG$ and word $w$ over $\WordSIG$,
we have:

$w \in \lang{\AH{\automaton}}$ $\Longleftarrow$ there is a saturable path for $\not\models_{\REL} w \le \automaton$.

Let $w = a_1 \dots a_n$ and $P = \tuple{G, \set{\tset[3]_{i}}_{i \in [0, n]}}$ be a saturable path for $\not\models_{\REL} w \le \automaton$.
Let $\mathcal{U} \defeq \bigcup_{i \in [0,n]} \tset[3]_i \times (|\automaton| \setminus \tset[3]_i) \times \tset[3]_i \times (|\automaton| \setminus \tset[3]_i)$.
Then we have

* $\tuple{{\blacktriangleright}, \tuple{\mathcal{U}, \tset[3]_{0}}} \in \delta_{\const{I}}^{\AH{\automaton}}$ (by <ref>);

* for all $i \in [n]$, $\tuple{\tuple{\mathcal{U}, \tset[3]_{i-1}}, \tuple{\mathcal{U}, \tset[3]_{i}}} \in \delta_{a_i}^{\AH{\automaton}}$ (by <ref>);

* $\tuple{\tuple{\mathcal{U}, \tset[3]_{n}}, {\blacktriangleleft}} \in \delta_{\const{I}}^{\AH{\automaton}}$ (by <ref>).

Here, for $i \in [0,n]$, $\tuple{\mathcal{U}, \tset[3]_i} \in |\AH{\automaton}|$ holds, because
$\fml(\mathcal{U}, U_i)$ holds by <ref> with <Ref>
and $\delta_{\const{I}}^{\automaton}(U_i) \subseteq U_i$ holds by <ref>.
Hence, $w \in \lang{\AH{\automaton}}$.

For every NFA $\automaton$ over $\AutSIG$ and word $w$ over $\WordSIG$,
if $\automaton$ does not contain $\const{I}^{-}$, then we have:

$w \in \lang{\AH{\automaton}}$ $\Longrightarrow$ there is a saturable path for $\models_{\REL} w \le \automaton$.

Let $w = a_1 \dots a_n$.
By the form of $\AH{\automaton}$, there are $\mathcal{U}$, $\tset[3]_0$, $\dots$, and $\tset[3]_n$ such that

* $\tuple{{\blacktriangleright}, \tuple{\mathcal{U}, \tset[3]_{0}}} \in \delta_{\const{I}}^{\AH{\automaton}}$;

* for every $i \in [n]$, $\tuple{\tuple{\mathcal{U}, \tset[3]_{i-1}}, \tuple{\mathcal{U}, \tset[3]_{i}}} \in \delta_{a_i}^{\AH{\automaton}}$;

* $\tuple{\tuple{\mathcal{U}, \tset[3]_{n}}, {\blacktriangleleft}} \in \delta_{\const{I}}^{\AH{\automaton}}$.

Let $\graph[2]$ be the $\const{I}$-saturation of $G(w)$ such that

\[\mbox{$\const{I}^{\graph[2]}$ is the identity relation.}\]

$\graph[2]$ is consistent, because $G(w)$ is consistent and $\const{I}^{\graph[2]}$ is the identity relation.
$\graph[2]$ is an edge-extension of $G(w)$, because
$\const{I}^{\graph[2]} \supseteq \const{I}^{G(w)} = \emptyset$ and $\comnf{\const{I}}^{\graph[2]} = |\graph[2]|^2 \setminus \const{I}^{\graph[2]} \supseteq \comnf{\const{I}}^{G(w)}$.
Hence $\graph[2]$ is indeed an $\const{I}$-saturation of $G(w)$.

Then $P = \tuple{\graph[2], \set{U_{i}}_{i \in [0, n]}}$ is a saturable path for ${} \not\models_{\REL} w \le \automaton$ as follows.
For <ref>: By the definition of $\const{I}^{\AH{\automaton}}$, $\src^{\automaton} \in U_0$ and $\tgt^{\automaton} \not\in U_n$.
For <ref> for $a \in \SIG^{(-)}$: By the definition of $a_{i}^{\AH{\automaton}}$,
$\Con_{a_i}^{\automaton}(U_{i-1}, U_i)$.
(Note that the other edges do not exist.)
For <ref> for $a = \const{I}$:
Because $\const{I}^{\graph[2]}$ is the identity relation
and $U_{i} \in \delta_{\const{I}}^{\automaton}(U_i)$ for every $i \in [0, n]$ (by the definition of $|\AH{\automaton}|$).
For <ref> for $a = \comnf{\const{I}}$:
Because $\comnf{\const{I}}$ does not occur in $\automaton$, $\delta_{\comnf{\const{I}}}^{\automaton}(U_i) = \emptyset \subseteq U_j$ always holds for every $i, j \in [0, n]$.
Hence $\Con_{\comnf{\const{I}}}^{\automaton[1]}(U_{i}, U_{j})$.
For <ref>: Because $\mathcal{U}$ satisfies $\fml(\mathcal{U}, \tset[3]_i)$ for every $i \in [0, n]$ (by the definition of $|\AH{\automaton}|$), with <Ref>.

For every NFAs $\automaton[1], \automaton[2]$, over $\AutSIG$,
if $\automaton[2]$ does not contain $\const{I}^{-}$, then we have

\[\not\models_{\REL} \automaton[1] \le \automaton[2] \quad \iff \quad \lang{\automaton[1]} \cap \lang{\AH{\automaton[2]}} \neq \emptyset.\]

We have

\begin{align*}
& \not\models_{\REL} \automaton[1] \le \automaton[2]                                                                                \\
& \iff \exists w \in \lang{\automaton[1]}.\ \mbox{there is a saturable path for $\not\models_{\REL} w \le \automaton[2]$}. \tag{\Cref{theorem: Hintikka}}                       \\
& \iff \exists w \in \lang{\automaton[1]}.\ w \in \lang{\AH{\automaton[2]}} \tag{\Cref{lemma: automaton construction completeness,lemma: automaton construction soundness: I-}} \\
& \iff \lang{\automaton[1]} \cap \lang{\AH{\automaton[2]}} \neq \emptyset. \tag*{\qedhere}
\end{align*}

The equational theory of $\ExKA$ terms without $\const{I}^{-}$ (w.r.t. binary relations) is PSPACE-complete.

For hardness:
By <Ref>, as the term class subsumes $\Termset_{\set{\cdot, \cup, \bl^{*}}}$.
For upper bound:
Similar to <ref>, with (co-)NPSPACE = PSPACE (Savitch's theorem <cit.>), it suffices to show that the following problem is in NPSPACE:
given $\ExKA$ terms $\term[1], \term[2]$ without $\const{I}^{-}$, does $\not\models_{\REL} \term[1] \le \term[2]$ hold?
By <Ref> (with <Ref>),
we can reduce this problem into the emptiness problem of NFAs (of size exponential in the input).
Therefore, by using a standard on-the-fly algorithm for the non-emptiness problem of NFAs (which is essentially the graph reachability problem),
we can give a non-deterministic polynomial space algorithm.

§.§ Remark on the case of full $\ExKA$ terms

Additionally, we remark that the soundness also holds for $\ExKA$ terms without complements of term variables.

For every NFA $\automaton$ over $\AutSIG$ and word $w$ over $\WordSIG$,
if $w$ does not contain $a^{-}$ for any $a \in \SIG$, then we have:

$w \in \lang{\AH{\automaton}}$ $\Longrightarrow$ there is a saturable path for $\not\models_{\REL} w \le \automaton$.

Let $w = a_1 \dots a_n$.
By the form of $\AH{\automaton}$, there are $\mathcal{U}$, $\tset[3]_0$, $\dots$, and $\tset[3]_n$ such that

* $\tuple{{\blacktriangleright}, \tuple{\mathcal{U}, \tset[3]_{0}}} \in \delta_{\const{I}}^{\AH{\automaton}}$;

* for every $i \in [n]$, $\tuple{\tuple{\mathcal{U}, \tset[3]_{i-1}}, \tuple{\mathcal{U}, \tset[3]_{i}}} \in \delta_{a_i}^{\AH{\automaton}}$;

* $\tuple{\tuple{\mathcal{U}, \tset[3]_{n}}, {\blacktriangleleft}} \in \delta_{\const{I}}^{\AH{\automaton}}$.

Let $\graph[2]$ be the $\const{I}$-saturation of $G(w)$ such that

\[\const{I}^{\graph[2]} = \set{\tuple{i,j} \in [0, n]^2 \mid i = j \lor \lnot \Con_{\comnf{\const{I}}}^{\automaton}(U_{i}, U_{j})}.\]

We have $\Con_{\comnf{\const{I}}}^{\automaton}(U_{i}, U_{j}) \lor \Con_{\const{I}}^{\automaton}(U_{i}, U_{j})$ because $\mathcal{U}$ satisfies $\fml(\mathcal{U}, \tset[3]_i)$ for every $i \in [0, n]$ (<Ref>).
If $\lnot \Con_{\comnf{\const{I}}}^{\automaton}(U_{i}, U_{j})$, then $\Con_{\const{I}}^{\automaton}(U_{i}, U_{j})$; thus $U_{i} = U_{j}$.
Therefore, the binary relation $\set{\tuple{i, j} \in [0, n]^2 \mid \lnot \Con_{\comnf{\const{I}}}^{\automaton}(U_{i}, U_{j})}$ is symmetric and transitive;
thus $\const{I}^{\graph[2]}$ is an equivalence relation.
Additionally, $\graph[2]$ is consistent, because $a^{-}$ does not occur in $\graph[2]$ for any $a \in \SIG$.
$\graph[2]$ is an edge-extension of $G(w)$, because
$\const{I}^{\graph[2]} \supseteq \const{I}^{G(w)} = \emptyset$ and $\comnf{\const{I}}^{\graph[2]} \supseteq \comnf{\const{I}}^{G(w)}$ (by the definition of $\const{I}^{\graph[2]}$).
Hence $\graph[2]$ is indeed an $\const{I}$-saturation of $G(w)$.

Then $P = \tuple{\graph[2], \set{U_{i}}_{i \in [0, n]}}$ is a saturable path for ${} \not\models_{\REL} w \le \automaton$ as follows.
For <ref>, <ref>, and <ref> for $a \in \SIG^{(-)}$: Similarly for <Ref>.
For <ref> for $a = \const{I}$:
for every $\tuple{i, j} \in \const{I}^{\graph[2]}$,
if $i = j$, then $\delta_{\const{I}}^{\automaton}(U_{i}) \subseteq U_{j}$ by the definition of $|\AH{\automaton}|$; thus $\Con_{\const{I}}^{\automaton}(U_{i}, U_{j})$.
If $\lnot \Con_{\comnf{\const{I}}}^{\automaton}(U_{i}, U_{j})$, then $\Con_{\const{I}}^{\automaton}(U_{i}, U_{j})$ by <ref>.
For <ref> for $a = \comnf{\const{I}}$:
By the definition of $\const{I}^{\graph[2]}$,
we have $\Con_{\comnf{\const{I}}}^{\automaton}(U_{i}, U_{j})$ for every $\tuple{i, j} \in [0,n]^2 \setminus \const{I}^{\graph[2]}$.

For every NFAs $\automaton[1], \automaton[2]$, over $\AutSIG$,
if $\automaton[1]$ does not contain $a^{-}$ for any $a \in \SIG$, then we have

\[\not\models_{\REL} \automaton[1] \le \automaton[2] \quad \iff \quad \lang{\automaton[1]} \cap \lang{\AH{\automaton[2]}} \neq \emptyset.\]

Cf. <Ref> (use <Ref> instead of <Ref>).

The equational theory of $\ExKA$ terms without $a^{-}$ for any $a \in \SIG$ (w.r.t. binary relations) is PSPACE-complete.

Cf. <Ref> (use <Ref> instead of <Ref>).

However, we leave open the precise complexity of the equational theory of $\ExKA$ terms, while it is decidable in coNEXP (<Ref>) and at least PSPACE-hard (<Ref>).
The problematic case is when both $\const{I}^{-}$ and $a^{-}$ occur.
Our automata construction cannot apply to the full case, as follows:

Consider the soundness (<Ref>) for $\ExKA$ terms:
for a given word $w \in \lang{\AH{\automaton}}$, construct a saturable path for $\not\models_{\REL} w \le \automaton$.
The essence of the proofs in <Ref>
is that an $\const{I}$-saturation of $G(w)$ always exists.
However, for (full) $\ExKA$ terms, the situation is changed.
For example, let $\automaton$ be the NFA obtained from the term $a \comnf{\const{I}} \cup \comnf{\const{I}} \comnf{a}$ (cf. <Ref>) and $w = a b \comnf{a}$:

\begin{align*}
\automaton & = \hspace{-.5em} \scalebox{.9}{\begin{tikzpicture}[baseline = -2.ex]
\graph[grow right = 1.cm, branch down = 1.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);
\graph[use existing nodes, edges={color=black, pos = .5, earrow}, edge quotes={fill=white, inner sep=1pt,font= \scriptsize}]{
1 ->["$a$"] 2;
2 ->["$\comnf{\const{I}}$"] 4;
1 ->["$\comnf{\const{I}}$"] 3;
3 ->["$\comnf{a}$"]4;
\end{tikzpicture}}                    &
G(w)       & = \hspace{-.5em} \scalebox{.9}{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.cm, branch down = 6ex, nodes={mysmallnode, font = \scriptsize}]{
{0/{$0$}[draw, circle]}-!-{1/{$1$}[draw, circle]}-!-{2/{$2$}[draw, circle]}-!-{3/{$3$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 3](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 = 1.5pt, font = \scriptsize, opacity = 1](a12){$b$}(2);
\path (2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a23){$\comnf{a}$}(3);
\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;
2 -- a23 -> 3;
l -> 0; 3 -> r;
\end{tikzpicture}}.
\end{align*}

Then $w \in \lang{\AH{\automaton}}$ holds because

* $\tuple{{\blacktriangleright}, \tuple{\mathcal{U}, \tset[3]_{0}}} \in \delta_{\const{I}}^{\AH{\automaton}}$;

* $\tuple{\tuple{\mathcal{U}, \tset[3]_{0}}, \tuple{\mathcal{U}, \tset[3]_{1}}} \in \delta_{a}^{\AH{\automaton}}$;

* $\tuple{\tuple{\mathcal{U}, \tset[3]_{1}}, \tuple{\mathcal{U}, \tset[3]_{2}}} \in \delta_{b}^{\AH{\automaton}}$;

* $\tuple{\tuple{\mathcal{U}, \tset[3]_{2}}, \tuple{\mathcal{U}, \tset[3]_{3}}} \in \delta_{\comnf{a}}^{\AH{\automaton}}$;

* $\tuple{\tuple{\mathcal{U}, \tset[3]_{3}}, {\blacktriangleleft}} \in \delta_{\const{I}}^{\AH{\automaton}}$,

by letting $U_0 = U_2 = \set{\mathtt{A}, \mathtt{D}}$, $U_1 = U_3 = \set{\mathtt{B}, \mathtt{C}}$,
and $\mathcal{U} = \bigcup_{i \in [0, 3]} \tset[3]_{i} \times (|\automaton| \setminus \tset[3]_{i}) \times \tset[3]_{i} \times (|\automaton| \setminus \tset[3]_{i})$.
However, there does not exist any saturable path for $\not\models_{\REL} w \le \automaton$, because ${} \models_{\REL} w \le \automaton$ (<Ref>).
Additionally, if exists, an $\const{I}$-saturation $\graph[2]$ of $G(w)$ should satisfy $\tuple{0, 2} \in \const{I}^{\graph[2]}$ (by $\comnf{\const{I}} \comnf{a} \in \lang{\automaton}$) and $\tuple{1, 3} \in \const{I}^{\graph[2]}$ (by $a \comnf{\const{I}} \in \lang{\automaton}$) for $\graph[2]^{\Quo} \not\models \automaton$:

\[\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]}-!-{3/{$3$}[draw, circle]}
\node[left = .5em of 0](l){};
\node[right = .5em of 3](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 = 1.5pt, font = \scriptsize, opacity = 1](a12){$b$}(2);
\path (2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a23){$\comnf{a}$}(3);
\path (0) edge [draw = white, opacity = 0, bend right = 30] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I02){$\const{I}$}(2);
\path (1) edge [draw = white, opacity = 0, bend left = 30] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](I13){$\const{I}$}(3);
\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;
2 -- a23 -> 3;
0.south <-[bend right = 5] I02 ->[bend right = 5] 2.south;
1.north <-[bend left = 5] I13 ->[bend left = 5] 3.north;
l -> 0; 3 -> r;
\end{tikzpicture}.\]

However, $\graph[2]$ does not satisfy <ref>; thus we cannot construct consistent $\graph[2]$ even if $w \in \lang{\AH{\automaton}}$.

One may think that $\AH{\automaton}$ behaves as a complement of an NFA $\automaton$ (cf. <Ref>).
Note that $\AH{\automaton}$ is not the language complement of an NFA $\automaton$, i.e., the following does not hold:
for every word $w$, $w \in \lang{\AH{\automaton}} \iff w \not\in \lang{\automaton}$.
E.g., let $\automaton$ be the NFA obtained from the term $a \cup \comnf{a}$ and $w = \const{I}$:

\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]}
\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, bend left = 25] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](tau1){$a$}(2);
\path (1) edge [draw = white, opacity = 0, bend right = 25] node[pos= 0.5, inner sep = 1.pt, font = \scriptsize, opacity = 1](tau2){$\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;
1 -- {tau2} -> 2;
\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]}
\node[left = 4pt of 1](l){} edge[earrow, ->] (1);
\node[right = 4pt of 1](r){}; \path (1) edge[earrow, ->] (r);
\end{tikzpicture}.
\end{align*}

By the form of $\automaton$, $w \not\in \lang{\automaton}$.
However, $w \not\in \lang{\AH{\automaton}}$, as follows.
Assume that $w \in \lang{\AH{\automaton}}$.
By the form of $\AH{\automaton}$, there are $\mathcal{U}$ and $\tset[3]_0$ such that $\tuple{{\blacktriangleright}, \tuple{\mathcal{U}, \tset[3]_{0}}} \in \delta_{\const{I}}^{\AH{\automaton}}$, $\tuple{\tuple{\mathcal{U}, \tset[3]_{0}}, {\blacktriangleleft}} \in \delta_{\const{I}}^{\AH{\automaton}}$,
$\mathtt{A} \in U_0$, and $\mathtt{B} \not\in U_0$.
By <Ref>, $\Con_{\automaton}^{a}(\tset[3]_0, \tset[3]_0) \lor \Con_{\automaton}^{\comnf{a}}(\tset[3]_0, \tset[3]_0)$.
In either case, $\mathtt{B} \in U_0$, which contradicts $\mathtt{B} \not\in U_0$.
Thus $w \not\in \lang{\AH{\automaton}}$.

§ UNDECIDABILITY FOR

A context-free grammar (CFG) $\mathcal{C}$ over a finite set $\CSIG$ is a tuple $\tuple{X, \mathcal{R}, \const{s}}$, where

* $X$ is a finite set of non-terminal labels s.t. $\CSIG \cap X = \emptyset$;

* $\mathcal{R}$ is a finite set of rewriting rules $x \leftarrow w$ of $x \in X$ and $w \in (\CSIG \cup X)^*$;

* $\const{s} \in X$ is the start label.

The relation $x \vdash_{\mathcal{C}} w$, where $x \in X$ and $w \in \CSIG^*$, is defined as the minimal relation closed under the following rule:
if $x \leftarrow w_0 x_1 w_1 \dots x_n w_n \in \mathcal{R}$ (where $x, x_1, \dots, x_n \in X$ and $w_0, \dots, w_n \in \CSIG^*$),
x_1 ⊢_𝒞 v_1
x_n ⊢_𝒞 v_n
3x ⊢_𝒞 w_0 v_1 w_1 …v_n w_n
The language $\lang{\mathcal{C}} \subseteq \CSIG^*$ is the set $\set{w \mid \const{s} \vdash_{\mathcal{C}} w}$.
It is well-known that the universality problem for CFGs—given a CFG $\mathcal{C}$, does $\lang{\mathcal{C}} = \CSIG^*$ hold?—is $\Pi_{1}^{0}$-complete.

Let $\Gamma$ be a set of equations.
We write:

\begin{align*}
\struc \models \Gamma                     & \defiff \struc \models \term[1] = \term[2] \mbox{ for every ${\term[1] = \term[2]} \in \Gamma$};     \\
\Gamma \models_{\REL} \term[1] = \term[2] & \defiff \struc \models \term[1] = \term[2] \mbox{ for every $\struc$ s.t.\ $\struc \models \Gamma$}.
\end{align*}

For a CFG $\mathcal{C} = \tuple{X, \mathcal{R}, \const{s}}$ and a word $w = a_1 \dots a_m$,
let $\Gamma_{\mathcal{C}} \defeq \set{w \le x \mid x \leftarrow w \in \mathcal{R}}$.
Here, $\ppmodel_{\mathcal{C}, w} \defeq \model_{\mathcal{C}, w}[0, m]$, where $\model_{\mathcal{C}, w} \defeq \tuple{|\model|, \set{a^{\model}}_{a \in A \cup X}}$ is the structure over $A \cup X$, defined as follows:

* $|\model| = [0, m]$;

* for $a \in \CSIG$, $a^{\model} = \set{\tuple{i-1, i} \mid i \in [1, m] \mbox{ and } a_i = a}$;

* the elements of $\set{x^{\model}}_{x \in X}$ are the minimal relations closed under the following rule:
if $(w_0 x_1 w_1 \dots x_n w_n \le x) \in \Gamma_{\mathcal{C}}$ (where $x_1, \dots, x_n \in X$ and $w_0, \dots, w_n \in A^*$),

\[\begin{prooftree}
\hypo{\stackanchor{$\tuple{i_0, j_0} \in \jump{w_0}_{\model}$ \quad $\tuple{j_0, i_1} \in x_1^{\model}$ \qquad \dots}{
$\tuple{j_{n-1}, i_n} \in x_n^{\model}$ \quad $\tuple{i_n, j_n} \in \jump{w_n}_{\model}$}}
\infer1{\tuple{i_0,j_n} \in x^{\model}}
\end{prooftree}.\]

For example, if $A = \set{(,)}$,
$\mathcal{C} = \tuple{\set{\const{s}}, \set{\const{s} \ \leftarrow \ (\const{s}) \const{s},\  \const{s} \ \leftarrow \ \const{I}}, \const{s}}$ (i.e., $\lang{\mathcal{C}}$ is the Dyck-1 language), and $w = (()())$, then $\model_{\mathcal{C}, w}$ is the following:

\[\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]}
-!-{3/{$3$}[draw, circle]}
-!-{4/{$4$}[draw, circle]}
-!-{5/{$5$}[draw, circle]}
-!-{6/{$6$}[draw, circle]}
\path (0) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a01){$($}(1);
\path (1) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = 1.5pt, font = \scriptsize, opacity = 1](a12){$($}(2);
\path (2) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a23){$)$}(3);
\path (3) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a34){$($}(4);
\path (4) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a45){$)$}(5);
\path (5) edge [draw = white, opacity = 0] node[pos= 0.5, inner sep = .5pt, font = \scriptsize, opacity = 1](a56){$)$}(6);
\node(a00)[above = 1.5ex of 0,  inner sep = 1.5pt, font = \scriptsize,]{$\const{s}$};
\node(a11)[above = 1.5ex of 1,  inner sep = 1.5pt, font = \scriptsize,]{$\const{s}$};
\node(a22)[above = 1.5ex of 2,  inner sep = 1.5pt, font = \scriptsize,]{$\const{s}$};
\node(a33)[above = 1.5ex of 3,  inner sep = 1.5pt, font = \scriptsize,]{$\const{s}$};
\node(a44)[above = 1.5ex of 4,  inner sep = 1.5pt, font = \scriptsize,]{$\const{s}$};
\node(a55)[above = 1.5ex of 5,  inner sep = 1.5pt, font = \scriptsize,]{$\const{s}$};
\node(a66)[above = 1.5ex of 6,  inner sep = 1.5pt, font = \scriptsize,]{$\const{s}$};
\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;
2 -- a23 -> 3;
3 -- a34 -> 4;
4 -- a45 -> 5;
5 -- a56 -> 6;
0 --[bend left = 15] a00 ->[bend left = 15] 0;
1 --[bend left = 15] a11 ->[bend left = 15] 1;
2 --[bend left = 15] a22 ->[bend left = 15] 2;
3 --[bend left = 15] a33 ->[bend left = 15] 3;
4 --[bend left = 15] a44 ->[bend left = 15] 4;
5 --[bend left = 15] a55 ->[bend left = 15] 5;
6 --[bend left = 15] a66 ->[bend left = 15] 6;
1 ->["$\const{s}$", font=\scriptsize, bend right = 20] 3;
3 ->["$\const{s}$", font=\scriptsize, bend right = 20] 5;
1 ->["$\const{s}$", font=\scriptsize, bend right = 20] 5;
0 ->["$\const{s}$", font=\scriptsize, bend right = 20] 6;
\end{tikzpicture}.\]

Then we have the following:

Let $\mathcal{C} = \tuple{X, \mathcal{R}, \const{s}}$ be a CFG.
For every $x \in X$ and $w \in \CSIG^*$, the following are equivalent:

*  $x \vdash_{\mathcal{C}} w$;

*  $\ppmodel_{\mathcal{C}, w} \models x$;

*  $\Gamma_{\mathcal{C}} \models_{\REL} w \le x$.

<ref> $\Longrightarrow$ <ref>:
By induction on the derivation tree of $x \vdash_{\mathcal{C}} w$.
This derivation tree is of the following form:

x_1 ⊢_𝒞 v_1
x_n ⊢_𝒞 v_n
3x ⊢_𝒞 w_0 v_1 w_1 …v_n w_n
where $n \in \nat$, $x_1, \dots, x_n \in X$, $w_0, \dots, w_n \in \CSIG^*$, $v_1, \dots, v_n \in \CSIG^*$ s.t.    $w = w_0 v_1 w_1 \dots v_n w_n$ and $x \leftarrow w_0 x_1 w_1 \dots x_n w_n \in \mathcal{R}$.
W.r.t. $\Gamma_{\mathcal{C}} \models_{\REL}$, we have

\begin{align*}
w & =  w_0 v_1 w_1 \dots v_n w_n                                                                                \\
& \le w_0 x_1 w_1 \dots x_n w_n                  \tag{$\Gamma_{\mathcal{C}} \models_{\REL} v_i \le x_i$ for $i \in [n]$ (IH)} \\
& \le x \tag{$(w_0 x_1 w_1 \dots x_n w_n \le x) \in \Gamma_{\mathcal{C}}$}.
\end{align*}

Hence $\Gamma_{\mathcal{C}} \models_{\REL} w \le x$.
<ref> $\Longrightarrow$ <ref>:
Because $\model_{\mathcal{C}, w} \models \Gamma_{\mathcal{C}}$ and $\ppmodel_{\mathcal{C}, w} \models w$ hold.
<ref> $\Longrightarrow$ <ref>:
We show the following:

For every $i, j \in [0, m]$ and $x \in X$,
if $\model_{\mathcal{C}, w}[i,j] \models x$, then $i \le j$ and $x \vdash_{\mathcal{C}} a_i \dots a_{j-1}$.

By induction on the derivation tree from the definition of $\set{x^{\model_{\mathcal{C}, w}}}_{x \in X}$.
This derivation tree is of the following form
\hypo{\stackanchor{$\tuple{i_0, j_0} \in \jump{w_0}_{\model_{\mathcal{C}, w}}$ \quad $\tuple{j_0, i_1} \in x_1^{\model_{\mathcal{C}, w}}$ \quad \dots}{
$\tuple{j_{n-1}, i_n} \in x_n^{\model_{\mathcal{C}, w}}$ \quad $\tuple{i_n, j_n} \in \jump{w_n}_{\model_{\mathcal{C}, w}}$}}
\infer1{\tuple{i_0,j_n} \in x^{\model_{\mathcal{C}, w}}}
\end{prooftree}$,
where $x_1, \dots, x_n \in X$, $w_0, \dots, w_n \in \CSIG^*$,
$i_0, j_0, \dots, i_n, j_n \in |\model_{\mathcal{C}, w}|$,
and $\tuple{i_0, j_n} = \tuple{i, j}$.
By the definition of $a^{\model_{\mathcal{C}, w}}$ (where $a \in \CSIG$), we have $i_k \le j_k$ and $w_k = a_{i_k} \dots a_{j_k - 1}$.
By IH, we have $j_{k-1} \le i_k$ and $x_k \vdash_{\mathcal{C}} a_{j_{k-1}} \dots a_{i_{k}-1}$.
Combining them yields $i \le j$ and $x \vdash_{\mathcal{C}}  a_i \dots a_{j-1}$ (because $x \leftarrow w_0 x_1 w_1 \dots x_n w_n \in \mathcal{R}$).

By specializing this sub-lemma with $\tuple{i,j} = \tuple{0,m}$, this completes the proof.

For every CFG $\mathcal{C} = \tuple{X, \mathcal{R}, \const{s}}$, we have

\[ \lang{\mathcal{C}} = \CSIG^* \quad \iff \quad \Gamma_{\mathcal{C}} \models_{\REL} \CSIG^* \le \const{s}.\]

(Here, $\CSIG^*$ denotes the term $(a_1 \cup \dots \cup a_n)^*$ in the right-hand side, where $\CSIG = \set{a_1, \dots, a_n}$.)

We have

\begin{align*}
\lang{\mathcal{C}} = \CSIG^* & \iff \forall w \in \CSIG^*.\ \const{s} \vdash_{\mathcal{C}} w                    \tag{Def.\ of $\lang{}$}         \\
& \iff \forall w \in \CSIG^*.\ \Gamma_{\mathcal{C}} \models_{\REL} w \le \const{s} \tag{\Cref{lemma: CFG encoding}} \\
& \iff \Gamma_{\mathcal{C}} \models_{\REL} \CSIG^* \le \const{s}. \tag*{\qedhere}
\end{align*}

Additionally, we prepare the following deduction lemma for Hoare hypotheses $\term[3] = \bot$ (cf. <cit.> for KAT):

For every $\ECoRTC$ terms $\term[1], \term[2], \term[3]$ and every set $\Gamma$ of equations,
we have

\[\Gamma \cup \set{\term[3] = \bot} \models_{\REL} \term[1] \le \term[2] \iff \Gamma \models_{\REL} \term[1] \le \term[2] \cup (\top \term[3] \top).\]

We have

\begin{align*}
& \Gamma \cup \set{\term[3] = \bot} \models_{\REL} \term[1] \le \term[2]                                                   \\
& \iff \mbox{for every ${\struc}[x,y]$ s.t.\ $\struc \models \Gamma \cup \set{\term[3] = \bot}$,}                          \\
& \hspace{10em} \mbox{${\struc}[x,y] \models \term[1] \le \term[2]$} \tag{Def.\ of $\models_{\REL}$}                       \\
& \iff \mbox{for every ${\struc}[x,y]$ s.t.\  $\struc \models \Gamma$ and ${\struc}[x,y] \not\models \top \term[3] \top$,} \\
\label{lemma: deduction theorem 1} & \hspace{10em} \mbox{${\struc}[x,y] \models \term[1] \le \term[2]$}  \tag{$\clubsuit$1}                                   \\
\label{lemma: deduction theorem 2} & \iff \mbox{for every ${\struc}[x,y]$ s.t.\  $\struc \models \Gamma$,}                                                    \\
& \hspace{10em} {\struc}[x,y] \models \term[1] \le \term[2] \cup (\top \term[3] \top)\tag{$\clubsuit$2}                    \\
& \iff \Gamma \models_{\REL} \term[1] \le \term[2] \cup (\top \term[3] \top).  \tag{Def.\ of $\models_{\REL}$}
\end{align*}

Here, (<ref>) is because $\model \models \term[3] = \bot \iff \jump{\term[3]}_{\model} = \emptyset \iff {\model}[x, y] \not\models \top \term[3] \top$.
(<ref>) is because:

\begin{align*}
& ({\struc}[x,y] \not\models \top \term[3] \top) \mbox{ implies } ({\struc}[x,y] \models \term[1] \le \term[2])                      \\
& \iff {\struc}[x,y] \models \top \term[3] \top \ \lor\  {\struc}[x,y] \not\models \term[1] \ \lor \  {\struc}[x,y] \models \term[2] \\
& \iff {\struc}[x,y] \not\models \term[1] \ \lor \  {\struc}[x,y] \models \term[2] \cup (\top \term[3] \top)                         \\
& \iff {\struc}[x,y] \models \term[1] \le \term[2] \cup (\top \term[3] \top).  \tag*{\qedhere}
\end{align*}

By <Ref>, we have the following:

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

For upper bound:
By <Ref>.
For hardness:
Let $\mathcal{C} = \tuple{X, \set{x_i \leftarrow w_i \mid i \in [n]}, \const{s}}$ be a CFG.
Then we have

\begin{align*}
& \lang{\mathcal{C}} = A^*                                                                                \\
& \iff \set{w_i \le x_i \mid i \in [n]} \models_{\REL} A^* \le \const{s}                                                                     \tag{\Cref{lemma: CFG encoding lang}}                                                              \\
& \iff \set{w_i \cap x_i^{-} = \bot \mid i \in [n]} \models_{\REL} A^* \le \const{s}                                                         \tag{For every $\struc$, $\model \models w_i \le x_i \iff \model \models w_i \cap x_i^{-} = \bot$} \\
& \iff {} \models_{\REL} A^* \le \const{s} \cup \left(\bigcup_{i = 1}^{n} \top (w_i \cap x_i^{-}) \top\right) \tag{\Cref{lemma: deduction theorem}}                                                                                \\
& \iff {} \models_{\REL} A^* \le \const{s} \cup \left(\bigcup_{i = 1}^{n} (a \cup a^{-}) (w_i \cap x_i^{-}) (a \cup a^{-})\right). \tag{${} \models_{\REL} \top = a \cup a^{-}$, where $a$ is some element in $A$.}
\end{align*}

Thus we can reduce the universality problem for CFGs, which is $\Pi_{1}^{0}$-hard, to the equational theory of $\ECoRTC$ (precisely, $\Termset_{\set{\cdot, \cup, \cap, \bl^{*}}}$ with the complement of term variables).

§ CONCLUSION AND FUTURE WORK

We have studied the computational complexity of existential calculi of relations with transitive closure, using edge saturations.
A natural interest is to extend our complexity results for more general syntaxes.
We believe that the upper bound results for intersection-free fragments hold even if we extend them with tests in KAT (by considering guarded strings <cit.> instead of words (strings), in saturable paths); e.g., KAT with top (w.r.t. binary relations), which are recently studied for modeling incorrectness logic <cit.>.

Another future work is to study the axiomatizability of them.
Unfortunately, the equational theory of (full) $\ECoRTC$ is not finitely axiomatizable because it is not recursively enumerable (<Ref>);
but we leave it open to finding some complete (finite) axiomatization for its fragments, including KA terms with complements of term variables.
(The equation (<ref>) indicates that, at least, we need axioms of KA with top w.r.t. binary relations <cit.>.)

We would like to thank the anonymous reviewers for their useful comments.

§ PROOF OF THE EQUATIONS IN THE INTRODUCTION

(The notations in this section depend on <Ref>.)

For <Ref>: ${}  \models_{\REL} \top = a \cup a^{-}$.
For every structure $\struc$ and $x, y \in |\struc|$,
we have

\begin{align*}
\tuple{x, y} \in \jump{\top}_{\struc}
& \iff \mathsf{true}                                                                  \\
& \iff \tuple{x, y} \in \jump{a}_{\struc} \lor \tuple{x, y} \not\in \jump{a}_{\struc} \\
& \iff \tuple{x, y} \in \jump{a \cup a^{-}}_{\struc}.                    \tag*{\qed}
\end{align*}

For <Ref>: ${}  \models_{\REL} a b a^{-}         \le \const{I}^{-} a^{-} \cup a \const{I}^{-}$.
Assume $\tuple{x_0, x_3} \in \jump{a b a^{-}}_{\struc}$.
Let $x_1$ and $x_2$ be s.t. $\tuple{x_0, x_1} \in \jump{a}_{\struc}$, $\tuple{x_1, x_2} \in \jump{b}_{\struc}$, and $\tuple{x_2, x_3} \in \jump{a^{-}}_{\struc}$.
Because $\tuple{x_0, x_1} \in a^{\struc}$ and $\tuple{x_2, x_3} \not\in a^{\struc}$, $\tuple{x_0, x_1} \neq \tuple{x_2, x_3}$ should hold.
We distinguish the following cases:

* If $x_0 \neq x_2$, then $\tuple{x_0, x_2} \in \jump{\const{I}^{-}}_{\struc}$ and $\tuple{x_2, x_3} \in \jump{a^{-}}_{\struc}$.
Thus, $\tuple{x_0, x_3} \in \jump{\const{I}^{-} a^{-} \cup a \const{I}^{-}}_{\struc}$.

* Otherwise ($x_1 \neq x_3$), $\tuple{x_0, x_1} \in \jump{a}_{\struc}$ and $\tuple{x_1, x_3} \in \jump{\const{I}^{-}}_{\struc}$.
Thus, $\tuple{x_0, x_3} \in \jump{\const{I}^{-} a^{-} \cup a \const{I}^{-}}_{\struc}$.

This completes the proof.

For <Ref>: ${} \models_{\REL} a               \le \const{I}^{-} \cup a a$.
Assume $\tuple{x, y} \in \jump{a}_{\struc}$.
We distinguish the following cases:

* If $x \neq y$, then $\tuple{x,y} \in \jump{\const{I}^{-}}_{\struc}$.
Thus, $\tuple{x,y} \in \jump{\const{I}^{-} \cup a a}_{\struc}$.

* Otherwise ($x = y$),
$\tuple{x, y} \in \jump{a}_{\struc}$, $y = x$, and $\tuple{x, y} \in \jump{a}_{\struc}$.
Thus, $\tuple{x,y} \in \jump{\const{I}^{-} \cup a a}_{\struc}$.

This completes the proof.

For <Ref>: ${} \models_{\REL} a^{\smile} a^{-} \le \const{I}^{-}$.
Assume $\tuple{x_0, x_2} \in \jump{a^{\smile} a^{-}}_{\struc}$.
Let $x_1$ be s.t. $\tuple{x_0, x_1} \in \jump{a^{\smile}}_{\struc}$ and $\tuple{x_1, x_2} \in \jump{a^{-}}_{\struc}$.
Because $\tuple{x_1, x_0} \in a^{\struc}$ and $\tuple{x_1, x_2} \not\in a^{\struc}$, $x_0 \neq x_2$ should hold.
Thus, we have $\tuple{x_0, x_2} \in \jump{\const{I}^{-}}_{\struc}$.
This completes the proof.

§ NOTE: SUPPLEMENT OF <REF>

Let $\genTermset$ be the set of terms defined as follows:

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

The binary relation $\jump{\term}_{\model} \subseteq |\model|^2$ of an $\genTermset$ term $\term$ on a structure $\model$ is defined as follows, where $a \in \SIG$ and $b \in \SIG \cup \set{\const{I}, \bot, \top}$:

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

_                        ∅
⊤_                        ||^2

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

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 every pairs $\term[1] = \term[2]$ of terms in $\Termset_{\sig}$ s.t. $\models_{\REL} \term[1] = \term[2]$.
We use the notation $\models$ (<Ref>) also for $\genTermset$.

For term $\term \in \genTermset$,
the converse normal form $\widebreve{\term}$ (e.g., <cit.>) of the term $\term^{\smile}$ is defined by:

\begin{align*}
\widebreve{a}                            & \defeq a^{\smile}                                      & \widebreve{a^{\smile}}                         & \defeq a     \tag{$a \in \SIG^{(-)}$}                                                 \\
\widebreve{a}                            & \defeq a                                               & \widebreve{a^{\smile}}                         & \defeq a \tag{$a \in \set{\const{I}, \const{I}^{-}, \top, \top^{-}, \bot, \bot^{-}}$} \\
\widebreve{\term[1] \cdot \term[2]}      & \defeq \widebreve{\term[2]} \cdot \widebreve{\term[1]} & \widebreve{(\term[1] \cdot \term[2])^{\smile}} & \defeq \widebreve{\term[1]^{\smile}} \cdot \widebreve{\term[2]^{\smile}}              \\
\widebreve{\term[1]^*}                   & \defeq (\widebreve{\term[1]})^*                        & \widebreve{(\term[1]^*)^{\smile}}              & \defeq (\widebreve{\term[1]^{\smile}})^*                                              \\
\widebreve{\term[1] \cup \term[2]}       & \defeq \widebreve{\term[1]} \cup \widebreve{\term[2]}  & \widebreve{(\term[1] \cup \term[2])^{\smile}}  & \defeq \widebreve{\term[1]^{\smile}} \cup \widebreve{\term[2]^{\smile}}               \\
\widebreve{(\term[1]^{\smile})^{\smile}} & \defeq \widebreve{\term[1]}.
\end{align*}

For every term $\term \in \genTermset$, $\models_{\REL} \widebreve{\term} = \term^{\smile}$.

By straightforward induction on $\term$.
For example, if $\term = \term[2] \cdot \term[3]$,
for every ${\model}[x,y]$, we have

\begin{align*}
{\model}[x,y] \models \widebreve{\term[2] \cdot \term[3]} & \iff  {\model}[x,y] \models \widebreve{\term[3]} \cdot \widebreve{\term[2]} \tag{Def.\ of $\widebreve{\bullet}$}                             \\
& \iff \exists z.\   {\model}[x,z] \models \widebreve{\term[3]} \ \land \  {\model}[z,y] \models \widebreve{\term[2]} \tag{Def.\ of $\jump{}$} \\
& \iff \exists z.\  {\model}[x,z] \models \term[3]^{\smile} \  \land \  {\model}[z,y] \models \term[2]^{\smile} \tag{IH}                       \\
& \iff {\model}[x,y] \models \term[3]^{\smile} \cdot \term[2]^{\smile}  \tag{Def.\ of $\jump{}$}                                               \\
& \iff  {\model}[x,y] \models (\term[3] \cdot \term[2])^{\smile}. \tag{Def.\ of $\jump{}$}
\end{align*}

The equational theory of $\genTermset$ can be reduced to that of $\ECoRTC$ in polynomial time.

Let $\term[1]$ and $\term[2]$ be terms in $\genTermset$.
Let $\term[1]'$ (resp. $\term[2]'$) be the term $ \widebreve{\widebreve{\term[1]}}$ (resp. $\widebreve{\widebreve{\term[2]}}$)
in which each $\top^{-}$ has been replaced with $\bot$ and each $\bot^{-}$ has been replaced with $\top$.
Then, ${} \models_{\REL} \term[1] = \term[2] \iff {} \models_{\REL} \term[1]' = \term[2]'$ by
<Ref> with $\models_{\REL} \top^{-} = \bot$ and $\models_{\REL} \bot^{-} = \top$.
By the construction, $\term[1]'$ and $\term[2]'$ can be obtained from $\term[1]$ and $\term[2]$ in polynomial time, respectively.
Also, $\term[1]'$ and $\term[2]'$ are $\genTermset$ terms, because $\smile$ only applies to $a \in \SIG^{(-)}$ and $\top^{-}$ and $\bot^{-}$ does not occur.

§ NOTE: PROOF OF <REF>

For every structure $\model$ and graphs $G, H$,

\begin{align*}
\label{proposition: graph operation: cap}\jump{G \cap H}_{\model}      & = \jump{G}_{\model} \cap \jump{H}_{\model} \tag{\Cref{proposition: graph operation}$\cap$}   \\
\label{proposition: graph operation: cdot} \jump{G \cdot H}_{\model}   & = \jump{G}_{\model} \cdot \jump{H}_{\model} \tag{\Cref{proposition: graph operation}$\cdot$} \\
\label{proposition: graph operation: smile} \jump{G^{\smile}}_{\model} & = \jump{G}_{\model}^{\smile}. \tag{\Cref{proposition: graph operation}$\smile$}
\end{align*}

By the definition of $\jump{}_{\model}$ (<Ref>), it suffices to show that for every $x, y \in |\model|$:

\begin{align*}
& \exists f.\ f \colon (G \cap H) \homo {\model}[x,y]                                                      \\
& \iff \exists f_{G}, f_{H}.\ f_{G} \colon G \homo {\model}[x,y] \land f_{H} \colon H \homo {\model}[x,y].
\end{align*}

By letting $f_{G} = \set{\tuple{x', f(x')} \mid x' \in |G|}$ and $f_{H} = \set{\tuple{x', f(x')} \mid x' \in |H|}$.
By letting $f = f_{G} \cup f_{H}$.
Note that $f_{G}(\src^{G}) = x = f_{H}(\src^{H})$ and $f_{G}(\tgt^{G}) = y = f_{H}(\tgt^{H})$ by <Ref>; so $f$ is indeed a map.

By the definition of $\jump{}_{\model}$, it suffices to show that for every $x, y \in |\model|$:

\begin{align*}
& \exists f.\ f \colon (G \cdot H) \homo {\model}[x,y]                                                         \\
& \iff \exists z, f_{G}, f_{H}.\  f_{G} \colon G \homo {\model}[x,z] \land f_{H} \colon H \homo {\model}[z,y].
\end{align*}

By letting $z = f(\tgt^{G})$, $f_{G} = \set{\tuple{x', f(x')} \mid x' \in |G|}$, and $f_{H} = \set{\tuple{x', f(x')} \mid x' \in |H|}$.
By letting $f = f_{G} \cup f_{H}$.
Note that $f_{G}(\tgt^{G}) = z = f_{H}(\src^{H})$ by <Ref>; so $f$ is indeed a map.

By the definition of $\jump{}_{\model}$, it suffices to show that for every $x, y \in |\model|$:

\begin{align*}
\exists f.\ f \colon G^{\smile} \homo {\model}[x,y] & \ \iff\  \exists f_{G}.\ f_{G} \colon G \homo {\model}[y,x].
\end{align*}

This is clear by using the same map.

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

By induction on $\term$.

Case $\term = a$ where $a \in \SIG$:
For every $x, y \in |\model|$, we have

\begin{align*}
\tuple{x, y} \in \jump{a}_{\model} & \iff \tuple{x, y} \in a^{\model}                                                         \tag{Def.\ of $\jump{}$}                                     \\
& \iff \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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} \homo {\model}[x,y]                        \\
& \iff \tuple{x, y} \in \jump{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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}}_{\model} \tag{\Cref{definition: semantics for graphs}} \\
& \iff \tuple{x, y} \in \jump{\glang(a)}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

Case $\term = \const{I}$:
For every $x, y \in |\model|$, we have

\begin{align*}
\tuple{x, y} \in \jump{\const{I}}_{\model} & \iff \tuple{x, y} \in \const{I}^{\model}                                                         \tag{Def.\ of $\jump{}$}                                                   \\
& \iff \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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){$\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} \homo {\model}[x,y]                        \\
& \iff \tuple{x, y} \in \jump{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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){$\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}}_{\model} \tag{\Cref{definition: semantics for graphs}} \\
& \iff \tuple{x, y} \in \jump{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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}}_{\model} \tag{$\const{I}^{\model}$ is the identity relation}                                                    \\
& \iff \tuple{x, y} \in \jump{\glang(\const{I})}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

Case $\term = \top$:
For every $x, y \in |\model|$, we have

\begin{align*}
\tuple{x, y} \in \jump{\top}_{\model} & \iff \const{true}                                                  \tag{Def.\ of $\jump{}$}                              \\
& \iff \tuple{x, y} \in \jump{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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}}_{\model} \tag{\Cref{definition: semantics for graphs}} \\
& \iff \tuple{x, y} \in \jump{\glang(\top)}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

Case $\term = \bot$:
For every $x, y \in |\model|$, we have

\begin{align*}
\tuple{x, y} \in \jump{\bot}_{\model} & \iff \const{false}                                                  \tag{Def.\ of $\jump{}$}  \\
& \iff \tuple{x, y} \in \jump{\emptyset}_{\model} \tag{\Cref{definition: semantics for graphs}} \\
& \iff \tuple{x, y} \in \jump{\glang(\bot)}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

Case $\term = \term[2] \cdot \term[3]$:

\begin{align*}
& \jump{\term[2] \cdot \term[3]}_{\model}  = \jump{\term[2]}_{\model} \cdot \jump{\term[3]}_{\model}  \tag{Def.\ of $\jump{}$}                                               \\
& = \jump{\glang(\term[2])}_{\model} \cdot \jump{\glang(\term[3])}_{\model}          \tag{IH}                                                                                \\
& = \bigcup_{G \in \glang(\term[2])} \bigcup_{H \in \glang(\term[3])} \jump{G}_{\model} \cdot \jump{H}_{\model}                 \tag{$\cdot$ is distributive w.r.t.\ $\cup$} \\
& = \bigcup_{G \in \glang(\term[2])} \bigcup_{H \in \glang(\term[3])} \jump{G \cdot H}_{\model} \tag{\Cref{proposition: graph operation: cdot}}                              \\
& = \jump{\glang(\term[2] \cdot \term[3])}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

Case $\term = \term[2] \cap \term[3]$:

\begin{align*}
& \jump{\term[2] \cap \term[3]}_{\model}   = \jump{\term[2]} \cap \jump{\term[3]}                     \tag{Def.\ of $\jump{}$}                                              \\
& = \jump{\glang(\term[2])}_{\model} \cap \jump{\glang(\term[3])}_{\model}            \tag{IH}                                                                              \\
& =  \bigcup_{G \in \glang(\term[2])} \bigcup_{H \in \glang(\term[3])} \jump{G}_{\model} \cap \jump{H}_{\model}                 \tag{$\cap$ is distributive w.r.t.\ $\cup$} \\
& =  \bigcup_{G \in \glang(\term[2])} \bigcup_{H \in \glang(\term[3])} \jump{G \cap H}_{\model} \tag{\Cref{proposition: graph operation: cap}}                              \\
& = \jump{\glang(\term[2] \cap \term[3])}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

Case $\term = \term[2] \cup \term[3]$:

\begin{align*}
\jump{\term[2] \cup \term[3]}_{\model} & = \jump{\term[2]}_{\model} \cup \jump{\term[3]}_{\model}                     \tag{Def.\ of $\jump{}$} \\
& = \jump{\glang(\term[2])}_{\model} \cup \jump{G(\term[3])}_{\model}            \tag{IH}               \\
& = \jump{\glang(\term[2]) \cup \glang(\term[3])}_{\model}                                              \\
& = \jump{\glang(\term[2] \cup \term[3])}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

Case $\term = \term[2]^*$:

\begin{align*}
& \jump{\term[2]^{*}}_{\model} = \bigcup_{n \in \nat} \jump{\term[2]^n}_{\model}                     \tag{Def.\ of $\jump{}$}                                                                                \\
& = \bigcup_{n \in \nat} \underbrace{\jump{\term[2]}_{\struc} \cdot \ldots \cdot \jump{\term[2]}_{\struc}}_{n \mbox{ times}}  \tag{Def.\ of $\jump{}$}                                                        \\
& = \bigcup_{n \in \nat} \underbrace{\jump{\glang(\term[2])}_{\struc} \cdot \ldots \cdot \jump{\glang(\term[2])}_{\struc}}_{n \mbox{ times}}       \tag{IH}                                                   \\
& = \bigcup_{n \in \nat} \bigcup_{G_1, \dots, G_n \in  \mathcal{G}(\term[2])} \jump{G_1}_{\model} \cdot \ldots \cdot \jump{G_n}_{\model}                         \tag{$\cdot$ is distributive w.r.t.\ $\cup$} \\
& = \bigcup_{n \in \nat} \bigcup_{G_1, \dots, G_n \in  \mathcal{G}(\term[2])} \jump{G_1 \cdot \ldots \cdot G_n}_{\model}  \tag{\Cref{proposition: graph operation: cdot}}                                     \\
& = \bigcup_{n \in \nat} \jump{\mathcal{G}(\term[2]^n)}_{\model}  \tag{Def.\ of $\term[2]^{n}$}                                                                                \\
& = \jump{\mathcal{G}(\term[2]^*)}_{\model}. \tag{Def.\ of $\mathcal{G}$}
\end{align*}

Case $\term = \term[2]^{\smile}$:

\begin{align*}
\jump{\term[2]^{\smile}}_{\model} & = \jump{\term[2]}_{\model}^{\smile} \tag{Def.\ of $\jump{}$}                                                    \\
& = \jump{\glang(\term[2])}_{\model}^{\smile}        \tag{IH}                                                     \\
& = \bigcup_{G \in \glang(\term[2])} \jump{G}_{\model}^{\smile}  \tag{$\smile$ is distributive w.r.t.\ $\cup$}    \\
& = \bigcup_{G \in \glang(\term[2])} \jump{G^{\smile}}_{\model}  \tag{\Cref{proposition: graph operation: smile}} \\
& = \jump{\glang(\term[2]^{\smile})}_{\model}.       \tag{Def.\ of $\mathcal{G}$}
\end{align*}

For every $\PCoRTC$ terms, $\term[1]$ and $\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. \]

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{\glang(\term[1])}_{\model} \subseteq  \jump{\glang(\term[2])}_{\model} \tag{\Cref{proposition: semantics for graphs}}              \\
& \iff \forall \model. \forall G \in \glang(\term[1]).\  \jump{G}_{\model} \subseteq \bigcup_{H \in \glang(\term[2])} \jump{H}_{\model} \tag{Def.\ of $\jump{}$} \\
& \iff \forall G \in \glang(\term[1]). \forall \model.\  \jump{G}_{\model} \subseteq \bigcup_{H \in \glang(\term[2])} \jump{H}_{\model}                          \\
& \iff \forall G \in \glang(\term[1]). \forall \ppmodel.                                                                                \\
& \quad (G \homo \ppmodel) \mbox{ implies } (\exists H \in \glang(\term[2]). H \homo \ppmodel)       \tag{Def.\ of $\jump{}$}                                    \\
& \iff \forall G \in \glang(\term[1]). \exists H \in \glang(\term[2]).\ H \homo G. \tag{$\heartsuit$}
\end{align*}

Here, for ($\heartsuit$),
Let $\ppstruc$ be the saturation (see <Ref>) of $G$ s.t.

* $a^{\ppstruc} = a^{G}$ for $a \in \SIG$;

* $\const{I}^{\ppstruc} = \set{\tuple{x, x} \mid x \in |\ppstruc|}$.

($\ppstruc$ is a $2$-pointed structure, because $\comnf{a}^{\ppstruc} = |\ppstruc|^2 \setminus a^{\ppstruc}$ and $\const{I}^{\ppstruc}$ is the identity relation.)
Since $G \homo \ppstruc$ by the identity map,
there is some $H \in \glang(\term[2])$ s.t. $H \homo \ppmodel$ (by the assumption).
Because $a^{H} = \emptyset$ for every $a \in \SIG_{\const{I}}^{(-)} \setminus \SIG$ (note that $\term[2]$ is positive) and $a^{\ppstruc} = a^{G}$ for every $a \in \SIG$,
we have $H \homo G$ by the same homomorphism for $H \homo \ppmodel$.
Let $H \in \glang(\term[2])$ be s.t. $H \homo G$.
Let $\ppmodel$ be any $2$-pointed structure s.t. $G \homo \ppmodel$.
Then, by transitivity of $\homo$, we have $H \homo \ppmodel$.
Hence, $\exists H \in \glang(\term[2]).\  H \homo \ppmodel$.

§ PROOF OF <REF>

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

By induction on $\term[1]$, as with <Ref>.

Case $\term = a$ where $a \in \SIG_{\const{I}}^{(-)} \setminus \SIG_{\const{I}}$:

\begin{align*}
\tuple{x, y} \in \jump{a}_{\model} & \iff \tuple{x, y} \in a^{\model}                                                         \tag{Def.\ of $\jump{}$}                                     \\
& \iff \begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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} \homo {\model}[x,y]                        \\
& \iff \tuple{x, y} \in \jump{\begin{tikzpicture}[baseline = -.5ex]
\graph[grow right = 1.2cm, 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}}_{\model} \tag{\Cref{definition: semantics for graphs}} \\
& \iff \tuple{x, y} \in \jump{\glang(a)}_{\model}. \tag{Def.\ of $\glang$}
\end{align*}

For the other cases, they are in the same way as the proof of <Ref>.

§ PROOF COMPLETION OF <REF>

For every $\ExKA$ term $\term[3]$ and structure $\struc$ over $\SIG$, we have

\[\jump{\term[3]}_{\struc} = \bigcup_{w \in [\term[3]]} \jump{w}_{\struc}.\]

Here, $[\term[3]] \subseteq (A_{\const{I}}^{(-, \smile)} \setminus \set{\const{I}})^*$ is the language of $\term[3]$ over $A_{\const{I}}^{(-, \smile)} \setminus \set{\const{I}}$ obtained by viewing $\term[3]$ as a term over $A_{\const{I}}^{(-, \smile)} \setminus \set{\const{I}}$.

By induction on $\term[3]$.

Case $\term[3] = a$ for $a \in A_{\const{I}}^{(-, \smile)}$ (including $a = \const{I}$):
Since $[a] = \set{a}$,
we have $\jump{a}_{\struc} = \bigcup_{w \in [a]} \jump{w}_{\struc}$.

Case $\term[3] = \bot$:
Since $[\bot] = \emptyset$,
we have
$\jump{\bot}_{\struc} = \emptyset = \bigcup_{w \in \emptyset} \jump{w}_{\struc} = \bigcup_{w \in [\bot]} \jump{w}_{\struc}$.

Case $\term[3] = \term[1] \cup \term[2]$:

\begin{align*}
\jump{\term[1] \cup \term[2]}_{\struc}
& = \jump{\term[1]}_{\struc} \cup \jump{\term[2]}_{\struc}                                                        \\
& = (\bigcup_{w \in [\term[1]]} \jump{w}_{\struc}) \cup (\bigcup_{w \in [\term[2]]} \jump{w}_{\struc})   \tag{IH} \\
& = \bigcup_{w \in [\term[1]] \cup [\term[2]]} \jump{w}_{\struc}                                                  \\
& = \bigcup_{w \in [\term[1] \cup \term[2]]} \jump{w}_{\struc}.
\end{align*}

Case $\term[3] = \term[1] \cdot \term[2]$:

\begin{align*}
\jump{\term[1] \cdot \term[2]}_{\struc}
& = \jump{\term[1]}_{\struc} \cdot \jump{\term[2]}_{\struc}                                                          \\
& = (\bigcup_{w \in [\term[1]]}\jump{w}_{\struc}) \cdot (\bigcup_{v \in [\term[2]]}\jump{v}_{\struc}) \tag{IH}       \\
& = \bigcup_{w \in [\term[1]], v \in [\term[2]]} (\jump{w}_{\struc} \cdot \jump{v}_{\struc}) \tag{By distributivity} \\
& = \bigcup_{w \in [\term[1]], v \in [\term[2]]} \jump{w v}_{\struc}                                                 \\
& = \bigcup_{w \in [\term[1] \cdot \term[2]]} \jump{w}_{\struc}.
\end{align*}

Case $\term[3] = \term[1]^*$:
We have

\begin{align*}
\jump{\term[1]^*}_{\struc}
& = \bigcup_{n \in \nat} \jump{\term[1]^n}_{\struc} = \bigcup_{n \in \nat} \jump{\term[1]}_{\struc}^n                                                  \\
& = \bigcup_{n \in \nat} (\bigcup_{w \in [\term[1]]}\jump{w}_{\struc})^n \tag{IH}                                                                      \\
& = \bigcup_{n \in \nat} \bigcup_{w_1, \dots, w_n \in [\term[1]]} (\jump{w_1}_{\struc} \cdot \ldots \cdot \jump{w_n}_{\struc}) \tag{By distributivity} \\
& = \bigcup_{n \in \nat} \bigcup_{w_1, \dots, w_n \in [\term[1]]} \jump{w_1 w_2 \dots w_n}_{\struc}                                                    \\
& = \bigcup_{n \in \nat} \bigcup_{w \in [\term[1]^n]} \jump{w}_{\struc} = \bigcup_{w \in [\term[1]^*]} \jump{w}_{\struc}. \tag*{\qedhere}
\end{align*}

§ PROOF COMPLETION OF <REF>

\[\tuple{l_0, \dots, l_{x}, l_{x+1}, \dots, l_{n'}} = \tuple{0, \dots, x, y + 1, \dots, n}.\]

(Here, “$y + 1, \dots, n$” is the empty sequence if $y = n$.)
Then, $w' = a_{l_0} \dots a_{l_{n'}}$ holds and $P' = \tuple{G', \set{U_{i}'}_{i \in [0, n']}}$ is as follows:

* $U_{i}' = U_{l_{i}}$, for each $i \in [0, n']$;

* $G'$ is the $\const{I}$-saturation of $G(w')$ such that $\const{I}^{G'} = \set{\tuple{i, j} \in [0, n']^2 \mid {i = j} \lor \lnot \Con_{\comnf{\const{I}}}^{\automaton[2]}(U_{i}', U_{j}')}$.

If $\lnot \Con_{\comnf{\const{I}}}^{\automaton[2]}(U_{i}', U_{j}')$, then $\Con_{\const{I}}^{\automaton[2]}(U_{i}', U_{j}')$ (by <ref> for $P$); thus $U_{i}' = U_{j}'$.
Therefore, the binary relation $\set{\tuple{i, j} \in [0, n]^2 \mid \lnot \Con_{\comnf{\const{I}}}^{\automaton[2]}(U_{i}', U_{j}')}$ is symmetric and transitive;
thus $\const{I}^{\graph[1]'}$ is an equivalence relation.
$G'$ is consistent because $G$ is consistent.
(In particular, when $\tuple{x, y+1} \in \const{I}^{G}$ and $a_{y+1} = \comnf{\const{I}}$,
we have $U_{x} = U_{y}$ (by the definition of $x$ and $y$) and $U_{x} = U_{y+1}$ (by $\tuple{x, y+1} \in \const{I}^{G}$),
thus $\Con_{\comnf{\const{I}}}^{\automaton[2]}(U_{x}', U_{x+1}')$ (since $a_{y+1} = \comnf{\const{I}}$ with <ref> for $P$).
Hence, $\tuple{x, x+1} \in \comnf{\const{I}}^{G'}$. Thus, since $a_{y+1} = \comnf{\const{I}}$, $G'$ is consistent.)
$\graph[1]'$ is an edge-extension of $G(w)$, because
$\const{I}^{\graph[1]'} \supseteq \const{I}^{G(w)} = \emptyset$ and $\comnf{\const{I}}^{\graph[1]'} \supseteq \comnf{\const{I}}^{G(w)}$ (by the definition of $\const{I}^{\graph[1]'}$).
Hence, $\graph[1]'$ is indeed an $\const{I}$-saturation of $G(w)$.

We show that $P'$ is an saturable path for $\not\models_{\REL} w' \le \automaton[2]$.

* For <ref>:
By $U_{0}' = U_{0}$ and $U_{n'}' = U_{n}$ with <ref> for $P$.

* For <ref>:

* for $a = \const{I}$:
Let $\tuple{i, j} \in \const{I}^{\graph[1]'}$.
If $i = j$, then we have $\Con_{\const{I}}^{\automaton[2]}(U_{i}', U_{j}')$ by <ref> for $P$.
If $\lnot \Con_{\comnf{\const{I}}}^{\automaton[2]}(U_{i}', U_{j}')$, then we have $\Con_{\const{I}}^{\automaton[2]}(U_{i}', U_{j}')$ by <ref> for $P$.

* for $a = \comnf{\const{I}}$:
By the definition of $\const{I}^{\graph[1]'}$.

* For $\Con_{a_{l_{i}}}^{\automaton[2]}(U_{i-1}', U_{i}')$ where $i \in [n']$:

Case $i \neq x + 1$:
By $\Con_{a_{l_{i}}}^{\automaton[2]}(U_{i-1}', U_{i}')$ (since $\tuple{l_{i-1}, l_{i}} \in a_{l_{i}}^{G}$ with <ref> for $P$).

Case $i = x + 1$:
Then, $U_{x}' = U_{l_{x}} = U_{x} = U_{y}$ and $U_{x+1}' = U_{l_{x+1}} = U_{y+1}$.
By $\Con_{a_{y}}^{\automaton[2]}(U_{y}, U_{y+1})$ (since $\tuple{y, y+1} \in a_{y}^{G}$ with <ref> for $P$),
we have $\Con_{a_{l_{x+1}}}^{\automaton[2]}(U_{x}', U_{x+1}')$.

* For <ref>:
By $\set{U_{i}' \mid i \in [0, n']} \subseteq \set{U_{i} \mid i \in [0, n]}$ with <ref> for $P$.

Hence, $P'$ is an saturable path for $\not\models_{\REL} w' \le \automaton[2]$.