# TE and TM Modes in Metallic Waveguide Filled With a Lossless and Fully
Anisotropic Medium

Wei Jiang and Jie Liu This work was supported by the National Natural Science
Foundation of China under Grant 61901131, the Natural Science Foundation of
Guizhou Minzu University under Grant GZMU[2019]YB07 and the China Postdoctoral
Science Foundation under Grant 2019M662244 _(Corresponding author: Wei
Jiang)._ W. Jiang is with the School of Mechatronics Engineering, Guizhou
Minzu University, Guiyang 550025, China (e-mail: jwmathphy@163.com). J. Liu is
with the Postdoctoral Mobile Station of Information and Communication
Engineering, School of Informatics, and Institute of Electromagnetics and
Acoustics, Xiamen University, Xiamen 361005, China (e-mail:
liujie190484@163.com).

###### Abstract

This letter gives a condition for the existence of the pure TE and TM modes in
the metallic waveguide filled with a homogeneous, fully anisotropic and
lossless medium. The condition is a relation between the permittivity and
permeability tensors of the fully anisotropic medium. The theory given in the
letter is the extension of the classic electromagnetic waveguide theory. At
last, we employ the commercial software COMSOL Multiphysics to simulate the
metallic waveguide problem filled with a homogeneous, fully anisotropic and
lossless medium. Numerical experiment shows that the condition supported in
the letter does confirm the existence of the pure TE and TM modes in the
anisotropic waveguide.

###### Index Terms:

fully anisotropic medium, metallic waveguide, pure TE mode, pure TM mode.

##  I Introduction

From the classic waveguide theory in electromagnetics [1], it is well known
that there exist the pure TE and TM modes in the metallic waveguide filled
with a homogeneous, isotropic and lossless medium. Moreover, in such a
metallic waveguide, the propagation mode is the pure TE and TM modes, instead
of EH mode. If the metallic waveguide filled with a homogenous, isotropic and
lossless medium has two independent perfect electric conductors at least, then
TEM mode will exist in the waveguide. The pure TE mode can be simulated by the
transversal components of electric field or the longitudinal component of
magnetic field. Similarly, the pure TM mode can be simulated by the
transversal components of magnetic field or the longitudinal component of
electric field. For the TE mode, if the transversal components of electric
field are applied to simulate it, then we have to solve an eigenvalue problem
of the curl-curl operator with a Dirichlet boundary condition, which is the
eigenvalue problem of a two-dimensional vector field. If the longitudinal
component of magnetic field is used to simulate the TE mode, then we have to
solve an eigenvalue problem of the Laplace operator with a Neumann boundary
condition, which is the eigenvalue problem of a scalar field. For the TM mode,
if we apply the transversal components of magnetic field to simulate it, then
we have to solve an eigenvalue problem of the curl-curl operator with two
Neumann boundary conditions, which is the eigenvalue problem of a two-
dimensional vector field. If we employ the longitudinal component of electric
field to simulate the TM mode, then we need to solve an eigenvalue problem of
the Laplace operator with a Dirichlet boundary condition, which is the
eigenvalue problem of a scalar field. The above discussion is the basic
knowledge of classic electromagnetic waveguide.
We now know that some media in nature exhibit anisotropic characteristics, for
example, bamboo, magnetized ferrite material, uniaxial crystal, biaxial
crystal and so on. In recent years, Hu _et.al_ [2] employ near-field optical
technology to quantitatively determine the full dielectric tensors of
nanometer-thin molybdenum disulfide and hexagonal boron nitride microcrystals,
the most-promising van der Waals semiconductor and dielectric. In addition,
they theoretically demonstrate the existence of the pure TE and TM mode in the
anisotropic van der Waals material. Therefore, it is worthwhile to propose the
mode theory of the metallic waveguide filled with a homogeneous, anisotropic
and lossless medium. In general, the propagation mode in the anisotropic
waveguide is EH mode, not the pure TE and TM modes because the coupling of
electromagnetic fields in an anisotropic medium is very strong. However, when
the permittivity and permeability tensors of an anisotropic medium satisfy
certain relationship, there are pure TE mode and TM mode in anisotropic
waveguide. For example, based on the Abelian group theory and the classic
electromagnetic waveguide theory, Jiang _et.al_ [3] establish a sufficient
condition which can ensure the existence of the pure TE and TM modes in the
anisotropic waveguide. On the basis of reference [3], Jiang _et.al_ [4]
propose a necessary and sufficient condition for the existence of the pure TE
and TM modes in the anisotropic waveguide. The medium considered in [3] and
[4] are only anisotropic in the plane of the waveguide cross section, and this
is to say that the medium considered in [3] and [4] is not fully anisotropic.
In this letter, to our surprising, the pure TE and TM modes may also exist in
the metallic waveguide filled with a homogeneous, fully anisotropic and
lossless medium when the permittivity and permeability tensors of the fully
anisotropic medium satisfy certain relationship, which is given in this
letter.
There are several calculation methods to analyze the propagation mode in the
waveguide. For example, the variational meshless method in conjunction with
radial basis functions can be used to solve the waveguide problem [5]. Jiang
_et. al._ [6] make use of mixed finite element method to analyze the
propagation mode in the metallic waveguide filled with anisotropic media.
Furthermore, there are many literatures about analyzing waveguide mode by edge
element method, (please see [7, 8, 9, 10] and references therein). In order to
obtain the propagation mode in the metallic waveguide filled with fully
anisotropic media, this letter simulates the waveguide problem by COMSOL
Multiphysics, in which finite element method will be used.
The outline of the letter is as follows. The governing equations for the
waveguide problem is given in Section II. In Section III, we give a necessary
condition for the existence of the pure TE and TM modes in the fully
anisotropic waveguide. In Section IV, a numerical experiment is carried out to
verify our theoretical result.

##  II Governing Equations for Waveguide Problem

Let $\overline{\overline{\epsilon}}$ and $\overline{\overline{\mu}}$ be the
permittivity and permeability tensors of an anisotropic medium, respectively.
As usual, $\overline{\overline{\epsilon}}$ and $\overline{\overline{\mu}}$ can
be written in the form of a matrix. Assume that the medium filled in the
metallic waveguide is homogeneous, lossless and fully anisotropic, then
$\overline{\overline{\epsilon}}$ and $\overline{\overline{\mu}}$ are both
Hermitian [11]. Therefore, $\overline{\overline{\epsilon}}$ and
$\overline{\overline{\mu}}$ can be written by the following form

$\displaystyle\overline{\overline{\epsilon}}=\left[\begin{array}[]{cc}\overline{\overline{\epsilon}}_{tt}&\bar{\epsilon}_{tz}\\\
\bar{\epsilon}_{tz}^{\dagger}&\epsilon_{zz}\\\
\end{array}\right],\quad\overline{\overline{\mu}}=\left[\begin{array}[]{cc}\overline{\overline{\mu}}_{tt}&\bar{\mu}_{tz}\\\
\bar{\mu}_{tz}^{\dagger}&\mu_{zz}\\\ \end{array}\right]$ (5)

where the superscript symbol ${\dagger}$ represents the complex conjugate,
$\overline{\overline{\epsilon}}_{tt}$ and $\overline{\overline{\mu}}_{tt}$ are
$2\times 2$ submatrices in the $\overline{\overline{\epsilon}}$ and
$\overline{\overline{\mu}}$ respectively. Notice that
$\overline{\overline{\epsilon}}_{tt}$ and $\overline{\overline{\mu}}_{tt}$ are
also both Hermitian.

Suppose that the electromagnetic wave in the waveguide propagates along
$+\hat{z}$ direction. For a time-harmonic field with angular frequency
$\omega>0$, we would like to seek several propagable physical modes in the
waveguide:

${{\bf E}}(x,y,z)={{\bf e}}(x,y)\textrm{e}^{-\textrm{j}k_{z}z},~{}{{\bf
H}}(x,y,z)={{\bf h}}(x,y)\textrm{e}^{-\textrm{j}k_{z}z}$ (6)

In the expression (6), $k_{z}$ is the propagation constant, which can be
applied to characterize the propagation characteristics of electromagnetic
fields in waveguide system. In the expression (6), ${{\bf e}}(x,y)$ and ${{\bf
h}}(x,y)$ are the field distribution in the waveguide system, and they are
independent with longitudinal coordinate $z$. Note that the vectors ${{\bf
e}}(x,y)$ and ${{\bf h}}(x,y)$ are composed of three components. They can be
split into transverse components and longitudinal components, and that is

$\displaystyle{{\bf e}}(x,y)={{\bf e}}_{t}(x,y)+\hat{z}e_{z}(x,y)$ (7)
$\displaystyle{{\bf h}}(x,y)={{\bf h}}_{t}(x,y)+\hat{z}h_{z}(x,y)$ (8)

In order to analyze the propagable modes in the waveguide, three-dimensional
del operator $\nabla$ needs to be split into transverse components and
longitudinal component, and that is

$\displaystyle\nabla=\nabla_{t}+\hat{z}{{\partial}\over{\partial
z}},~{}~{}~{}\nabla_{t}=\hat{x}{{\partial}\over{\partial
x}}+\hat{y}{{\partial}\over{\partial y}}.$ (9)

Since there is no source distribution in the waveguide, then the
electromagnetic field in the waveguide must satisfy the source-free Maxwell’s
equations

$\displaystyle\nabla\times{{\bf
E}}=-\textrm{j}\omega\overline{\overline{\mu}}{{\bf H}}\mbox{~{}in~{}}\Gamma$
(10a) $\displaystyle\nabla\times{{\bf
H}}=\textrm{j}\omega\overline{\overline{\epsilon}}{{\bf
E}}\mbox{~{}in~{}}\Gamma$ (10b) $\displaystyle\hat{n}\times{{\bf
E}}={\bf{0}}\mbox{~{}on~{}}\partial\Gamma$ (10c)
$\displaystyle\hat{n}\cdot(\overline{\overline{\mu}}{{\bf
H}})=0\mbox{~{}on~{}}\partial\Gamma$ (10d)

where $\Gamma$ is the cross section of a given waveguide and $\partial\Gamma$
is the boundary of the cross section $\Gamma$.

By substituting (5)-(9) into (10a) and (10b), one can obtain the following
partial differential equations (PDEs):

$\displaystyle\nabla_{t}\times{{\bf
e}}_{t}=-\textrm{j}\omega(\bar{\mu}_{tz}^{\dagger}{{\bf
h}}_{t}+\mu_{zz}h_{z})\hat{z}\mbox{~{}in~{}}\Gamma$ (11)
$\displaystyle-\hat{z}\times\nabla_{t}e_{z}-jk_{z}\hat{z}\times{{\bf
e}}_{t}=-\textrm{j}\omega(\overline{\overline{\mu}}_{tt}{{\bf
h}}_{t}+\bar{\mu}_{tz}h_{z})\mbox{~{}in~{}}\Gamma$ (12)
$\displaystyle\nabla_{t}\times{{\bf
h}}_{t}=\textrm{j}\omega(\bar{\epsilon}_{tz}^{\dagger}{{\bf
e}}_{t}+\epsilon_{zz}e_{z})\hat{z}\mbox{~{}in~{}}\Gamma$ (13)
$\displaystyle-\hat{z}\times\nabla_{t}h_{z}-jk_{z}\hat{z}\times{{\bf
h}}_{t}=\textrm{j}\omega(\overline{\overline{\epsilon}}_{tt}{{\bf
e}}_{t}+\bar{\epsilon}_{tz}e_{z})\mbox{~{}in~{}}\Gamma$ (14)

A counterclockwise rotation matrix $R=\begin{bmatrix}0&-1\\\ 1&0\\\
\end{bmatrix}$ is introduced for the purpose of mode analysis, and the matrix
$R$ exactly coincides with the rotation transformation $\hat{z}\times$ in the
$xy$-plane. After changing the $\hat{z}\times$ in (12) and (14) into the
matrix $R$, we can get the matrix system

$\displaystyle\textrm{j}k_{z}{{\bf e}}_{t}+j\omega
R\overline{\overline{\mu}}_{tt}{{\bf h}}_{t}=-\nabla_{t}e_{z}-\textrm{j}\omega
R\bar{\mu}_{tz}h_{z}~{}~{}~{}$ (15a) $\displaystyle-\textrm{j}\omega
R\overline{\overline{\epsilon}}_{tt}{{\bf e}}_{t}+\textrm{j}k_{z}{{\bf
h}}_{t}=\textrm{j}\omega R\bar{\epsilon}_{tz}e_{z}-\nabla_{t}h_{z}~{}~{}~{}$
(15b) Define ${\bf{f}}_{1}=-\nabla_{t}e_{z}-\textrm{j}\omega
R\bar{\mu}_{tz}h_{z},~{}{\bf{f}}_{2}=\textrm{j}\omega
R\bar{\epsilon}_{tz}e_{z}-\nabla_{t}h_{z}.$

From (15), it is easy to obtain the following equations:

$\displaystyle(-k_{z}^{2}\overline{\overline{I}}_{2}-\omega^{2}R\overline{\overline{\mu}}_{tt}R\overline{\overline{\epsilon}}_{tt}){{\bf
e}}_{t}=\textrm{j}k_{z}{\bf{f}}_{1}-\textrm{j}\omega
R\overline{\overline{\mu}}_{tt}{\bf{f}}_{2}$ (16)
$\displaystyle(-k_{z}^{2}\overline{\overline{I}}_{2}-\omega^{2}R\overline{\overline{\epsilon}}_{tt}R\overline{\overline{\mu}}_{tt}){{\bf
h}}_{t}=\textrm{j}\omega
R\overline{\overline{\epsilon}}_{tt}{\bf{f}}_{1}+\textrm{j}k_{z}{\bf{f}}_{2}$
(17)

where $\overline{\overline{I}}_{2}$ is second-order identity matrix. Set

$\displaystyle{{\bf F}}_{1}=\textrm{j}k_{z}{\bf{f}}_{1}-\textrm{j}\omega
R\overline{\overline{\mu}}_{tt}{\bf{f}}_{2},~{}{{\bf F}}_{2}=\textrm{j}\omega
R\overline{\overline{\epsilon}}_{tt}{\bf{f}}_{1}+\textrm{j}k_{z}{\bf{f}}_{2}$
$\displaystyle{{\bf
N}}_{1}=-k_{z}^{2}\overline{\overline{I}}_{2}-\omega^{2}R\overline{\overline{\mu}}_{tt}R\overline{\overline{\epsilon}}_{tt},~{}{{\bf
N}}_{2}=-k_{z}^{2}\overline{\overline{I}}_{2}-\omega^{2}R\overline{\overline{\epsilon}}_{tt}R\overline{\overline{\mu}}_{tt}$

The conclusion that $\det({{\bf N}}_{1})=\det({{\bf N}}_{2})$ can be proved by
the basis knowledge in linear algebra. When $\det({{\bf N}}_{1})=\det({{\bf
N}}_{2})\neq 0$, then from (16) and (17), one can get

$\displaystyle{{\bf e}}_{t}={{\bf N}}_{1}^{-1}{{\bf F}}_{1},~{}~{}{{\bf
h}}_{t}={{\bf N}}_{2}^{-1}{{\bf F}}_{2}.$ (18)

Substituting (18) into (11) and (13) respectively, we have

$\displaystyle\nabla_{t}\times({{\bf N}}_{1}^{-1}{{\bf
F}}_{1})=-\textrm{j}\omega(\bar{\mu}_{tz}^{\dagger}{{\bf N}}_{2}^{-1}{{\bf
F}}_{2}+\mu_{zz}h_{z})\hat{z}$ (19) $\displaystyle\nabla_{t}\times({{\bf
N}}_{2}^{-1}{{\bf F}}_{2})=\textrm{j}\omega(\bar{\epsilon}_{tz}^{\dagger}{{\bf
N}}_{1}^{-1}{{\bf F}}_{1}+\epsilon_{zz}e_{z})\hat{z}$ (20)

It is clear that (19) and (20) are only the PDEs for the longitudinal
components $(e_{z},h_{z})$ of the electromagnetic field.

##  III The Condition for the Existence of the Pure TE and TM Modes

The condition for the existence of the pure TE and TM modes is that (19) and
(20) are decoupled with respect to the unknown functions $e_{z}$ and $h_{z}$.

From [4], when $\bar{\epsilon}_{tz}=\bar{\mu}_{tz}=0$, the sufficient and
necessary condition is that ${{\bf N}}_{1}$ and ${{\bf N}}_{2}$ are two scalar
matrices. As a consequence, if (19) and (20) are decoupled, then ${{\bf
N}}_{1}$ and ${{\bf N}}_{2}$ must be two scalar matrices. Otherwise, the
equations (19) and (20) will be coupled if ${{\bf N}}_{1}$ and ${{\bf N}}_{2}$
are not two scalar matrices, which shows that the propagation mode in the
waveguide is EH mode, instead of the pure TE and TM modes. When ${{\bf
N}}_{1}$ and ${{\bf N}}_{2}$ are two scalar matrices, then ${{\bf
N}}_{1}={{\bf N}}_{2}$ is valid [4]. In this case, it is very easy to know
$-\omega^{2}A\overline{\overline{\mu}}_{tt}A\overline{\overline{\epsilon}}_{tt}=-\omega^{2}A\overline{\overline{\epsilon}}_{tt}A\overline{\overline{\mu}}_{tt}$
are also two scalar matrices. Set

$\displaystyle-\omega^{2}R\overline{\overline{\mu}}_{tt}R\overline{\overline{\epsilon}}_{tt}=-\omega^{2}R\overline{\overline{\epsilon}}_{tt}R\overline{\overline{\mu}}_{tt}=k^{2}\overline{\overline{I}}_{2}$
(21) $\displaystyle{{\bf N}}_{1}={{\bf
N}}_{2}=(k^{2}-k_{z}^{2})\overline{\overline{I}}_{2}=k_{t}^{2}\overline{\overline{I}}_{2},$
(22)

where $k$ and $k_{t}$ are called the medium and cut-off wavenumbers in an
anisotropic and lossless medium, respectively. It is impossible to define the
medium and cut-off wavenumbers in a general anisotropic medium, in which (21)
and (22) are not valid.

Suppose that ${{\bf N}}_{1}$ and ${{\bf N}}_{2}$ are two scalar matrices, then
${{\bf N}}_{1}={{\bf N}}_{2}$. In this case, PDEs (19) and (20) can be reduced
to the following PDEs:

$\displaystyle\nabla_{t}\times{{\bf
F}}_{1}=-\textrm{j}\omega(\bar{\mu}_{tz}^{\dagger}{{\bf
F}}_{2}+\mu_{zz}h_{z}k_{t}^{2})\hat{z}$ (23)
$\displaystyle\nabla_{t}\times{{\bf
F}}_{2}=\textrm{j}\omega(\bar{\epsilon}_{tz}^{\dagger}{{\bf
F}}_{1}+\epsilon_{zz}e_{z}k_{t}^{2})\hat{z}$ (24)

For the pure TM modes, we need to set $h_{z}=0$ in (23) and (24), and then
obtain

$\displaystyle\quad~{}\nabla_{t}\times(R\overline{\overline{\mu}}_{tt}R\bar{\epsilon}_{tz}e_{z})$
$\displaystyle=[\bar{\mu}_{tz}^{\dagger}(-R\overline{\overline{\epsilon}}_{tt}\nabla_{t}e_{z}+\textrm{j}k_{z}R\bar{\epsilon}_{tz}e_{z})]\hat{z}$
(25)
$\displaystyle\quad\nabla_{t}\times(-R\overline{\overline{\epsilon}}_{tt}\nabla_{t}e_{z}+\textrm{j}k_{z}R\bar{\epsilon}_{tz}e_{z})$
$\displaystyle=[\bar{\epsilon}_{tz}^{\dagger}(-\textrm{j}k_{z}\nabla_{t}e_{z}+\omega^{2}R\overline{\overline{\mu}}_{tt}R\bar{\epsilon}_{tz}e_{z})+\epsilon_{zz}e_{z}k_{t}^{2}]\hat{z}$
(26)

The equation (26) together with boundary condition can be applied to simulate
the pure TM mode. Obviously, (25) must be a trivial equation. Hence, we have

$\displaystyle\bar{\mu}_{tz}^{\dagger}R\bar{\epsilon}_{tz}=0$ (27)
$\displaystyle(\overline{\overline{\mu}}_{tt}R\bar{\epsilon}_{tz})^{T}=-\bar{\mu}_{tz}^{\dagger}R\overline{\overline{\epsilon}}_{tt}$
(28)

where the superscript $T$ stands for the transpose of a given matrix.
Similarly, if the pure TE modes exist in the waveguide, one can get

$\displaystyle\bar{\epsilon}_{tz}^{\dagger}R\bar{\mu}_{tz}$ $\displaystyle=$
$\displaystyle 0$ (29)
$\displaystyle(\overline{\overline{\epsilon}}_{tt}R\bar{\mu}_{tz})^{T}$
$\displaystyle=$
$\displaystyle-\bar{\epsilon}_{tz}^{\dagger}R\overline{\overline{\mu}}_{tt}$
(30)

When $\overline{\overline{\epsilon}}$ and $\overline{\overline{\mu}}$ are two
real matrices, it is very easy to prove that (27)-(28) are valid if and only
if (29)-(30) are valid.

We take $\overline{\overline{\epsilon}}$ and $\overline{\overline{\mu}}$ as
the following way:

$\overline{\overline{\epsilon}}=\begin{bmatrix}a_{11}&a_{12}&a_{13}\\\
a_{12}&a_{22}&a_{23}\\\
a_{13}&a_{23}&a_{33}\end{bmatrix}\nu_{1},~{}~{}\overline{\overline{\mu}}=\begin{bmatrix}a_{11}&a_{12}&a_{13}\\\
a_{12}&a_{22}&a_{23}\\\ a_{13}&a_{23}&b_{33}\end{bmatrix}\nu_{2}$ (31)

Figure 1: The magnitude of the electromagnetic transverse and longitudinal
components for the first mode.. $k_{z}^{(1)}=16.112$ rad/m. The unit of the
electric field amplitude is V/m. The unit of the magnetic field amplitude is
A/m. (a) $e_{z}^{(1)}$. (b) $h_{z}^{(1)}$. (c) ${{\bf e}}_{t}^{(1)}$. (d)
${{\bf h}}_{t}^{(1)}$.

Figure 2: The magnitude of the electromagnetic transverse and longitudinal
components for the second mode. $k_{z}^{(2)}=28.762$ rad/m. The unit of the
electric field amplitude is V/m. The unit of the magnetic field amplitude is
A/m. (a) $e_{z}^{(2)}$. (b) $h_{z}^{(2)}$. (c) ${{\bf e}}_{t}^{(2)}$. (d)
${{\bf h}}_{t}^{(2)}$.

where $a_{ik}$, $b_{33}$, $\nu_{1}$ and $\nu_{2}$ are all nonzero real
numbers, such that $\overline{\overline{\epsilon}}$ and
$\overline{\overline{\mu}}$ are two symmetric positive definite matrices. It
is easy to verify that (27)-(30) holds if $\overline{\overline{\epsilon}}$ and
$\overline{\overline{\mu}}$ are of the form (31). In next section, by a
numerical experiment, we verify that there exist the pure TE modes and TM
modes in the metallic waveguide filled with a homogenous, fully anisotropic
and lossless medium provided that $\overline{\overline{\epsilon}}$ and
$\overline{\overline{\mu}}$ satisfy the condition (31).

##  IV Numerical Example

It is very difficult to directly solve PDEs (10) by a numerical method. Hence,
after eliminating the magnetic field ${{\bf H}}$ in PDEs (10), we get the
following PDEs:

$\displaystyle\nabla\times\big{(}\overline{\overline{\mu}}^{-1}\nabla\times{{\bf
E}}\big{)}=\omega^{2}\overline{\overline{\epsilon}}{{\bf
E}}\mbox{~{}in~{}}\Gamma$ (32a) $\displaystyle\hat{n}\times{{\bf
E}}={\bf{0}}\mbox{~{}on~{}}\partial\Gamma$ (32b)

where ${{\bf E}}=[{{\bf
e}}_{t}(x,y)+\hat{z}e_{z}(x,y)]\textrm{e}^{-\textrm{j}k_{z}z}$ are unknown.
Once ${{\bf E}}$ is obtained by a numerical method, then ${{\bf
H}}=\textrm{j}\omega^{-1}\overline{\overline{\mu}}^{-1}\nabla\times{{\bf E}}$.
Due to the length of this letter, only one numerical experiment will be
considered in the section. Assume that the cross section $\Gamma$ of the
waveguide is a rectangle, whose length and width are 15 mm $\times$ 10 mm,
respectively. Furthermore, assume that the medium parameters
$\overline{\overline{\epsilon}}$ and $\overline{\overline{\mu}}$ of the
lossless and fully anisotropic medium in the metallic waveguide are of the
following form

$\overline{\overline{\epsilon}}=\begin{bmatrix}2&1&1\\\ 1&4&1\\\
1&1&2\end{bmatrix}\epsilon_{0},\quad\overline{\overline{\mu}}=\begin{bmatrix}4&2&2\\\
2&8&2\\\ 2&2&8\end{bmatrix}\mu_{0},$ (33)

where $\epsilon_{0}$ and $\mu_{0}$ are the permittivity and permeability of
free space, respectively. It is clear that (33) satisfy the above condition
(31). Set $k_{0}=\omega\sqrt{\epsilon_{0}\mu_{0}}=16$ $\textrm{m}^{-1}$.

Subject on all the numerical methods to solve PDEs (32), the finite element
method is most suitable for solving this kind of electromagnetic eigenvalue
problem. Therefore, COMSOL Multiphysics is employed to numerically simulate
the problem (32). In COMSOL Multiphysics, we use uniform rectangular division,
and divide $\Gamma$ into 532 congruent rectangles. In addition, the edge basis
function of three-order on rectangular element is used to discretize ${{\bf
e}}_{t}$ and the nodal basis function associated with standard cubic element
on rectangular element is used to discretize $e_{z}$. As seen from the
numerical results of COMSOL, there are eight propagable physical modes. Here,
the field distribution of the first and second propagable mode are listed in
Fig. 1 and Fig. 2, respectively.

From Fig.1(b), it can be observed that $h_{z}^{(1)}\approx 0$, which implies
that the first propagable mode is just a TM mode. From Fig.2(a), it can be
observed that $e_{z}^{(2)}\approx 0$, which implies that the second propagable
mode is just a TE mode. According to the numerical results of this example,
the proposed condition (31) does confirm the existence of the pure TE and TM
modes in the anisotropic waveguide.

##  V Conclusion

If the permittivity and permeability tensors of the lossless and fully
anisotropic material in the metallic waveguide is given by (31), then the pure
TE and TM modes will exist in this anisotropic waveguide as long as the
frequency of electromagnetic wave. This theory extends the classic
electromagnetic waveguide theory.

## References

  * [1] C. A. Balanis, _Advanced Engineering Electromagnetics_. New York: Wiley, 2013.
  * [2] D. Hu, X. Yang, et al., “Probing optical anisotropy of nanometer-thin van der waals microcrystals by near-field imaging,” _Nature Communications_ , vol. 8, no. 1, 2107.
  * [3] W. Jiang, J. Liu, Q. Li, T. Xia, X. Hu, and Q. H. Liu, “Are there the pure TE and TM modes in the closed waveguide filled with a homogeneous, anisotropic and lossless medium?” _IEEE Trans. Antennas Propag._ , vol. 66, no. 5, pp. 2439–2448, Mar. 2018.
  * [4] W. Jiang, J. Liu, T. Xia, N. Liu, and Q. H. Liu, “A necessary and sufficient condition for having independent TE and TM modes in an anisotropic waveguide,” _IEEE Trans. Microw. Theory Techn._ , vol. 65, no. 10, pp. 3660–3670, 2017.
  * [5] V. Lombardi, M. Bozzi, and L. Perregrini, “Mode matching analysis of waveguide components exploiting the variational meshless method,” _IEEE Microwave and Wireless Components Letters_ , vol. 29, no. 10, pp. 631–633, 2019\.
  * [6] W. Jiang, J. Liu, X. Xiong, and X. Hu, “Mixed finite-element method for the closed waveguide problem filled with anisotropic media,” _IEEE Trans. Magn._ , vol. 54, no. 4, pp. 1–7, 2018.
  * [7] M. Koshiba and K. Inoue, “Simple and efficient finite-element analysis of microwave and optical waveguides,” _IEEE Trans. Microw. Theory Techn._ , vol. 40, no. 2, pp. 371–377, Feb 1992.
  * [8] I. Bardi, O. Biro, K. Preis, G. Vrisk, and K. R. Richter, “Nodal and edge element analysis of inhomogeneously loaded waveguides,” _IEEE Trans. Magn._ , vol. 29, no. 2, pp. 1466–1469, Mar 1993.
  * [9] L. Zhou and L. E. Davis, “Finite-element method with edge elements for waveguides loaded with ferrite magnetized in arbitrary direction,” _IEEE Trans. Microw. Theory Techn._ , vol. 44, no. 6, pp. 809–815, Jun 1996\.
  * [10] L. Nuno, J. V. Balbastre, and H. Castane, “Analysis of general lossy inhomogeneous and anisotropic waveguides by the finite-element method (FEM) using edge elements,” _IEEE Trans. Microw. Theory Techn._ , vol. 45, no. 3, pp. 446–449, Mar 1997.
  * [11] W. C. Chew, _Waves and Fields in Inhomogeneous Media_. New York: Van Nostrand Reinhold, 1990.


J(\bar{a}|_{\textrm{dom}(\rho)})$, which must exist since the length of the
tuples in $\mathcal{K}^{n}(s)$ is bounded from above by the maximum arity of
relation symbols $w$, and $K>w$. By definition, $\mathcal{K}^{n+1}(t)$
contains a tuple $\bar{b}$ whose $i^{\textit{th}}$ component $b_{i}$ is
defined as:

$b_{i}=\left\\{\begin{array}[]{l@{\;}l}a_{\ell}&\textrm{ if
}(x_{\ell},x_{i})\in\rho\\\ f^{j}_{s,\rho,t,i}(\bar{a}|_{{\sf
dom}(\rho)}/_{1})&\textrm{ if
}x_{i}\notin\textrm{img}(\rho).\end{array}\right.$

By Lemma 8, ${\sf tp}_{\mathfrak{B},\widehat{\Sigma}}(\bar{b})=t$. Thus,
$\bar{b}$ witnesses that
$\mathfrak{B}\models\exists\bar{y}\,(\gamma\wedge\psi)[\bar{a}]$, as required.
∎

######  Lemma 10.

$\mathfrak{B}$ satisfies Conditions 1-4 from Lemma 1.

###### Proof.

Notice that in the case $\Delta=A$, we defined $\mathfrak{B}=\mathfrak{A}$ and
the conditions are trivially satisfied. We verify each condition for the case
$\Delta\subsetneq A$:

  1. 1.

We exhibit an upper bound on the size of $B$. We recall that $w\geq 2$ is the
maximal arity of predicates from $\phi$ and we let $p\geq 1$ be the number of
predicates occurring in $\phi$. Let us denote $T$ the number of types on
$\widehat{\Sigma}$. Since each $n$-type on $\widehat{\Sigma}$ is essentially
an interpretation over domain $\Delta\cup\\{x_{1},\dots,x_{n}\\}$, there are
at most $2^{{p({\left|{\Delta}\right|}+n)}^{w}}$ distinct $n$-types on
$\widehat{\Sigma}$. The type of a maximally guarded tuple from $\mathfrak{A}$
is a $n$-type on $\widehat{\Sigma}$ for some $n\leq w$, thus we obtain:

$T\leq\sum_{n=0}^{w}2^{{p({\left|{\Delta}\right|}+n)}^{w}}\leq
2^{{pw({\left|{\Delta}\right|}+w)}^{w}}.$

Now, notice $B$ is split between elements from $\Delta$ and those composed of
constant symbols $c^{j}_{t,i}$ and of functions symbols $f^{j}_{s,\rho,t,i}$.
The number of such partial bijection $\rho$ from $\\{x_{1},\dots,x_{m}\\}$ to
$\\{x_{1},\dots,x_{n}\\}$, assuming $s$ is a $m$-type and $t$ an $n$-type, is
bounded by $(w+1)^{w}$ thus by $2^{w^{2}}$. Recall that superscript $j$ ranges
over $1,\dots,K$, with $K=w^{4}$, and $i$ over $1,\dots,w$. Therefore, the
number $C$ of constant symbols $c^{j}_{t,i}$ is at most $Tw^{5}$, and the
number $F$ of function symbols at most $T^{2}2^{w^{6}}$. Because of the
truncation mechanism, every non-$\Delta$ element $e$ of $B$ can be determined
by a function that assigns to each node of the complete tree with depth $2$
and branching degree $w$, either a constant symbol, a function symbol, or a
special value indicating that this node is not needed to describe $e$. It
follows that there are at most $(C+F+1)^{w^{3}}$ non-$\Delta$ elements in $B$.
Therefore, unraveling the bounds on $C$ and $F$, we get:

${\left|{B}\right|}\leq{\left|{\Delta}\right|}+(Tw^{5}+T^{2}2^{w^{6}}+1)^{w^{3}},$

which we can abruptly bound with:

${\left|{B}\right|}\leq{\left|{\Delta}\right|}+2^{w^{9}}T^{w^{5}}.$

Now, unraveling the bound on $T$, we obtain:

${\left|{B}\right|}\leq{\left|{\Delta}\right|}+2^{w^{9}+{pw^{6}({\left|{\Delta}\right|}+w)}^{w}},$

which we can further bound by:

${\left|{B}\right|}\leq 2^{p({\left|{\Delta}\right|}+w)^{w+10}}.$

This exhibits a double-exponential dependency w.r.t. the maximal arity, but
only single-exponential dependency in terms of the number of predicates and
the size of $\Delta$. Now, using $p,w\leq{\left|{\phi}\right|}$, we can
slightly simplify this bound as:

${\left|{B}\right|}\leq
2^{({\left|{\Delta}\right|}+{\left|{\phi}\right|})^{{\left|{\phi}\right|}+11}}.$

  2. 2.

Let $a\in\Delta$. From $\Delta\subsetneq A$, we have that ${\sf
gtp}(\mathfrak{A})$ is non-empty. In particular, there is a type $t\in{\sf
gtp}(\mathfrak{A})$. Since $a$ is treated as a constant symbol by types on
$\widehat{\Sigma}$, we have $\alpha\in{\sf
tp}^{1}_{\mathfrak{A},\widehat{\Sigma}}(a)$ iff $\alpha[a]\in t$. In
particular, if $\alpha$ is positive literal, that is an atom, then
$\alpha\in{\sf tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(a)$. Furthermore, the
above equivalence holds for all type $t$ on $\widehat{\Sigma}$ from ${\sf
gtp}(\mathfrak{A})$, which guarantees that no other atom only involving $a$
occurs in ${\sf tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(a)$, thus ${\sf
tp}^{1}_{\mathfrak{A},\widehat{\Sigma}}(a)={\sf
tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(a)$.

  3. 3.

($\subseteq$). Let $t\in{\sf
tp}^{1}_{\mathfrak{A},\widehat{\Sigma}}(A\setminus\Delta)$. By definition,
there exists $e\in A\setminus\Delta$ with ${\sf
tp}^{1}_{\mathfrak{A},\widehat{\Sigma}}(e)=t$. Since $e\in A\setminus\Delta$,
there must exist some $\bar{a}\in{\sf mgt}(\mathfrak{A})$ such that $a_{i}=e$
for some $i$. Let $s={\sf tp}_{\mathfrak{A},\widehat{\Sigma}}(\bar{a})$. We
now prove that the element $c^{1}_{s,i}$, belonging to $B\setminus\Delta$, has
unary type ${\sf tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(c^{1}_{s,i})=t$.
Notice $s$ fully determines the unary type of its variable $x_{i}$ variable,
that is $t$. Thus, since
$(c^{1}_{s,1},\dots,c^{1}_{s,{\left|{\bar{a}}\right|}})\in\mathcal{K}^{0}(s)$
and from the definition of $\cdot^{\mathfrak{B}}$, every atom of $t$ is in
${\sf tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(c^{1}_{s,i})$. Lemma 8
guarantees there are no other atom in ${\sf
tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(c^{1}_{s,i})$, thus ${\sf
tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(c^{1}_{s,i})=t$.

($\supseteq$). Let $t\in{\sf
tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(B\setminus\Delta)$. By definition,
there exists $e\in B\setminus\Delta$ with ${\sf
tp}^{1}_{\mathfrak{B},\widehat{\Sigma}}(e)=t$. By definition of $B$, there
must exist a type $s\in{\sf gtp}(\mathfrak{A})$, an integer $m$ and a tuple
$\bar{a}\in\mathcal{K}^{m}(s)$ s.t. $a_{i}=e$ for some $i$. Since $s\in{\sf
gtp}(\mathfrak{A})$, there exists $\bar{b}\in{\sf mgt}(\mathfrak{A})$ such
that ${\sf tp}_{\mathfrak{A},\widehat{\Sigma}}(\bar{b})=s$. In particular,
$b_{i}\in A\setminus\Delta$, and it is easily verified that ${\sf
tp}^{1}_{\mathfrak{A},\widehat{\Sigma}}(b_{i})=t$.

  4. 4.

From the very definition of $B$, resp. of $\mathfrak{B}$, we have
$\Delta\subseteq B$, resp. $c^{\mathfrak{B}}=c^{\mathfrak{A}}$ for all
$c\in{\sf const}(\phi)$, as desired.

∎

##  Appendix D Proofs for Section 4.2

We start with explaining why it is not straightfoward to prove finite
controllability of circumscribed (U)CQ-querying in GF using the Rosati cover.
The whole point of using the Rosati cover in (?) is to start from a model
$\mathfrak{A}$ that satisfies a GF sentence $\varphi$ while not satisfying a
Boolean CQ $q$, and to convert it into a finite model $\mathfrak{B}$ with the
same properties. This only works, however, under the assumption that the
original model $\mathfrak{A}$ does not satisfy any ‘treeifications’ of $q$,
that is, there is no homomorphism $h$ from $q$ to $\mathfrak{A}$ such that the
homomorphic image of $q$ under $h$ is acyclic. In the case without
circumscription as in (?), this assumption is for free since we can simply
take $\mathfrak{A}$ to be a model of the GF sentence
$\varphi\wedge\neg\chi_{q}$ where $\chi_{q}$ is the disjunction of all
treeifications of $q$. This works, because, trivially, a model of
$\varphi\wedge\chi_{q}$ is also a model of $\varphi$. With circumscription,
however, we would need the same statement for _minimal_ models and it is easy
to find examples which falsify this.

###  D.1 Proof of Lemma 3

See 3

###### Proof.

Assume to the contrary of what is to be shown that $\mathfrak{B}$ is not a
${\sf CP}$-minimal model of $\phi$. As $\mathfrak{B}$ is a model of $\phi$ by
assumption, there is thus a model $\mathfrak{B}^{\prime}$ of $\phi$ with
$\mathfrak{B}^{\prime}<_{\sf CP}\mathfrak{B}$ (and thus $B^{\prime}=B$). To
derive a contradiction, we construct a model $\mathfrak{A}^{\prime}$ of $\phi$
with $\mathfrak{A}^{\prime}<_{\sf CP}\mathfrak{A}$.

Applying Proposition 3 to $\mathfrak{B}^{\prime}$ and $\Sigma$, we obtain a
model $\mathfrak{B}^{\prime\prime}$ of $\phi$ such that the following
conditions are satisfied:

  1. (a)

$|B^{\prime\prime}|\leq{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$;

  2. (b)

${\sf tp}^{1}_{\Sigma}({\mathfrak{B}^{\prime\prime}})={\sf
tp}^{1}_{\Sigma}(\mathfrak{B}^{\prime})$;

  3. (c)

$\\#_{\mathfrak{B}^{\prime\prime}}(t)\leq\\#_{\mathfrak{B}^{\prime}}(t)$ for
every 1-type $t$ on $\Sigma$;

  4. (d)

$c^{\mathfrak{B}^{\prime\prime}}=c^{\mathfrak{B}^{\prime}}$ for all constants
$c$ in $\phi$.

To assemble the desired model $\mathfrak{A}^{\prime}$, we first determine the
intended 1-type of each element $a$ of $\mathfrak{A}^{\prime}$. To this end,
we define a surjection from $A$ to $B^{\prime\prime}$ which is obtained as the
union of several mappings exposed as follows.

For each $t\in{\sf tp}^{1}_{\Sigma}(\mathfrak{A})$ s.t.
$\\#_{\mathfrak{A}}(t)\leq{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$, we set:

$\displaystyle D_{t}$ $\displaystyle:=\\{t\in A\mid{\sf
tp}^{1}_{\mathfrak{A},\Sigma}(a)=t\\}$ $\displaystyle S_{t}$
$\displaystyle:=\\{b\in\mathfrak{B}^{\prime\prime}\mid\exists b^{\prime}\in
B^{\prime},{\sf tp}^{1}_{\mathfrak{B},\Sigma}(b^{\prime})=t$
$\displaystyle\hskip 56.9055pt\wedge{\sf
tp}^{1}_{\mathfrak{B}^{\prime},\Sigma}(b^{\prime})={\sf
tp}^{1}_{\mathfrak{B}^{\prime\prime},\Sigma}(b)\\}$

Note that by definition ${\left|{D_{t}}\right|}=\\#_{\mathfrak{A}}(t)>{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$ while
${\left|{S_{t}}\right|}\leq{\left|{B^{\prime\prime}}\right|}\leq{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$ from Condition
(a) in the definition of $\mathfrak{B}^{\prime\prime}$. We can thus chose
$\pi_{t}:D_{t}\rightarrow S_{t}$ a surjective mapping.

We now form the union $\pi_{0}$ of all mappings $\pi_{t}$ s.t.
$\\#_{\mathfrak{A}}(t)\leq{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$. Note that the
domain of $\pi_{0}$ is $A\setminus\mathsf{core}_{\Sigma}(\mathfrak{A})$, and
that its range is exactly the elements from $B^{\prime\prime}$ whose type in
$\mathfrak{B}^{\prime\prime}$ is realized in $\mathfrak{B}^{\prime}$ at least
once outside of $\mathsf{core}_{\Sigma}(\mathfrak{A})$. Thus, the remaining
elements that need to be reached to cover all of $B^{\prime\prime}$ are those
whose type in $\mathfrak{B}^{\prime\prime}$ is realized in
$\mathfrak{B}^{\prime}$ exclusively in $\mathsf{core}_{\Sigma}(\mathfrak{A})$.
Let us denote the set of those latter types $S$. For each $t$ in $S$, it
follows from Point (c) in the definition of $\mathfrak{B}^{\prime\prime}$,
that we can pick a surjection $\sigma_{t}:\\{b\in B^{\prime}\mid{\sf
tp}^{1}_{\mathfrak{B}^{\prime},\Sigma}(b)=t\\}\rightarrow\\{b\in
B^{\prime\prime}\mid{\sf
tp}^{1}_{\mathfrak{B}^{\prime\prime},\Sigma}(b)=t\\}$. We complete $\pi_{0}$
into $\pi_{1}$ by adding to $\pi_{0}$ the union of all mappings $\sigma_{t}$
for $t\in S$. Note that the range of $\pi_{1}$ is already the whole
$B^{\prime\prime}$, but that it’s domain is still missing those elements of
$\mathsf{core}_{\Sigma}(\mathfrak{A})$ whose type in $\mathfrak{B}^{\prime}$
is not among $S$. To complete $\pi_{1}$ we simply pick, for each such
$a\in\mathsf{core}_{\Sigma}(\mathfrak{A})$ s.t. ${\sf
tp}^{1}_{\mathfrak{B}^{\prime},\Sigma}(a)\notin S$ an element $b\in
B^{\prime\prime}$ s.t. ${\sf tp}^{1}_{\mathfrak{B}^{\prime},\Sigma}(a)={\sf
tp}^{1}_{\mathfrak{B}^{\prime\prime},\Sigma}(b)$. We denote $\pi$ the
resulting surjection from $A$ to $B^{\prime\prime}$.

Since $\pi$ is surjective, we can pick a partial inverse function:
$\rho:B^{\prime\prime}\rightarrow A$ being s.t. $\rho\circ\pi=\mathsf{Id}$.

We can now define the restriction of $\mathfrak{A}^{\prime}$ to ${\sf
ran}(\rho)$:

  * •

$R^{\mathfrak{A}^{\prime}}=\\{\rho(\bar{a})\mid\bar{a}\in
R^{\mathfrak{B}^{\prime\prime}}\\}$ for every relation symbol $R$;

  * •

$c^{\mathfrak{A}^{\prime}}=\rho(c^{\mathfrak{B}^{\prime}})$ for every constant
$c$.

As a consequence, the restriction of $\mathfrak{A}^{\prime}$ to ${\sf
ran}(\rho)$ is simply an isomorphic copy of $\mathfrak{B}^{\prime\prime}$. By
definition of $\pi$ and due to Points (b) in the definition of
$\mathfrak{B}^{\prime\prime}$ and Condition 2 on $\mathfrak{B}$, it
additionally satisfies the condition that for all $a\in{\sf ran}(\rho)$,

  * ($*$)

there is a $b\in B$ such that ${\sf
tp}^{1}_{\mathfrak{A}^{\prime},\Sigma}(a)={\sf
tp}^{1}_{\mathfrak{B}^{\prime},\Sigma}(b)$ and ${\sf
tp}^{1}_{\mathfrak{A},\Sigma}(a)={\sf tp}^{1}_{\mathfrak{B},\Sigma}(b)$

We want to extend the definition of $\mathfrak{A}^{\prime}$ to the elements
$a\in A\setminus{\sf ran}(\rho)$ so that Condition ($*$) is satisfied.
Informally, we do this by ‘cloning’ already existing elements. It is then easy
to use Condition ($*$) to show that $\mathfrak{A}^{\prime}<_{\sf
CP}\mathfrak{A}$ as desired, details are left to the reader.

We can do the cloning for any $a\in A\setminus{\sf ran}(\rho)$ in isolation.
We want to assign to $a$ the type ${\sf
tp}^{1}_{\mathfrak{B}^{\prime\prime},\Sigma}(\pi(a))$ by making it a clone of
the element $a^{\prime}:=\rho(\pi(a))$ that already satisfies this property
and is already present in $\mathfrak{A}^{\prime}$. This is done by setting,
for every relation symbol $R$,

$R^{\mathfrak{A}^{\prime}}=R^{\mathfrak{A}^{\prime}}\cup\\{\bar{a}[a/a^{\prime}]\mid\bar{a}\in
R^{\mathfrak{B}^{\prime\prime}}\\}$

where $\bar{a}[a/a^{\prime}]$ denotes the tuple obtained from $\bar{a}$ by
replacing every occurrence of $a^{\prime}$ with $a$. This finishes the
construction of the structure $\mathfrak{A}^{\prime}$.

Using the fact that $\mathfrak{B}^{\prime\prime}$ is a model of $\phi$, it is
now straightforward to show that, as desired, also $\mathfrak{A}^{\prime}$ is
a model of $\phi$. ∎

###  D.2 Proof of Lemma 4

See 4

###### Proof.

We apply Proposition 3 on $\mathfrak{A}$ and $\Sigma$ to obtain a model
$\mathfrak{A}^{\prime}$ whose size is at most ${\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$. By Point 2 of
Proposition 3, for each type $t\in{\sf tp}^{1}_{\mathfrak{A},\Sigma}(A)$, we
can find an element $a_{t}\in A^{\prime}$ whose type is $t$. We now extend
$\mathfrak{A}^{\prime}$ into a model $\mathfrak{B}$ by cloning those elements
$a_{t}$ until we have:

  * •

$\\#_{\mathfrak{B}}(t)=\\#_{\mathfrak{A}}(t)$ if $t\in{\sf
tp}^{1}_{\mathfrak{A},\Sigma}(\Delta)$;

  * •

$\\#_{\mathfrak{B}}(t)=1+{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$ if $t\in{\sf
tp}^{1}_{\mathfrak{A},\Sigma}(A\setminus\Delta)$.

For types $t\in{\sf tp}^{1}_{\mathfrak{A},\Sigma}(\Delta)$, this is well-
defined as we know that
$\\#_{\mathfrak{A}^{\prime}}(t)\leq\\#_{\mathfrak{A}}(t)$ from Point 3 of
Proposition 3. For types $t\in{\sf
tp}^{1}_{\mathfrak{A},\Sigma}(A\setminus\Delta)$, this is also well-defined as
we know that
$\\#_{\mathfrak{A}^{\prime}}(t)\leq{\left|{\mathfrak{A}^{\prime}}\right|}\leq{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$. It is readily
verified that $\mathfrak{B}$ satisfies all the desired properties. In
particular, Lemma 3 using $\mathfrak{A}$ as the reference model applies and
guarantees the ${\sf CP}$-minimality of $\mathfrak{B}$. Regarding the size of
$\mathfrak{B}$, it is exactly ${\left|{\Delta}\right|}+M(1+{\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|}))$ where $M$ is the
number of types in ${\sf tp}^{1}_{\mathfrak{A},\Sigma}(A\setminus\Delta)$.
Using ${\left|{\Delta}\right|}\leq(2^{\left|{\Sigma}\right|}-M){\sf
tower}(4^{{\left|{\Sigma}\right|}+4},{\left|{\phi}\right|})$ and $M\leq
2^{\left|{\Sigma}\right|}$, we obtained the claimed bound. ∎

###  D.3 Proof of Lemma 5

See 5

To prove the “$\Leftarrow$” direction of Lemma 5, assume we are given a good
mosaic $M_{0}$. For each good mosaic $M$, each $1\leq i\leq n_{\exists}$, if
$\bar{a}\in R_{i}^{\mathfrak{B}_{M}}$, then we choose a good mosaic
$M^{\prime}$ such that:

  1. 1.

${\sf tp}_{\mathfrak{B}_{M},\Sigma}(\bar{a})={\sf
tp}_{\mathfrak{B}_{M^{\prime}},\Sigma}(\bar{a})$;

  2. 2.

$\mathfrak{B}_{M^{\prime}}\models\exists\bar{y}\,(\gamma_{i}\wedge\psi_{i})[\bar{a}]$;

  3. 3.

if $(p,\widehat{p},h^{\prime})\in S_{M^{\prime}}$, then $(p,\widehat{p},h)\in
S_{M}$ where $h$ is the restriction of $h^{\prime}$ to range
$A_{0}\cup\bar{a}$.

We use $\mathsf{ch}^{i}_{M,\bar{a}}$ to denote this chosen $M^{\prime}$. Then,
starting from $M_{0}$, we build a forest-shaped set of words which witnesses
the acceptance of $M_{0}$.

######  Definition 2.

The mosaic forest $\mathsf{MTree}$ is the smallest set of words such that:

  * •

$(M_{0},\emptyset,\emptyset)\in\mathsf{MTree}$;

  * •

If $w\in\mathsf{MTree}$ ends with $(M,x,y)$ with $M$ a mosaic, and $\bar{a}\in
R^{\mathfrak{B}_{M}}$ for some $1\leq i\leq n_{\exists}$ with
$\beta_{i}=R(\bar{z})$, then
$w\cdot(\mathsf{ch}^{i}_{M,\bar{a}},i,\bar{a})\in\mathsf{MTree}$.

It remains to ‘glue’ together the interpretations $\mathfrak{B}_{M}$ according
to the structure of $\mathsf{MTree}$. Since a mosaic $M$ may occur more than
once, we create a copy of $\mathfrak{B}_{M}$ for each node in $\mathsf{MTree}$
of the form $w\cdot(M,x,y)$. We do not duplicate elements from $A_{0}$ as they
precisely are those we want to reuse. Hence only elements from $U^{+}$ may be
duplicated. We also take into consideration the overlap between successive
mosaics in the tree and introduce a copy of an element only when necessary.
Formally, this is achieved by the following duplicating functions, defined
inductively on $\mathsf{MTree}$. For $(M_{0},\emptyset,\emptyset)$, define:

$\begin{array}[]{r@{~}c@{~}l}\lambda_{(M_{0},\emptyset,\emptyset)}:B_{M_{0}}~{}&\rightarrow\hfil~{}&A_{0}\cup\\{x^{(M_{0},\emptyset,\emptyset)}\mid
x\in B_{M_{0}}\\}\\\
b~{}&\mapsto\hfil~{}&\left\\{\begin{array}[]{ll}b&\text{if }b\in A_{0}\\\
b^{(M_{0},\emptyset,\emptyset)}&\text{otherwise}\end{array}\right.\end{array}$

If $w\cdot(M,i,\bar{a})\in\mathsf{MTree}$ with $w$ not empty, define:

$\begin{array}[]{r@{~}c@{~}l}\lambda_{w\cdot(M,i,\bar{a})}:\mathfrak{B}_{M}~{}&\rightarrow\hfil~{}&A_{0}\cup\\{u^{m}\mid
u\in U^{+},m\in\mathsf{MTree}\\}\\\
b~{}&\mapsto\hfil~{}&\left\\{\begin{array}[]{ll}b&\text{if }b\in A_{0}\\\
\lambda_{w\cdot(M,i,\bar{a})}(b)&\text{if }b\in\bar{a}\setminus A_{0}\\\
b^{w\cdot(M,i,\bar{a})}&\text{otherwise}\end{array}\right.\end{array}$

The desired model ${\mathfrak{A}}$ can then be defined as:

${\mathfrak{A}}:=\bigcup_{\begin{subarray}{c}w\cdot(M,i,\bar{a})\in\mathsf{MTree}\\\
w\text{ possibly
empty}\end{subarray}}\lambda_{w\cdot(M,i,\bar{a})}({\mathfrak{B}_{M}}),$

that is the domain (resp. the interpretation of each predicate) of
${\mathfrak{A}}$ is the union across all
$w\cdot(M,i,\bar{a})\in\mathsf{MTree}$ of the image by
$\lambda_{w\cdot(M,i,\bar{a})}$ of the domain (resp. the interpretation of
each predicate) of $\mathfrak{B}_{M}$.

By definition, each $\lambda_{w\cdot(M,i,\bar{a})}$ is a homomorphism from
$\mathfrak{B}_{M}$ to ${\mathfrak{A}}$. It is also easily verified that this
homomorphism is injective. Due to Point 1 in the definition of good mosaics,
if the range of two duplicating functions overlap, then the common element
agree on the interpretation of all predicates. More formally, the following
lemma is an immediate consequence of the definition of functions
$\lambda_{w\cdot(M,i,\bar{a})}$ and Point 1 in the definition of good mosaics.

######  Lemma 11.

For all $w\cdot(M,i,\bar{a})\in\mathsf{MTree}$ and all $\bar{b}\in
B_{M}^{{\left|{\bar{b}}\right|}}$, we have ${\sf
tp}_{{\mathfrak{A}},\Sigma}(\lambda_{w\cdot(M,i,\bar{a})}({\bar{b}}))={\sf
tp}_{\mathfrak{B}_{M},\Sigma}({\bar{b}})$.

Note that, in the above, exact values of $i$ and $\bar{a}$ do not affect the
statement. Henceforth, we often use $w\cdot(M,\\_,\\_)$ to refer to an element
of $\mathsf{MTree}$ in which values of the second and third components of its
last triple are not important. We are ready to show that ${\mathfrak{A}}$ is a
model of $\phi$.

######  Lemma 12.

${\mathfrak{A}}$ is a model of $\phi$.

###### Proof.

Let $1\leq i\leq n_{\forall}$. We prove ${\mathfrak{A}}$ satisfies
$\forall\bar{x}\,(\alpha_{i}\rightarrow\varphi_{i})$. Assume there is
$\bar{a}\in R^{\mathfrak{A}}$, where $\alpha_{i}=R(\bar{z})$. By definition of
$\bar{a}$, there exists $w\cdot(M,\\_,\\_)$ and $\bar{b}\in
R^{\mathfrak{B}_{M}}$ s.t. $\bar{a}=\lambda_{w\cdot(M,\\_,\\_)}({\bar{b}})$.
From Point 4 of the definition of a mosaic, we get
$\mathfrak{B}_{M}\models\varphi_{i}[\bar{b}]$. By Lemma 11 we obtain
${\mathfrak{A}}\models\varphi_{i}[\lambda_{w\cdot(M,\\_,\\_)}({\bar{b}})]$
that is ${\mathfrak{A}}\models\varphi_{i}[\bar{a}]$ as desired.

Let $1\leq i\leq n_{\exists}$. We prove ${\mathfrak{A}}$ satisfies
$\forall\bar{x}\,(\beta_{i}\rightarrow\exists\bar{y}\,(\gamma_{i}\wedge\psi_{i}))$.
Assume there is $\bar{a}\in R^{\mathfrak{A}}$, where $\beta_{i}=R(\bar{z})$.
By definition of $\bar{a}$, there exists $w\cdot(M,\\_,\\_)$ and $\bar{b}\in
R^{\mathfrak{B}_{M}}$ s.t. $\bar{a}=\lambda_{w\cdot(M,\\_,\\_)}({\bar{b}})$.
By definition of the mosaic tree, we get
$w\cdot(M,\\_,\\_)\cdot(\mathsf{ch}^{i}_{M,\bar{b}},i,\bar{b})\in\mathsf{MTree}$.
We let $M^{\prime}:=\mathsf{ch}^{i}_{M,\bar{b}}$ for readability. By
definition of $M^{\prime}$ and from Point 2 of the definition of good mosaics,
we obtain
$\mathfrak{B}_{M^{\prime}}\models\exists\bar{y}(\gamma_{i}\wedge\psi_{i})[\bar{b}]$.
Thus there exists an extension $\bar{d}\in S^{\mathfrak{B}_{M^{\prime}}}$ of
$\bar{b}$ such that $\mathfrak{B}_{M^{\prime}}\models\psi_{i}[\bar{d}]$, where
$\gamma_{i}=S(\bar{z}^{\prime})$. By Lemma 11, we obtain
${\mathfrak{A}}\models\psi_{i}[\lambda_{w\cdot(M,\\_,\\_)\cdot(M^{\prime},i,\bar{b})}({\bar{d}})]$.
By definition of $\lambda_{w\cdot(M,\\_,\\_)\cdot(M^{\prime},i,\bar{b})}$, we
have
$\lambda_{w\cdot(M,\\_,\\_)\cdot(M^{\prime},i,\bar{b})}({\bar{b}})=\bar{a}$.
Thus the tuple
$\lambda_{w\cdot(M,\\_,\\_)\cdot(M^{\prime},i,\bar{b})}({\bar{d}})$ is an
extension of $\bar{a}$ (that extends $\bar{a}$ as $\bar{d}$ extends $\bar{b}$)
that satisfies $\gamma_{i}\wedge\psi_{i}$ in ${\mathfrak{A}}$ as desired. ∎

This proves $\mathfrak{A}_{0}$ can indeed by extended into a model of $\phi$.
Notice that Condition (a) is clearly satisfied due to Point 2 in the
definition of mosaics. The $\subseteq$ direction of Condition (b) is clearly
satisfied from Point 3 in the definition of mosaics joint with Lemma 11. Its
$\supseteq$ direction of Condition (b) is satisfied from the basic conditions
on the pair $(\mathfrak{A}_{0},T_{\mathsf{\overline{core}}})$, that is
$\mathfrak{A}_{0}$ already contains at least one witness for each type from
$T_{\mathsf{\overline{core}}}$. It remains to verify Condition (c), that is
for all $p\in q$, there is no homomorphism from $p$ in ${\mathfrak{A}}$.

By contradiction, assume there exists a CQ $p\in q$ and a homomorphism
$\pi:p\rightarrow{\mathfrak{A}}$. Therefore, for each atom
$\alpha:=R(\bar{z})$ in $p$, it follows from the definition of
$R^{\mathfrak{A}}$ that there exists a node
$w_{\alpha}:=w\cdot(M,\\_,\\_)\in\mathsf{MTree}$ and $\bar{a}\in
R^{\mathfrak{B}_{M}}$ s.t. $\lambda_{w_{\alpha}}({\bar{a}})=\pi(\bar{z})$. We
assume chosen such a node $w_{\alpha}$ for each $\alpha\in p$. On
$\mathsf{MTree}$, we consider the order given by the prefix relation, that is
for all $w_{1},w_{2}\in\mathsf{MTree}$, we denote $w_{1}\leq w_{2}$ iff
$w_{1}$ is a prefix of $w_{2}$. We define a set of words $W_{p}$ as containing
all words from $\mathsf{MTree}$ that are prefixes of a word $w_{\alpha}$ for
some $\alpha\in p$. We let $p_{0}:=\\{\alpha\in
p\mid\mathfrak{A}_{0}\models\pi(\alpha)\\}$ the subquery of $p$ that is mapped
by $\pi$ in $\mathfrak{A}_{0}$ and $h_{0}:=\pi|_{{\sf var}(p_{0})}$ the
corresponding mapping of variables. For a word $w\in\mathsf{MTree}$, we set
$p_{w}:=p_{0}\cup\\{\alpha\in p\setminus p_{0}\mid w\leq w_{\alpha}\\}$ and
$h_{w}$ a mapping defined on every $v\in{\sf var}(p_{u})$ s.t.
$\pi(v)\in\lambda_{u}({B_{M}})$ by $h(v)=(\lambda_{u})^{-1}(\pi(v))$. Note
that $h_{w}$ always extends $h_{0}$ since all mosaics agree on the
interpretation of $\mathfrak{A}_{0}$ (Point 2 in the definition of mosaics).

######  Lemma 13.

For all $w\cdot(M,\\_,\\_)\in W_{p}$, $(p,p_{w},h_{w})\in S_{M}$.

In particular, since $(M_{0},\emptyset,\emptyset)\in W_{p}$ and
$p_{(M_{0},\emptyset,\emptyset)}=p$, this guarantees
$(p,p,h_{(M_{0},\emptyset,\emptyset)})\in S_{(M_{0},\emptyset,\emptyset)}$,
which contradicts $M_{0}$ being a mosaic (it contains a complete match
triple!) and thus concludes the proof of Condition (c).

We now prove the above lemma.

###### Proof.

We proceed by induction on elements of $W_{p}$, starting from its maximal
elements w.r.t. $\leq$. Notice there are at most ${\left|{p}\right|}$ such
maximal elements.

Base case. Assume $u=w\cdot(M,\\_,\\_)\in W_{p}$ is maximal for $\leq$.
Therefore, $p_{u}=p_{0}\cup\\{\alpha\in p\setminus p_{0}\mid w_{\alpha}=u\\}$.
By definition of each $w_{\alpha}$, $h_{u}$ defines a homomorphism from
$p_{u}$ to $\mathfrak{B}_{M}$. Since $S_{M}$ is saturated, it follows from the
first saturation condition that $(p,p_{u},h_{u})\in S_{M}$.

Induction case. Consider $u=w\cdot(M,\\_,\\_)\in W_{p}$ and assume the
property holds for all $u^{\prime}\in W_{p}$ with $u\leq u^{\prime}$. We
refine the subset $p_{u}\subseteq p$ of atoms by a smaller subset
$p_{=u}:=p_{0}\cup\\{\alpha\in p_{u}\setminus p_{0}\mid w_{\alpha}=u\\}$. As
in the base case, the definition of words $w_{\alpha}$ guarantees there is a
homomorphism from $p_{=u}$ to $\mathfrak{B}_{M}$ given by
$h_{=u}:=\lambda_{u}^{-1}\circ\pi|_{D_{u}}$ where
$D_{u}=\pi^{-1}(\lambda_{u}({B_{M}}))$. From $S_{M}$ being saturated, we
obtain $(p,p_{=u},h_{=u})\in S_{M}$. For the other atoms of $p_{u}$, that is
$\alpha\in p_{u}\setminus p_{=u}$, we have $u<w_{\alpha}$ thus there exists
$u_{\alpha}=u\cdot(M_{\alpha},i_{\alpha},\bar{a}_{\alpha})\in W_{p}$ with
$u_{\alpha}\leq w_{\alpha}$. We denote $u_{1},\dots,u_{n}$ the distinct
elements from $\\{u_{\alpha}\mid\alpha\in p_{u}\setminus p_{=u}\\}$ and if
$u_{k}=u_{\alpha}$, we let
$(M_{k},i_{k},\bar{a}_{k}):=(M_{\alpha},i_{\alpha},\bar{a}_{\alpha})$. Note
that $p_{u}$ can now be partitioned as
$p_{=u}\uplus\biguplus_{k=1}^{n}(p_{u_{k}}\setminus p_{0})$. For each $1\leq
k\leq n$, we apply the induction hypothesis to obtain
$(p,p_{u_{k}},h_{u_{k}})\in S_{M_{k}}$. From
$w\cdot(M,\\_,\\_)\cdot(M_{k},i_{k},\bar{a}_{k})\in\mathsf{MTree}$ and Point 3
of in the definition of a good mosaic, we obtain $(p,p_{u_{k}},g_{u_{k}})\in
S_{M}$ where $g_{u_{k}}$ is the restriction of $h_{u_{k}}$ to range
$A_{0}\cup\bar{a}_{k}$. Recall that $S_{M}$ is saturated, thus using the
second condition from definition of saturation, we can derive
$(p,p_{u},h_{=u}\cup\bigcup_{k=1}^{n}g_{u_{k}})\in S_{M}$ if we prove that
partial mappings $h_{=u},g_{u_{1}},\dots,g_{u_{n}}$ are pairwise compatible
(in the sense specified in the definition of saturation).

We first treat the case of $g_{u_{1}}$ and $g_{u_{2}}$ (any other combination
of $g_{u_{k}}$ and $g_{u_{\ell}}$ with $k\neq\ell$ being treated similarly).
Assume $x\in{\sf var}(p_{u_{1}})\cap{\sf var}(p_{u_{2}})$, we have to prove
that both $g_{u_{1}}$ and $g_{u_{2}}$ are defined on $x$ and that
$g_{u_{1}}(x)=g_{u_{2}}(x)$. If $x\in{\sf var}(p_{0})$, this is clear.
Otherwise, $\pi(x)=d^{w^{\prime}}$ for some $d\in U^{+}$ and
$w^{\prime}\in\mathsf{MTree}$. By definition of $h_{u_{1}}$ and $h_{u_{2}}$,
we get $d^{w^{\prime}}\in\lambda_{u_{1}}({B_{M_{1}}})$ and
$d^{w^{\prime}}\in\lambda_{u_{1}}({B_{M_{2}}})$ respectively. Thus
$w^{\prime}$ must be a prefix of both $u_{1}$ and $u_{2}$, by definition of
the functions $\lambda_{u_{1}}$ and $\lambda_{u_{2}}$. The longest common
prefix of $u_{1}$ and $u_{2}$ being $u$, we obtain that $w^{\prime}$ is a
prefix of $u$. In particular, $d^{w^{\prime}}\in\lambda_{u}({B_{M}})$ and
$h_{u_{1}}(x)\in\bar{a}_{1}$ and $h_{u_{2}}(x)\in\bar{a}_{2}$. Thus
$g_{u_{1}}$ and $g_{u_{2}}$ are both defined on $x$ and equal to
$\lambda_{u}^{-1}(\pi(x))$, that is $h_{u}(x)$.

The argument for the case of $h_{=u}$ and $g_{u_{k}}$ is similar, observing
that if $x\in({\sf var}(p_{=u})\cap{\sf var}(p_{u_{k}}))\setminus{\sf
var}(p_{0})$, we have $h_{u_{k}}\in\bar{a}_{k}$ thus $g_{u_{k}}$ being defined
on $x$ and equal to $\lambda_{u}^{-1}(\pi(x))$, that is $h_{u}(x)$.

We thus obtain $(p,p_{u},h_{=u}\cup\bigcup_{k=1}^{n}g_{u_{k}})\in S_{M}$ and
it was already verified within the above cases that
$h_{u}=h_{=u}\cup\bigcup_{k=1}^{n}g_{u_{k}}$, thus $(p,p_{u},h_{u})\in S_{M}$
as desired.

∎

This concludes the proof of the ‘$\Leftarrow$’ direction in Lemma 5.

We now turn to the ‘$\Rightarrow$’ direction. Assume that $\mathfrak{A}_{0}$
can be extended to a model $\mathfrak{A}$ of $\phi$ that satisfies Conditions
(a) to (c). We extract a set of good mosaics from $\mathfrak{A}$. To this end,
we define the notion of paths in $\mathfrak{A}$.

A _path_ in $\mathfrak{A}$ is a sequence $\bar{a}_{1},\dots,\bar{a}_{n}$ of
maximally guarded tuples from ${\sf mgt}(\mathfrak{A})$ that contain at least
one element of $A\setminus\Delta$. For each path
$p=\bar{a}_{1},\dots,\bar{a}_{n}$ in $\mathfrak{A}$, we now inductively define
a mosaic $M_{p}$ as follows.

If $p=\bar{a}$ is of length $1$, we let $L_{p}:=\\{i\mid
a_{i}\in\bar{a}\setminus A_{0}\\}$ and pick for each $i\in L_{p}$ a fresh
element $u_{i}\in U$. We denote $\lambda_{p}:a_{i}\mapsto u_{i}$ the
corresponding bijection between elements of $\bar{a}$ that are not in $A_{0}$
and the chosen fresh elements. We extend $\lambda_{p}$ to $A_{0}\cup\bar{a}$
by defining $\lambda_{p}$ to be the identity on elements from $A_{0}$. We now
define $M_{p}$ by
$\mathfrak{B}_{M_{p}}=\lambda_{p}(\mathfrak{A}|_{A_{0}\cup\bar{a}})$ and
$S_{M_{p}}$ as the set of all triples $(p,\widehat{p},\lambda_{p}\circ
h|_{A_{0}\cup\bar{a}})$ s.t. $p\in q$, $\widehat{p}\subseteq p$ and
$h:\widehat{p}\rightarrow\mathfrak{A}$ is a homomorphism. Note that $M_{p}$ is
a well-defined mosaic: regarding $\mathfrak{B}_{M_{p}}$, Point 1 is clear by
construction, Points 2 and 3 follow respectively from Conditions (a) and (b)
being satisfied by $\mathfrak{A}$, Point 4 from $\mathfrak{A}$ being a model
of $\phi$; regarding $S_{M_{p}}$, it is saturated by construction and does not
contain a complete match triple from Condition (c) being satisfied by
$\mathfrak{A}$.

If $p=\bar{a}_{1},\dots,\bar{a}_{n},\bar{a}_{n+1}$ has length $>1$, we let
$L_{p}:=\\{i\mid a_{i}\in\bar{a}_{n+1}\setminus(A_{0}\cup\bar{a}_{n})\\}$ and
pick for each $i\in L_{p}$ a fresh element $u_{i}\in U$. Note that this is
always possible as $U$ has size twice the maximal arity of a predicate. We
denote $\lambda_{p}:a_{i}\mapsto u_{i}$ the corresponding bijection elements
of $\bar{a}_{n+1}$ that are neither in $A_{0}$ nor in $\bar{a}_{n}$, and the
chosen fresh elements. We extend $\lambda_{p}$ to $A_{0}\cup\bar{a}_{n+1}$ by
defining $\lambda_{p}$ to be the identity on elements from $A_{0}$ and to be
$\lambda_{\bar{a}_{1},\dots,\bar{a}_{n}}$ on elements from
$\bar{a}_{n}\cap\bar{a}_{n+1}$. We now define $M_{p}$ by
$\mathfrak{B}_{M_{p}}=\lambda_{p}(\mathfrak{A}|_{A_{0}\cup\bar{a}_{n+1}})$ and
$S_{M_{p}}$ as the set of all triples
$(q^{\prime},\widehat{q^{\prime}},\lambda_{p}\circ
h|_{A_{0}\cup\bar{a}_{n+1}})$ s.t. $q^{\prime}\in q$,
$\widehat{q^{\prime}}\subseteq q^{\prime}$ and
$h:\widehat{q^{\prime}}\rightarrow\mathfrak{A}$ is a homomorphism. As in the
base case, it is easily verified that $M_{p}$ is a well-defined mosaic.

We now let $\mathcal{M}:=\\{M_{p}\mid p\textrm{ is a path in }\mathfrak{A}\\}$
and claim all mosaics in $\mathcal{M}$ are good in $\mathcal{M}$. Let
$M_{p}\in\mathcal{M}$ for some path $p=\bar{a}_{1},\dots,\bar{a}_{n}$ in
$\mathfrak{A}$. Assume there exists $\bar{a}\in R^{\mathfrak{B}_{M_{p}}}$
where $R(\bar{z})=\beta_{i}$ for some $1\leq i\leq n_{\exists}$. Since
$\mathfrak{A}$ is a model of $\phi$, there exists a tuple $\bar{a}^{\prime}\in
S^{\mathfrak{A}}$ where $S(\bar{z}^{\prime})=\gamma_{i}$ s.t.
$\bar{a}^{\prime}$ witnesses $\mathfrak{A}\models\exists
y(\gamma_{i}\wedge\psi_{i})[\bar{a}]$. Consequently,
$p^{\prime}=\bar{a}_{1},\dots,\bar{a}_{n},\bar{a}^{\prime}$ is a path in
$\mathfrak{A}$. We prove $M_{p^{\prime}}$ is a mosaic satisfying Conditions 1
to 3 in the definition of good mosaics. Condition 1 is clear by construction
of $M_{p^{\prime}}$, which is inductively defined from $M_{p}$ and thus their
‘overlap’ is consistent as expected. Condition 2 is also guaranteed from the
very definition of $\bar{a}^{\prime}$. For Condition 3, recall that each match
triple $(q^{\prime},\widehat{q^{\prime}},h)\in S_{M_{p^{\prime}}}$ is such
that $\lambda_{p^{\prime}}{{}^{-}1}\circ h$ is the restriction to
$A_{0}\cup\bar{a}^{\prime}$ of a complete homomorphism from
$\widehat{q^{\prime}}$ to $\mathfrak{A}$. By considering instead the
restriction of $\widehat{q^{\prime}}$ to $A_{0}\cup\bar{a}$ we obtain the
desired match triple in $S_{M_{p}}$.

##  Appendix E Proofs for Section 5

To fix notation, we recall that an ATM $\mathcal{M}$ is specified by a
$6$-tuple $\mathcal{M}=(Q,\Sigma,\Gamma,\delta,q_{0},g)$ where:

  * •

$Q$ is the finite set of states;

  * •

$\Sigma$ is the finite input alphabet;

  * •

$\Gamma\supseteq\Sigma$ is the finite tape alphabet with a special blank
symbol $\textvisiblespace\in\Gamma\setminus\Sigma$;

  * •

$\delta:Q\times\Gamma\rightarrow(Q\times\Gamma\times\\{\triangleleft,\triangleright\\})^{2}$
is the transition function;

  * •

$q_{0}\in Q$ is the initial state;

  * •

$g:Q\rightarrow\\{{\sf univ},{\sf exist},{\sf accept},{\sf reject}\\}$
specifies the type of each state.

Note that without loss of generality, we consider TMs having the following
properties:

  * •

for every universal or existential configuration, there exist exactly two
applicable transitions;

  * •

the machine directly accepts any configuration whose state $s$ is such that
$g(s)={\sf accept}$;

  * •

the ATM never tries to go to the left of the initial position.

We say that $\mathcal{M}$ is _polynomially space-bounded_ if there exists a
polynomial $p$ such that on input $x$, $\mathcal{M}$ visits only the first
$p({\left|{x}\right|})$ tape cells. $\mathcal{M}$ being _$\kappa$
-exponentially space-bounded_, for some $\kappa\geq 1$, is defined
accordingly, allowing the ATM to visit ${\sf
tower}(\kappa,p({\left|{x}\right|}))$ tape cells. We consider only ATMs that
terminate on every input. It is known that there is a fixed polynomially
space-bounded ATM $\mathcal{M}=(Q,\Sigma,\Gamma,\delta,q_{0},g)$ whose word
problem is Exp-hard (?).

###  E.1 Proof of Theorem 6

$\displaystyle{\sf conf}_{q}(x,x_{h})$
$\displaystyle\rightarrow\overline{}{\sf
conf}_{\triangleleft}(x,x_{h}),\overline{}{\sf
conf}_{\triangleright}(x,x_{h})$ (4) $\displaystyle\overline{}{\sf
conf}_{\triangleleft}(x,x_{p}),\ \overline{{\sf start}}(x_{p})$
$\displaystyle\rightarrow\exists y_{p}\,{\sf
next}(y_{p},x_{p}),\overline{}{\sf conf}_{q^{\prime}}(x,y_{p}),\overline{}{\sf
conf}_{\triangleleft}(x,y_{p})$ (5) $\displaystyle\overline{}{\sf
conf}_{\triangleright}(x,x_{p}),\ \overline{{\sf end}}(x_{p})$
$\displaystyle\rightarrow\exists y_{p}\,{\sf
next}(x_{p},y_{p}),\overline{}{\sf conf}_{q^{\prime}}(x,y_{p}),\overline{}{\sf
conf}_{\triangleright}(x,y_{p}).$ (6) $\displaystyle{\sf
nextConf}_{i}(x,y,x_{h})$ $\displaystyle\rightarrow{\sf
copy_{\triangleleft}}(x,y,x_{h}),{\sf copy_{\triangleright}}(x,y,x_{h})$ (7)
$\displaystyle{\sf copy_{\triangleleft}}(x,y,x_{p}),\overline{{\sf
start}}(x_{p})$ $\displaystyle\rightarrow\exists y_{p}\,{\sf
next}(y_{p},x_{p}),{\sf copy_{\triangleleft}}(x,y,y_{p}),{\sf
copy}(x,y,y_{p})$ (8) $\displaystyle{\sf
copy_{\triangleright}}(x,y,x_{p}),\overline{{\sf end}}(x_{p})$
$\displaystyle\rightarrow\exists y_{p}\,{\sf next}(x_{p},y_{p}),{\sf
copy_{\triangleright}}(x,y,y_{p}),{\sf copy}(x,y,y_{p})$ (9)
$\displaystyle{\sf copy}(x,y,x_{p}),{\sf tape}_{s}(x,x_{p})$
$\displaystyle\rightarrow{\sf tape}_{s}(y,x_{p})$ (10) Figure 3: Additional
rules used in the proof of Theorem 6, for all $i\in\\{1,2\\}$.

We exhibit a set of existential rules $\mathcal{O}$ and a circumscription
pattern ${\sf CP}$ such that, given a word $e=e_{1}\cdots e_{n}\in\Sigma^{*}$,
we can construct in polynomial time a database $D$ such that $\mathcal{M}$
accepts $e$ iff ${\sf Circ_{\sf CP}}(\mathcal{O},D)\models{\sf goal}(a)$,
where ${\sf goal}$ is a unary predicate and $a$ a dedicated constant symbol.
To give a better intuition of the involved mechanisms, we describe the
constructions of $\mathcal{O}$ and $D$ together. It can, however, be verified
that $\mathcal{O}$ is independent of $e$.

We use all tape positions $i$ with $1\leq i\leq p(n)$ as constants in the
database $D$. In addition, we use the constant $a$ that occurs inside the
query above. In $D$, we mark the constant symbols that represent positions by
a

${\sf pos}(i)\textrm{ for }1\leq i\leq p(n).$

To ensure that, in every minimal model, the positions are picked from the
intended constants, we require the predicate ${\sf pos}$ to be minimized.

We introduce binary predicates ${\sf config}_{q}$ for every $q\in Q$ and ${\sf
tape}_{s}$ for every $s\in\Gamma$. Intuitively, ${\sf config}_{q}(x,x_{h})$
says that $x$ is a configuration of $\mathcal{M}$ where $\mathcal{M}$ is in
state $q$ and the head is on position $x_{h}$ of the tape. Likewise, ${\sf
tape}_{s}(x,x_{p})$ says that in configuration $x$, the symbol $s$ is on
position $x_{p}$ of the tape. For all $q\in Q$ and $s\in\Gamma$, we require
that

$\begin{array}[]{rcl}{\sf conf}_{q}(x,x_{h})&\rightarrow&{\sf
pos}(x_{h})\\\\[2.84526pt] {\sf tape}_{s}(x,x_{p})&\rightarrow&{\sf
pos}(x_{p}).\end{array}$

The initial configuration is now encoded by

$\displaystyle{\sf conf}_{q_{0}}(a,1)$ $\displaystyle{\sf tape}_{e_{i}}(a,i)$
$\displaystyle\textrm{ for }1\leq i\leq n$ $\displaystyle{\sf
tape}_{\textvisiblespace}(a,i)$ $\displaystyle\textrm{ for }n<i\leq p(n).$

To generate the other configurations of the ATM computation on input $e$, we
use existential quantifiers in rules. We need some preparation. To start with,
we add auxiliary facts on the constants $1,\dots,n$ that pertain to their
order:

$\displaystyle\overline{{\sf succ}}(i,j)$ $\displaystyle\textrm{ for }1\leq
i,j\leq p(n)\text{ with }i\neq j$ $\displaystyle\overline{{\sf start}}(i)$
$\displaystyle\textrm{ for }1<i\leq p(n)$ $\displaystyle\overline{{\sf
end}}(i)$ $\displaystyle\textrm{ for }1\leq i<p(n).$

We will later also use a ‘positive’ version ${\sf next}$ of the
$\overline{{\sf succ}}$ predicate. We want these predicates to be disjoint in
models that falsify ${\sf goal}(a)$. This is achieved by adding the rules

$\displaystyle{\sf next}(x,y),\overline{{\sf next}}(x,y)$
$\displaystyle\rightarrow{\sf err}(x)$ $\displaystyle{\sf getError}(x,y),{\sf
err}(x)$ $\displaystyle\rightarrow{\sf goal}(x).$

and facts

${\sf getError}(a,i)\textrm{ for }1\leq i\leq p(n).$

This mechanism will be used in the following to detect also other violations
of the intended encoding. We also want ${\sf next}$ to be restricted to
positions:

${\sf next}(x,y)\rightarrow{\sf pos}(x),{\sf pos}(y).$

We next make sure that the state, head position, and tape content is unique
for every configuration. Regarding the tape content, for all distinct
$s,s^{\prime}\in\Gamma$ we put

${\sf tape}_{s}(x,x_{p}),{\sf tape}_{s^{\prime}}(x,x_{p})\rightarrow{\sf
error}(x_{p}).$

To ensure uniqueness of the state and head position, for all $q,q^{\prime}\in
Q$ we add Rules (4) to (6) shown in Figure 3. Moreover, for distinct
$q,q^{\prime}\in Q$, we add

$\displaystyle{\sf conf}_{q}(x,x_{h}),{\sf conf}_{q^{\prime}}(x,x_{h})$
$\displaystyle\rightarrow{\sf error}(x_{h})$ $\displaystyle{\sf
conf}_{q}(x,x_{p}),\overline{}{\sf conf}_{q}(x,x_{p})$
$\displaystyle\rightarrow{\sf error}(x_{p}).$

We now generate the additional configurations. For all $q\in Q$ with
$g(q)\notin\\{{\sf accept},{\sf reject}\\}$, all $s\in\Gamma$, if
$\delta(q,s)=(q_{1},s_{1},m_{1},q_{2},s_{2},m_{2})$ then put for all
$i\in\\{1,2\\}$,

$\begin{array}[]{l@{}c@{}r}{\sf conf}_{q}(x,x_{h}),{\sf
tape}_{s}(x,x_{h})&\rightarrow&\exists y\,\exists y_{h}\,{\sf
nextConf}_{i}(x,y,x_{h}),\\\ &&{\sf conf}_{q_{i}}(y,y_{h}),{\sf
tape}_{s_{i}}(y,x_{h}),\\\ &&{\sf MOV}\end{array}$

where ${\sf MOV}$ is ${\sf next}(x_{h},y_{h})$ if $m_{i}=\triangleright$ and
${\sf next}(y_{h},x_{h})$ if $m_{i}=\triangleleft$. The above rule sets up
correctly the state and head position of the new configuration, as well as the
symbol on the tape at the position where the head was located previously. We
still need to say that the other symbols didn’t change. For all $q\in Q$,
$i\in\\{1,2\\}$, and $s\in\Gamma$, add Rules (7) to (10) shown in Figure 3.

Note that the constant $a$ is the root of a tree of configurations that are
connected by the (projection to the first two components of the) predicates
${\sf nextConf}_{i}$, $i\in\\{1,2\\}$. We now propagate acceptance information
upwards in that tree. For all states $q\in Q$ with $g(q)={\sf accept}$, add

${\sf conf}_{q}(x,x_{h})\rightarrow{\sf acc}(x).$

Further add, for all $q\in Q$ and $i\in\\{1,2\\}$,

${\sf nextConf}_{i}(x,y,x_{h}),{\sf acc}(y)\rightarrow{\sf acc}_{i}(x).$

Now, for all $q\in Q$ with $g(q)={\sf univ}$, all $q^{\prime}\in Q$ with
$g(q^{\prime})={\sf exist}$, and all $i\in\\{1,2\\}$, add

$\displaystyle{\sf conf}_{q}(x,x_{h}),{\sf acc}_{1}(x),{\sf acc}_{2}(x)$
$\displaystyle\rightarrow{\sf acc}(x)$ $\displaystyle{\sf
conf}_{q^{\prime}}(x,x_{h}),{\sf acc}_{i}(x)$ $\displaystyle\rightarrow{\sf
acc}(x).$

At the root of the configuration tree, which is $a$, acceptance makes the
query true:

$\displaystyle{\sf acc}(x)$ $\displaystyle\rightarrow{\sf goal}(x).$

We use $\mathcal{O}$ to denote the obtained set of rules and $D$ for the
obtained database. The circumscription pattern ${\sf CP}$ has a minimized
predicate ${\sf pos}$ and all other predicates are varying. In particular,
${\sf CP}$ has no fixed predicates. It is now straightforward to prove the
following.

######  Lemma 14.

$\mathcal{M}$ accepts on input $e$ iff ${\sf Circ_{\sf
CP}}(\mathcal{O},D)\models{\sf goal}(a)$.

We omit the details, but remark that, as a crucial point, in every minimal
model $\mathfrak{A}$ of $\mathcal{K}=(\mathcal{O},D)$, we must have ${\sf
pos}^{\mathfrak{A}}=\\{1,\dots,p(n)\\}$. This can be seen as follows. First,
$1,\dots,p(n)$ have been asserted to satisfy ${\sf pos}$ in $D$ and must be
distinct due to the semantics of databases. And second, for any model
$\mathfrak{B}$ of $\mathcal{K}$ in which ${\sf pos}^{\mathfrak{B}}$ is a
strict superset of $\\{1,\dots,p(n)\\}$, we can create a model $\mathfrak{A}$
of $\mathcal{K}$ with $\mathfrak{A}<_{\sf CP}\mathfrak{B}$ in the following
way:

  * •

set ${\sf pos}^{\mathfrak{A}}=\\{1,\dots,p(n)\\}$;

  * •

set ${\sf next}^{\mathfrak{A}}={\sf pos}^{\mathfrak{A}}\times{\sf
pos}^{\mathfrak{A}}$;

  * •

set $R^{\mathfrak{A}}=A\times\\{1,\dots,p(n)\\}$ for all relations $R$ of the
form ${\sf conf}_{q}$ and ${\sf tape}_{s}$;

  * •

interpret all other predicates as total.

We now consider the second part of Theorem 6, claiming that when switching
from AQ-querying to UCQ-querying we can make do with predicates of arity at
most two. Note that the only predicates in the above reduction that are of
higher arity are ${\sf nextConf}_{i}$, ${\sf copy}$, ${\sf
copy_{\triangleleft}}$, and ${\sf copy_{\triangleright}}$. These predicates
are used to ensure that the content of tape cells that are not under the head
remain the same when the ATM makes a transition.

We modify the reduction by making ${\sf nextConf}_{i}$ binary, dropping the
third position that records the head position of the configuration that is in
the first position. The (important) rule that generates additional
configurations otherwise remains unchanged. We drop the relations ${\sf
copy}$, ${\sf copy_{\triangleleft}}$, and ${\sf copy_{\triangleright}}$ as
well as Rules (4) to (7) in Figure 3 in which they are used.

To compensate for this, we add additional disjuncts to the query. In fact, we
use one disjunct for any two distinct $s,s^{\prime}\in\Gamma$ and all
$i\in\\{1,2\\}$:

$\begin{array}[]{l}{\sf nextConf}_{i}(x,y)\wedge{\sf tape}_{s}(x,p)\wedge{\sf
tape}_{s^{\prime}}(y,p)\;\wedge\\\\[2.84526pt] \bigwedge_{q\in
Q}\overline{}{\sf conf}_{q}(x,p).\end{array}$

###  E.2 Proof of Theorem 7

It remains to describe how the computation of the ATM
$\mathcal{M}=(Q,\Sigma,\Gamma,\delta,q_{0},g)$ is represented.

We introduce a unary predicate ${\sf state}_{q}$ for every $q\in Q$ and binary
predicates ${\sf head}$ and ${\sf tape}_{s}$ for every $s\in\Gamma$.
Intuitively, ${\sf state}_{q}(x)$ and ${\sf head}(x,x_{h})$ say that $x$ is a
configuration of $\mathcal{M}$ where $\mathcal{M}$ is in state $q$ and the
head is on position $x_{h}$ of the tape. Likewise, ${\sf tape}_{s}(x,x_{p})$
says that in configuration $x$, the symbol $s$ is written on position $x_{p}$
of the tape. For all $s\in\Gamma$, we require that

$\begin{array}[]{rcl}{\sf head}(x,x_{h})&\rightarrow&{\sf
ord}_{\kappa}(x_{h})\\\ {\sf tape}_{s}(x,x_{p})&\rightarrow&{\sf
ord}_{\kappa}(x_{p}).\end{array}$

$\displaystyle\overline{{\sf head}}_{\triangleleft}(x,y),\ \overline{{\sf
start}}(y)$ $\displaystyle\rightarrow\exists y^{\prime}\,\overline{{\sf
head}}_{\triangleleft}(x,y^{\prime}),{\sf
succ}_{\kappa}(y^{\prime},y),\overline{{\sf head}}(x,y^{\prime})$ (11)
$\displaystyle\overline{{\sf head}}_{\triangleright}(x,y),\ \overline{{\sf
end}}(y)$ $\displaystyle\rightarrow\exists y^{\prime}\,\overline{{\sf
head}}_{\triangleright}(x,y^{\prime}),{\sf
succ}_{\kappa}(y,y^{\prime}),\overline{{\sf head}}(x,y^{\prime})$ (12)
$\displaystyle{\sf blanks}_{\triangleright}(x,y),\overline{{\sf end}}(y)$
$\displaystyle\rightarrow\exists y^{\prime}\;{\sf
blanks}_{\triangleright}(x,y^{\prime}),{\sf succ}_{\kappa}(y,y^{\prime}),{\sf
tape}_{\textvisiblespace}(x,y^{\prime})$ (13) $\displaystyle{\sf
zeros}_{\triangleright}(x,y),\overline{{\sf end}}(y),{\sf ord}_{k-1}(y)$
$\displaystyle\rightarrow\exists y^{\prime}\;{\sf
zeros}_{\triangleright}(x,y^{\prime}),{\sf succ}_{k-1}(y,y^{\prime}),{\sf
bit}_{k,0}(x,y^{\prime})$ (14) $\displaystyle{\sf
copy}_{\triangleleft}(x,x^{\prime},y),\overline{{\sf start}}(y),{\sf
ord}_{k-1}(y)$ $\displaystyle\rightarrow\exists y^{\prime}\;{\sf
copy}_{\triangleleft}(x,x^{\prime},y^{\prime}),{\sf
succ}_{k-1}(y,y^{\prime}),{\sf copy}(x,x^{\prime},y^{\prime})$ (15) Figure 4:
Additional rules used in the proof of Theorem 7 for every
$k\in\\{2,\dots,\kappa\\}$.

We next make sure that the state, head position, and tape content are unique
for every configuration. Regarding the state and tape content, for all
distinct $s,s^{\prime}\in\Gamma$ and all distinct $q,q^{\prime}\in Q$ we put:

$\displaystyle{\sf state}_{q}(x),{\sf state}_{q^{\prime}}(x)$
$\displaystyle\rightarrow\exists y\;{\sf err}_{\kappa+1}(y)$
$\displaystyle{\sf tape}_{s}(x,x_{p}),{\sf tape}_{s^{\prime}}(x,x_{p})$
$\displaystyle\rightarrow\exists y\;{\sf err}_{\kappa+1}(y).$

To ensure uniqueness of the head position, we scan the tape in both
directions, which is initialized by the rule

$\displaystyle{\sf head}(x,x_{h})$ $\displaystyle\rightarrow\overline{{\sf
head}}_{\triangleleft}(x,x_{h}),\overline{{\sf
head}}_{\triangleright}(x,x_{h}).$

Predicates $\overline{{\sf head}}_{\triangleleft}$ and $\overline{{\sf
head}}_{\triangleright}$ follow the same propagation mechanism as ${\sf
zeros}_{\triangleleft}$, ${\sf ones}_{\triangleleft}$ and ${\sf
copy}_{\triangleright}$, see Rules 11 and 12 in Figure 4. To prevent multiple
head positions, we add the rule

$\displaystyle{\sf head}(x,x_{p}),\overline{{\sf head}}(x,x_{p})$
$\displaystyle\rightarrow\exists y\;{\sf err}_{\kappa+1}(y).$

The initial configuration is represented by the constant $a$ and encoded with
the following facts in $D$:

$\displaystyle{\sf state}_{q_{0}}(a)$ $\displaystyle{\sf
head}(a,c^{\kappa}_{0})$ $\displaystyle{\sf tape}_{e_{i}}(a,c^{\kappa}_{i-1})$
$\displaystyle\textrm{ for }1\leq i\leq n$ $\displaystyle{\sf
tape}_{\textvisiblespace}(a,c^{\kappa}_{n}),{\sf
blanks}_{\triangleright}(a,c^{\kappa}_{n})$

The predicate ${\sf blanks}_{\triangleright}(a,c^{\kappa}_{n})$ initiates
another propagation, see Rule 13 in Figure 4. For the above to work, we want
each constant $c^{\kappa}_{i}$ to represent the $i^{\text{th}}$ element of the
$\kappa^{\text{th}}$ order, for $1\leq i\leq n$. To achieve this, we actually
need constants $c^{k}_{i}$ for _all_ $k\in\\{1,\dots,\kappa\\}$ and all
$i\in\\{1,\dots,n\\}$. This is because we need to properly setup the bit
values for the constants $c^{\kappa}_{n}$ for which we need the first elements
of the $(\kappa-1)^{\text{st}}$, and so on, recursively. For
$i\in\\{1,\dots,n\\}$, we use $b^{(i)}_{0}\dots b^{(i)}_{n}$ to denote the
binary encoding of $i$ with $n+1$ bits. Notice that $b^{(i)}_{n}$ is always
$0$ since we use $n+1$ bits to encode an integer that is bounded by $n$. For
every $k\in\\{2,\dots,\kappa\\}$, every $i,j\in\\{0,\dots,n\\}$, we now add
facts:

$\displaystyle{\sf bit}_{k,b^{(i)}_{j}}(c^{k}_{i},c^{k-1}_{j})$
$\displaystyle{\sf zeros}_{\triangleright}(c^{k}_{i},c^{k-1}_{n}).$

Also here, a predicate ${\sf zeros}_{\triangleright}$ is used to complete the
encoding on long tapes, via Rule 14 in Figure 4.

To generate the other configurations of the ATM computation on input $e$, we
use existential quantifiers in rules. For all $q\in Q$ with $g(q)\notin\\{{\sf
accept},{\sf reject}\\}$, all $s\in\Gamma$, if
$\delta(q,s)=(q_{1},s_{1},m_{1},q_{2},s_{2},m_{2})$ then put for all
$i\in\\{1,2\\}$:

$\begin{array}[]{l@{}r}{\sf state}_{q}(x),{\sf head}(x,x_{h}),{\sf
tape}_{s}(x,x_{h})\ \rightarrow\vskip 3.0pt plus 1.0pt minus 1.0pt\\\ &\exists
y\,\exists y_{h}\,{\sf nextConf}_{i}(x,y,x_{h}),{\sf state}_{q_{i}}(y)\vskip
3.0pt plus 1.0pt minus 1.0pt\\\ &{\sf conf}(y,y_{h}),{\sf
tape}_{s_{i}}(y,x_{h}),{\sf MOV}.\end{array}$

where ${\sf MOV}$ is ${\sf succ}_{\kappa}(x_{h},y_{h})$ if
$m_{i}=\triangleright$ and ${\sf succ}_{\kappa}(y_{h},x_{h})$ if
$m_{i}=\triangleleft$. The above rule sets up correctly the state and head
position of the new configuration, as well as the symbol on the tape at the
position where the head was located previously. We still need to ensure that
the other symbols didn’t change. To this end, we reuse the predicate ${\sf
copy}$ used to copy bit values when moving along each ${\sf succ}_{k}$. First,
we add the following rule:

$\displaystyle{\sf nextConf}_{i}(x,y,x_{h})$ $\displaystyle\rightarrow{\sf
copy_{\triangleleft}}(x,y,x_{h}),{\sf copy_{\triangleright}}(x,y,x_{h}),$

along with copies of Rule 15 from Figure 4 and Rule 3 from Figure 1 for
$k=\kappa$. To guarantee that the symbols are copied, we add, for every
$s\in\Gamma$, the rule

$\displaystyle{\sf copy}(x,y,x_{p}),{\sf tape}_{s}(x,x_{p})\rightarrow{\sf
tape}_{s}(y,x_{p}).$

Note that the constant $a$ is the root of a tree of configurations that are
connected by the (projection to the first two components of the) predicates
${\sf nextConf}_{i}$, $i\in\\{1,2\\}$. We now propagate acceptance information
upwards in that tree. For all states $q\in Q$ with $g(q)={\sf accept}$, add

${\sf state}_{q}(x)\rightarrow{\sf acc}(x).$

Further add, for all $q\in Q$ and $i\in\\{1,2\\}$,

${\sf nextConf}_{i}(x,y,x_{h}),{\sf acc}(y)\rightarrow{\sf acc}_{i}(x).$

Now, for all $q\in Q$ with $g(q)={\sf univ}$, all $q^{\prime}\in Q$ with
$g(q^{\prime})={\sf exist}$, and all $i\in\\{1,2\\}$, add

$\displaystyle{\sf state}_{q}(x),{\sf acc}_{1}(x),{\sf acc}_{2}(x)$
$\displaystyle\rightarrow{\sf acc}(x)$ $\displaystyle{\sf
state}_{q^{\prime}}(x),{\sf acc}_{i}(x)$ $\displaystyle\rightarrow{\sf
acc}(x).$

At the root of the configuration tree, which is $a$, acceptance makes the
query true:

$\displaystyle{\sf acc}(x)$ $\displaystyle\rightarrow{\sf goal}(x).$

We denote $\mathcal{O}$ the obtained set of rules and $D$ the obtained
database. We can now prove the following.

######  Lemma 15.

$\mathcal{M}$ accepts on input $e$ iff $\mathcal{O},D\models_{\sf CP}{\sf
goal}(a)$.

First, notice every ${\sf CP}$-minimal model $\mathfrak{A}$ of
$(\mathcal{O},D)$ satisfies ${\sf
root}^{\mathfrak{A}}=\\{a^{\mathfrak{A}}\\}$. It is clear, from $D$, that
$a^{\mathfrak{A}}\in{\sf root}^{\mathfrak{A}}$. Now assume by contradiction
that $\\{a^{\mathfrak{A}}\\}\subsetneq{\sf root}^{\mathfrak{A}}$. Then we
easily construct a model $\mathfrak{B}<_{\sf CP}\mathfrak{A}$ by setting $B=A$
and interpreting every constant by $a^{\mathfrak{A}}$ and every predicate of
arity $r\geq 1$ as $\\{a^{\mathfrak{A}}\\}^{r}$.

From there and the rules stating each ${\sf err}_{k}$ is subsumed by ${\sf
root}$ and ${\sf goal}$, it follows that in every ${\sf CP}$-minimal model
$\mathfrak{A}$ of $(\mathcal{O},D)$ and for every
$k\in\\{1,\dots,\kappa+1\\}$, if ${\sf err}_{k}^{\mathfrak{A}}\neq\emptyset$,
then ${\sf err}_{k}^{\mathfrak{A}}=\\{a^{\mathfrak{A}}\\}$ and
$\mathfrak{A}\models{\sf goal}(a)$.

For the $(\Rightarrow)$ direction of Lemma 15, it thus remains to treat the
case of ${\sf CP}$-minimal models $\mathfrak{A}$ of $(\mathcal{O},D)$ such
that ${\sf err}_{k}^{\mathfrak{A}}=\emptyset$ for every
$k\in\\{1,\dots,\kappa+1\\}$. We prove that in such a model $\mathfrak{A}$, we
have ${\left|{{\sf ord}_{1}^{\mathfrak{A}}}\right|}=p(n)$ and for every
$k\in\\{2,\dots,\kappa\\}$: ${\left|{{\sf
ord}_{k}^{\mathfrak{A}}}\right|}=2^{{\left|{{\sf
ord}_{k-1}^{\mathfrak{A}}}\right|}}$.

For ${\sf ord}_{1}$, recall that $D$ already specifies $p(n)$ instances of
this predicate, namely the constants $c^{1}_{0},\dots,c^{1}_{p(n)-1}$.
Furthermore, with the predicate ${\sf diff}$, all these constants must be
interpreted as distinct elements, as otherwise ${\sf err}_{1}\neq\emptyset$.
Thus ${\left|{{\sf ord}_{1}^{\mathfrak{A}}}\right|}\geq p(n)$. Now, assume by
contradiction that there exists another instance of ${\sf ord}_{1}$ somewhere
in $A$. We can then construct a model $\mathfrak{B}<_{\sf CP}\mathfrak{A}$,
yielding a contradiction, by interpreting ${\sf ord}_{1}$ as specified in $D$
and by collapsing every further constants and predicates on
$a^{\mathfrak{A}}$. Notice that $a^{\mathfrak{A}}$ cannot be among
interpretations of constants $c^{1}_{0},\dots,c^{1}_{p(n)-1}$ as it would have
triggered ${\sf err}_{1}$. Note that the obtained model $\mathfrak{B}$
satisfies ${\sf err}_{k}^{\mathfrak{B}}=\\{a^{\mathfrak{A}}\\}\supsetneq{\sf
err}_{k}^{\mathfrak{A}}$ for $k\in\\{2,\dots,\kappa+1\\}$ but that
$\mathfrak{B}<_{\sf CP}\mathfrak{A}$ still holds due to the preference order
on minimized predicates, prioritizing ${\sf ord}_{1}$ over those further
predicates.

We then proceed by induction on $k$. The argument is sensibly the same: due to
${\sf err}_{k}^{\mathfrak{A}}=\emptyset$ and the $(k-1)^{\textrm{th}}$ tape
having the intended size, it is readily verified that each constant
$c^{k}_{0}$ starts a tape, following predicate ${\sf succ}_{k}$, of length at
least $2^{{\left|{{\sf ord}_{k-1}^{\mathfrak{A}}}\right|}}$. The existence of
an extra instance beyond those $2^{{\left|{{\sf
ord}_{k-1}^{\mathfrak{A}}}\right|}}$ is denied in the same manner, that is by
constructing a $\mathfrak{B}<_{\sf CP}\mathfrak{A}$ collapsing all predicates
concerning further tapes on $a^{\mathfrak{A}}$ and crucially relying on the
preference order.

We thus proved that all ${\sf CP}$-minimal models of $(\mathcal{O},D)$ either
have a non-empty ${\sf err}_{k}$ for some $k\in\\{1,\dots,\kappa+1\\}$, in
which case they satisfy the query, or produce a $\kappa^{\textrm{th}}$ tape
with exactly the correct size for our ATM to run on. In this latter case,
${\sf err}_{\kappa+1}$ being empty guarantees that the model $\mathfrak{A}$
encodes a valid computation of $\mathcal{M}$ on input $e$. Therefore, if
$\mathcal{M}$ accepts on input $e$, then the ${\sf acc}$ predicate is carried
back to the root and yields $\mathfrak{A}\models{\sf goal}(a)$, which
concludes the $(\Rightarrow)$ direction of Lemma 15. For the $(\Leftarrow)$
direction, we assume $\mathcal{M}$ does not accept on input $e$, and we
construct $\mathfrak{A}$ representing the computation of $\mathcal{M}$ on $e$
exactly as intended. ${\sf CP}$-minimality of $\mathfrak{A}$ follows from the
intermediate claims we already proved.


* [65] C. Hahn, M. J. Wilson, O. Ruiz-Macias, S. Cole, D. H. Weinberg, J. Moustakas, A. Kremin, J. L. Tinker, A. Smith, R. H. Wechsler, S. Ahlen, S. Alam, S. Bailey, D. Brooks, A. P. Cooper, T. M. Davis, K. Dawson, A. Dey, B. Dey, S. Eftekharzadeh, D. J. Eisenstein, K. Fanning, J. E. Forero-Romero, C. S. Frenk, E. Gaztañaga, S. G. A. Gontcho, J. Guy, K. Honscheid, M. Ishak, S. Juneau, R. Kehoe, T. Kisner, T.-W. Lan, M. Landriau, L. L. Guillou, M. E. Levi, C. Magneville, P. Martini, A. Meisner, A. D. Myers, J. Nie, P. Norberg, N. Palanque-Delabrouille, W. J. Percival, C. Poppett, F. Prada, A. Raichoor, A. J. Ross, S. Safonova, C. Saulder, E. Schlafly, D. Schlegel, D. Sierra-Porta, G. Tarle, B. A. Weaver, C. Yèche, P. Zarrouk, R. Zhou, Z. Zhou, and H. Zou, DESI Bright Galaxy Survey: Final Target Selection, Design, and Validation, The Astronomical Journal 165 (June, 2023) 253, [arXiv:2208.08512].
  * [66] E. Chaussidon, C. Yèche, N. Palanque-Delabrouille, D. M. Alexander, J. Yang, S. Ahlen, S. Bailey, D. Brooks, Z. Cai, S. Chabanier, T. M. Davis, K. Dawson, A. de la Macorra, A. Dey, B. Dey, S. Eftekharzadeh, D. J. Eisenstein, K. Fanning, A. Font-Ribera, E. Gaztañaga, S. G. A. Gontcho, A. X. Gonzalez-Morales, J. Guy, H. K. Herrera-Alcantar, K. Honscheid, M. Ishak, L. Jiang, S. Juneau, R. Kehoe, T. Kisner, A. Kovács, A. Kremin, T.-W. Lan, M. Landriau, L. L. Guillou, M. E. Levi, C. Magneville, P. Martini, A. M. Meisner, J. Moustakas, A. Muñoz-Gutiérrez, A. D. Myers, J. A. Newman, J. Nie, W. J. Percival, C. Poppett, F. Prada, A. Raichoor, C. Ravoux, A. J. Ross, E. Schlafly, D. Schlegel, T. Tan, G. Tarlé, R. Zhou, Z. Zhou, and H. Zou, Target Selection and Validation of DESI Quasars, The Astrophysical Journal 944 (Feb., 2023) 107, [arXiv:2208.08511].
  * [67] A. Raichoor, J. Moustakas, J. A. Newman, T. Karim, S. Ahlen, S. Alam, S. Bailey, D. Brooks, K. Dawson, A. de la Macorra, A. de Mattia, A. Dey, B. Dey, G. Dhungana, S. Eftekharzadeh, D. J. Eisenstein, K. Fanning, A. Font-Ribera, J. Garcia-Bellido, E. Gaztanaga, S. G. A. Gontcho, J. Guy, K. Honscheid, M. Ishak, R. Kehoe, T. Kisner, A. Kremin, T.-W. Lan, M. Landriau, L. L. Guillou, M. E. Levi, C. Magneville, P. Martini, A. M. Meisner, A. D. Myers, J. Nie, N. Palanque-Delabrouille, W. J. Percival, C. Poppett, F. Prada, A. J. Ross, V. Ruhlmann-Kleider, C. G. Sabiu, E. F. Schlafly, D. Schlegel, G. Tarle, B. A. Weaver, C. Yeche, R. Zhou, Z. Zhou, and H. Zou, Target Selection and Validation of DESI Emission Line Galaxies, The Astronomical Journal 165 (Mar., 2023) 126, [arXiv:2208.08513].
  * [68] F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay, Scikit-learn: Machine Learning in Python, Journal of Machine Learning Research 12 (2011) 2825–2830.