S&C of SpeCS
M. Spasić and M. Vujošević Janičić

mode = title]Soundness and Completeness of SPARQL Query Containment Solver SpeCS
[1]

[1]This work was partially supported by Eurostars Project 3DFed (GA no. E!114681) and by the
European Research Network on Formal Proofs (COST Action CA20111).

1,2]Mirko Spasić[auid=000,bioid=1,
[1]

[url]www.matf.bg.ac.rs/ mirko

[1]Faculty of Mathematics University of Belgrade, Studentski Trg 16, Belgrade, Serbia

1] Milena Vujošević Janičić

[2]OpenLink Software, London, United Kingdom

[cor1]Corresponding author

Tool  implements an efficient automated approach for reasoning about the  query containment problem. In this paper, we prove the correctness of this approach. We give precise semantics of the core subset of  language. We briefly discuss the procedure used for reducing the query containment problem into a formal logical framework. We prove that such reduction is both sound and complete for conjunctive queries, and also for some important cases of non-conjunctive queries containing operator union, operator optional, and subqueries. Soundness and completeness proofs are considered in both containment and subsumption forms.

SPARQL query containment FOL modeling SpeCS solver correctness soundness completeness

§ INTRODUCTION

(Simple Protocol and  Query Language) is a query language and data access protocol [Prud'hommeaux and Seaborne, 2013, Prud'hommeaux and Seaborne, 2008] used for querying data in the form of Resource Description Framework () [Klyne et al., 2004, Lassila and Swick, 1999, Auer et al., 2011] within Semantic Web [Kashyap et al., 2008, Hitzler et al., 2009, Hogan, 2020].
There is a large number of  data sources available [40].
For achieving practical usability of these large amounts of data, executions of  queries have to be highly optimized [Spasić and Vujošević Janičić, 2022].

One of the central problems for  query optimizations is query containment, namely deciding if each result
of one query is at the same time a result of another query despite of a dataset being queried, i.e. this property should hold for any given dataset [Chandra and Merlin, 1977, Chekol et al., 2018, Pichler and Skritek, 2014, Chekol et al., 2012].
In the case of  query language, many authors consider a weaker form of the containment relation, i.e. subsumption [Pérez et al., 2009, Letelier et al., 2013, Arenas and Perez, 2011, Pichler and Skritek, 2014].
Instead of the strict requirement that each result of the first query should be also a result of the second one, for the subsumption relation it is enough that for each result of the first query, there is a result of the second query in which it can be embedded (subsumed), i.e. the result of the second query contains the same projections as in the result of the first query and eventually some additional ones.
An example of  queries that are in the query containment relation and in the subsumption relation  is given in Figure <ref>.

Many other important problems, like query equivalence and query satisfiablity [Chekol et al., 2018, Pichler and Skritek, 2014, Chekol et al., 2012], can be reduced to query containment [Spasić and Vujošević Janičić, 2022]. Additional applications of query containment solvers can be adopted from applications within relational databases [Levy et al., 1996, Friedman et al., 1999, Fernández et al., 1999, Gupta et al., 1994, Levy and Rousset, 1998, Calvanese et al., 2000].

Query $\kod{Q}_1$

select ?x ?y

?x a :Album .
?x :artist ?y .
?y a :SoloArtist .
?y :hometown ?z .
?z :name ?w .
filter (?w = "Los Angeles")

Query $\kod{Q}_2$

select ?x ?y
?x a :Album .
?x :artist ?y .

$\kod{Q}_1$ (left) is a sub-query of $\kod{Q}_2$ (right). Additional filters that are present in $\kod{Q}_1$ make the results obtained by $\kod{Q}_1$ a subset of the results obtained by $\kod{Q}_2$. If a projection $?y$ is removed form $\kod{Q}_1$, then the query $\kod{Q}_1$ is subsumed by $\kod{Q}_2$.

For being practically usable, it is important that a query containment solver is efficient, that it covers a wide range of the  language constructs and that it always gives correct answers.
While efficiency and coverage of a solver can be experimentally assessed, e.g. by using the relevant benchmarks [Chekol et al., 2013, Saleem et al., 2017], the correctness of an approach should be formally proved as experimental evaluation can only confirm the presence of correctness violations (and not the absence of correctness violations in general case [Dijkstra, 1972]).

Correctness of an approach includes soundness and completeness.
In the context of query containment, soundness means that the approach cannot prove that two input queries are in the containment relation if they are not. Completeness guarantees that for each pair of queries that are in the containment relation the approach will confirm that.

Correctness can be considered on two levels: procedure level and implementation level.
Correctness of the procedure level guarantees that the proposed approach is correct.  Unsound approaches are usually not useful and therefore soundness is considered as a basic requirement.
For example, in the case of query containment, a trivial procedure that returns always true (stating for any two queries that these are in the containment relation) is not a sound one, because there exist two queries for which the procedure will claim the containment (as it always does), while they are not in the relation.
On the other hand, completeness of this procedure is present as for any two queries satisfying the relation, the procedure will confirm that.
Having completeness together with soundness is desirable, but it is usually achievable only on a subset of the considered problem.
Correctness of the implementation level guarantees that the procedure is correctly implemented, i.e. that the software meets its specification.

Frameworks like Isabelle [Nipkow et al., 2002] and Coq [Bertot and Castran, 2010], incorporate development of formally verified software. There are different solvers and tools developed within these frameworks [Leroy, 2009, Marić, 2010, Spasić and Marić, 2012]. However, such development is very expensive and time consuming. A step towards formally verified software is a formal correctness proof of the proposed procedure while correctness of the implementation is based on the standard software development techniques. There are several different approaches for deciding  query containment, and for some of them, correctness of their procedures is proved.

The most important  solvers that deal with query containment or query equivalence include  [Chekol et al., 2018],  [22],  [Letelier et al., 2013],  [Stadler et al., 2018],  [Salas and Hogan, 2018] and  [Spasić and Vujošević Janičić, 2022].
solver uses an expressive modal logic i.e. $\mu$-calculus, and reduces [Chekol et al., 2012, Chekol et al., 2012] the containment problem to a satisfiability problem in a fragment of the $\mu$-calculus without alternation [Kozen, 1982].
It uses a tool for deciding satisfiablility  within $\mu$-calculus [Tanabe et al., 2005].
solver also uses a variant of $\mu$-calculus without alternation, specially designed for reasoning over finite trees [Genevès et al., 2015].
For  and , soundness and completeness of their procedures are proved [Chekol et al., 2018, Genevès et al., 2015].
solver introduces an algebra of query plans for a subset of  graph patterns. The solver is a prototype used for theoretical examination of complexity of the query containment problem and its correctness is not considered.
Similarly,  solver is based on algebra expression trees that are constructed after  queries and on a subgraph isomorphism solver. Correctness of its procedure is also not considered.
On the other hand,  is a tool (not a containment solver) for canonicalisation of monotone  queries, i.e. it reduces a query to an equivalent one in a canonical form.
It can be used for checking the equivalence of queries in a syntactic way by comparing the string representations of their canonical forms.
Soundness and completeness of this procedure is proved [Salas and Hogan, 2018, Salas and Hogan, 2018].

[Spasić and Vujošević Janičić, 2022] is an open source query containment solver which is based on transforming the query containment problem into a satisfiability problem [Barrett et al., 2009] in first order logic ().  and  have the same expressive power [Angles and Gutierrez, 2008] so reducing query containment into  satisfiability problem is a promising approach. According to thorough evaluation on the two most important benchmarks, Query Containment Benchmark [Chekol et al., 2013] and SQCFramework [Saleem et al., 2017],   covers all widely used  language constructs and it is highly efficient. Compared to other state-of-the-art solvers,  has a better performance and it supports a bigger number of language constructs [Spasić and Vujošević Janičić, 2022].

In this paper, we prove the correctness of the approach used by . We give the precise semantics of the covered  constructs and all definitions and proofs of lemmas that are necessary for proving correctness.
All definitions are given recursively and proofs are done inductively, so when the approach is extended with additional language constructs, the definitions and proofs can also be incrementally extended.

Overview of the paper.

Section <ref> defines a relevant subset of  syntax and semantics, and formally defines problems of query containment, query subsumption, query equivalence and query satisfiability.
Section <ref> defines the signature of the used theory, the procedure for transforming conjunctive queries into  formulas and logical formulation of the containment and subsumption problem. It also gives proofs of lemmas that are connecting  terms, variables, expressions, conditions, graph patterns and queries with corresponding terms, variables, expressions, conditions and formulas in .
Section <ref> gives necessary definitions and lemmas for proving correctness of the proposed modeling. It gives proofs of soundness and completeness of the proposed approach for both containment and subsumption problem.
Section <ref> deals with queries that are not conjunctive: queries that contain operators union and optional and that contain subqueries.
Section <ref> gives final conclusions and presents possible directions for further work.

§ SPARQL AND QUERY CONTAINMENT PROBLEM

The Resource Description Framework (), as a World Wide Web Consortium (W3C) recommendation, is an accepted data model for expressing information about World Wide Web resources in a flexible and extensible way.
It is represented as a directed graph consisting of triple statements, i.e.  triples, where each of them is composed of a node for the subject, an edge for the predicate connecting the subject to an object, and a node for the object.
Each of these three parts can be identified by an internationalized resource identifier -  (generalisation of the uniform resource identifiers) [Dürst and Suignard, 2005], subject and object can be unidentified resources, i.e.  blank nodes, while the object can also be a literal value.
As we follow the standard definition of mutually disjoint, countable sets V (a set which contains variables), I (a set which contains s), B (a set which contains blank nodes) and L (a set which contains literals) [Gutierrez et al., 2004, Pérez et al., 2009, Chekol et al., 2012, Schmidt et al., 2010, Angles and Gutiérrez, 2016],
an  triple is an element of the set $\kod{IB} \times \kod{I} \times \ibl{}$.[Like in [Chekol et al., 2018], we abbreviate any union of sets I, B, L and V as, for instance, $\ibl{} \Eqdef \kod{I} \cup \kod{B} \cup \kod{L}$.]
Sets of  triples are called  graphs, which can further form an  dataset, precisely introduced in the following definition.

Let $\kod{i}_k$ denote an  and let $\kod{\gr}_k$ denote an  graph. Let different  graphs have disjoint sets of blank nodes. According to [Spasić and Vujošević Janičić, 2022] we introduce the following definitions.

An  dataset D is defined as a set containing a default graph named $\dg$ and zero or more named graphs $\langle \kod{i}_k, \kod{\gr}_k \rangle$:

$$\kod{D} \eqdef \{\dg, \langle \kod{i}_1, \kod{\gr}_1 \rangle, \ldots, \langle \kod{i}_n, \kod{\gr}_n \rangle \}$$

Function $\mathit{df}$ maps a dataset $\kod{D}$ to its default graph:
$$\mathit{df}(\kod{D}) \eqdef \dg$$

Function $names$ maps a dataset $\kod{D}$ to the set of s of its named graphs:
$$names(\kod{D}) \eqdef \{\kod{i}_1, \ldots , \kod{i}_n\}$$

Function $gr$ maps a dataset and an $\iri$ into a graph corresponding to the $\iri$ within the given dataset:[For readability reasons, the first parameter is written in subscript.]

$$gr_\kod{\,D}(\kod{i}_k) \eqdef
\begin{cases}
\kod{\gr}_k, & \text{if } \langle \kod{i}_k, \kod{\gr}_k \rangle \in \kod{D}\\
\kod{\gr}_{\varnothing}, & \text{otherwise,}
\end{cases}$$

where $\kod{\gr}_{\varnothing}$ is an empty graph.

Function $merge$ maps a subset $\{\kod{\gr}_{k_1}, \ldots, \kod{\gr}_{k_m}\}$[Note that sets of blank nodes of different graphs $\kod{\gr}_{k_i}$ are disjoint.] of  graphs into a graph containing a union of their nodes:

$$merge\,(\{\kod{\gr}_{k_1}, \ldots, \kod{\gr}_{k_m}\})  \eqdef \bigcup_{i=1}^{m} \kod{\gr}_{k_i}$$

§.§  Syntax

is a language for querying data stored in the relevant datasets, i.e.  graphs.
The main feature of  logic used in the evaluation of queries is a pattern matching facility, i.e. a finding of relevant triple statements within a queried dataset based on a pattern specified by a query in question.

precisely defined the  query grammar in the ebnf notation [Prud'hommeaux and Seaborne, 2013].
In this paper we discuss the simplified subset of this grammar, given in Figure <ref>, containing the most relevant language constructs used in practice.

Query   ::= @'select'@ Vars
(@'from'@ @iri@)*
(@'from'@ @'named'@ @iri@)*
@'where'@ @''@ GPatt @''@
Vars    ::= @'*'@ | @var@+
GPatt   ::= TPatt
| GPatt @'.'@ GPatt
| GPatt @'union'@ GPatt
| GPatt @'minus'@ GPatt
| GPatt @'diff'@ GPatt
| GPatt @'optional'@ GPatt
| GPatt @'filter'@ Cond
|  @''@ GPatt @''@
| @''@ SubQuery @''@
| @'graph'@ @var@ @''@ GPatt @''@
| @'graph'@ @iri@ @''@ GPatt @''@
TPatt   ::= Subject Predicate Object
Subject ::= @var@ | @iri@ | @blankNode@

Predicate ::= @var@ | @iri@
Object    ::= @var@ | @iri@ | @blankNode@
| @rdfLiteral@
Cond      ::=  Expr @'='@ Expr
| UnOp Cond
| Cond BinOp Cond
| @'('@ Cond @')'@
| @'isliteral'@ @'('@ Expr @')'@
| ... (*     $//~other ~ built$-$in ~ functions$ *)
(*     $//~ and ~ relational ~ operators$ *)
Expr      ::= @var@ | @iri@ | @rdfLiteral@
| @'datatype'@ @'('@ Expr @')'@
| ... (*     $//~other ~ built$-$in ~ functions$ *)
(*     $//~ and ~ arithmetic ~ operators$ *)
UnOp      ::= @'!'@
BinOp     ::= @'      '@ | @'||'@
SubQuery  ::= @'select'@ Vars
@'where'@ @''@ GPatt @''@

A core subset of the  grammar, taken from [Spasić and Vujošević Janičić, 2022].

Similar to other query languages, a  query contains:

* a select clause, specifying a set of variables of interest, i.e. distinguished variables, (described by nonterminal Vars in the grammar).
Instead of listing them, this clause can contain symbol *, meaning that the set of distinguished variables contains all the variables present in the graph pattern within where clause.

* (optionally) from and from named clauses for precise specification of the relevant dataset.
Normally, a query is executed against an  dataset denoted by $\dataq$.
Using these two clauses, a query defines a different dataset on which query evaluation is performed, i.e. query dataset (Definition <ref>).

* a where clause containing a graph pattern (described by nonterminal GPatt) for pattern matching within the query dataset.

A query dataset $\ag$ which is specified by the from and from named clauses of a query executed against an  dataset $\dataq$, is defined in the following way:

$\circ$ If a query does not contain neither from nor from named clauses,
$$\ag \eqdef \dataq$$

$\circ$ Otherwise,
$$\ag \eqdef \{\dg, \langle \kod{i}_{l_1}, gr_{\dataq}(\kod{i}_{l_1}) \rangle, \ldots, \langle \kod{i}_{l_n}, gr_{\dataq}(\kod{i}_{l_n}) \rangle \}$$

$$\dg =
\begin{cases}
\kod{\gr}_{\varnothing} , & \text{if a query contains \kod{from named} clauses} \\
& \text{and no \kod{from} clauses } \\
merge\,(gr_{\dataq}(\kod{i}_{k_1}),\ldots,gr_{\dataq}(\kod{i}_{k_m})), \hspace*{-35mm}  & \\
& \text{for \iri{}s }\kod{i}_{k_j} , j \in \{1, \ldots, m\}, \text{ apearing in}\\
& \text{\kod{from} clauses of the query,} \\
\end{cases}

and $i_{l_1}, \ldots, i_{l_n}$ are s appearing in from named clauses (if a query does not contain from named clauses, than the dataset does not contain named graphs).

Note that if some  $\kod{k}$ mentioned in a from or from named clause does not belong to $names(\dataq)$, by Definition <ref> it holds $gr_{\dataq}(\kod{k}) = \varnothing$.

The simplest form of graph pattern is a triple pattern, defined as a nonterminal TPatt by the grammar, i.e. an element of the set $\kod{VIB} \times \kod{VI} \times \vibl{}$.
Elements of sets V, I, B and L correspond to the  terms, i.e. var, iri, blankNode and rdfLiteral of the grammar given in Figure <ref>.
Graph patterns may contain different operators, like ., union, minus, diff [Angles and Gutiérrez, 2016], optional, filter, braces and graph, but also it can be a subquery (described by nonterminal SubQuery).
A filter clause can contain different conditions (described by nonterminal Cond in the grammar), i.e. a relational comparison of expressions and built-in functions (isliteral, isuri, contains, bound, regex) and their logical combinations.
Expressions (described by nonterminal Expr in the grammar) can be variables, s, literals, and also arithmetic operators and built-in functions (datatype, round, abs, str, lcase) over them.

§.§  Semantics

The following definition specifies variables appearing in a language construct.

Let t be an  term,  be a triple pattern, E, $\kod{E}_1$, $\kod{E}_2$ expressions (described by nonterminal Expr in the grammar), R, $\kod{R}_1$, $\kod{R}_2$ built-in conditions (described by nonterminal Cond in the grammar), and , $\kod{\pat}_1$, $\kod{\pat}_2$ graph patterns.
Variables appearing in the  term t, triple pattern , expression E, condition R and graph pattern , in notation $\kod{var}(\kod{t})$, $\kod{var}(\kod{\tpat})$, $\kod{var}(\kod{E})$, $\kod{var}(\kod{R})$ and $\kod{var}(\kod{\pat})$ respectively, are

\begin{align*}
\kod{var}(\kod{t}) \  \eqdef & \
\begin{cases}
\{\kod{t}\},& \kod{t} \in \kod{VB}\\
\varnothing,& \kod{t} \in \kod{IL}\\
\end{cases}     \\
\kod{var}(\kod{\tpat}) \  \eqdef & \
\begin{cases}
\kod{var}(\kod{s}) \cup \kod{var}(\kod{p}) \cup \kod{var}(\kod{o}),
& \kod{\tpat} \text{ is \codebox{$\kod{s p o}$}, } \kod{s} \in \kod{VIB}, \\
& \kod{p} \in \kod{VI}, \kod{o} \in \kod{VIBL}\\
\end{cases}     \\
\kod{var}(\kod{E}) \  \eqdef & \
\begin{cases}
\kod{var}(\kod{t}),& \kod{E} \text{ is } \kod{t} \text{ and } \kod{t} \in \kod{VIL}\\
\kod{var}(\kod{E}_1), & \kod{E} \text{ is } \kod{datatype(E}_1\kod{)}
\end{cases}     \\
\kod{var}(\kod{R}) \  \eqdef & \
\begin{cases}
\kod{var}(\kod{E}_1) \cup \kod{var}(\kod{E}_2),
& \kod{R} \text{ is } \kod{E}_1 = \kod{E}_2\\
\kod{var}(\kod{E}_1),
& \kod{R} \text{ is } \kod{isliteral(E}_1\kod{)} \\
\kod{var}(\kod{R}_1),
& \kod{R} \text{ is } \kod{!R}_1 \text{ or } \\
& \kod{R} \text{ is } \kod{(R}_1\kod{)}\\
\kod{var}(\kod{R}_1) \cup \kod{var}(\kod{R}_2),
& \kod{R} \text{ is } \kod{R}_1 \kod{\&\&} \kod{R}_2 \text{ or } \\
& \kod{R} \text{ is } \kod{R}_1 \kod{||} \kod{R}_2\\
\end{cases}     \\
\kod{var}(\kod{\pat}) \  \eqdef & \
\begin{cases}
\kod{var}(\kod{\tpat}),& \kod{\pat} \text{ is } \kod{\tpat}\\
\kod{var}(\kod{\pat}_1),& \kod{\pat} \text{ is } \kod{\pat}_1 \  \kod{filter} \ \kod{R} \text{ or } \\
& \kod{\pat} \text{ is } \kod{\{\pat}_1\kod{\}} \text{ or }\\
& \kod{\pat} \text{ is } \kod{\pat}_1 \  \kod{minus} \ \kod{\pat}_2 \text{ or }\\
& \kod{\pat} \text{ is } \kod{\pat}_1 \  \kod{diff} \ \kod{\pat}_2 \text{ or }\\
& \kod{\pat} \text{ is } \kod{graph i \{\pat}_1\kod{\}} \\
\kod{var}(\kod{\pat}_1) \cup \kod{var}(\kod{\pat}_2),
& \kod{\pat} \text{ is } \kod{\pat}_1 \  . \ \kod{\pat}_2 \text{ or }\\
& \kod{\pat} \text{ is } \kod{\pat}_1 \  \kod{optional} \ \kod{\pat}_2 \text{ or } \\
& \kod{\pat} \text{ is } \kod{\pat}_1 \  \kod{union} \ \kod{\pat}_2 \\
\kod{var}(\kod{\pat}_1) \cup \{\kod{x}\},
& \kod{\pat} \text{ is } \kod{graph x \{\pat}_1\kod{\}} \\
\overline{\kod{dv}_\kod{sq}},& \kod{\pat} \text{ is } \kod{\{Q$_\kod{sq}$\}} \text{ and } \overline{\kod{dv}_\kod{sq}} \text{ is a}\\
& \text{set of distinguished} \\
& \text{variables of } \kod{Q$_\kod{sq}$}
\end{cases}
\end{align*}

Note that we assume $\kod{var}(\kod{R}) \subseteq \kod{var}(\kod{\pat}_1)$ for each graph pattern $\kod{\pat} = \kod{\pat}_1 \  \kod{filter} \ \kod{R}$, as the opposite is not
computationally desirable [Pérez et al., 2006].

We follow the standard notation and set semantics of a  query and of a graph pattern evaluation [Chekol et al., 2018, Pérez et al., 2006, Pérez et al., 2009, Angles and Gutierrez, 2008].[Different semantics are also possible, like the standard bag semantics [Pérez et al., 2009, Angles and Gutierrez, 2008, Angles and Gutierrez, 2016].
A comparison [Pérez et al., 2009] of set and bag semantics presents the reasons why set semantics is of fundamental importance in the development and implementation of a query language.]

Intuitively, a result of a  query execution connects variables (and blank nodes which cannot be retrieved by the query) from the graph pattern of query to the values within a graph of the query dataset, i.e. to the values of .
Therefore, the function $\mu$ denotes a partial mapping from the set of variables and blank nodes VB to the set .
In the following text, $dom(m)$ denotes the domain of a mapping $m$, while the function $\mu_{\kod{x} \rightarrow \kod{c}}$ denotes a mapping such that $dom(\mu_{\kod{x} \rightarrow \kod{c}}) \eqdef \{\kod{x}\}$ and $\mu_{\kod{x} \rightarrow \kod{c}}(\kod{x}) \eqdef \kod{c}$.

Mappings $m_1$ and $m_2$ are compatible, denoted by $m_1 \comp m_2$, if for each ${x}$ such that ${x} \in dom(m_1) \cap dom(m_2)$ it holds that $m_1({x}) = m_2({x})$.

Note that two mappings with disjoint domains are always compatible.
Also, if $m_1 \comp m_2$, then $m_1 \cup m_2$ is also a mapping, such that it holds:

\begin{align*}
dom(m_1 \cup m_2) = & ~ dom(m_1) \cup dom(m_2)\\
(m_1 \cup m_2)(x) = & \begin{cases}
m_1(x), & x \in dom(m_1)\\
m_2(x), & \text{otherwise}
\end{cases}
\end{align*}

Furthermore, $m_1 \cup m_2$ is compatible with both $m_1$ and $m_2$.

Let $\Omega_1$ and $\Omega_2$ be sets of mappings.
Operations union, join, difference, minus and left outer-join are defined as follows [Pérez et al., 2009]:

\begin{align*}
\hspace*{5mm}
\Omega_1 \cup \Omega_2  \eqdef & \ \{ m \ | \ m \in \Omega_1 \ \text{or} \ m \in \Omega_2 \}&\\
\Omega_1 \bowtie \Omega_2  \eqdef & \ \{ m_1 \cup m_2 \ | \ m_1 \in \Omega_1, m_2 \in \Omega_2, m_1 \comp m_2 \}&\\
\Omega_1 \setminus \Omega_2  \eqdef & \ \{ m_1 \ | \ m_1 \in \Omega_1 \ \text{and for all} \ m_2 \in \Omega_2\text{,} &\\
& ~~~ m_1 \text{ and } m_2 \text{ are not compatible}\} &\\
\Omega_1 - \Omega_2  \eqdef & \ \{ m_1 \ | \ m_1 \in \Omega_1 \ \text{and for all} \ m_2 \in \Omega_2\text{,} &\\
& ~~~ m_1 \text{ and } m_2 \text{ are not compatible, or } &\\
& ~~~ dom(m_1) \cap dom(m_2) = \varnothing\}&\\
\Omega_1 \leftouterjoin \Omega_2  \eqdef & \ (\Omega_1 \bowtie \Omega_2) \cup (\Omega_1 \setminus \Omega_2)&
\end{align*}

Let $\overline{x}$ denote a set containing variables $x_i$, for each $i \in \{1, \ldots, n\}$, i.e. $\overline{x} = \{x_1, ..., x_n\}$.

A mapping $m_1$ is an extension of a mapping $m_2$ (a mapping $m_2$ is a restriction of a mapping $m_1$), denoted by $m_1 \succeq m_2$ ($m_2 \preceq m_1$), if $m_1 \comp m_2$ and $dom(m_1) \supseteq dom(m_2)$.
Projection of a mapping $m$ to the set $\overline{x}$, denoted by $m_{\overline{x}}$, is a mapping such that $dom(m_{\overline{x}}) = dom(m) \cap \overline{x}$ and $m_{\overline{x}} \preceq m$.

Note that if sets $dom(m)$ and $\overline{x}$ are disjoint, $m_{\overline{x}}$ is an empty mapping, i.e a mapping with an empty domain.

Let $\Omega$ be a set of mappings, and $\overline{x}$ be a set of variables.
Then, a projection operator over the sets $\overline{x}$ and $\Omega$, denoted $\PP_{\overline{x}}(\Omega)$, is defined as:

$$\PP_{\overline{x}}(\Omega) \eqdef \{m_{\overline{x}} \;|\; m \in \Omega\}$$

According to the  semantics [Prud'hommeaux and Seaborne, 2013], the following function is needed in Definition <ref>.

Let l be a literal, function $\kod{dt}: \kod{L} \rightarrow \kod{I}$ is defined as follows:

\begin{align*}
\kod{dt(l)} \eqdef
\begin{cases}
\kod{i}\,, & \kod{l} \text{  is typed literal, with }\\
& \kod{\^}\hspace*{-2pt}\kod{\^}\hspace*{-2pt}\kod{i} \text{ in suffix, \kod{i}} \hspace*{-1mm}\in\hspace*{-1mm} \text{\kod{I},}\\
\kod{xsd:string}\,, & \kod{l} \text{  is untyped literal.}
\end{cases}
\end{align*}

A mapping may be naturally extended on s, literals and variables and blank nodes outside of its domain, by introducing an additional constant named $\error$, as specified in the following definition.

A value of an  term t, an expression $\kod{E}$, and a triple pattern $\kod{\tpat}$, according to the mapping $\mu$, in notation
$\valuation{\kod{t}}{\mu}$, $\valuation{\kod{E}}{\mu}$, and $\valuation{\kod{\tpat}}{\mu}$ respectively,
is a value from , defined in the following way:

\begin{align*}
\valuation{\kod{t}}{\mu} & \eqdef \
\begin{cases}
\kod{t} \; ,\hphantom{---} & \kod{t} \in \kod{IL} \\
\mu(\kod{t}) \; , \hphantom{--} & \kod{t} \in \kod{VB} \text{ and } \kod{t} \in dom(\mu)\\
\error \; , \hphantom{--} & \kod{t} \in \kod{VB} \text{ and } \kod{t} \notin dom(\mu)\\
\end{cases} \\
\valuation{\kod{E}}{\mu} & \eqdef \
\begin{cases}
\valuation{\kod{t}}{\mu} \; ,\hphantom{--}& \kod{E} \ \text{is} \ \kod{t} \text{, } \kod{t} \in \kod{VIL} \\
\kod{dt}(\valuation{\kod{E}_1}{\mu}),&  \kod{E} \text{ is } \kod{datatype(E}_1\kod{)} \text{ and } \valuation{\kod{E}_1}{\mu} \not= \error \\
\error, & \kod{E} \text{ is } \kod{datatype(E}_1\kod{)} \text{ and } \valuation{\kod{E}_1}{\mu} = \error
\end{cases} \\
\valuation{\kod{\tpat}}{\mu} & \eqdef \
\begin{cases}
\valuation{\kod{s}}{\mu} \kod{ } \valuation{\kod{p}}{\mu} \kod{ } \valuation{\kod{o}}{\mu} \; ,  \\
\hspace*{18mm} \kod{\tpat} \text{ is \codebox{$\kod{s p o}$} and } \kod{s} \in \kod{VIB},\\
\hspace*{18mm} \kod{p} \in \kod{VI}, \kod{o} \in \vibl{}\\
\end{cases}
\end{align*}

A set  is an extension of the set  containing this constant, i.e. $\ible \Eqdef \ibl \cup \{ \error \}$.

Let E, $\kod{E}_1$ and $\kod{E}_2$ be expressions, R, $\kod{R}_1$ and $\kod{R}_2$ built-in conditions.
A mapping $\mu$ satisfies built-in condition R, denoted $\mu \zadovoljava \kod{R}$, if:

\begin{align*}
\hspace*{3mm}
\mu \zadovoljava \kod{R} \  \eqdef \
\begin{cases}
\valuation{\kod{E}_1}{\mu} \not= \error, \\ \valuation{\kod{E}_2}{\mu} \not= \error \text{ and } \\
\valuation{\kod{E}_1}{\mu} = \valuation{\kod{E}_2}{\mu} \; , & \kod{R} \ \text{is} \ \kod{E}_1 = \kod{E}_2\\
\text{if not } \mu \zadovoljava \kod{R}_1 \; , \text{ } & \kod{R} \ \text{is} \ \kod{!R}_1\\
\mu \zadovoljava \kod{R}_1 \text{ and } \mu \zadovoljava \kod{R}_2 \; , & \kod{R} \ \text{is} \ \kod{R}_1 \kod{\&\&} \kod{R}_2\\
\mu \zadovoljava \kod{R}_1 \text{ or } \mu \zadovoljava \kod{R}_2 \; , & \kod{R} \ \text{is} \ \kod{R}_1 \kod{||} \kod{R}_2\\
\mu \zadovoljava \kod{R}_1 \; , & \kod{R} \ \text{is} \ \kod{(R}_1\kod{)}\\
\valuation{\kod{E}_1}{\mu} \not= \error  \text{ and } \\
\valuation{\kod{E}_1}{\mu} \in \kod{L}, & \kod{R} \text{ is } \kod{isliteral(E}_1\kod{)}
\end{cases}
\end{align*}

Let $\ag$ be an  dataset,  a graph within $\ag$,  a triple pattern, , $\kod{\pat}_1$, $\kod{\pat}_2$ graph patterns, and R a built-in condition.
An evaluation of a graph pattern over the graph $\kod{\gr}$, which is in this context called the active graph, within the dataset $\ag$,
is defined recursively as follows:

\begin{align*}
\semdg{\kod{\tpat}}{\ag}{\kod{\gr}} &\eqdef \{ \mu \ | \ dom(\mu) = \kod{var}(\kod{\tpat}) \; \wedge  \valuation{\kod{\tpat}}{\mu} \in \kod{\kod{\gr}} \} \\
\semdg{\kod{\pat}_1 \  . \ \kod{\pat}_2}{\ag}{\kod{\gr}} &\eqdef \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \bowtie \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}\\
\semdg{\kod{\pat}_1 \  \kod{union} \ \kod{\pat}_2}{\ag}{\kod{\gr}} &\eqdef \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \cup \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}} \\
\semdg{\kod{\pat} \  \kod{filter} \ \kod{R}}{\ag}{\kod{\gr}} &\eqdef \{ \mu \in \semdg{\kod{\pat}}{\ag}{\kod{\gr}} \ | \ \mu \zadovoljava \kod{R} \}\\
\semdg{\kod{\{\pat\}}}{\ag}{\kod{\gr}} &\eqdef \semdg{\kod{\pat}}{\ag}{\kod{\gr}} \\
\semdg{\kod{\pat}_1 \  \kod{minus} \ \kod{\pat}_2}{\ag}{\kod{\gr}} & \eqdef \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} - \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}} \\
\semdg{\kod{\pat}_1 \  \kod{diff} \ \kod{\pat}_2}{\ag}{\kod{\gr}} & \eqdef \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \setminus \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}} \\
\semdg{\kod{\pat}_1 \  \kod{optional} \ \kod{\pat}_2}{\ag}{\kod{\gr}} & \eqdef \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \leftouterjoin \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}} \\
\semdg{\kod{graph x \{\pat\}}}{\ag}{\kod{\gr}} & \eqdef \hspace*{-3mm} \underset{\kod{i} \in names(\ag)} \bigcup \hspace*{-3mm} \left(\semdg{\kod{\pat}}{\ag}{gr_{\,\ag}(\kod{i})} \bowtie  \{ \mu_{\kod{x} \rightarrow \kod{i}} \} \right)\\
\semdg{\kod{graph i \{\pat\}}}{\ag}{\kod{\gr}} & \eqdef \semdg{\kod{\pat}}{\ag}{gr_{\,\ag}(\kod{i})} \\
\semdg{\kod{\{Q$_\kod{sq}$\}}}{\ag}{\kod{G}} & \eqdef \semd{\kod{Q}_\kod{sq}}{\ag} ~ \footnotemark
\end{align*}

$\semd{\kod{Q}_\kod{sq}}{\ag}$ represents the evaluation of query $\kod{Q}_\kod{sq}$ over a dataset $\ag$, introduced later in Definition <ref>.

The following lemma connects a domain of an evaluation of a graph pattern and variables of a graph pattern.

Let $\ag$ be an  dataset,  a graph within $\ag$,  a graph pattern which is union-free, optional-free and without subqueries, and $\mu$ a mapping such that $\mu \in \semdg{\kod{\pat}}{\ag}{\kod{\gr}}$.

$dom(\mu) = \kod{var}(\kod{\pat})$.

The lemma is proved by induction over graph pattern $\kod{\pat}$.

*  is

By Definition <ref>, from $\mu \in \semdg{\kod{\tpat}}{\ag}{\kod{\gr}}$, it holds $dom(\mu) = \kod{var}(\kod{\tpat})$.

* $\kod{\pat}$ is $\kod{\pat}_1 . \kod{\pat}_2$

By Definition <ref>, from $\mu \in \semdg{\kod{\pat}_1 . \kod{\pat}_2}{\ag}{\kod{\gr}}$, it holds

$$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \bowtie \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$$

By Definition <ref>, there exist compatible mappings $\mu_1$ and $\mu_2$, such that $\mu = \mu_1 \cup \mu_2$,

$$\mu_1 \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \text{ and }\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$$

Therefore, it holds $dom(\mu) = dom(\mu_1) \cup dom(\mu_2)$.
By induction hypothesis, it holds

$$dom(\mu_1) = \kod{var}(\kod{\pat}_1) \text{ and } dom(\mu_2) = \kod{var}(\kod{\pat}_2).$$

Then, $dom(\mu) = \kod{var}(\kod{\pat}_1) \cup \kod{var}(\kod{\pat}_2)$, i.e. by Definition <ref>, it holds $dom(\mu) = \kod{var}(\kod{\pat}_1 . \kod{\pat}_2)$.

* $\kod{\pat}$ is $\kod{\pat}_1 \kod{ filter } \kod{R}$

By Definition <ref>, from $\mu \in \semdg{\kod{\pat}_1 \kod{ filter } \kod{R}}{\ag}{\kod{\gr}}$, it holds
$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$.
By induction hypothesis, it also holds
$dom(\mu) = \kod{var}(\kod{\pat}_1)$.
Therefore, by Definition <ref>, it holds $dom(\mu) = \kod{var}(\kod{\pat}_1 \kod{ filter } \kod{R})$.

* $\kod{\pat}$ is $\kod{\{\pat}_1\kod{\}}$

By Definition <ref>, from $\mu \in \semdg{\kod{\{\pat}_1\kod{\}}}{\ag}{\kod{\gr}}$, it holds
$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$.
By induction hypothesis, it holds
$dom(\mu) = \kod{var}(\kod{\pat}_1)$.
Therefore, by Definition <ref>, it also holds $dom(\mu) = \kod{var}(\kod{\{\pat}_1\kod{\}})$.

* $\kod{\pat}$ is $\kod{\pat}_1 \; \kod{diff} \; \kod{\pat}_2$

By Definition <ref>, from $\mu \in \semdg{\kod{\pat}_1 \; \kod{diff} \; \kod{\pat}_2}{\ag}{\kod{\gr}}$, it holds

$$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \setminus \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$$

Therefore, by Definition <ref>, it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$.
By induction hypothesis, it holds
$dom(\mu) \hspace*{-3pt}=\hspace*{-3pt} \kod{var}(\kod{\pat}_1)$.
Then, by Definition <ref>, it holds $dom(\mu) = \kod{var}(\kod{\pat}_1 \; \kod{diff} \; \kod{\pat}_2)$.

* $\kod{\pat}$ is $\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2$

By Definition <ref>, from $\mu \in \semdg{\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2}{\ag}{\kod{\gr}}$, it holds

$$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} - \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$$

Therefore, by Definition <ref>, it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$.
By induction hypothesis, it holds
$dom(\mu) \hspace*{-3pt}=\hspace*{-3pt} \kod{var}(\kod{\pat}_1)$.
Then, by Definition <ref>, it holds $dom(\mu) \hspace*{-2pt}=\hspace*{-2pt} \kod{var}(\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2)$.

* $\kod{\pat}$ is $\kod{graph x \{\pat}_1\kod{\}}$

By Definition <ref>, from
$$\mu \in \semdg{\kod{graph x \{\pat}_1\kod{\}}}{\ag}{\kod{\gr}},$$
it holds

$$\mu \in \underset{\kod{i} \in names(\ag)} \bigcup \left(\semdg{\kod{\pat}}{\ag}{gr_{\,\ag}(\kod{i})} \bowtie  \{ \mu_{\kod{x} \rightarrow \kod{i}} \} \right).$$

Therefore, by Definition <ref> and induction hypothesis, it holds

$$dom(\mu) = \kod{var}(\kod{\pat}_1) \cup \{\kod{x}\}.$$

Then, by Definition <ref>, it holds

$$dom(\mu) = \kod{var}(\kod{graph x \{\pat}_1\kod{\}}).$$

* $\kod{\pat}$ is $\kod{graph i \{\pat}_1\kod{\}}$

By Definition <ref>, from
$$\mu \in \semdg{\kod{graph i \{\pat}_1\kod{\}}}{\ag}{\kod{\gr}},$$
it holds

$$\mu \in \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})}.$$

Therefore, by induction hypothesis, it holds

$$dom(\mu) = \kod{var}(\kod{\pat}_1).$$

Then, by Definition <ref>, it holds

$$dom(\mu) = \kod{var}(\kod{graph i \{\pat}_1\kod{\}}).$$

An evaluation of a query Q over a dataset $\dataq$
is defined as

$$\semdq{\kod{Q}} \eqdef \PP_{\overline{\kod{dv}}}(\semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)})$$

where within the query Q, qpat is a query pattern, $\overline{\kod{dv}}$ is a set of distinguished variables, and $\ag$ is a query dataset.

In a case when a mapping $\mu$ from $\semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}$ has a disjoint domain with $\overline{\kod{dv}}$, $\semdq{\kod{Q}}$ contains the empty mapping, corresponding to the empty  solution.
In a case when the set $\semdq{\kod{Q}}$ is an empty set, there is no result of a query evaluation.

Note that each query specifies the active graphs that are used for evaluation of its graph patterns.
For each considered graph pattern (Figure <ref>) the active graph is equal to the default graph of the query dataset, except in case for $\kod{graph x \{ \pat{} \}}$ and $\kod{graph i \{ \pat{} \}}$.
These two constructs give a possibility to match the graph pattern $\kod{\pat}$ against named graphs in the query dataset [Angles and Gutierrez, 2008].

For an  dataset $\dataq$, a query Q and a mapping $\mu$ such that $\mu \in \semdq{\kod{Q}}$, all variables from $dom(\mu)$ are called relevant variables.

There is a slight but important difference between relevant and distinguished variables. Although every relevant variable is at the same time a distinguished variable, in the opposite direction this does not hold. A projection variable appearing only in the select clause and nowhere else in the query pattern is an example of a distinguished variable that is not relevant.
The following lemma connects the relevant variables with the corresponding query pattern and distinguished variables.

Let Q be a query, $\overline{\kod{dv}}$ a set of its distinguished variables, $\kod{qpat}$ its graph pattern which is union-free, optional-free and without subqueries, and $\overline{\kod{rv}}$ a set of its relevant variables.

$\overline{\kod{rv}}= \kod{var}(\kod{qpat}) \cap \overline{\kod{dv}}$.

By Definition <ref>, there is a mapping $\mu$ and a dataset $\dataq$ such that $\mu \in \semd{\kod{Q}}{\dataq}$ and $\overline{\kod{rv}} = dom(\mu)$.
Then, by Definition <ref>, it holds

$$\mu \in \PP_{\overline{\kod{dv}}}(\semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}).$$

By Definition <ref>, there exists $\mu'$ such that $\mu = \mu'_{\overline{\kod{dv}}}$ and

$$\mu' \in \semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}.$$

By Lemma <ref>, it holds $dom(\mu') = \kod{var}(\kod{qpat})$.
Therefore, by Definition <ref>, it holds
$$dom(\mu) = dom(\mu') \cap \overline{\kod{dv}} = \kod{var}(\kod{qpat}) \cap \overline{\kod{dv}},$$

$$\overline{\kod{rv}} = \kod{var}(\kod{qpat}) \cap \overline{\kod{dv}}.$$

§.§ Containment, subsumption, equivalence and satisfiability

Given two queries $\kod{Q}_1$ and $\kod{Q}_2$, $\kod{Q}_1$ is contained in $\kod{Q}_2$,
if for every  dataset $\dataq$, it holds $\semdq{\kod{Q}_1} \subseteq \semdq{\kod{Q}_2}$.

If $\kod{Q}_1$ is contained in $\kod{Q}_2$, then $\kod{Q}_2$ is called a super-query, and $\kod{Q}_1$ is called a sub-query. The query containment problem is a problem to determine whether $\kod{Q}_1$ is contained in $\kod{Q}_2$.
The problem is undecidable if query $\kod{Q}_2$ contains projections [Pichler and Skritek, 2014].
Therefore, we assume that all variables in the graph pattern of $\kod{Q}_2$ appear in the select clause.

Given two queries $\kod{Q}_1$ and $\kod{Q}_2$,
$\kod{Q}_1$ is subsumed by $\kod{Q}_2$,
if for every  dataset $\dataq$, for each mapping $\mu$ from $\semdq{\kod{Q}_1}$ there exists an extension $\mu'$ ($\mu' \succeq \mu$), such that $\mu'$ belongs to $\semdq{\kod{Q}_2}$.

Subsumption relation can be considered as a weaker form of containment [Pérez et al., 2009, Letelier et al., 2013, Arenas and Perez, 2011, Pichler and Skritek, 2014], as $\kod{Q}_1 \sqsubseteq \kod{Q}_2$ implies $\kod{Q}_1 \dot{\sqsubseteq} \kod{Q}_2$ (a proof uses Definition <ref> and an extension $\mu' = \mu$). The same terminology concerning $\kod{Q}_2$ as a super-query and $\kod{Q}_1$ as a sub-query is used when subsumption relation is considered instead of query containment relation.
The subsumption problem is a problem to determine whether $\kod{Q}_1$ is subsumed in $\kod{Q}_2$. Unlike query containment problem, query subsumption problem is not undecidable when query $\kod{Q}_2$ contains projections [Pichler and Skritek, 2014].

Given two queries $\kod{Q}_1$ and $\kod{Q}_2$,
$\kod{Q}_1$ is equivalent to $\kod{Q}_2$,
if for every  dataset $\dataq$, it holds $\semdq{\kod{Q}_1} = \semdq{\kod{Q}_2}$.

Query equivalence corresponds to satisfying containment relation in both directions.
But, if two queries satisfy the subsumption relation in both directions, they do not have to be equivalent (if either of them contains  or projection operator) [Pichler and Skritek, 2014].

Query $\kod{Q}$ is satisfiable if there exist a dataset $\dataq$ and a mapping $\mu$ such that $\mu \in \semdq{\kod{Q}}$.
Otherwise, Q is unsatisfiable.

For each query it holds that an unsatisfiable query is its sub-query.

§ MODELING THE QC PROBLEM OF CONJUNCTIVE QUERIES

In this section, we model a subset of  queries presented by the grammar in Figure <ref>, i.e. conjunctive queries [Chandra and Merlin, 1977, Chaudhuri and Vardi, 1993] extended by  negation, the operator graph and built-in functions, while the rest of language constructs are covered in Section <ref>.
We translate such queries into  formulas (Section <ref>) that are used for reasoning about query relations (Section <ref>).
We have already presented the modeling in [Spasić and Vujošević Janičić, 2022], while here, we reshow the definitions that are necessary to prove the correctness of our reduction.

§.§ Theory signature

The theory signature used for reasoning about queries $\kod{Q}_1$ and $\kod{Q}_2$, denoted by $\mathcal{L}$, is given in Definition <ref> (Figure <ref>) as a tuple
$$(\mathcal{C} \cup \fun, ~~ \mathcal{P} \cup \{ \ppp, \pp \}, ~~ ar).$$

For example, for queries presented in Figure <ref>, the set $\mathcal{C}$ contains only constants $LosAngeles_l$ (corresponding to the literal "Los Angeles") and $a_i$, $Album_i$, $artist_i$, $SoloArtist_i$, $hometown_i$ and $name_i$ (corresponding to the s a, :Album, :artist, :SoloArtist, :hometown and :name).
For the same pair of queries, the set $\fun$ is an empty set, while the set $\mathcal{P}$ contains only the equality predicate symbol. Considering the grammar presented in Figure <ref>, the set $\fun$ can contain the symbol $\textit{datatype}$, corresponding to the  function datatype while the set $\mathcal{P}$ can also have the symbol isliteral, corresponding to the  predicate isliteral, in cases where these built-in functions are used within the relevant queries.
Predicate symbols $\ppp$ and $\pp$ model belonging of a triple to the graphs of an  dataset $\dataq$, e.g.:

* $\ppp(x_v,a_i,Album_i)$ models that the triple $\kod{?x a :Album}$ belongs to the default graph of an  dataset $\dataq$,

* $\pp(x_v,a_i,Album_i, g_i)$ models that the triple $\kod{?x a :Album}$ belongs to the named graph specified by the  g of an  dataset $\dataq$, where $g_i$ is a corresponding constant to the  g.

A set of variables $\vars$ corresponds to the variables and blank nodes from the  queries $\kod{Q}_1$ and $\kod{Q}_2$. For the query pair presented in Figure <ref>, $\vars$ is equal to a set containing variables $x_v$, $y_v$, $z_v$ and $w_v$, corresponding to the  variables ?x, ?y, ?z and ?w, respectively.

§.§ Transforming Conjunctive Queries Into Formulas

The following auxiliary definition extends a function to a subset of its domain.

Let ${A}$ be a set of elements, and $f$ a function such that ${A} \subseteq dom(f)$.
Function $f$ over set ${A}$, in notation $f({A})$, denotes the set $\{ f(e) \;|\; {e} \in {A} \}$.

A translation of the  queries into the corresponding  formulas is performed by function $\sigma$ recursively,  construct by construct, using the auxiliary functions $\sigvibl$ and $\context$.
Their definitions are given in Figure <ref>.

Function $\sigvibl$ assigns a  constant to a   or a literal, and a  variable to a  variable or a blank node.

Function $\context$ maps an active graph to the set of corresponding graph  constants.[The function $\context$ is not defined on the default graph of the  dataset $\dataq$ as there is no  associated to it.]
Note that, according to the semantics, the active graph $\kod{\gr}$ can be the default graph or a named graph of a query dataset $\kod{\ag}$.
If $\kod{\gr}$ is the default graph, it can be equal to the default graph of $\dataq$, an  merge of one or more graphs, or an empty graph $\kod{\gr}_{\varnothing}$.
These possibilities correspond to the cases present in Definition <ref>.

Definition <ref> presents a translation of the  terms, expressions, conditions and graph patterns into the corresponding  formulas from the signature $\mathcal{L}$.
The full notation of the function $\sigma$ includes an active graph $\kod{\gr}$ used for matching the pattern within the query. For readability reasons, the active graph is denoted in superscript, i.e. $\sigma^{\kod{\gr}}$, and is omitted when it is obvious from the context and for terms, expressions and conditions as these to do not depend on the active graph. Note that the active graph can be changed only in case of the operator graph.

Definition <ref> specifies formula $\Phi(\overline{v})$ corresponding to a query Q, with a graph pattern qpat specifying a query dataset $\ag$.
As a parameter, this formula has a set $\overline{v}$ of some variables from $\vars$, while $\overline{ov}$ denote other free variables in the formula $\sigma(\kod{qpat})$. If distinguished variables are used as a parameter $\overline{v}$, then, intuitively, variables $\overline{ov}$ within formula $\Phi(\overline{dv})$ denote variables form $\mathcal{V}$ that correspond to variables from V that are used in the query $\kod{Q}$ but that are not selected.

$$(\funs, \preds, ar)$$

* $\funs \Eqdef \mathcal{C} \cup \fun$ is a set of function symbols, where:

* $\mathcal{C}$ is a set of constants (function symbols with arity 0) corresponding to the literals and s that appear in the queries, and a constant $\err$, corresponding to $\error$ in .

* $\fun$ is a set of function symbols corresponding to the built-in  functions used in the queries $\kod{Q}_1$ and $\kod{Q}_2$.

* $\preds \Eqdef \mathcal{P} \; \cup \; \{ \ppp, \pp \}  $ is a set of predicate symbols, where:

* $\mathcal{P}$ is a set which contains the equality predicate symbol ($=$) and other predicate symbols corresponding to the boolean  functions used in $\kod{Q}_1$ and $\kod{Q}_2$.

* $\ppp$ and $\pp$ are predicate symbols that intuitively model belonging of a triple
to the default graph of an  dataset $\dataq$, or to a named graph specified by an , respectively.

* $ar$ is an arity function:

$$ar(\alpha) \Eqdef
\begin{cases}
0\,, ~~\text{if } \alpha \in \mathcal{C},\\
1\,, ~~\text{if } \alpha \in \fun \text{ and } \alpha \text{ is } datatype,\\
1\,, ~~\text{if } \alpha \in \mathcal{P} \text{ and } \alpha \text{ is } isliteral,\\
2\,, ~~\text{if } \alpha \in \mathcal{P} \text{ and } \alpha \text{ is } =,\\
3\,, ~~\text{if } \alpha \in \preds \text{ and } \alpha \text{ is } \ppp,\\
4\,, ~~\text{if } \alpha \in \preds \text{ and } \alpha \text{ is } \pp.
\end{cases}$$

$$\sigvibl(\kod{t}) \Eqdef
\begin{cases}
c \ (c \in \mathcal{C})\,, &\text{if } \kod{t} = \kod{c} \text{ and } \kod{c} \in \kod{IL},\\
v \ (v \in \vars)\,, &\text{if } \kod{t} = \kod{v} \text{ and } \kod{v} \in \kod{VB},\\
\err\,, &\text{if } \kod{t} = \error .
\end{cases}$$

\begin{align*}
\context(\kod{\gr}) \Eqdef  \begin{cases}
\begin{lrdcases}
\sigvibl(\{ \kod{i}_{k_1}, \cdots, \kod{i}_{k_m} \}), & \kod{G} = merge(\kod{\gr}_{k_1}, ..., \kod{\gr}_{k_m}) \text{ and} \\ & gr_{\dataq}(\kod{i}_{k_j})=\kod{\gr}_{k_j}, j \in \{1, \cdots, m\}\\
\varnothing, & \kod{\gr} = \kod{\gr}_{\varnothing}\\
\end{lrdcases}, & \begin{tabular}{l} \text{if }  \kod{\gr} \text{ is the default graph} \\ \text{of the query dataset } \ag \end{tabular}\\
\\[-8pt]
\begin{lrdcases}
~ \\
\sigvibl(\{ \kod{i} \}), \hspace*{12mm} & gr_{\dataq}(\kod{i})=\kod{\gr} \hspace*{22mm} \\
\end{lrdcases}, & \begin{tabular}{l} \text{if } \kod{\gr} \text{ is a named graph} \\ \text{of the query dataset } \ag \end{tabular}
\end{cases}
\end{align*}

\begin{align*}
& \text{\textbf{Term} \kod{t}} \\
\sigma(\kod{t}) & \Eqdef \sigvibl(\kod{t}), & \kod{t} \in \vibl{}
\end{align*}

\begin{align*}
& \text{\textbf{Expression} \kod{E}} \\
\sigma(\kod{E}) & \Eqdef \begin{cases}
\sigvibl(\kod{E}_1), & \text{if } \kod{E} \text{ is } \kod{E}_1 \text{ and } \kod{E}_1 \in \kod{VILe} \\
datatype(\sigma(\kod{E}_1)), & \text{if } \kod{E} \text{ is } \kod{datatype(E}_1\kod{)}
\end{cases}
\end{align*}

\begin{align*}
& \text{\textbf{Condition} \kod{R}} \\
\sigma(\kod{R}) & \Eqdef \begin{cases}
\sigma(\kod{E}_1) = \sigma(\kod{E}_2), & \text{if } \kod{R} \text{ is } \kod{E}_1 = \kod{E}_2\\
\neg\;\sigma(\kod{R}_1), & \text{if } \kod{R} \text{ is } \kod{!R}_1 \\
\sigma(\kod{R}_1) \wedge \sigma(\kod{R}_2), & \text{if } \kod{R} \text{ is } \kod{R}_1 \;\kod{\&\&}\; \kod{R}_2 \\
\sigma(\kod{R}_1) \vee \sigma(\kod{R}_2), & \text{if } \kod{R} \text{ is } \kod{R}_1 \;\kod{||}\; \kod{R}_2 \\
\sigma(\kod{R}_1), & \text{if } \kod{R} \text{ is } \kod{(R}_1\kod{)} \\
isliteral(\sigma(\kod{E}_1)), & \text{if } \kod{R} \text{ is } \kod{isliteral(E}_1\kod{)}
\end{cases}\\
\end{align*}

\begin{align*}
& \text{\textbf{Pattern} \kod{\pat}} \\
\sigma^{\kod{\gr}}(\kod{\pat}) & \Eqdef
\begin{cases}
\begin{lrdcases}
\ppp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})), &
\kod{\gr} \notin dom(\context)\\
\underset{i_j \in \context(\kod{\gr})} \bigvee \pp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}), i_j), & \kod{\gr} \in dom(\context), \context(\kod{\gr}) \not= \varnothing \\
\bot , & \kod{\gr} \in dom(\context), \context(\kod{\gr}) = \varnothing \\
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\text{\codebox{$\kod{s p o}$}}\\
\\[-8pt]
\begin{lrdcases}
\sigma^{\kod{\gr}}(\kod{\pat}_1) \wedge \sigma^{\kod{\gr}}(\kod{\pat}_2) & \hspace*{40mm}
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\kod{\pat}_1 \; . \; \kod{\pat}_2 \\
\\[-8pt]
\begin{lrdcases}
\sigma^{\kod{\gr}}(\kod{\pat}_1) \wedge \sigma(\kod{R}_1) & \hspace*{42.3mm}
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\kod{\pat}_1 \kod{\;filter R}_1\\
\\[-8pt]
\begin{lrdcases}
\sigma^{\kod{\gr}}(\kod{\pat}_1) & \hspace*{51.3mm}
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\{\kod{\pat}_1\}\\
\\[-8pt]
\begin{lrdcases}
\sigma^{\kod{\gr}}(\kod{\pat}_1), & \kod{var}(\kod{\pat}_1) \cap \kod{var}(\kod{\pat}_2) = \varnothing\\
\sigma^{\kod{\gr}}(\kod{\pat}_1) \wedge \big( \forall \overline{x} \ \neg \sigma^{\kod{\gr}}(\kod{\pat}_2) \big) , & \kod{var}(\kod{\pat}_1) \cap \kod{var}(\kod{\pat}_2) \not= \varnothing \hspace*{3.2mm}
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\kod{\pat}_1 \kod{ minus } \kod{\pat}_2\\
\\[-8pt]
\begin{lrdcases}
\sigma^{\kod{\gr}}(\kod{\pat}_1) \wedge \big( \forall \overline{x} \ \neg \sigma^{\kod{\gr}}(\kod{\pat}_2) \big) & \hspace*{32mm}
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\kod{\pat}_1 \kod{ diff } \kod{\pat}_2, \\
\\[-8pt]
\begin{lrdcases}
\underset{i \in \agfn}\bigvee \Big( \sigma^{gr_{\,\ag}(\siginv(i))}(\kod{\pat}_1) \wedge \sigma(\kod{x}) = i \Big), & \agfn \not= \varnothing \\
\bot, & \agfn = \varnothing \hspace*{11mm}\\
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\kod{graph x \{\pat}_1 \kod{\}} \\
\\[-8pt]
\begin{lrdcases}
\sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1), &  \sigma(\kod{i}) \in \agfn\\
\bot, & \sigma(\kod{i}) \notin \agfn \hspace*{33.8mm}
\end{lrdcases}, \hspace*{-2mm} & \text{if } \kod{\pat} \text{ is }\kod{graph i \{\pat}_1 \kod{\}} \\
\end{cases}
\end{align*}

qpat - a graph pattern within the query Q;
- a query dataset;
$\overline{ov}$ - $var(\sigma(\kod{qpat})) \setminus \overline{v}$

$$\Phi(\overline{v}) \Eqdef \exists \overline{ov}  \ \sigma^{\mathit{df}({\ag})}(\kod{qpat})$$

Definitions taken from [Spasić and Vujošević Janičić, 2022] are given here in a short form: theory signature $\mathcal{L}$ corresponding to the queries $\kod{Q}_1$ and $\kod{Q}_2$, functions $\sigvibl$, $\context$ and $\sigma$ for transforming queries into formulas and formula $\Phi(\overline{x})$ corresponding to the query Q.
$\kod{E}_1$ and $\kod{E}_2$ are used for expressions, $\kod{R}_1$ and $\kod{R}_2$ for conditions, s, p and o for subjects, predicates and objects, respectively ($\kod{s} \in \kod{VIB}, \kod{p} \in \kod{VI}, \kod{o} \in \vibl{}$), $\kod{\pat}_1$ and $\kod{\pat}_2$ for graph patterns, x for a  variable, i for an , while $\agfn$ is a set containing all graph  constants corresponding to the named graphs of the query dataset $\ag$. $\overline{x}$ stands for $var(\sigma(\kod{\pat}_2)) \setminus var(\sigma(\kod{\pat}_1))$.

\begin{align*}
\hspace*{-1mm}
\exists \, z_v \, \exists \,  w_v ~ \Big(
& \ppp(x_v,a_i,Album_i) \; \wedge \; \ppp(x_v,artist_i,y_v) \; \wedge \\
&\ppp(y_v,a_i,SoloArtist_i) \; \wedge \; \ppp(y_v,hometown_i,z_v) \; \wedge\\
&\ppp(z_v,name_i,w_v) \; \wedge \; w_v = LosAngeles_l ~ \Big)
\end{align*}

Formula $\Phi(x_v, y_v)$ corresponding to the upper query given in Figure <ref>.
For readability, each , literal and variable is denoted by a corresponding subscript $i$, $l$ and $v$, respectively.

Let $\Phi$ be a  formula.
$var(\Phi)$ denotes a set of free variables appearing in the formula $\Phi$.

The following four lemmas connect functions $\kod{var}$, $\sigma$ and $var$.

Let $\kod{t}$ be a term.

$var(\sigma(\kod{t})) = \sigma(\kod{var}(\kod{t}))$.

The specified equality is proved by induction over a term $\kod{t}$.

* t  is  $\kod{c}, \kod{c} \in \kod{IL}$

\begin{align*}
&\hspace*{20mm} var(\sigma(\kod{c})) \hspace*{-14mm} &  = \ \\
&\text{(by Def \ref{def:sigma})} & = \ & var(\sigma_{\kod{t}} (\kod{c})) \\
&\text{(by Def \ref{def:sigmat})} & = \ & var(c) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & \varnothing\\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\varnothing)\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{c}))
\end{align*}

* t  is  $\kod{v}, \kod{v} \in \kod{VB}$

\begin{align*}
&\hspace*{20mm} var(\sigma(\kod{v})) \hspace*{-14mm} & = \ \\
&\text{(by Def \ref{def:sigma})} & = \ & var(\sigma_{\kod{t}} (\kod{v})) \\
&\text{(by Def \ref{def:sigmat})} & = \ & var(v) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & \{ v \}\\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\{ \kod{v} \})\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{v}))
\end{align*}

Let $\kod{E}$ be an expression.

$var(\sigma(\kod{E})) = \sigma(\kod{var}(\kod{E}))$.

The specified equality is proved by induction over an expression $\kod{E}$.

* E is $\kod{t}$

\begin{align*}
& \hspace*{15mm} var(\sigma(\kod{t})) \hspace*{-9mm} & = \ \\
&\text{(by Lemma \ref{thm:dom_mu_nuT})}  & = \  & \sigma(\kod{var}(\kod{t}))
\end{align*}

* E  is  $\kod{datatype(E}_1\kod{)}$

\begin{align*}
&var(\sigma(\kod{datatype(E}_1\kod{)})) \hspace*{-20mm}  & = \ \\
&\text{(by Def \ref{def:sigma}} ) & = \ & var(datatype(\sigma(\kod{E}_1))) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & var(\sigma(\kod{E}_1)) \\
&\text{(by induc.hyp.)} & = \ & \sigma(\kod{var}(\kod{E}_1)) \\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{datatype(E}_1\kod{)}))
\end{align*}

Let $\kod{R}$ be a condition.

$var(\sigma(\kod{R})) = \sigma(\kod{var}(\kod{R}))$.

The specified equality is proved by induction over a condition $\kod{R}$.

* R  is  $\kod{E}_1$ = $\kod{E}_2$

\begin{align*}
& \hspace*{5mm} var(\sigma(\kod{E}_1 = \kod{E}_2)) \hspace*{-3mm}& = \ \\
&\text{(by Def \ref{def:sigma}} ) & = \ & var(\sigma(\kod{E}_1) = \sigma(\kod{E}_2)) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & var(\sigma(\kod{E}_1)) \cup var(\sigma(\kod{E}_2)) \\
&\text{(by Lemma \ref{thm:dom_mu_nuE})} & = \ & \sigma(\kod{var}(\kod{E}_1)) \cup \sigma(\kod{var}(\kod{E}_2)) \\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\kod{var}(\kod{E}_1) \cup \kod{var}(\kod{E}_2)) \\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{E}_1 = \kod{E}_2))
\end{align*}

* $\kod{R} \text{ is } \kod{!R}_1$

\begin{align*}
& \hspace*{15mm} var(\sigma(\kod{!R}_1)) \hspace*{-15mm}& = \  \\
&\text{(by Def \ref{def:sigma}} ) & = \ & var(\neg \sigma(\kod{R}_1)) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & var(\sigma(\kod{R}_1)) \\
&\text{(by induc.hyp.)} & = \ & \sigma(\kod{var}(\kod{R}_1)) \\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{!R}_1))
\end{align*}

* $\kod{R} \text{ is } \kod{R}_1 \kod{\&\&} \kod{R}_2$

\begin{align*}
& \hspace*{2mm} var(\sigma(\kod{R}_1 \kod{\&\&} \kod{R}_2)) \hspace*{-10mm} & = \  \\
&\text{(by Def \ref{def:sigma}} ) & = \ & var(\sigma(\kod{R}_1) \wedge \sigma(\kod{R}_2)) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & var(\sigma(\kod{R}_1)) \cup var(\sigma(\kod{R}_2))\\
&\text{(by induc.hyp.)} & = \ & \sigma(\kod{var}(\kod{R}_1)) \cup \sigma(\kod{var}(\kod{R}_2))\\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\kod{var}(\kod{R}_1) \cup \kod{var}(\kod{R}_2))\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{R}_1 \kod{\&\&} \kod{R}_2))
\end{align*}

* $\kod{R} \text{ is } \kod{R}_1 \kod{||} \kod{R}_2$

Proof is analogous to the previous case.

* $\kod{R} \text{ is } \kod{(R}_1\kod{)}$

Proof is analogous to the case $\kod{R} \text{ is } \kod{!R}_1$.

* R  is  $\kod{isliteral(E)}$

\begin{align*}
&~~~var(\sigma(\kod{isliteral(E)})) = \hspace*{-28mm}&  \\
&\text{(by Def \ref{def:sigma}} ) & = \ & var(isliteral(\sigma(\kod{E}))) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & var(\sigma(\kod{E})) \\
&\text{(by induc.hyp.)} & = \ & \sigma(\kod{var}(\kod{E})) \\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{isliteral(E)}))
\end{align*}

In the following text, $\exists \overline{a}$ abbreviates $\exists  a_1 ... \exists a_n$, and $\forall \overline{a}$ abbreviates $\forall a_1 ... \forall a_n$, when $n$ is clear from the context.

Let $\kod{\pat}$ be a graph pattern. Then, if all active graphs that are used for matching $\kod{\pat}$ are nonempty, it holds:

$var(\sigma(\kod{\pat})) = \sigma(\kod{var}(\kod{\pat}))$.

The specified equality is proved by induction over a graph pattern $\kod{\pat}$.

*  is , where  is s p o

Let $\kod{\gr}$ be an active graph for matching $\kod{\tpat{}}$.

If $\kod{\gr} \notin dom(cx)$:

\begin{align*}
& var(\sigma^{\kod{\gr}}(\kod{s\,p\,o})) \hspace*{-20mm}&  = \ \\
&\text{(by Def \ref{def:sigma}} ) & = \ & var( \ppp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}))) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & \{ \sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})\} \cap \vars \\
&\text{(by Def \ref{def:sigmat})} & = \ & \{ \sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})\} \cap \sigvibl(\kod{VB}) \\
&\text{(by Def \ref{def:sigma})} & = \ & \{ \sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})\} \cap \sigma(\kod{VB}) \\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\{ \kod{s}, \kod{p}, \kod{o}\} \cap \kod{VB}) \\
&\text{(by Def of } \cup) & = \ & \sigma( (\{ \kod{s} \} \cup  \{ \kod{p} \} \cup \{ \kod{o} \}) \cap \kod{VB}) \\
&\text{(by dist. of } \cap  & = \ & \sigma( (\{ \kod{s} \} \cap \kod{VB}) \; \cup \\
&\text{ over } \cup\text{)}&& (\{ \kod{p} \} \cap \kod{VB}) \cup (\{ \kod{o} \} \cap \kod{VB})) \\
&\text{(by Def \ref{def:var})}  & = \ & \sigma(\kod{var}(\kod{s}) \cup  \kod{var}(\kod{p}) \cup  \kod{var}(\kod{o})  ))\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{s p o}))\\
\end{align*}

If $\kod{\gr} \in dom(cx)$, as graph  is a nonempty graph, by Definition <ref>, it holds $cx(\kod{\gr}) \not= \varnothing$.

\begin{align*}
& var(\sigma^{\kod{\gr}}(\kod{s p o})) \hspace*{-28mm}&  \\
&\text{(by Def \ref{def:sigma}} ) & = \ & var( \hspace*{-3mm} \underset{i_j \in \context(\kod{\gr})} \bigvee \hspace*{-3mm} \pp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}), i_j)) \\
&\text{(by Def \ref{def:var_sigma})} & = \ & \hspace*{-3mm} \underset{i_j \in \context(\kod{\gr})} \bigcup \hspace*{-2mm} var( \pp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}), i_j)) \\
&\text{(by Def \ref{def:context})} & = \ & \{ \sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})\} \cap \vars \\
&\text{(by Def \ref{def:sigmat})} & = \ & \{ \sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})\} \cap \sigvibl(\kod{VB}) \\
&\text{(by Def \ref{def:sigma})} & = \ & \{ \sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})\} \cap \sigma(\kod{VB}) \\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\{ \kod{s}, \kod{p}, \kod{o}\} \cap \kod{VB}) \\
&\text{(by Def of } \cup) & = \ & \sigma( (\{ \kod{s} \} \cup  \{ \kod{p} \} \cup \{ \kod{o} \}) \cap \kod{VB}) \\
&\text{(by dist. of } \cap  & = \ & \sigma( (\{ \kod{s} \} \cap \kod{VB}) \; \cup \\
&\text{ over } \cup\text{)} && (\{ \kod{p} \} \cap \kod{VB}) \cup (\{ \kod{o} \} \cap \kod{VB})) \\
&\text{(by Def \ref{def:var})}  & = \ & \sigma(\kod{var}(\kod{s}) \cup  \kod{var}(\kod{p}) \cup  \kod{var}(\kod{o})  ))\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{s p o}))
\end{align*}

* $\kod{\pat}$  is $\kod{\pat}_1 . \kod{\pat}_2$

\begin{align*}
& var(\sigma(\kod{\pat}_1 . \kod{\pat}_2)) \hspace*{-4mm} & = \  \\
&\text{(by Def \ref{def:sigma}} ) &  = \ & var( \sigma(\kod{\pat}_1) \wedge \sigma(\kod{\pat}_1))\\
&\text{(by Def \ref{def:var_sigma})} & = \ & var( \sigma(\kod{\pat}_1)) \cup var(\sigma(\kod{\pat}_1)) \\
&\text{(by induc.hyp.)} \hspace*{-3mm}& = \ & \sigma(\kod{var}(\kod{\pat}_1)) \cup \sigma(\kod{var}(\kod{\pat}_1)) \\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\kod{var}(\kod{\pat}_1) \cup \kod{var}(\kod{\pat}_2)) \\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{\pat}_1 . \kod{\pat}_2))
\end{align*}

* $\kod{\pat}$ is $\kod{\pat}_1 \kod{ filter } \kod{R}$

\begin{align*}
& var(\sigma(\kod{\pat}_1 \kod{ filter } \kod{R})) \ =  \hspace*{-15mm} &  \\
&\text{(by Def \ref{def:sigma}} ) &  = \ & var( \sigma(\kod{\pat}_1) \wedge \sigma(\kod{R}))\\
&\text{(by Def \ref{def:var_sigma})} & = \ & var( \sigma(\kod{\pat}_1)) \cup var(\sigma(\kod{R})) \\
&\text{(by induc.hyp.)} \hspace*{-3mm} & = \ & \sigma(\kod{var}(\kod{\pat}_1)) \cup \kod{var}(\sigma(\kod{R})) \\
&\text{(by Lemma \ref{thm:dom_mu_nuR})} & = \ & \sigma(\kod{var}(\kod{\pat}_1)) \cup \sigma(\kod{var}(\kod{R})) \\
&\text{(by Def \ref{def:function_over_sets})} & = \ & \sigma(\kod{var}(\kod{\pat}_1) \cup \kod{var}(\kod{R})) \\
&\text{(as } \kod{var}(\kod{R}) \hspace*{-1mm}\subseteq\hspace*{-1mm} \kod{var}(\kod{\pat}_1) \text{)} \hspace*{-3mm} & = \ & \sigma(\kod{var}(\kod{\pat}_1)) \\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{\pat}_1 \kod{ filter } \kod{R}))
\end{align*}

* $\kod{\pat}$ is $\kod{\{\pat}_1\kod{\}}$

\begin{align*}
& \hspace*{8mm} var(\sigma(\kod{\{\pat}_1\kod{\}}) \hspace*{-8mm} & = \  \\
&\text{(by Def \ref{def:sigma}} ) &  = \ & var( \sigma(\kod{\pat}_1))\\
&\text{(by induc.hyp.)} \hspace*{-3mm} & = \ & \sigma(\kod{var}(\kod{\pat}_1)) \\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{\{\pat}_1\kod{\}}))
\end{align*}

* $\kod{\pat}$ is $\kod{\pat}_1 \; \kod{diff} \; \kod{\pat}_2$

\begin{align*}
& var(\sigma(\kod{\pat}_1 \; \kod{diff} \; \kod{\pat}_2))  = \hspace*{-30mm} \\
&\text{(by Def \ref{def:sigma}} ) &  = \ & var(\sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2))\\
&\text{(by Def \ref{def:var_sigma}} ) &  = \ & var(\sigma(\kod{\pat}_1)) \\
&\text{(by induc.hyp.)} &  = \ & \sigma(\kod{var}(\kod{\pat}_1))\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{\pat}_1 \; \kod{diff} \; \kod{\pat}_2))
\end{align*}

* $\kod{\pat}$ is $\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2$

If $\kod{var}(\kod{\pat}_1) \cap \kod{var}(\kod{\pat}_2) = \varnothing$ then:

\begin{align*}
& var(\sigma(\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2))  = \hspace*{-30mm} \\
&\text{(by Def \ref{def:sigma}} ) &  = \ & var(\sigma(\kod{\pat}_1))\\
&\text{(by induc.hyp.)} &  = \ & \sigma(\kod{var}(\kod{\pat}_1))\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2))
\end{align*}

\begin{align*}
& var(\sigma(\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2))  = \hspace*{-30mm} \\
&\text{(by Def \ref{def:sigma}} ) &  = \ & var(\sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2))\\
&\text{(by Def \ref{def:var_sigma}} ) &  = \ & var(\sigma(\kod{\pat}_1)) \\
&\text{(by induc.hyp.)} &  = \ & \sigma(\kod{var}(\kod{\pat}_1))\\
&\text{(by Def \ref{def:var})} & = \ & \sigma(\kod{var}(\kod{\pat}_1 \; \kod{minus} \; \kod{\pat}_2))
\end{align*}

* $\kod{\pat}$ is $\kod{graph x} \ \{ \kod{\pat}_1 \}$

If $\agfn = \varnothing$, there is no active graph for matching $\kod{\pat}_1$. Then, by Definition <ref>, this case is equivalent to a case when the active graph is empty, which does not correspond to the assumption of this lemma. Therefore, we can assume that $\agfn \not= \varnothing$.

From $\agfn \not= \varnothing$, according to Definition <ref>, it holds that for all $i \in \agfn$ graph $gr_{\,\ag}(\siginv(i))$ is a nonempty one.

\begin{align*}
&var(\sigma(\kod{graph x} \  \{ \kod{\pat}_1 \})) = \hspace*{-30mm}&  \\
&\text{(by Def \ref{def:sigma}} ) \hspace*{-2mm}&  = & var(\underset{i \in \agfn}\bigvee ( \sigma^{gr_{\,\ag}(\siginv(i))}(\kod{\pat}_1) \\
&&& \hspace*{7mm} \wedge \sigma(\kod{x}) = i ))\\
&\text{(by Def \ref{def:var_sigma}} ) &  = & \underset{i \in \agfn}\bigcup ( var(\sigma^{gr_{\,\ag}(\siginv(i))}(\kod{\pat}_1)) \\
&&& \hspace*{7mm} \cup var(\sigma(\kod{x}) = i ))\\
&\text{(by induc.hyp.)} \hspace*{-5mm}&  = & \underset{i \in \agfn}\bigcup ( \sigma(\kod{var}(\kod{\pat}_1))\\
&&& \hspace*{7mm} \cup var(\sigma(\kod{x}) = i ))\\
&\text{(as $\agfn \cap \vars$ is $\varnothing$)} \hspace*{-2mm}& = & \sigma(\kod{var}(\kod{\pat}_1)) \cup \{ \sigma(  \kod{x})\} \\
&\text{(by Def \ref{def:function_over_sets})} & = & \sigma(\kod{var}(\kod{\pat}_1) \cup \{ \kod{x} \}) \\
&\text{(by Def \ref{def:var})} \hspace*{-2mm} & = & \sigma(\kod{var}(\kod{graph x} \  \{ \kod{\pat}_1 \}))
\end{align*}

* $\kod{\pat}$ is $\kod{graph i} \; \{ \kod{\pat}_1 \}$

If $\sigma(\kod{i}) \notin \agfn$, by Definition <ref>, it holds $\kod{i} \notin names(\ag)$, i.e. by Definition <ref> $gr_\kod{\,D}(\kod{i}) = \varnothing$. Then, according to Definition <ref>, an active graph that is used for matching $\kod{\pat}_1$ is empty, which does not correspond to the assumption of this lemma. Therefore, we can assume that $\sigma(\kod{i}) \in \agfn$.

From $\sigma(\kod{i}) \in \agfn$, according to Definition <ref>, the graph $gr_{\,\ag}(\kod{i})$ is a nonempty graph.

\begin{align*}
&var(\sigma(\kod{graph i} \; \{ \kod{\pat}_1 \})) =  \hspace*{-35mm}&  \\
&\text{(by Def \ref{def:sigma}} )  &  = & var( \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1))\\
&\text{(by induc.hyp.)}  &  =  & \sigma(\kod{var}(\kod{\pat}_1)) \\
&\text{(by Def \ref{def:var})}  & = & \sigma(\kod{var}(\kod{graph i} \; \{ \kod{\pat}_1 \}))
\end{align*}

Let $\overline{rv}$ be a set of variables from $\vars$ that correspond to the relevant variables of a query Q and let $\Phi(\overline{rv})$ be a formula that corresponds to Q.

$var(\Phi(\overline{rv})) = \overline{rv}$.

Let qpat and $\ag$ be a query pattern and a query dataset of the query $\kod{Q}$, respectively.
Let $\overline{ov}$ denote $var(\sigma(\kod{qpat})) \setminus \overline{rv}$.

\begin{align*}
& \hspace*{12mm} var(\Phi(\overline{rv})) \hspace*{-4mm} &=\; \\
&\text{(by Def \ref{def:phi})} &=\;&  var(\exists \overline{ov} \  \sigma^{\mathit{df}(\ag)}(\kod{qpat})) \\
& \text{(By Def \ref{def:var_sigma})} &=\;&  var(\sigma^{\mathit{df}(\ag)}(\kod{qpat})) \setminus \overline{ov}\\
&\text{(by Def \ref{def:phi})} &=\;& var(\sigma^{\mathit{df}(\ag)}(\kod{qpat})) \setminus\\
&&& (var(\sigma^{\mathit{df}(\ag)}(\kod{qpat})) \setminus \overline{rv}) \\
&&=\;& var(\sigma^{\mathit{df}(\ag)}(\kod{qpat})) \cap \overline{rv} \\
& \text{(as } \sigma(\overline{\kod{rv}}) = \overline{rv} \text{)} &=\;&  var(\sigma^{\mathit{df}(\ag)}(\kod{qpat})) \cap \sigma(\overline{\kod{rv}})\\
&\text{(by Lemma \ref{thm:dom_mu_nu1})} &=\;&  \sigma(var(\kod{qpat})) \cap \sigma(\overline{\kod{rv}})\\
&\text{(by Def \ref{def:function_over_sets})} &=\;& \sigma(var(\kod{qpat}) \cap \overline{\kod{rv}})\\
&\text{(by Lemma \ref{thm:query_domain})} &=\;& \sigma(\overline{\kod{rv}})\\
& \text{(as } \sigma(\overline{\kod{rv}}) = \overline{rv} \text{)} &=\;& \overline{rv}
\end{align*}

§.§ Modeling the Containment Relation

Modeling the query containment problem and subsumption problem include defining formulas $\Theta$ and $\Psi$, and relation $\seleq$, for containment, and relation $\dot{\seleq}$ for subsumption. These are defined in [Spasić and Vujošević Janičić, 2022] and given in a short form in Figure <ref>.

Definition <ref> specifies formula $\Theta$, based on a query $\kod{Q}_1$ (a candidate for sub-query), where $\overline{rv_1}$ denote variables from $\vars$ that correspond to the relevant variables of $\kod{Q}_1$, while $\Phi_1(\overline{rv_1})$ is a formula that corresponds to $\kod{Q}_1$ according to Definition <ref>.

Definition <ref> specifies formula $\Psi$, based of queries $\kod{Q}_1$ and $\kod{Q}_2$, where $\overline{rv_1}$ denote variables from $\vars$ that correspond to the relevant variables of $\kod{Q}_1$, while $\Phi_1(\overline{rv_1})$ and $\Phi_2(\overline{rv_1})$ are formulas that correspond to $\kod{Q}_1$ and $\kod{Q}_2$, respectively according to Definition <ref>.

$$\neg \big(\exists \overline{rv_1} \ \Phi_1(\overline{rv_1})\big)$$

$$\forall \overline{rv_1} \ \big( \Phi_1(\overline{rv_1}) \Rightarrow \Phi_2(\overline{rv_1}) )$$

$$\kod{Q}_1 \seleq \kod{Q}_2 \text{~~~iff~~~} \overline{\kod{rv}_1} = \overline{\kod{rv}_2}$$

$$\kod{Q}_1 \dot{\seleq} \kod{Q}_2  \text{~~~iff~~~} \overline{\kod{rv}_1} \subseteq \overline{\kod{rv}_2}$$

Formula $\Theta$ (based on $\kod{Q}_1$), formula $\Psi$ (based on $\kod{Q}_1$ and $\kod{Q}_2$) and relations $\seleq$ and $\dot{\seleq}$ (according to [Spasić and Vujošević Janičić, 2022]).

Relations $\seleq$ and $\dot{\seleq}$ are given within Definition <ref>. These relations connect queries $\kod{Q}_1$ and $\kod{Q}_2$ based on a relation between their relevant variables $\overline{\kod{rv}_1}$ and $\overline{\kod{rv}_2}$, respectively.

The following lemma connects the relevant variables of $\kod{Q}_1$ and variables of $\kod{Q}_2$ if relation $\seleq$ holds.

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, such that $\kod{Q}_2$ does not contain projections and $\kod{Q}_1 \seleq \kod{Q}_2$ holds.
Let $\overline{\kod{rv}_1}$ be a set of relevant variables of $\kod{Q}_1$ and $\kod{qpat}_2$ a query pattern of $\kod{Q}_2$.

$\overline{\kod{rv}_1} = \kod{var}(\kod{qpat}_2)$.

By Definition <ref>, from $\kod{Q}_1 \seleq \kod{Q}_2$, it holds

$$\overline{\kod{rv}_1} = \overline{\kod{rv}_2}.$$

Then, by Lemma <ref>, it holds

$$\overline{\kod{rv}_1} = \kod{var}(\kod{qpat}_2) \cap \overline{\kod{dv}_2}.$$

By Definition <ref>, as $\kod{Q}_2$ does not contain projections, it holds

$$\overline{\kod{rv}_1} = \kod{var}(\kod{qpat}_2).$$

The following lemma is dual to Lemma <ref>, but considering relation $\dot{\seleq}$ instead of $\seleq$ and without a restriction regarding projections of $\kod{Q}_2$.

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, such that $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$.
Let $\overline{\kod{rv}_1}$ be a set of relevant variables of $\kod{Q}_1$ and $\kod{qpat}_2$ and $\overline{\kod{dv}_2}$ a query pattern and a set of distinguished variables of $\kod{Q}_2$, respectively.

$\overline{\kod{rv}_1} \subseteq \kod{var}(\kod{qpat}_2) \cap \overline{\kod{dv}_2}$.

By Definition <ref>, from $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$, it holds

$$\overline{\kod{rv}_1} \subseteq \overline{\kod{rv}_2}.$$

Then, by Lemma <ref>, it holds

$$\overline{\kod{rv}_1} \subseteq \kod{var}(\kod{qpat}_2) \cap \overline{\kod{dv}_2}.$$

The following lemma simplifies the formula $\Psi$ in cases when the relation $\seleq$ holds and $\kod{Q}_2$ does not contain projections.

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, let $\overline{rv_1}$ denote variables from $\vars$ that correspond to the relevant variables of the query $\kod{Q}_1$, and let $\Phi_1(\overline{rv_1})$ correspond to the query $\kod{Q}_1$.
Let $\kod{qpat}_2$ and $\ag_2$ be a query pattern and a query dataset of $\kod{Q}_2$, respectively.
If $\kod{Q}_2$ does not contain projections and $\kod{Q}_1 \seleq \kod{Q}_2$ holds, then formula $\Psi$ is equal to:

$$\forall \overline{rv_1} \ \big( \Phi_1(\overline{rv_1}) \Rightarrow \sigma^{\mathit{df}(\ag_2)}(\kod{qpat}_2)\big).$$

By Definition <ref>, $\Psi$ is defined as

$$\forall \overline{rv_1} \ \big( \Phi_1(\overline{rv_1}) \Rightarrow \Phi_2(\overline{rv_1})),$$

i.e. by Definition <ref>

$$\forall \overline{rv_1} \ \big( \Phi_1(\overline{rv_1}) \Rightarrow \exists \overline{ov_2}  \ \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2)\big),$$

where $\overline{ov_2}$ is equal to $var(\sigma(\kod{qpat}_2)) \setminus \overline{rv_1}$.
By Definition <ref>, as $\kod{Q}_1 \seleq \kod{Q}_2$, it holds
$\overline{\kod{rv}_1} = \overline{\kod{rv}_2}$, i.e. by Lemma <ref>,

$$\overline{\kod{rv}_1} = \kod{var}(\kod{qpat}_2)  \cap \overline{\kod{dv}_2}.$$

As $\kod{Q}_2$ does not contain projections, it holds

$$\overline{\kod{rv}_1} = \kod{var}(\kod{qpat}_2),$$

$$\kod{var}(\kod{qpat}_2) \setminus \overline{\kod{rv}_1} = \varnothing.$$

Therefore, by Definition <ref>, it holds

$$\sigma(\kod{var}(\kod{qpat}_2) \setminus \overline{\kod{rv}_1}) = \varnothing,$$

$$\sigma(\kod{var}(\kod{qpat}_2)) \setminus \sigma(\overline{\kod{rv}_1}) = \varnothing,$$

i.e. by Lemma <ref>,

$$var(\sigma(\kod{qpat}_2)) \setminus \overline{rv_1} = \varnothing.$$

Therefore, $\overline{ov_2}$ is equal to an empty set.
Then, the formula $\Psi$ is reduced to

$$\forall \overline{rv_1} \ \big( \Phi_1(\overline{rv_1}) \Rightarrow \sigma^{\mathit{df}(\ag_2)}(\kod{qpat}_2)\big).$$

We propose the following reductions of the containment problem and the subsumption problem.
[Logical formulation of the  query containment problem]

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, $\Theta$ be a formula generated from $\kod{Q}_1$ (Def <ref>) and $\Psi$ be a formula generated from $\kod{Q}_1$ and $\kod{Q}_2$ (Def <ref>).
The query containment problem, i.e. if $\kod{Q}_1 \sqsubseteq \kod{Q}_2$ holds, is reduced to a satisfiability of a  disjunction of the following two conditions:

(1) $\Theta$ is valid

(2) $\kod{Q}_1 \seleq \kod{Q}_2$ holds and $\Psi$ is valid.

Correctness of the procedure <ref> is a direct consequence of proofs for theorems <ref> (Section <ref>) and <ref> (Section <ref>).

[Logical formulation of the  query subsumption problem]

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, $\Theta$ be a formula generated from $\kod{Q}_1$ (Def <ref>) and $\Psi$ be a formula generated from $\kod{Q}_1$ and $\kod{Q}_2$ (Def <ref>).
The query subsumption problem, i.e. if $\kod{Q}_1 \dot{\sqsubseteq} \kod{Q}_2$ holds, is reduced to a satisfiability of a disjunction of the following two conditions:

(1) $\Theta$ is valid

(2) $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$ holds and $\Psi$ is valid.

Correctness of the procedure <ref> is a direct consequence of proofs for theorems <ref> (Section <ref>) and <ref> (Section <ref>).

§ CORRECTNESS OF THE PROPOSED MODELING

In this section, we prove the correctness of our modeling. We start with introducing necessary definitions and proving auxiliary lemmas (Section <ref>) and continue by proving soundness (Section <ref>) and completeness (Section <ref>) of the proposed reduction.

§.§ Interpretations and Models

There is a standard definition of $\mathcal{L}$-structure over a signature $\mathcal{L}$ given in model theory textbooks [Chang and Keisler, 1976, Marker, 2002].
The following definition represents its concretization over the  theory signature $\mathcal{L}$ corresponding to queries $\kod{Q}_1$ and $\kod{Q}_2$.

An $\mathcal{L}$-structure corresponding to a dataset $\dataq$ over the  theory signature $\mathcal{L}$ corresponding to the queries $\kod{Q}_1$ and $\kod{Q}_2$, named $\mathfrak{D}$, is a pair $(\mathcal{D},\intrprt^{\mathcal{D}})$ where:

* $\mathcal{D}$ is a nonempty domain equal to $\ible{} \cup \siginv(\mathcal{C})$, where I, B, L are sets of s, blank nodes and literals respectively, appearing in the dataset $\dataq$,

* $\intrprt^{\mathcal{D}}$ is a function that maps the non-logical terms of the signature in the following way:

* The interpretation $\intrprt^{\mathcal{D}}$ of constants from $\mathcal{C}$ are from $\ibl{}\kod{e}$, and are defined as $\intrprt^{\mathcal{D}}(c) \eqdef \siginv(c)$, for $c \in \mathcal{C}$.

* The interpretation $\intrprt^{\mathcal{D}}$ of the function symbol $datatype$ is a function $\kod{DATATYPE}: \ibl{} \rightarrow \kod{IBLe}$, which is defined in the following way:

$$\kod{DATATYPE}(\kod{t}) \eqdef
\begin{cases}
\kod{dt}(\kod{t}), & \kod{t} \in \kod{L}\\
\error, & \text{otherwise}
\end{cases}

* The interpretation $\intrprt^{\mathcal{D}}$ of the predicate symbol $isliteral$ is a function $\kod{ISLITERAL}: \ibl{} \rightarrow \bool$, which is defined in the following way:

$$\kod{ISLITERAL}(\kod{t}) = \top \text{ if and only if } \kod{t} \in \kod{L}$$

* The interpretation $\intrprt^{\mathcal{D}}$ of the predicate symbol $\ppp$ is a function $\pppi: \kod{IB} \times \kod{I} \times \ibl{} \rightarrow \bool$, which is defined in the following way:

$$\pppi(\kod{s}, \kod{p}, \kod{o}) = \top \text{ if and only if } (\kod{s}, \kod{p}, \kod{o}) \in \mathit{df}(\dataq)$$

* The interpretation $\intrprt^{\mathcal{D}}$ of the predicate symbol $\pp$ is a function $\ppi: \kod{IB} \times \kod{I} \times \ibl{} \times \kod{I} \rightarrow \bool$, which is defined in the following way:

$$\ppi(\kod{s}, \kod{p}, \kod{o}, \kod{i}) = \top \text{ if and only if } (\kod{s}, \kod{p}, \kod{o}) \in gr_\kod{\,$\dataq$}(\kod{i})$$

Note that $\sigvibl$ is bijective by Definition <ref>, therefore $\siginv$ is well defined.
As a direct consequence of this definition, if $\ppi(\kod{s}, \kod{p}, \kod{o}, \kod{i}) = \top$ then $\kod{i} \in names(\dataq)$. Otherwise, $gr_\kod{\,$\dataq$}(\kod{i})$ would be equal to $\kod{\gr}_{\varnothing}$ and $(\kod{s}, \kod{p}, \kod{o})$ does not belong to $\kod{\gr}_{\varnothing}$.

Note also that the domain $\mathcal{D}$ is at most countable.

A valuation of $\mathcal{L}$-formulas within $\mathcal{L}$-structure $\mathfrak{D}$, usually denoted by $\nu$, is a partial function from the set of variables $\vars$ to $\ibl{}$.

For an $\mathcal{L}$-structure $\mathfrak{M}$, valuation $\nu$, and formula $\Upsilon$ over the given  theory signature $\mathcal{L}$, we use standard notation $(\mathfrak{M}, \nu) \models \Upsilon$ denoting that $\mathfrak{M}$ with valuation $\nu$ is a model of formula $\Upsilon$. If formula $\Upsilon$ is a sentence, i.e. if it does not contain free variables, we use the common notation $\mathfrak{M} \models \Upsilon$.

Let $\Upsilon$ be a formula over the given  theory signature $\mathcal{L}$, and let $(\mathfrak{D}, \nu)$ be a model of it, i.e. $(\mathfrak{D}, \nu) \models \Upsilon$. For interpretation function of $(\mathfrak{D}, \nu)$ defined in the standard way for , we use a notation $\intrprt_\nu$, i.e. $\intrprt_\nu(\Upsilon)$ is true.

If a formula $\Upsilon$ contains variables $\overline{x}$, and a valuation $\nu$ maps them to $\overline{c}$, then $(\mathfrak{D}, \nu) \models \Upsilon(\overline{c})$ denotes that $\intrprt_\nu(\Upsilon(\overline{x}))$ is true.

There are standard definitions of embeddings, isomorphisms, and substructures given in model theory textbooks [Chang and Keisler, 1976, Marker, 2002].
The following definition represents their concretization over the presented signature $\mathcal{L}$ corresponding to $\kod{Q}_1$ and $\kod{Q}_2$.

Let $\mathcal{M}$ and $\mathcal{N}$ be nonempty domains.
Let $\mathfrak{M} = (\mathcal{M}, \intrprt^{\mathcal{M}})$ and $\mathfrak{N} = (\mathcal{N}, \intrprt^{\mathcal{N}})$ be $\mathcal{L}$-structures.

$\mathcal{L}$-embedding An $\mathcal{L}$-embedding $\theta: \mathfrak{M} \rightarrow \mathfrak{N}$ is a function $\theta: \mathcal{M} \rightarrow \mathcal{N}$ with the following properties:

(i) $\theta$ is injective,

(ii) for relation symbols $\ppp$ and $\pp$ in signature $\mathcal{L}$, and all $s, p, o, i \in \mathcal{M}$

$(s, p, o) \in \intrprt^{\mathcal{M}}(\ppp)$ if and only if $(\theta(s), \theta(p), \theta(o)) \in \intrprt^{\mathcal{N}}(\ppp)$, and

$(s, p, o, i) \in \intrprt^{\mathcal{M}}(\pp)$ if and only if $(\theta(s), \theta(p), \theta(o), \theta(i)) \in \intrprt^{\mathcal{N}}(\pp)$,

(iii) for any constant symbol $c$ in the signature $\mathcal{L}$

$\theta(\intrprt^{\mathcal{M}}(c)) = \intrprt^{\mathcal{N}}(c)$.

$\mathcal{L}$-isomorphism An $\mathcal{L}$-isomorphism from $\mathfrak{M}$ to $\mathfrak{N}$ is a bijective $\mathcal{L}$-embedding from $\mathfrak{M}$ to $\mathfrak{N}$.

Relation $\cong$ $\mathfrak{M}$ and $\mathfrak{N}$ are isomorphic, denoted by $\mathfrak{M} \cong \mathfrak{N}$, if there is an $\mathcal{L}$-isomorphism $\theta: \mathfrak{M} \rightarrow \mathfrak{N}$.

$\mathcal{L}$-substructure $\mathfrak{M}$ is an $\mathcal{L}$-substructure of $\mathfrak{N}$ if $\mathcal{M} \subseteq \mathcal{N}$ and the inclusion map $\iota : \mathcal{M} \rightarrow \mathcal{N}$, such that $\iota(a) = a$ for all $a \in \mathcal{M}$, is an $\mathcal{L}$-embedding.

Note that the definition of $\mathcal{L}$-embedding should provide the congruence of all relation symbols from $\preds$.
The property (ii) should hold not only for $\ppp$ and $\pp$, but also for the equality symbol, but it can be proven from property (i), i.e. from the injectiveness of $\theta$:

- for all $m_1, m_2 \in \mathcal{M}$, if $m_1 = m_2$ then $\theta(m_1) = \theta(m_2)$, as $\theta$ is a function;

- the converse holds because $\theta$ is injective.

From the other side, if we include the property (ii) for the equality symbol, the property (i) is not necessary, as it is a corollary of property (ii) for the equality symbol.

Let $\Upsilon$ be a sentence over a given signature $\mathcal{L}$,
and let $\mathfrak{D'}$ and $\mathfrak{D''}$ be $\mathcal{L}$-structures such that $\mathfrak{D'} \cong \mathfrak{D''}$.

$\mathfrak{D'} \models \Upsilon$    if and only if    $\mathfrak{D''} \models \Upsilon$

A proof of this lemma can be found in [Marker, 2002].

Let $\mathfrak{D'} = (\mathcal{D'}, \intrprt^{\mathcal{D'}})$ be an $\mathcal{L}$-structure over the  theory signature $\mathcal{L}$ that corresponds to $\kod{Q}_1$ and $\kod{Q}_2$.
Let $\Upsilon$ be a sentence over a given signature $\mathcal{L}$, such that
$\mathfrak{D'} \models \Upsilon$.
Then, there exists a dataset $\dataq$ and the corresponding $\mathcal{L}$-structure $\mathfrak{D} = (\mathcal{D}, \intrprt^{\mathcal{D}})$ over the same signature, such that
$\mathfrak{D} \models \Upsilon$.

According to Definition <ref>, $\mathfrak{D'}$ has a nonempty domain $\mathcal{D'}$, possibly infinite.
By the downward Löwenheim-Skolem Theorem, there exists an $\mathcal{L}$-structure
$$\mathfrak{D''} = (\mathcal{D''}, \intrprt^{\mathcal{D''}})$$
over the same signature, such that
its domain $\mathcal{D''}$ is countable and $\mathfrak{D}'' \models \Upsilon$.

Let us construct an  dataset $\dataq$ and the corresponding $\mathcal{L}$-structure $\mathfrak{D} = (\mathcal{D}, \intrprt^{\mathcal{D}})$, such that it holds $\mathfrak{D''} \cong \mathfrak{D}$.
First, we define a function $\theta: \mathcal{D''} \rightarrow \ible{}$ as follows:

$\circ$ for all $c'' \in \mathcal{D''}$ such that $c'' = \intrprt^{\mathcal{D''}}(c)$ for some constant from $\mathcal{C}$, $\theta(c'')$ is equal to $\siginv(c)$. Note that the restriction of $\theta$ to the set of such $c''$ is injective, due to Definition <ref>.

$\circ$ for all other $x$ from $\mathcal{D''}$, $\theta(x)$ is equal to an arbitrary element from $\ibl{}$, but taking into account that function $\theta$ should stay injective.
This is possible, as $\ibl{}$ and $\mathcal{D''}$ are countable sets.

Then, we construct an  dataset $\dataq$ as follows:

- for each constant $i$ from $\mathcal{D''}$ we define graph $\kod{G}_i$, and function $gr_\kod{\,$\dataq$}$:

\begin{align*}
\kod{G}_i &:= \{ \ \big( \,\theta(s), \theta(p), \theta(o)\,\big) \ | \ s, p, o \in \mathcal{D''} \\
&\hspace*{10mm} \text{ and } \intrprt^\mathcal{D''}(\pp)(s, p, o, i) \text{ is true}\}\\
gr_\kod{\,$\dataq$}(\theta(i)) &:= \kod{G}_i
\end{align*}

- we define default graph $\dg$:

\begin{align*}
\dg &:= \{ \ \big( \,\theta(s), \theta(p), \theta(o)\,\big) \ | \ s, p, o \in \mathcal{D''} \\
& \hspace*{10mm} \text{ and } \intrprt^\mathcal{D''}(\ppp)(s, p, o) \text{ is true}\}
\end{align*}

Then, dataset $\dataq$ contains default graph $\dg$ and named graphs $\kod{G}_i$ with the corresponding names $\theta(i)$.
Note that according to the modeling of queries where formula contains predicates $\ppp$ and/or $\pp$ and the existence of its model in $\mathfrak{D''}$, these graphs are not empty.

The function $\theta$ is an $\mathcal{L}$-embedding, according to Definition <ref>, because:

(i) $\theta$ is injective, by its construction;

(ii) for all $s, p, o, i \in \mathcal{D''}$, it holds

\begin{align*}
& \hspace*{-3mm} \intrprt^\mathcal{D''}(\ppp)(s, p, o) \hspace*{-4mm} & \text{ iff } \\
& \text{(by constr.)} & \text{ iff } &( \,\theta(s), \theta(p), \theta(o)\,) \hspace*{-1mm} \in \hspace*{-1mm} \dg \\
& \text{(by Def \ref{defn:l_structure})}& \text{ iff } &\pppi(\theta(s), \theta(p), \theta(o))  \\
& \text{(by Def \ref{defn:l_structure})}& \text{ iff }  &\intrprt^\mathcal{D}(\ppp)(\theta(s), \theta(p), \theta(o)), \\
& \hspace*{-3mm} \intrprt^\mathcal{D''}(\pp)(s, p, o, i) \hspace*{-4mm} & \text{ iff } \\
& \text{(by constr.)} & \text{ iff } &( \,\theta(s), \theta(p), \theta(o)\,) \hspace*{-1mm} \in \hspace*{-1mm} gr_\kod{\,$\dataq$}(\theta(i))\\
& \text{(by Def \ref{defn:l_structure})} & \text{ iff } &\ppi(\theta(s), \theta(p), \theta(o), \theta(i)) \\
& \text{(by Def \ref{defn:l_structure})} & \text{ iff } &\intrprt^\mathcal{D}(\pp)(\theta(s), \theta(p), \theta(o), \theta(i));
\end{align*}

(iii) for each constant symbol $c$ of the signature $\mathcal{L}$, $\intrprt^{\mathcal{D''}}\hspace*{-2pt}(c) \hspace*{-2pt} \in \hspace*{-2pt} \mathcal{D''}$, and $\theta(\intrprt^{\mathcal{D''}}(c)) = \intrprt^\mathcal{D}(c)$ by construction.

Function $\theta$ is surjective, because for each $\kod{x} \in \mathcal{D}$, there is an element $x \in \mathcal{D''}$ such that $\theta(x) = \kod{x}$:

- if $\kod{x}$ is the interpretation of a constant from $\mathcal{C}$, according to Definition <ref>, construction of $\theta$ and the fact that $\mathfrak{D''}$ and $\mathfrak{D}$ are corresponding $\mathcal{L}$-structures, there is an element $x$ such that $\theta(x) = \kod{x}$;

- otherwise, each other element from $\mathcal{D}$ is an image of an element from $\mathcal{D''}$ by the construction of $\theta$ and the dataset $\dataq$.

Therefore, $\mathcal{L}$-embedding $\theta$ is bijective, and by Definition <ref>, it holds $\mathfrak{D''} \cong \mathfrak{D}$.
Then, by Lemma <ref>, it holds

$$\mathfrak{D} \models \Upsilon.$$

Let $\mu {: \kod{VB} \rightarrow \ibl{}}$ be a mapping and $\nu {: \vars \rightarrow \ibl{}}$ be a valuation.

-	Mapping $\mu$ defines a valuation $\nu$, denoted $\mu \definisemini \nu$,  if $\sigvibl(dom(\mu)) \subseteq dom(\nu)$ and for each $\kod{x} \in dom(\mu)$ it holds
$\nu (\sigvibl(\kod{x})) = \mu (\kod{x}).$

-	Mapping $\mu$ is defined by a valuation $\nu$, denoted $\mu \definisenimi \nu$, if $dom(\mu) \supseteq \sigvibl^{-1}(dom(\nu))$ and for each  ${x} \in dom(\nu)$ it holds
$\mu(\sigvibl^{-1}(x)) = \nu(x).$

-	Mapping $\mu$ corresponds to valuation $\nu$, denoted $\mu \povezano \nu$, if $\mu \definisemini \nu$ and $\mu \definisenimi \nu$.

These relations are well defined as $\sigvibl$ is bijective.
Note that if $\mu \povezano \nu$ holds, $dom(\mu) = \sigvibl^{-1}(dom(\nu))$ and $dom(\nu) = \sigvibl(dom(\mu))$.

Similarly to the notation $\mu_{\kod{x} \rightarrow \kod{c}}$, we introduce $\nu_{x \rightarrow \kod{c}}$ denoting a valuation such that $dom(\nu_{x \rightarrow \kod{c}}) \eqdef \{x\}$ and $\nu_{x \rightarrow \kod{c}}(x) \eqdef \kod{c}$.
Note that, by Definition <ref>, $\mu_{\kod{x} \rightarrow \kod{c}} \povezano \nu_{x \rightarrow \kod{c}}$, as $dom(\nu) = \{x\} = \{\sigma(\kod{x})\} = \sigma(\{\kod{x}\}) = \sigma(dom(\mu))$, and $\nu(x) = \kod{c} = \mu(\kod{x})$.

Definition <ref> can be used in the context of valuations as well: $\nu_1$ and $\nu_2$ are compatible, denoted by $\nu_1 \comp \nu_2$, if for each ${x}$ such that $x \in dom(\nu_1) \cap dom(\nu_2)$ it holds that $\nu_1(x) = \nu_2(x)$.

Let ${\mu}_{1}, \mu_{2} : \kod{VB} \rightarrow \ibl{}$ be mappings, and let ${\nu}_{1}, {\nu}_{2} {: \vars \rightarrow \ibl{}}$ be valuations such that ${\mu}_{1} \povezano {\nu}_{1}$ and ${\mu}_{2} \povezano {\nu}_{2}$.

$\mu_1 \comp \mu_2$

if and only if

$\nu_1 \comp \nu_2$.

If $dom(\nu_1) \cap dom(\nu_2)$ is an empty set, by Definition <ref>, it holds $\nu_1 \comp \nu_2$.
Otherwise, let $x$ be an element of $dom(\nu_1) \cap dom(\nu_2)$, i.e. $x \in dom(\nu_1)$ and $x \in dom(\nu_2)$.
From $\mu_1 \povezano \nu_1$ and $\mu_2 \povezano \nu_2$, by Definition <ref>, it holds
$x \in \{ \sigvibl(\kod{x}) \ | \ \kod{x} \in dom(\mu_1) \}$ and $x \in \{ \sigvibl(\kod{x}) \ | \ \kod{x} \in dom(\mu_2) \}$.
Therefore, since $\sigvibl$ is a bijective function, there exists a unique $\kod{x}$, such that

$$x = \sigvibl(\kod{x}), \ \kod{x} \in dom(\mu_1) \text{ and } \kod{x} \in dom(\mu_2)$$
i.e. $\kod{x} \in dom(\mu_1) \cap dom(\mu_2)$.
As it holds $\mu_1 \comp \mu_2$ (Definition <ref>), it holds

and by the assumptions $\mu_1 \povezano \nu_1$ and $\mu_2 \povezano \nu_2$, it holds

$$\nu_1(\sigvibl(\kod{x}))=\mu_1(\kod{x}) \text{ and } \mu_2(\kod{x})=\nu_2(\sigvibl(\kod{x})).$$

Therefore, it holds

$$\nu_1(\sigvibl(\kod{x}))=\nu_2(\sigvibl(\kod{x})), \text{ i.e. } \nu_1(x)=\nu_2(x).$$

By Definition <ref>, it holds $\nu_1 \comp \nu_2$.

If $dom(\mu_1) \cap dom(\mu_2)$ is an empty set, by Definition <ref>, it holds $\mu_1 \comp \mu_2$.
Otherwise, let $\kod{x}$ be an element of $dom(\mu_1) \cap dom(\mu_2)$, i.e. $\kod{x} \in dom(\mu_1)$ and $x \in dom(\mu_2)$.
From $\mu_1 \povezano \nu_1$ and $\mu_2 \povezano \nu_2$, by Definition <ref>, it holds
$\kod{x} \in \{ \siginv(x) \ | \ x \in dom(\nu_1) \}$ and $\kod{x} \in \{ \siginv(x) \ | \ x \in dom(\nu_2) \}$.
Therefore, since $\siginv$ is a bijective function, there exists a unique $x$, such that

$$\kod{x} = \siginv(x), \ x \in dom(\nu_1) \text{ and } x \in dom(\nu_2)$$
i.e. $x \in dom(\nu_1) \cap dom(\nu_2)$.
As it holds $\nu_1 \comp \nu_2$ (Definition <ref>), it holds

and by the assumptions $\mu_1 \povezano \nu_1$ and $\mu_2 \povezano \nu_2$, it holds

$$\mu_1(\siginv(x))=\nu_1(x) \text{ and } \nu_2(x)=\mu_2(\siginv(x)).$$

Therefore, it holds

$$\mu_1(\siginv(x))=\mu_2(\siginv(x)), \text{ i.e. } \mu_1(\kod{x})=\mu_2(\kod{x}).$$

By Definition <ref>, it holds $\mu_1 \comp \mu_2$.

Let $\mu, \mu_1, \mu_2 : \kod{VB} \rightarrow \ibl{}$ be mappings, and $\nu, \nu_1, \nu_2 : \vars \rightarrow \ibl{}$ be valuations such that $\mu \povezano \nu$, $\mu_1 \povezano \nu_1$ and $\mu_2 \povezano \nu_2$.

$\mu_1 \comp \mu_2$  and  $\mu = \mu_1 \cup \mu_2$

if and only if

$\nu_1 \comp \nu_2$  and  $\nu = \nu_1 \cup \nu_2$.

From $\mu_1 \povezano \nu_1$, $\mu_2 \povezano \nu_2$ and  $\mu_1 \comp \mu_2$, by Lema <ref> it holds that

$$	\nu_1 \comp \nu_2.$$

Therefore, $\nu_1 \cup \nu_2$ is a well defined valuation.

From $\mu \povezano \nu$, $\mu_1 \povezano \nu_1$ and $\mu \comp \mu_1$ (as $\mu$ is an extension of $\mu_1$), by Lemma <ref> it holds that
$$\nu \comp \nu_1.$$

Similarly, from $\mu \povezano \nu$, $\mu_2 \povezano \nu_1$, and $\mu \comp \mu_2$ (as $\mu$ is an extension of $\mu_2$),  by Lemma <ref>, it holds that
$$\nu \comp \nu_2.$$

\begin{align*}
&\hspace*{20mm} dom(\nu) \hspace*{-20mm} & = \;\\
&\text{(by Def \ref{def:povezano} as } \mu \povezano \nu) \hspace*{-3mm} & = \; & \sigvibl(dom(\mu)) \\
&\text{(as } \mu = \mu_1 \cup \mu_2 \text{)} & = \; & \sigvibl(dom(\mu_1) \cup dom(\mu_2)) \\
& \text{(by Def \ref{def:function_over_sets})} & = \; &  \sigvibl(dom(\mu_1)) \cup \sigvibl(dom(\mu_2)) \\
& \text{(by Def \ref{def:povezano}, as } \mu_1 \povezano \nu_1 \text{ and } \mu_2 \povezano \nu_2) \hspace*{-30mm}\\
& & = \; & dom(\nu_1) \cup dom(\nu_2)\\
&\text{ (} \nu_1 \text{ and } \nu_2 \text{ are comp.)} \hspace*{-8mm} & = \; & dom(\nu_1 \cup \nu_2)
\end{align*}

As $dom(\nu) = dom(\nu_1) \cup dom(\nu_2)$, for $x \in dom(\nu)$, it holds
$$x \in dom(\nu_1) \text{ or } x \in dom(\nu_2).$$

From $\nu \comp \nu_1$ and $\nu \comp \nu_2$, by Definition <ref>, it holds
$$\nu(x) = \nu_1(x) \text{ or } \nu(x) = \nu_2(x).$$

Therefore, as $\nu_1 \comp \nu_2$,

$$x \in dom(\nu) \text{ implies } \nu(x) = (\nu_1 \cup \nu_2)(x) \text{.}$$

Finally, from $dom(\nu) = dom(\nu_1 \cup \nu_2)$ and the last equation, it holds

$$\nu = \nu_1 \cup \nu_2.$$

From $\mu_1 \povezano \nu_1$, $\mu_2 \povezano \nu_2$ and $\nu_1 \comp \nu_2$, by Lema <ref> it holds that

$$\mu_1 \comp \mu_2.$$

Therefore, $\mu_1 \cup \mu_2$ is a well defined mapping.

From $\mu \povezano \nu$, $\mu_1 \povezano \nu_1$ and $\nu \comp \nu_1$ (as $\nu$ is an extension of $\nu_1$), by Lemma <ref> it holds that
$$\mu \comp \mu_1.$$

Similarly, from $\mu \povezano \nu$, $\mu_2 \povezano \nu_1$, and $\nu \comp \nu_2$ (as $\nu$ is an extension of $\nu_2$),  by Lemma <ref>, it holds that
$$\mu \comp \mu_2.$$

\begin{align*}
&\hspace*{20mm} dom(\mu) \hspace*{-20mm} & = \;\\
&\text{(by Def \ref{def:povezano} as } \mu \povezano \nu) \hspace*{-4mm} &=\;& \siginv(dom(\nu)) \\
& \text{ (as } \nu = \nu_1 \cup \nu_2 \text{)}&=\;&  \siginv(dom(\nu_1) \cup dom(\nu_2))\\
& \text{(by Def \ref{def:function_over_sets})} &=\;&  \siginv(dom(\nu_1)) \ \cup\\
&&& \siginv(dom(\nu_2)) & \\
& \text{(by Def \ref{def:povezano}, as }\mu_1 \povezano \nu_1 \text{ and } \mu_2 \povezano \nu_2 \text{)} \hspace*{-40mm}\\
&&=\;& dom(\mu_1) \cup dom(\mu_2)\\
&\text{ (} \mu_1 \text{ and } \mu_2 \text{ are comp.)} \hspace*{-3mm} &=\;& dom(\mu_1 \cup \mu_2)
\end{align*}

As $dom(\mu) = dom(\mu_1) \cup dom(\mu_2)$, for  $\kod{x} \in dom(\mu)$, it holds

$$\kod{x} \in dom(\mu_1) \text{ or } \kod{x} \in dom(\mu_2).$$

From $\mu \comp \mu_1$ and $\mu \comp \mu_2$, by Definition <ref>, it holds
$$\mu(\kod{x}) = \mu_1(\kod{x}) \text{ or } \mu(\kod{x}) = \mu_2(x).$$

Therefore, as $\mu_1 \comp  \mu_2$,

$$\kod{x} \in dom(\mu) \text{ implies } \mu(\kod{x}) = (\mu_1 \cup \mu_2)(\kod{x}) \text{.}$$

Finally, from $dom(\mu) = dom(\mu_1 \cup \mu_2)$ and the last equation, it holds

$$\mu = \mu_1 \cup \mu_2.$$

Let $\nu$ be a valuation, and $t$ a term over  theory signature $\mathcal{L}$.
A value of the term $t$, according to the valuation $\nu$, in notation $\valuation{t}{\nu}$ is a value from $\ible$, defined in the following way:

\begin{align*}
\valuation{t}{\nu} & \eqdef \
\begin{cases}
\error,& t \in \vars \text{ and } t \notin dom(\nu)\\
\error,& t \text{ is } datatype(t_1) \text{ and } \valuation{t_1}{\nu}=\error\\
\error,& t \text{ is } isliteral(t_1) \text{ and } \valuation{t_1}{\nu}=\error\\
\intrprt_\nu(t) ,& \text{otherwise}.\\
\end{cases}
\end{align*}

Let $\kod{E}$ be an expression.
Let $\mu : \kod{VB} \rightarrow \ibl{}$ be a mapping and $\nu {: \vars \rightarrow \ibl{}}$ be a valuation such that $\mu \povezano \nu$.

$\valuation{\kod{E}}{\mu} = \valuation{\sigma(\kod{E})}{\nu}$.

The lemma is proved by induction on an expression $\kod{E}$.

* E  is  c, $\kod{c} \in \kod{IL}$

\begin{align*}
&\hspace*{22mm} \valuation{\kod{c}}{\mu} \hspace*{-20mm} & = \;\\
& \text{(by Def \ref{defn:expr_in_mu})} & = \; & \kod{c} \\
& \text{(by Def \ref{def:sigmat})} & = \; & \siginv(\sigvibl(\kod{c})) \\
& \text{(by Def \ref{defn:l_structure})} & = \; & \intrprt^{\mathcal{D}}(\sigvibl(\kod{c})) \\
& \text{(by Def \ref{def:sigma})} & = \; &\intrprt^{\mathcal{D}}(\sigma(\kod{c})) \\
& \text{(by Def \ref{defn:expr_in_nu})} & = \; &\valuation{\sigma(\kod{c})}{\nu} \\
\end{align*}

* E  is  $\kod{v}$, $\kod{v} \in \kod{V}$

* $\kod{v} \in dom(\mu)$

As $\mu \povezano \nu$ and $\kod{v} \in dom(\mu)$, by Definition <ref>, it holds $\sigma(\kod{v}) \in dom(\nu)$.

\begin{align*}
&\hspace*{37mm} \valuation{\kod{v}}{\mu} \hspace*{-20mm} & = \;\\
& \text{(by Def \ref{defn:expr_in_mu}, as } \kod{v} \in dom(\mu) \text{)} & =\;  &\mu(\kod{v}) \\
& \text{(by Def \ref{def:povezano} as $\mu \povezano \nu$)} & =\;  &\nu(\sigvibl(\kod{v}))\\ &\text{(by Def \ref{def:sigma})} & =\;  &\nu(\sigma(\kod{v})) \\
& \text{(by Def \ref{defn:model})}  & =\;  &\intrprt_\nu(\sigma(\kod{v}))\\
& \text{(by Def \ref{defn:expr_in_nu}, as } \sigma(\kod{v}) \hspace*{-1mm} \in \hspace*{-1mm} dom(\nu) \text{)}  \hspace*{-3mm} & =\;  &\valuation{\sigma(\kod{v})}{\nu}
\end{align*}

* $\kod{v} \notin dom(\mu)$

As $\mu \povezano \nu$ and $\kod{v} \notin dom(\mu)$, by Definition <ref>, it holds $\sigma(\kod{v}) \notin dom(\nu)$.

\begin{align*}
& \hspace*{37mm} \valuation{\kod{v}}{\mu} \hspace*{-20mm} & = \;\\
& \text{(by Def \ref{defn:expr_in_mu}, as } \kod{v} \notin dom(\mu) \text{)} & =\; & \error \\
& \text{(by Def \ref{defn:expr_in_nu}, as } \sigma(\kod{v}) \hspace*{-1mm} \notin \hspace*{-1mm} dom(\nu) \text{)} \hspace*{-3mm} & =\; & \valuation{\sigma(\kod{v})}{\nu}
\end{align*}

* E  is  $\kod{datatype(E}_1\kod{)}$

* $\valuation{\kod{E}_1}{\mu} = \error$

By induction hypothesis, it holds $\valuation{\kod{E}_1}{\mu} = \error$ iff $\valuation{\sigma(\kod{E}_1)}{\nu} = \error$.

\begin{align*}
& \hspace*{-6mm} \valuation{\kod{datatype(E}_1\kod{)}}{\mu} \hspace*{-3mm} & = \\
& \text{(by Def \ref{defn:expr_in_mu})} \hspace*{-3mm} & = &\error \\
& \text{(by induc. hyp.)} \hspace*{-3mm}& = &\valuation{\sigma(\kod{E}_1)}{\nu} \\
& \text{(by Def \ref{defn:expr_in_nu})} \hspace*{-3mm}& = &\valuation{datatype(\sigma(\kod{E}_1))}{\nu} \\
& \text{(by Def \ref{def:sigma})} \hspace*{-3mm}& = &\valuation{\sigma(\kod{datatype(E}_1\kod{)})}{\nu}
\end{align*}

* $\valuation{\kod{E}_1}{\mu} \not= \error$ and $\valuation{\kod{E}_1}{\mu} \notin \kod{L}$:

By induc. hypothesis, it holds $\valuation{\sigma(\kod{E}_1)}{\nu} \hspace*{-1mm} \notin \hspace*{-1mm} \kod{L}$.

\begin{align*}
&\hspace*{-6mm} \valuation{\kod{datatype(E}_1\kod{)}}{\mu} \hspace*{-3mm} & = \\
& \text{(by Def \ref{defn:expr_in_mu})} \hspace*{-3mm}& =  &\error\\
& \text{(by Def \ref{defn:l_structure})} \hspace*{-3mm}& = &\kod{DATATYPE}(\valuation{\sigma(\kod{E}_1)}{\nu}) \\
& \text{(by Def \ref{defn:l_structure})} \hspace*{-3mm}& = &\intrprt^{\mathcal{D}}(datatype)(\valuation{\sigma(\kod{E}_1)}{\nu}) \\
& \text{(by Def \ref{defn:expr_in_nu})} \hspace*{-3mm}& = &\valuation{datatype(\sigma(\kod{E}_1))}{\nu} \\
& \text{(by Def \ref{def:sigma})} \hspace*{-3mm}& = &\valuation{\sigma(\kod{datatype(E}_1\kod{)})}{\nu}
\end{align*}

* $\valuation{\kod{E}_1}{\mu} \not= \error$ and $\valuation{\kod{E}_1}{\mu} \in \kod{L}$:

By induc. hypothesis, it holds $\valuation{\kod{E}_1}{\mu} \not= \error$ iff $\valuation{\sigma(\kod{E}_1)}{\nu} \not= \error$.

\begin{align*}
&\hspace*{-9mm} \valuation{\kod{datatype(E}_1\kod{)}}{\mu} \hspace*{-3mm} & = \\
&\hspace*{-3mm} \text{(by Def \ref{defn:expr_in_mu})} \hspace*{-3mm} & =  &\kod{dt}(\valuation{(\kod{E}_1)}{\mu})\\
&\hspace*{-3mm} \text{(by induc. hyp.)} \hspace*{-3mm} & = &\kod{dt}(\valuation{\sigma(\kod{E}_1)}{\nu}) \\
&\hspace*{-3mm} \text{(by Def \ref{defn:l_structure})} \hspace*{-3mm} & = &\kod{DATATYPE}(\valuation{\sigma(\kod{E}_1)}{\nu}) \\
&\hspace*{-3mm} \text{(by Def \ref{defn:l_structure})} \hspace*{-3mm} & = &\intrprt^{\mathcal{D}}(datatype)(\valuation{\sigma(\kod{E}_1)}{\nu}) \\
&\hspace*{-3mm} \text{(by Def \ref{defn:expr_in_nu})} \hspace*{-3mm} & = &\valuation{datatype(\sigma(\kod{E}_1))}{\nu} \\
&\hspace*{-3mm} \text{(by Def \ref{def:sigma})} \hspace*{-3mm} & = &\valuation{\sigma(\kod{datatype(E}_1\kod{)})}{\nu}
\end{align*}

Let $\kod{E}$ be an expression, and $\kod{v}$ a variable.
Let $\mu : \kod{VB} \rightarrow \ibl{}$ be a mapping and $\nu {: \vars \rightarrow \ibl{}}$ be a valuation such that $\mu \povezano \nu$.

$\mu(\kod{v}) = \valuation{\kod{E}}{\mu}$    if and only if    $\model{\nu} \models \sigma(\kod{v})=\sigma(\kod{E})$.

\begin{align*}
& \hspace*{16mm} \mu(\kod{v}) = \valuation{\kod{E}}{\mu} \hspace*{-10mm} & \text{ iff } \\
& \text{(by Lemma \ref{thm:expr_mu_nu})} & \text{ iff } & \mu(\kod{v}) = \valuation{\sigma(\kod{E})}{\nu} \\
& \text{(by Def \ref{defn:expr_in_nu})} & \text{ iff } & \mu(\kod{v}) = \intrprt_\nu(\sigma(\kod{E})) \\
& \text{(by Def \ref{def:povezano} as $\mu \povezano \nu$)} & \text{ iff } & \nu(\sigma(\kod{v})) = \intrprt_\nu(\sigma(\kod{E})) \\
& \text{(by Def \ref{defn:model})} & \text{ iff } & \model{\nu} \models \sigma(\kod{v})=\sigma(\kod{E})
\end{align*}

Let $\mu : \kod{VB} \rightarrow \ibl{}$ be a mapping and $\nu {: \vars \rightarrow \ibl{}}$ be a valuation such that $\mu \povezano \nu$.

$\mu \zadovoljava \kod{R}$    if and only if    $\model{\nu} \models \sigma(\kod{R})$.

The lemma is proved by induction on a condition $\kod{R}$.

* R  is  $\kod{E}_1$ = $\kod{E}_2$

\begin{align*}
& \hspace*{10mm} \mu \zadovoljava \kod{E}_1 = \kod{E}_2 \hspace*{-3mm} & \text{ iff } \\
& \text{(by Def \ref{defn:definition_filter})} & \text{ iff } &\valuation{\kod{E}_1}{\mu} \not= \error \text{ and }\\
&&& \valuation{\kod{E}_2}{\mu} \not= \error \text{ and } \\
&&& \valuation{\kod{E}_1}{\mu} = \valuation{\kod{E}_2}{\mu} \\
& \text{(by Lemma \ref{thm:expr_mu_nu})} &\text{ iff } &\valuation{\sigma(\kod{E}_1)}{\nu} \not= \error \text{ and } \\
&&& \valuation{\sigma(\kod{E}_2)}{\nu} \not= \error \text{ and } \\
&&& \valuation{\sigma(\kod{E}_1)}{\nu} = \valuation{\sigma(\kod{E}_2)}{\nu} \\
& \text{(by Def \ref{defn:model} and \ref{defn:expr_in_nu})} \hspace*{-3mm} &\text{ iff } &\model{\nu} \models \sigma(\kod{E}_1) = \sigma(\kod{E}_2)  \\
& \text{(by Def \ref{def:sigma})} & \text{ iff } & \model{\nu} \models \sigma(\kod{E}_1 = \kod{E}_2) &
\end{align*}

* R  is  $\kod{!R}_1$

\begin{align*}
& \hspace*{17mm} \mu \zadovoljava \kod{!R}_1 \hspace*{-10mm} & \text{ iff } \\
& \text{(by Def \ref{defn:definition_filter})} & \text{ iff } & \text{not } \mu \zadovoljava \kod{R}_1 \\
& \text{(by induc. hyp.)} & \text{ iff } & \text{not } \model{\nu} \models \sigma(\kod{R}_1) \\
& \text{(by Def \ref{defn:model})} & \text{ iff } & \model{\nu} \models \neg \sigma(\kod{R}_1)\\
& \text{(by Def \ref{def:sigma})} & \text{ iff } & \model{\nu} \models \sigma(\kod{!R}_1) &
\end{align*}

* R  is  $\kod{R}_1 \kod{\&\&} \kod{R}_2$

\begin{align*}
& \hspace*{10mm} \mu \zadovoljava \kod{R}_1 \kod{\&\&} \kod{R}_2 \hspace*{-3mm} & \text{ iff } \\
& \text{(by Def \ref{defn:definition_filter})} & \text{ iff } & \mu \zadovoljava \kod{R}_1 \text{ and } \mu \zadovoljava \kod{R}_2 \\
& \text{(by induc. hyp.)} & \text{ iff } & \model{\nu} \models \sigma(\kod{R}_1) \text{ and } \\
&&& \model{\nu} \models \sigma(\kod{R}_2) \\
& \text{(by Def \ref{defn:model})} & \text{ iff } & \model{\nu} \models \sigma(\kod{R}_1) \wedge \sigma(\kod{R}_2) \\
& \text{(by Def \ref{def:sigma})} & \text{ iff } & \model{\nu} \models \sigma(\kod{R}_1 \kod{\&\&} \kod{R}_2) &
\end{align*}

* $\kod{R} \text{ is } \kod{R}_1 \kod{||} \kod{R}_2$

Proof is analogous to the previous case.

* $\kod{R} \text{ is } \kod{(R}_1\kod{)}$

Proof is analogous to the case $\kod{R} \text{ is } \kod{!R}_1$.

* R  is  $\kod{isliteral(E)}$

\begin{align*}
& \hspace*{-5mm} \mu \zadovoljava \kod{isliteral(E)} \hspace*{-5mm} & \text{ iff } \\
& \text{(by Def \ref{defn:definition_filter})} &\text{ iff }  &\valuation{\kod{E}}{\mu} \not= \error \text{ and }\\
&&& \valuation{\kod{E}}{\mu} \in \kod{L}\\
& \text{(by Lemma \ref{thm:expr_mu_nu})} &\text{ iff }  & \valuation{\sigma(\kod{E})}{\nu} \not= \error \text{ and }\\
&&& \valuation{\sigma(\kod{E})}{\nu} \in \kod{L}\\
& \text{(by Def \ref{defn:l_structure} } & \text{ iff }  & \kod{ISLITERAL}(\valuation{\sigma(\kod{E})}{\nu})\\
& \text{(by Def \ref{defn:l_structure} } & \text{ iff } & 	\intrprt^{\mathcal{D}}(isliteral)(\valuation{\sigma(\kod{E})}{\nu}) \\
& \text{(by Def \ref{defn:model})} & \text{ iff } & \model{\nu} \models isliteral(\sigma(\kod{E})) \\
& \text{(by Def \ref{def:sigma})} & \text{ iff }  & \model{\nu} \models \sigma(\kod{isliteral(E)}) &
\end{align*}

Let $\ag$ be a query dataset,  a graph within $\ag$, and  a
graph pattern.
Let $\mu : \kod{VB} \rightarrow \ibl{}$ be a mapping and $\nu {: \vars \rightarrow \ibl{}}$ be a valuation such that $\mu \povezano \nu$.

$\mu \in \semdg{\kod{\pat}}{{\ag}}{\kod{\gr}}$

if and only if

$\model{\nu} \models \sigma^{\kod{\gr}}(\kod{\pat})$  and  $dom(\nu) = var(\sigma^{\kod{\gr}}(\kod{\pat}))$.

By Lemma <ref>, from $\mu \in \semdg{\kod{\pat}}{{\ag}}{\kod{G}}$, it holds $dom(\mu) = \kod{var}(\kod{\pat})$.
Therefore, by Definitions <ref> and <ref>, as $\mu \povezano \nu$, it holds $dom(\nu) = \sigma(dom(\mu)) = \sigma(\kod{var}(\kod{\pat}))$.
Then, by Lemma <ref>, it holds $dom(\nu) = var(\sigma(\kod{\pat}))$.
The rest of specified equivalence is proved by induction over graph pattern $\kod{\pat}$.

*  is  where  is s p o

By Definition <ref>,

$$\mu \in \semdg{\kod{s p o}}{{\ag}}{\kod{G}} \text{ implies } \valuation{\kod{s p o}}{\mu} \in \kod{G},$$

i.e. by Definition <ref>
$$\valuation{\kod{s}}{\mu} \kod{ } \valuation{\kod{p}}{\mu} \kod{ } \valuation{\kod{o}}{\mu} \in \kod{G}.$$

By Definition <ref>, $\kod{\gr}$ is equal to $\dg$ ($\dg = \mathit{df}(\dataq)$) or to an  merge of a nonempty set of named graphs, i.e. $merge(\kod{\gr}_{k_1}, \ldots, \kod{\gr}_{k_m}), m > 0$, or a named graph $\kod{\gr}_{l_j}$, $j \in \{1, n\}$ within dataset $\ag$.
Therefore, one option of the following three holds:

\begin{equation}
\label{thm34:eq1}
\valuation{\kod{s}}{\mu} \kod{\,} \valuation{\kod{p}}{\mu} \kod{\,} \valuation{\kod{o}}{\mu} \hspace*{-2pt} \in \hspace*{-2pt} \dg
\end{equation}

\begin{equation}
\label{thm34:eq2}
\valuation{\kod{s}}{\mu} \kod{\,} \valuation{\kod{p}}{\mu} \kod{\,} \valuation{\kod{o}}{\mu} \hspace*{-2pt} \in \hspace*{-2pt} \kod{\gr}_{k_j}\text{, for some }j \hspace*{-2pt} \in \hspace*{-2pt} \{1,...,m\} \hspace*{-1pt}
\end{equation}

\begin{equation}
\label{thm34:eq3}
\valuation{\kod{s}}{\mu} \kod{\,} \valuation{\kod{p}}{\mu} \kod{\,} \valuation{\kod{o}}{\mu} \hspace*{-2pt} \in \hspace*{-2pt} \kod{\gr}_{l_j}\text{, for some }j \hspace*{-2pt} \in \hspace*{-2pt} \{1,..., n \}.
\end{equation}

From option (<ref>), by Definitions <ref>, it holds

$$\pppi(\valuation{\kod{s}}{\mu}, \valuation{\kod{p}}{\mu}, \valuation{\kod{o}}{\mu}) = \top \text{. }$$

Therefore, by Lemma <ref>, from $\mu \povezano \nu$, it holds

$$\pppi(\valuation{\sigma(\kod{s})}{\nu}, \valuation{\sigma(\kod{p})}{\nu}, \valuation{\sigma(\kod{o})}{\nu}) = \top \text{, }$$

i.e. by Definitions <ref>, <ref> and <ref>:

$$\model{\nu} \models \ppp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})).$$

From option (<ref>), by Definition <ref>, the set $\context(\kod{\gr})$ contains  constants from $\mathcal{C}$ corresponding to graphs that form $\kod{G}$. Therefore, there exists $i \in \context(\kod{\gr})$, such that $i$ corresponds to a graph that forms $\kod{G}$, i.e. $i$ is equal to an $i_{k_j}$ from $\context(\kod{\gr})$, corresponding to the named graph $\kod{\gr}_{k_j}$, i.e. $gr_\kod{\,D}(\kod{i}) = \kod{\gr}_{k_j}$.
By Definition <ref>, from
$\valuation{\kod{s}}{\mu} \kod{ } \valuation{\kod{p}}{\mu} \kod{ } \valuation{\kod{o}}{\mu} \in \kod{\gr}_{k_j}$,
it holds

$$\ppi(\valuation{\kod{s}}{\mu}, \valuation{\kod{p}}{\mu}, \valuation{\kod{o}}{\mu}, i) = \top.$$

From option (<ref>), by Definition <ref>, there is a constant $i = i_{l_j}$, corresponding to the named graph $\kod{\gr}_{l_j}$, i.e. $gr_\kod{\,D}(\kod{i}) = \kod{\gr}_{l_j}$.
Note that $i \in \context(\kod{\gr})$.
By Definition <ref>, from  $\valuation{\kod{s}}{\mu} \kod{\,} \valuation{\kod{p}}{\mu} \kod{\,} \valuation{\kod{o}}{\mu} \in \kod{\gr}_{l_j}$,
it holds (the same as in the previous option):

$$\ppi(\valuation{\kod{s}}{\mu}, \valuation{\kod{p}}{\mu}, \valuation{\kod{o}}{\mu}, i) = \top \text{. }$$

Therefore, from $\mu \povezano \nu$, by Lemma <ref>, it holds

$$\ppi(\valuation{\sigma(\kod{s})}{\nu}, \valuation{\sigma(\kod{p})}{\nu}, \valuation{\sigma(\kod{o})}{\nu}, i) = \top.$$

By Definitions <ref>, <ref> and <ref>, it holds

$$\model{\nu} \models \pp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}), i),$$

$$\model{\nu} \models \underset{i_j \in \context(\kod{\gr})} \bigvee \pp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}), i_j).$$

Putting all options together, by Definition <ref>, it holds

$$\model{\nu} \models \sigma^\kod{\gr}(\kod{s p o}).$$

($\Leftarrow$) By Lemma <ref>, from $dom(\nu) = var(\sigma^{\kod{\gr}}(\kod{\tpat}))$, it holds $dom(\nu) = \sigma(\kod{var}(\kod{\tpat}))$.
By Definitions <ref>, as $\mu \povezano \nu$, it holds
$$dom(\mu) \hspace*{-3pt} = \hspace*{-3pt} \siginv(dom(\nu)) \hspace*{-2pt} = \hspace*{-2pt} \siginv(\sigma(\kod{var}(\kod{\tpat}))) \hspace*{-2pt} = \hspace*{-2pt} \kod{var}(\kod{\tpat})$$

From $\model{\nu} \models \sigma^\kod{\gr}(\kod{s p o})$,
by Definition <ref>, one option of the following two holds:

\begin{multline}
\label{thm34:eq4}
\model{\nu} \models  \ppp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o})),\\ \text{if } \kod{\gr} \notin dom(\context)
\end{multline}

\begin{multline}
\label{thm34:eq5}
\model{\nu} \models \underset{i_j \in \context(\kod{\gr})} \bigvee \pp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}), i_j), \\ \text{if } \kod{\gr} \in dom(\context)
\end{multline}

From option (<ref>), by Definitions <ref>, <ref> and <ref>, it holds

$$\pppi(\valuation{\sigma(\kod{s})}{\nu}, \valuation{\sigma(\kod{p})}{\nu}, \valuation{\sigma(\kod{o})}{\nu}) = \top \text{. }$$

Therefore, by Lemma <ref>, from $\mu \povezano \nu$, it holds

$$\pppi(\valuation{\kod{s}}{\mu}, \valuation{\kod{p}}{\mu}, \valuation{\kod{o}}{\mu}) = \top \text{. }$$

Then, by Definition <ref>, it holds

$$\valuation{\kod{s}}{\mu} \kod{\,} \valuation{\kod{p}}{\mu} \kod{\,} \valuation{\kod{o}}{\mu} \in \mathit{df}(\dataq),$$

i.e. as $\kod{\gr} \notin dom(\context)$,

$$\valuation{\kod{s}}{\mu} \kod{\,} \valuation{\kod{p}}{\mu} \kod{\,} \valuation{\kod{o}}{\mu} \in \kod{\gr}.$$

From option (<ref>), there exists $i_j \in \context(\kod{\gr})$, $gr_{\kod{\,D}}(\kod{i}_j)=\kod{\gr}_j$, such that
$$\model{\nu} \models \pp(\sigma(\kod{s}), \sigma(\kod{p}), \sigma(\kod{o}), i_j).$$

By Definitions <ref>, <ref> and <ref>, it holds:

$$\ppi(\valuation{\sigma(\kod{s})}{\nu}, \valuation{\sigma(\kod{p})}{\nu}, \valuation{\sigma(\kod{o})}{\nu}, i_j) = \top.$$

Therefore, by Lemma <ref>, from $\mu \povezano \nu$, it holds

$$\ppi(\valuation{\kod{s}}{\mu}, \valuation{\kod{p}}{\mu}, \valuation{\kod{o}}{\mu}, i_j) = \top.$$

By Definition <ref>, it holds

$$\valuation{\kod{s}}{\mu} \kod{ } \valuation{\kod{p}}{\mu} \kod{ } \valuation{\kod{o}}{\mu} \in gr_{\kod{\,D}}(\siginv(i_j)),$$

$$\valuation{\kod{s}}{\mu} \kod{ } \valuation{\kod{p}}{\mu} \kod{ } \valuation{\kod{o}}{\mu} \in \kod{\gr}_j.$$

By Definition <ref>, it holds $\valuation{\kod{s}  \kod{ p }  \kod{o}}{\mu} \in \kod{\gr}_j$ for some $\kod{\gr}_j$ that forms $\kod{G}$, i.e. $\valuation{\kod{s}  \kod{ p }  \kod{o}}{\mu} \in \kod{\gr}$.
Therefore, putting all options together, by Definition <ref>, as $dom(\mu) = \kod{var}(\kod{\tpat})$, it holds

$$\mu \in \semdg{\kod{s p o}}{\ag}{\kod{G}}.$$

* $\kod{\pat}$ is $\kod{\pat}_1 . \kod{\pat}_2$

($\Rightarrow$) By Definition <ref>,

$$\mu \in \semdg{\kod{\pat}_1 . \kod{\pat}_2}{\ag}{\kod{G}} \text{ implies } \mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2}{\ag}{\kod{G}}.$$

By Definition <ref>, $\mu = \mu_1 \cup \mu_2$, where $\mu_1 \in \semdg{\kod{\pat}_1}{\ag}{\kod{G}}$, $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{G}}$ and $\mu_1 \comp \mu_2$.
By induction hypotheses on $\kod{\pat}_1$ and $\kod{\pat}_2$, mappings $\mu_1$ and $\mu_2$, and their corresponding valuations $\nu_1$ and $\nu_2$, where $\mu_1 \povezano \nu_1$ and $\mu_2 \povezano \nu_2$, it holds:[Until the end of this proof, we use notation $\sigma$ instead of $\sigma^{\kod{\gr}}$, for brevity.]

$$\model{\nu_1} \models \sigma(\kod{\pat}_1) \text{ and } \model{\nu_2} \models \sigma(\kod{\pat}_2).$$

By Lemma <ref>, from $\mu_1\comp \mu_2$, $\mu = \mu_1 \cup \mu_2$, $\mu_1 \povezano \nu_1$, $\mu_2 \povezano \nu_2$ and $\mu \povezano \nu$, it holds $\nu_1 \comp \nu_2$ and $\nu = \nu_1 \cup \nu_2$.
Therefore, $\nu \succeq \nu_1$ and $\nu \succeq \nu_2$, and it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } \model{\nu} \models \sigma(\kod{\pat}_2),$$

i.e. by Definition <ref>,

$$\model{\nu} \models \sigma(\kod{\pat}_1) \wedge \sigma(\kod{\pat}_2).$$

Then, by Definition <ref>, it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1 . \kod{\pat}_2).$$

By Definition <ref>, from $\model{\nu} \models \sigma(\kod{\pat}_1 . \kod{\pat}_2)$, it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1) \wedge \sigma(\kod{\pat}_2),$$

i.e. by Definition <ref>,

$$\model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } \model{\nu} \models \sigma(\kod{\pat}_2).$$

All free variables appearing in these two formulas belong to $var(\sigma(\kod{\pat}_1))$ and $var(\sigma(\kod{\pat}_2))$, while restrictions of $\nu$ to these domains are denoted $\nu_1$ and $\nu_2$, respectively.
Note that it holds
$$dom(\nu) = dom(\nu_1) \cup dom(\nu_2) \text{ and } \nu = \nu_1 \cup \nu_2.$$

Therefore, models $\model{\nu_1}$ and $\model{\nu_2}$ can be used in the previous formulas:

$$\model{\nu_1} \models \sigma(\kod{\pat}_1) \text{ and } \model{\nu_2} \models \sigma(\kod{\pat}_2).$$

By induction hypotheses on $\kod{\pat}_1$ and $\kod{\pat}_2$, valuations $\nu_1$ and $\nu_2$, and their corresponding mappings $\mu_1$ and $\mu_2$, such that $\mu_1 \povezano \nu_1$ and $\mu_1 \povezano \nu_1$, as $dom(\nu_1) = var(\sigma(\kod{\pat}_1))$ and $dom(\nu_2) = var(\sigma(\kod{\pat}_2))$, it holds $\mu_1 \in \semdg{\kod{\pat}_1}{\ag}{\kod{G}}$ and $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{G}}$.
By Lemma <ref>, from $\nu_1 \comp \nu_2$, $\nu = \nu_1 \cup \nu_2$, $\mu \povezano \nu$, $\mu_1 \povezano \nu_1$ and $\mu_2 \povezano \nu_2$, it holds $\mu_1 \comp \mu_2$ and $\mu = \mu_1 \cup \mu_2$.
Therefore, by Definition <ref> of $\bowtie$, it holds

$$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2}{\ag}{\kod{G}}.$$

Then, by Definition <ref>, it holds
$$\mu \in \semdg{\kod{\pat}_1.\kod{\pat}_2}{\ag}{\kod{G}}.$$

* $\kod{\pat}$ is $\kod{\pat}_1 \kod{ filter } \kod{R}$

\begin{align*}
& \mu \in \semdg{\kod{\pat}_1 \kod{ filter } \kod{R}}{\ag}{\kod{G}} \text{ iff } \hspace*{-18mm} \\
& \text{(by Def \ref{definition_sem})} & \text{ iff }  & \mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{G}} \text{ and } \\
&&& \mu \zadovoljava \kod{R} \\
& \text{(by induc.hyp.)} \hspace*{-3mm} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } \\
&&& dom(\nu)=var(\sigma(\kod{\pat}_1))  \\
&&& \text{ and } \mu \zadovoljava \kod{R} \\
& \text{(by Lemma \ref{thm:thm56})} \hspace*{-3mm} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } \\
&&& dom(\nu)=var(\sigma(\kod{\pat}_1))  \\
&&& \text{ and } \model{\nu} \models \sigma(\kod{R})\\
& \text{(by Def \ref{defn:model})} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\pat}_1) \wedge \sigma(\kod{R}) \text{ and }\\
&&& dom(\nu)=var(\sigma(\kod{\pat}_1)) \\
& \text{(by Def \ref{def:var}, as} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\pat}_1) \wedge \sigma(\kod{R}) \text{ and }\\
& ~\kod{var}(\kod{R}) \hspace*{-1mm}\subseteq\hspace*{-1mm} \kod{var}(\kod{\pat}_1) \text{)} \hspace*{-7mm} && dom(\nu)=var(\sigma(\kod{\pat})) \\
& \text{(by Def \ref{def:sigma})} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\pat}_1 \kod{ filter } \kod{R})\\
&&& dom(\nu)=var(\sigma(\kod{\pat}))
\end{align*}

* $\kod{\pat}$ is $\kod{\{\pat}_1\kod{\}}$

\begin{align*}
& \hspace*{5mm} \mu \in \semdg{\kod{\{\pat}_1\kod{\}}}{\ag}{\kod{G}} \hspace*{-3mm} & \text{ iff } \\
& \text{(by Def \ref{definition_sem})} & \text{ iff }  & \mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{G}} \\
& \text{(by induc.hyp.)} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\pat}_1) \text{ and }\\
&&& dom(\nu) = var(\sigma(\kod{\pat}_1)) \\
& \text{(by Def \ref{def:var})} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\pat}_1) \text{ and }\\
&&& dom(\nu) = var(\sigma(\kod{\{\pat}_1\kod{\}})) \\
& \text{(by Def \ref{def:sigma})} & \text{ iff }  & \model{\nu} \models \sigma(\kod{\{\pat}_1\kod{\}}) \text{ and } \\
&&& dom(\nu) = var(\sigma(\kod{\{\pat}_1\kod{\}})) \\
\end{align*}

* $\kod{\pat}$ is $\kod{\pat}_1 \kod{ diff } \kod{\pat}_2$

By Definiton <ref>, from

$$\mu \in \semdg{\kod{\pat}_1 \  \kod{ diff } \ \kod{\pat}_2}{\ag}{\kod{\gr}}$$

it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \setminus \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$
By Definition <ref>, it holds
$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$
and there is no $\mu_2$ such that
$\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$ and $\mu \comp \mu_2$.
By induction hypothesis, from $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$, for mapping $\mu$ and a corresponding valuation $\nu$ ($\mu \povezano \nu$), it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } dom(\nu) = var(\sigma(\kod{\pat}_1)).$$

Let us prove by contraposition that it holds
$\model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2)$,
i.e. let us assume

$$\model{\nu} \models \exists \overline{x} \ \sigma(\kod{\pat}_2).$$

This means that we can extend the valuation $\nu$ to all the variables from $var(\sigma(\kod{\pat}_2))$ (by adding values to the variables from $\overline{x}$), and then restrict it only to the variables from $var(\sigma(\kod{\pat}_2))$ (by removing variables from $var(\sigma(\kod{\pat}_1))$ that are not in $var(\sigma(\kod{\pat}_2))$).
Let $\nu_2$ denote such valuation.
Then, it holds

$$\model{\nu_2} \models \sigma(\kod{\pat}_2).$$

Note that it holds $\nu_2 \comp \nu$ by construction.
From the induction hypothesis applied on $\nu_2$ and a mapping $\mu_2$ such that $\mu_2 \povezano \nu_2$, it holds
$\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$.
By Lemma <ref>, from $\mu \povezano \nu$, $\mu_2 \povezano \nu_2$ and $\nu\comp \nu_2$, it holds $\mu \comp \mu_2$.
This is a contradiction with nonexistence of a mapping compatible with $\mu$ and from $\semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$.
Therefore, it holds:

$$\model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2),$$

and then by Definition <ref>

$$\model{\nu} \models \sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2).$$

By Definition <ref>, it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1 \kod{ diff } \kod{\pat}_2).$$

By Lemma <ref>, from $dom(\nu) = var(\sigma(\kod{\pat}_1))$, it holds $dom(\nu) = \sigma(\kod{var}(\kod{\pat}_1))$, and then by Definition <ref> it holds $dom(\nu) = \sigma(\kod{var}(\kod{\pat}_1 \kod{ diff } \kod{\pat}_2))$.
Therefore, by Lemma <ref>, it holds
$dom(\nu) = var(\sigma(\kod{\pat}_1 \kod{ diff } \kod{\pat}_2))$.

By Definition <ref>, from

$$dom(\nu) = var(\sigma(\kod{\pat}_1  \kod{ diff } \kod{\pat}_2)), \text{ and }$$

$$\model{\nu} \models \sigma(\kod{\pat}_1  \kod{ diff } \kod{\pat}_2)$$

it holds

$$dom(\nu) = var(\sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2)), \text{ and }$$

$$\model{\nu} \models \sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2),$$

i.e. by Definition <ref>,

$$\model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } \model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2).$$

By Definition <ref>, as $\overline{x}$ denotes all variables that appear in $\sigma(\kod{\pat}_2)$, but not in $\sigma(\kod{\pat}_1)$, it holds $dom(\nu) = var(\sigma(\kod{\pat}_1))$.
Applying the induction hypothes on the valuation $\nu$ and its corresponding mapping $\mu$ ($\mu \povezano \nu$), it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$.

It should also be proved that there does not exist a $\mu_2$ such that $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$ and $\mu_2 \comp \mu$.
This can be proved by contraposition, i.e. let us assume the existence of such a mapping $\mu_2$.
By induction hypothesis, applied on the mapping $\mu_2$ and a valuation $\nu_2$ such that $\mu_2 \povezano \nu_2$, it holds

$$\model{\nu_2} \models \sigma(\kod{\pat}_2).$$

By Lemma <ref>, from $\mu_2 \comp \mu$, $\mu \povezano \nu$ and $\mu_2 \povezano \nu_2$, it holds  $\nu_2 \comp \nu$.
Then, $\nu \cup \nu_2$ is a well defined valuation, denoted by $\nu'$.
As $\nu'$ is an extension of $\nu_2$, from $\model{\nu_2} \models \sigma(\kod{\pat}_2)$, it holds

$$\model{\nu'} \models \sigma(\kod{\pat}_2).$$

As $\nu'$ is an extension of $\nu$, from $\model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2)$, it holds

$$\model{\nu'} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2).$$

Therefore, there is an extension $\nu''$ of $\nu'$, such that

$$\model{\nu''} \models \neg \sigma(\kod{\pat}_2).$$

Also, as $\nu''$ is an extension of $\nu'$, from $\model{\nu'} \models \sigma(\kod{\pat}_2)$, it holds

$$\model{\nu''} \models \sigma(\kod{\pat}_2).$$

Therefore, $\model{\nu''}$ is a model of formula $\sigma(\kod{\pat}_2)$ and its negation as well, which is a contradiction.

As it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$ and it holds that there does not exist $\mu_2$ such that $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$ and $\mu_2 \comp \mu$, then, by Definition <ref>
$$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \setminus \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$$

Then, by Definition <ref>, it holds
$$\mu \in \semdg{\kod{\pat}_1 \  \kod{ diff } \ \kod{\pat}_2}{\ag}{\kod{\gr}}.$$

* $\kod{\pat}$ is $\kod{\pat}_1 \kod{ minus } \kod{\pat}_2$

If $\kod{var}(\kod{\pat}_1) \cap \kod{var}(\kod{\pat}_2) = \varnothing$ then:

By Definiton <ref>, from

$$\mu \in \semdg{\kod{\pat}_1 \  \kod{ minus } \ \kod{\pat}_2}{\ag}{\kod{\gr}}$$

it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} - \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$
By Definition <ref>, it holds
$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$.

By induction hypothesis, from $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$, for mapping $\mu$ and a corresponding valuation $\nu$ ($\mu \povezano \nu$), it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } dom(\nu) = var(\sigma(\kod{\pat}_1)).$$

By Definition <ref>, it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1 \kod{ minus } \kod{\pat}_2).$$

By Lemma <ref>, from $dom(\nu) = var(\sigma(\kod{\pat}_1))$, it holds $dom(\nu) = \sigma(\kod{var}(\kod{\pat}_1))$, and then by Definition <ref> it holds $dom(\nu) = \sigma(\kod{var}(\kod{\pat}_1 \kod{ minus } \kod{\pat}_2))$.
Therefore, by Lemma <ref>, it holds
$dom(\nu) = var(\sigma(\kod{\pat}_1 \kod{ minus } \kod{\pat}_2))$.

By Definition <ref>, from

$$dom(\nu) = var(\sigma(\kod{\pat}_1  \kod{ minus } \kod{\pat}_2)), \text{ and }$$

$$\model{\nu} \models \sigma(\kod{\pat}_1  \kod{ minus } \kod{\pat}_2)$$

it holds

$$dom(\nu) = var(\sigma(\kod{\pat}_1)) \text{ and } \model{\nu} \models \sigma(\kod{\pat}_1).$$

Applying the induction hypothesis on the valuation $\nu$ and its corresponding mapping $\mu$ ($\mu \povezano \nu$), it holds $\mu \hspace*{2pt} \in \hspace*{2pt} \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$ .
Therefore, by Lemma <ref>, it holds $dom(\mu) = \kod{var}(\kod{\pat}_1)$.
For all $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$, by Lemma <ref>, it holds $dom(\mu_2) = \kod{var}(\kod{\pat}_2)$.
Therefore, from $\kod{var}(\kod{\pat}_1) \cap \kod{var}(\kod{\pat}_2) = \varnothing$, for all $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$, it holds

$$dom(\mu) \cap dom(\mu_2) = \varnothing.$$

As it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$ and for all $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$ it holds $dom(\mu) \cap dom(\mu_2) = \varnothing$, then, by Definition <ref>
$$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} - \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$$

Then, by Definition <ref>, it holds
$$\mu \in \semdg{\kod{\pat}_1 \  \kod{ minus } \ \kod{\pat}_2}{\ag}{\kod{\gr}}.$$

By Definiton <ref>, from

$$\mu \in \semdg{\kod{\pat}_1 \  \kod{ minus } \ \kod{\pat}_2}{\ag}{\kod{\gr}}$$

it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} - \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$
By Definition <ref>, it holds
$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$
and there is no $\mu_2$ such that
$\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$, $\mu \comp \mu_2$ and $dom(\mu) \cap dom(\mu_2) \not= \varnothing$.
By induction hypothesis, from $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$, for mapping $\mu$ and a corresponding valuation $\nu$ ($\mu \povezano \nu$), it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } dom(\nu) = var(\sigma(\kod{\pat}_1)).$$

Let us prove by contraposition that it holds
$\model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2)$,
i.e. let us assume

$$\model{\nu} \models \exists \overline{x} \ \sigma(\kod{\pat}_2).$$

This means that we can extend the valuation $\nu$ to all the variables from $var(\sigma(\kod{\pat}_2))$ (by adding values to the variables from $\overline{x}$), and then restrict it only to the variables from $var(\sigma(\kod{\pat}_2))$ (by removing variables from $var(\sigma(\kod{\pat}_1))$ that are not in $var(\sigma(\kod{\pat}_2))$).
Let $\nu_2$ denote such valuation.
Then, it holds

$$\model{\nu_2} \models \sigma(\kod{\pat}_2).$$

Note that it holds $\nu_2 \comp \nu$ by construction.
From the induction hypothesis applied on $\nu_2$ and a mapping $\mu_2$ such that $\mu_2 \povezano \nu_2$, it holds
$\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$.
By Lemma <ref>, from $\mu \povezano \nu$, $\mu_2 \povezano \nu_2$ and $\nu\comp \nu_2$, it holds $\mu \comp \mu_2$.
By Lemma <ref>, from $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$ and $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$, it holds $dom(\mu_1) = \kod{var}(\kod{\pat}_1)$ and $dom(\mu_2) = \kod{var}(\kod{\pat}_2)$.
From $\kod{var}(\kod{\pat}_1) \cap \kod{var}(\kod{\pat}_2) \not= \varnothing$, it holds $dom(\mu_1) \cap dom(\mu_2) \not= \varnothing$.
This is a contradiction with nonexistence of a mapping compatible with $\mu$, from $\semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$ such that $dom(\mu_1) \cap dom(\mu_2) \not= \varnothing$.
Therefore, it holds:

$$\model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2),$$

and then by Definition <ref>

$$\model{\nu} \models \sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2).$$

By Definition <ref>, it holds

$$\model{\nu} \models \sigma(\kod{\pat}_1 \kod{ minus } \kod{\pat}_2).$$

By Lemma <ref>, from $dom(\nu) = var(\sigma(\kod{\pat}_1))$, it holds $dom(\nu) = \sigma(\kod{var}(\kod{\pat}_1))$, and then by Definition <ref> it holds $dom(\nu) = \sigma(\kod{var}(\kod{\pat}_1 \kod{ minus } \kod{\pat}_2))$.
Therefore, by Lemma <ref>, it holds
$dom(\nu) = var(\sigma(\kod{\pat}_1 \kod{ minus } \kod{\pat}_2))$.

By Definition <ref>, from

$$dom(\nu) = var(\sigma(\kod{\pat}_1  \kod{ minus } \kod{\pat}_2)), \text{ and }$$

$$\model{\nu} \models \sigma(\kod{\pat}_1  \kod{ minus } \kod{\pat}_2)$$

it holds

$$dom(\nu) = var(\sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2)), \text{ and }$$

$$\model{\nu} \models \sigma(\kod{\pat}_1) \wedge \forall \overline{x} \ \neg \sigma(\kod{\pat}_2),$$

i.e. by Definition <ref>,

$$\model{\nu} \models \sigma(\kod{\pat}_1) \text{ and } \model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2).$$

By Definition <ref>, as $\overline{x}$ denotes all variables that appear in $\sigma(\kod{\pat}_2)$, but not in $\sigma(\kod{\pat}_1)$, it holds $dom(\nu) = var(\sigma(\kod{\pat}_1))$.
Applying the induction hypothes on the valuation $\nu$ and its corresponding mapping $\mu$ ($\mu \povezano \nu$), it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$.

It should also be proved that there does not exist a $\mu_2$ such that $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$, $\mu_2 \comp \mu$ and $dom(\mu_2) \cap dom(\mu) \not= \varnothing$.
This can be proved by contraposition, i.e. let us assume the existence of such a mapping $\mu_2$.
By induction hypothesis, applied on the mapping $\mu_2$ and a valuation $\nu_2$ such that $\mu_2 \povezano \nu_2$, it holds

$$\model{\nu_2} \models \sigma(\kod{\pat}_2).$$

By Lemma <ref>, from $\mu_2 \comp \mu$, $\mu \povezano \nu$ and $\mu_2 \povezano \nu_2$, it holds  $\nu_2 \comp \nu$.
Then, $\nu \cup \nu_2$ is a well defined valuation, denoted by $\nu'$.
As $\nu'$ is an extension of $\nu_2$, from $\model{\nu_2} \models \sigma(\kod{\pat}_2)$, it holds

$$\model{\nu'} \models \sigma(\kod{\pat}_2).$$

As $\nu'$ is an extension of $\nu$, from $\model{\nu} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2)$, it holds

$$\model{\nu'} \models \forall \overline{x} \ \neg \sigma(\kod{\pat}_2).$$

Therefore, there is an extension $\nu''$ of $\nu'$, such that

$$\model{\nu''} \models \neg \sigma(\kod{\pat}_2).$$