\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H_1)\wedge H_1(i)=\langle i,a\rangle \wedge Con_n^{([\mathscr{R}_{\Theta}],i)}(a,a') \rightarrow \exists H_2\leq \langle n,\langle n,l\rangle\rangle,\\
\hspace {0pt}\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H_2)\wedge H_2(i)=\langle i,a'\rangle \wedge(\forall j\neq i<n,\, H_1(j)=H_2(j)).
\end{gathered}
\end{equation}

Finally, we say that the solution set $\mathscr{R}_{\Theta}$ to $\Theta$ is rectangular if all its variables are rectangular:

\begin{equation}
RectInst(\mathscr{R}_{\Theta})\iff \forall i<n,\,RectPr(\mathscr{R}_{\Theta},i).
\end{equation}

Note that $RectPr(\mathscr{R}_{\Theta},i)$ is $\Sigma^{1,b}_2$-formula.

Note that the parallelogram property implies rectangularity, and if $i$th coordinate of the relation $R$ is rectangular, then $Con^{([\mathscr{R}_{\Theta}],i)}$ is a congruence.

A binary relation $R\leq D_i\times D_j$ is called essential if it cannot be represented as a conjunction of relations with smaller arities. A pair $(a_i,a_j)\in D_i\times D_j$ is called essential for $R$ if

\begin{equation}
\begin{gathered}
EssPair(a_i,a_j,R)\iff \neg R(a_i,a_j)\wedge \exists b_i\in D_i,\exists b_j\in D_j,\, \\
\hspace {0pt}R(a_i,b_j)\wedge R(b_i,a_j).
\end{gathered}
\end{equation}

It is known [20] that for a relation $R$ being an essential is equivalent to having an essential pair. Thus, we can define an essential binary relation $R$ as follows:

\begin{equation}
\begin{gathered}
EssRel_2(R)\iff \exists a_i\in D_i,\exists a_j\in D_j,\,EssPair(a_i,a_j,R).
\end{gathered}
\end{equation}

For a solution set $\mathscr{R}_{\Theta}$ we define an essential tuple by the following $\Sigma^{1,b}_1$-formula:

\begin{equation}
\begin{gathered}
EssTuple(H,\mathscr{R}_{\Theta})\iff \neg \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H)\wedge \forall i<n,\exists b<l,\exists H'\leq \langle n,\langle n,l\rangle\rangle,\\
\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H')\wedge H'(i) = \langle i, b\rangle\wedge \forall j\neq i<n,\, H'(j) = H(j).
\end{gathered}
\end{equation}

Thus, $\mathscr{R}_{\Theta}$ is essential if there exists an essential tuple.

\begin{equation}
\begin{gathered}
EssRel(\mathscr{R}_{\Theta})\iff \exists H\leq \langle n,\langle n,l\rangle\rangle,\,EssTuple(H,\mathscr{R}_{\Theta}).
\end{gathered}
\end{equation}

We say that a relation $\mathscr{R}\leq D_{0}\times ...\times D_{n-1}$ is $(C_0,...,C_{n-1})$-essential if $\mathscr{R}\cap (C_0,...,C_{n-1})=\emptyset$, but for every $i\leq k$, $\mathscr{R}\cap (C_0,...,C_{i-1},D_i,C_{i+1},...,C_{n-1})\neq \emptyset$. We can formalize the tuple $(C_0,...,C_{n-1})$ as usual, by one set $C(i,a)\iff C_i(a)$.

\begin{equation}
\begin{gathered}
\hspace {0pt}EssRel(\mathscr{R},C)\iff \neg (\exists H\in \mathscr{R},\,\forall i<n, \exists c_i\in C_i,\,\,H(i)=\langle i,c_i\rangle)\wedge \\
\forall i<n,\exists H\in \mathscr{R},\exists a_i\in D_i\backslash C_i,\,H(i)=\langle i,a_i\rangle\wedge \\
\wedge \forall j\neq i, j<n,\,\exists c_j\in C_j,\,\,H(j)=\langle j,c_j\rangle.
\end{gathered}
\end{equation}

This is $\Sigma^{\mathscr{B}}_0$-formula, but if we restrict ourselves to solution sets, we get a Boolean combination of $\Sigma^{1,b}_1$ and $\Pi^{1,b}_1$ formulas.

Finally, to define a key relation, we first present a unary vector function that preserves the relation. Suppose $R\leq D_0\times...\times D_{s-1}$ and define a tuple $\Psi=(\psi_0,...,\psi_{s-1})$, where $\psi_i:D_i\to D_i$, is called a unary-vector function. We say that $\psi$ preserves $R$ if $(\psi_0(a_0),...,\psi_{s-1}(a_{s-1}))\in R$ for every $(a_0,...,a_{s-1})\in R$. We say that $R$ is a key relation if there exists a tuple $(b_0,...,b_{s-1})\notin R$ such that for any tuple $(c_0,...,c_{s-1})\notin R$ there exists a vector function $\Psi$ which preserves $R$ and gives $\psi_i(c_i)=b_i$ for any $i<s$. For a binary relation $R\leq D_i\times D_j$ there is a pair of unary functions $\psi_i,\psi_j$, represented by two-dimensional sets, such that:
\begin{equation}
\begin{gathered}
VecFun_2(R,\psi_i,\psi_j)\iff MAP(D_i,l,D_i,l,\psi_i)\wedge MAP(D_j,l,D_j,l,\psi_j)\wedge\\
\hspace{0pt}\wedge\forall a_i,b_i\in D_i,\forall a_j,b_j\in D_j,\,R(a_i,a_j)\wedge \psi_i(a_i,b_i)\wedge \psi_j(a_j,b_j)\rightarrow R(b_i,b_j).
\end{gathered}
\end{equation}

Obviously, both $\psi_i,\psi_j$ are polymorphisms. We say that a binary relation $R$ is a key relation if there exists a tuple $(b_i,b_j)\notin R$ such that for every $(c_i,c_j)\notin R$ there exists a unary vector function represented by sets $\psi_i,\psi_j$ that preserves $R$ and $\psi(c_i,b_i)$ and $\psi_j(c_j,b_j)$:

\begin{equation}
\begin{gathered}
\hspace{0pt}KeyRel_2(R)\iff \exists b_i,b_j<l,\forall c_i,c_j<l\,\\
\neg R(b_i,b_j)\wedge \neg R(c_i,c_j)\rightarrow \bigvee_{\psi_i,\psi_j < l^2} \,VecFun_2(R,\psi_i,\psi_j)\wedge\psi_i(c_i,b_i)\wedge \psi_j(c_j,b_j).
\end{gathered}
\end{equation}

Note that already for binary relations it would be $\Sigma^{1,b}_1$-formula if we do not fix the algebra $\mathbb{A}$. But in our case, we can go through all possible endomorphisms on $D_i,D_j$. For a solution set $\mathscr{R}_{\Theta}\leq D_{0}\times ...\times D_{n-1}$ we can represent a unary vector function as a three-dimensional set $\Psi(i,a,b)$, where each $\Psi_i$ represents a function from $D_i$ to $D_i$. Consider the following $\Pi^{1,b}_1$-formula:

\begin{equation}\label{laalks34523}
\begin{gathered}
\hspace{0pt}VecFun(\mathscr{R}_{\Theta},\Psi) \iff \forall i<n,\,MAP(D_i,l,D_i,l,\Psi_i)\wedge\\
\wedge \forall H,H'\leq \langle n,\langle n,l\rangle\rangle,\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H)\wedge\\
\wedge (\forall i<n,\forall a_i,b_i\in D_i,\,H(i)=\langle i,a_i\rangle\wedge \Psi_i(a_i,b_i)\rightarrow H'(i)=\langle i,b_i\rangle  )\rightarrow \\
\rightarrow\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H').
\end{gathered}
\end{equation}

Then for a solution set $\mathscr{R}_{\Theta}\leq D_{0}\times ...\times D_{n-1}$ we have the following $\Sigma^{1,b}_4$-formula:

\begin{equation}
\begin{gathered}
\hspace {0pt}KeyRel(\mathscr{R}_{\Theta})\iff \exists H\leq \langle n,\langle n,l\rangle\rangle, \forall H'\leq \langle n,\langle n,l\rangle\rangle,\,\neg \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H)\wedge \\
\wedge \neg \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H')\rightarrow\exists \Psi\leq \langle n,l,l\rangle,\,VecFun(\mathscr{R}_{\Theta},\Psi)\wedge \\
\wedge (\forall i<n,\forall a_i,b_i<l,\,\,H'(i)=\langle i,a_i\rangle\wedge \Psi_i(a_i,b_i) \rightarrow H(i)=\langle i,b_i\rangle).
\end{gathered}
\end{equation}

§.§.§ Bridges and connectivity

We say that a congruence $\sigma$ on $D_i$ is irreducible if it is proper, and it cannot be represented as an intersection of other binary relations stable under $\sigma$.

\begin{equation}
\begin{gathered}
\hspace{0pt}irCong_m(\sigma,D_i)\iff pCong_m(D_i,\Omega,\sigma)\wedge\exists a,b\in D_i, \forall j<2^{l^2},\\
\hspace {0pt}\sigma\subsetneq\Gamma^2_{\mathcal{D},j}\wedge Stable_2(\Gamma^2_{\mathcal{D},j},\sigma)\rightarrow(\Gamma^2_{\mathcal{D},j}(a,b)\wedge \neg \sigma(a,b)).
\end{gathered}
\end{equation}

We denote the set of all irreducible congruences on $D$ by $\Sigma^{ir}_{\mathcal{D}}$. For an irreducible congruence $\sigma$ on set $D$ by $\sigma^*$ is denoted the minimal binary relation $\sigma\subsetneq\sigma^*$ stable under $\sigma$. We can define a string function

\begin{equation}
\begin{gathered}
\cdot^*(\sigma)(a,b)=\sigma^*(a,b)\iff \bigvee_{\sigma'\leq \langle l,l\rangle} Stable_2(\sigma',\sigma)\wedge \sigma\subsetneq\sigma'\wedge\forall j<2^{l^2},\\
\hspace {0pt}Stable_2 (\Gamma^2_{\mathcal{D},j},\sigma)\wedge \sigma\subsetneq \Gamma^2_{\mathcal{D},j}\rightarrow \sigma'\subseteq \Gamma^2_{\mathcal{D},j}\wedge \sigma(a,b).
\end{gathered}
\end{equation}

Any congruence $\sigma'$ containing $\sigma$ is stable under $\sigma$, but a binary relation stable under $\sigma$ does not need to be a congruence.

For two domains $D_i,D_j$ and congruences on them $\sigma_i,\sigma_j$ respectively, we say that a $4$-ary relation $\rho\subseteq D_i^2\times D^2_j$ is a bridge from $\sigma_i$ to $\sigma_j$ if the first two variables of $\rho$ are stable under $\sigma_1$ and the last two variables of $\rho$ are stable under $\sigma_2$, $\sigma_1\subsetneq pr_{1,2}(\rho)$ and $\sigma_2\subsetneq pr_{3,4}(\rho)$, and $(a_1,a_2,a_3,a_4)\in \rho$ implies

$$(a_1,a_2)\in \sigma_1\iff (a_3,a_4)\in \sigma_2.

We can define it by $\Sigma^{1,b}_0$-formula:

\begin{equation}
\begin{gathered}
\hspace {0pt}Bridge(\rho,\sigma_i,\sigma_j)\iff (\exists a,a'\in D_i,\exists b,b'\in D_j,\\
\hspace{0pt}pr_{1,2}(\rho)(a,a')\wedge \neg\sigma_i(a,a')\wedge pr_{3,4}(\rho)(b,b')\wedge \neg\sigma_j(b,b'))\wedge\\
\wedge Stable_2(\rho,1,\sigma_i)\wedge Stable_2(\rho,2,\sigma_i)\wedge Stable_2(\rho,3,\sigma_j)\wedge Stable_2(\rho,4,\sigma_j)\wedge \\
\hspace {0pt}\wedge (\forall a,a'\in D_i,\forall b,b'\in D_j,\ \rho(a,a',b,b')\rightarrow (\sigma_i(a,a')\leftrightarrow \sigma_j(b,b'))).
\end{gathered}
\end{equation}

In words, the projection of $\rho$ to the first two coordinates strictly contains $\sigma_i$ and is a full relation between some set of congruence blocks on the first coordinate and some set of blocks on the second coordinate, and the same for the projection of $\rho$ to the last two coordinates, and the first two coordinates contain elements from one congruence block of $\sigma_i$ if and only if the last two coordinates also contain elements from one congruence block of $\sigma_j$. A bridge $\rho\subseteq D^4$ is called reflexive if $(a,a,a,a)\in \rho$ for every $a\in D$. For a bridge $\rho$, denote by $\tilde{\rho}$ the binary relation defined by $\tilde{\rho}(x,y)=\rho(x,x,y,y)$, we define it as a string function:

\begin{equation}
\tilde{\cdot}(\rho)(x,y) = \tilde{\rho}(x,y)\iff \rho(x,x,y,y).
\end{equation}

A reflexive bridge $\rho$ from an irreducible congruence $\sigma_i$ to an irreducible congruence $\sigma_j$ is
called optimal if there is no a reflexive bridge $\rho'$ from $\sigma_i$ to $\sigma_j$ such that $\tilde{\rho}\subsetneq \tilde{\rho}'$, i.e. a bridge that contains more congruence blocks than $\rho$.

\begin{equation}
\begin{gathered}
OptBridge(\rho,\sigma_i,\sigma_j)\iff irCong_m(\sigma_i,D)\wedge irCong_m(\sigma_j,D)\wedge \\
\wedge\neg (\bigvee_{\rho'\leq (4l)^{2^4}} Bridge(\rho',\sigma_i,\sigma_j)\wedge \forall a\in D,\,\rho'(a,a,a,a)\wedge \tilde{\rho}\subsetneq \tilde{\rho}').
\end{gathered}
\end{equation}

If $\rho$ is optimal, then $\tilde{\rho}$ is a congruence. For an irreducible congruence $\sigma$, define a string function $opt$ as

\begin{equation}
opt(\sigma)(x,y) \iff \bigvee_{\rho\leq (4l)^{2^4}} OptBridge(\rho,\sigma,\sigma)\wedge \tilde{\rho}(x,y).
\end{equation}

It returns the congruence $\tilde{\rho}$ for an optimal bridge $\rho$ from $\sigma$ to $\sigma$, which is well-defined since we can compose two reflexive bridges. For a set of irreducible congruences $\Sigma^{ir}_{\mathcal{D}}$, we define a string function $optset$ that returns the set of $opt(\sigma)$ for all $\sigma\in \Sigma^{ir}_{\mathcal{D}}$:

\begin{equation}
\begin{gathered}
optset(\Sigma^{ir}_{\mathcal{D}})(i,a,b)\iff \Sigma^{ir}_{\mathcal{D},i}\neq \emptyset\wedge opt(\Sigma^{ir}_{\mathcal{D},i})(a,b).
\end{gathered}
\end{equation}

We say that two congruences $\sigma_i,\sigma_j$ on a set $D$ are adjacent if there exists a reflexive bridge from $\sigma_i$ to $\sigma_j$. Since we consider only finite and fixed set of binary constraints $\Gamma^2_{\mathcal{A}}$, including the set of all congruences on $A$ and all its subuniverses, we know in advance all bridges for all congruences, the list denoted by $\Xi$:

\begin{equation}
\begin{gathered}
Adj(\sigma_i,\sigma_j)\iff \bigvee_{\rho\,\in \,\Xi}Bridge(\rho,\sigma_i,\sigma_j)\wedge \forall a\in D,\,\rho(a,a,a,a).
\end{gathered}
\end{equation}

Note that $Adj(\sigma_i,\sigma_j)$ is $\Sigma^{1,b}_0$-formula. We say that two rectangular constraints $C_1,C_2$ are adjacent in a common variable $x$ if $Con_2^{(C_1,x)}$ and $Con_2^{(C_2,x)}$ are adjacent.
A formula is called connected if every constraint in the formula is critical and rectangular, and the graph, whose vertices are constraints and edges are adjacent constraints, is connected. To define connectivity, recall that there is a path from $i$ to $j$ in the input digraph $\mathcal{X}$ if there exists a path $\mathcal{P}_t$ of some length $t$ that can be homomorphically mapped to $\mathcal{X}$ such that $H(0)=i$ and $H(t)=j$. For an instance $\Theta$, we define the following $\Sigma^{1,b}_1$-relation of being connected:

\begin{equation}
\begin{gathered}
Connected(\Theta)\iff\forall i,j<n,\,E_{\mathcal{X}}(i,j)\rightarrow Critical_2(E^{ij}_{\ddot{\mathcal{A}}})\wedge \\
\wedge RectPr_2(E^{ij}_{\ddot{\mathcal{A}}},i)\wedge RectPr_2(E^{ij}_{\ddot{\mathcal{A}}},j)\wedge \\
\hspace {0pt}\wedge \forall i,j,k,s<n,\,E_{\mathcal{X}}(i,j)\wedge E_{\mathcal{X}}(k,s) \rightarrow \exists \mathcal{P}_t< \langle n,4n^2\rangle,\exists H\leq \langle t,n \rangle,\,PATH(V_{\mathcal{P}_t}) \wedge\\
\hspace {0pt}\wedge HOM(\mathcal{P}_t,\mathcal{X},H)\wedge(H(0,i)\wedge H(t,s)) \wedge \\
\hspace {0pt}\wedge \forall p\leq t-2,\, Adj(Con_2^{(E_{\mathcal{X}}(H(p),H(p+1)), H(p+1))},Con_2^{(E_{\mathcal{X}}(H(p+1),H(p+2)),H(p+1))}),
\end{gathered}
\end{equation}

where by $E_{\mathcal{X}}(H(p),H(p+1)))$ and $E_{\mathcal{X}}(H(p+1),H(p+2))$ we abbreviate all four combinations of non-symmetric constraints.

§.§ One-of-four subuniverses

In this section, we will define $4$ different subuniverses for an algebra $\mathbb{D}=(D,\Omega)$. For $D$ being a subuniverse for a fixed algebra $\mathbb{A}=(A,\Omega)$, all these definitions are $\Sigma^{1,b}_0$-formulas. The part of the content of the section repeats the formalization previously introduced in [8]. We cannot omit it here due to the crucial importance of these concepts for the understanding of the paper.

§.§.§ Binary absorption subuniverse

For the fixed algebra $\mathbb{A}=(A,\Omega)$, Due to Theorem <ref> $Clone(\Omega)=Pol(\Gamma_{\mathcal{A}})$. Thus, for any binary term operation $T$ over $A$ the condition $T\in Clone(\Omega)$ can be encoded as:

\begin{equation}
T\in Clone(\Omega) \iff Pol_{2}(T,A, \Gamma_{\mathcal{A}}).
\end{equation}

For any three sets $D,B,T$ the following $\Sigma^{1,b}_0$-definable relation indicates that the subset $B$ absorbs $D$ with binary operation $T$.

\begin{equation}
\begin{gathered}
BAsubS(B,D,T)\iff subS(B,D)\wedge \forall a\in D, \forall b\in B, \exists c_1,c_2\in B,\\
\hspace {0pt}T(a,b)=c_1\wedge T(b,a)=c_2.
\end{gathered}
\end{equation}

If we want to define a subuniverse, then

\begin{equation}
\begin{gathered}
BAsubU(B,D,T,\Omega)\iff SwNU(\Omega,B)\wedge Pol_2(T,D,\Gamma_{\mathcal{A}})\wedge\\
\hspace {0pt}\wedge BAsubS(B,D,T).
\end{gathered}
\end{equation}

Recall that a binary absorbing subuniverse can be trivial, i.e. $B=D$.

§.§.§ Central subuniverse

To define a central subuniverse $C$ of an algebra $\mathbb{A}=(A,\Omega)$ we need to encode a set $Sg$ for the subset $X=\{\{a\}\times C,C\times \{a\}\}$ of $A^2$ for any $a\in A$. Recall that $Sg(X)$ can be constructed by the closure operator

\begin{equation}
\begin{gathered}
\hspace{0pt}Cl(X)=X\cup\{\Omega(a_1,...,a_m): a_1,...,a_m\in X\}\\
\hspace{0pt}\forall t\geq 0, Cl^0(X)=X, Cl^{t+1}(X) = Cl(Cl^t(X)).
\end{gathered}
\end{equation}

Since $\mathbb{A}$ is finite of size $l$ and $|X|=2|C|$, we do not need more than $(l^2-2|C|)$ applications of the closure operator $Cl$ because at any application we either add to the set at least one element or, after some $t$, $Cl^t(X)=Cl^{t+r}(X)$ for any $r$. Not to depend on $C$, let us choose the value $l^2$. Thus, for any set $X\leq \langle l,l\rangle$, we will iteratively define the following set $Cl^{l^2}_X$ up to $l^2$:

\begin{equation}
\begin{gathered}
\hspace{0pt}\forall b,c<l,\,Cl^{0}_X(b,c)\iff X(b,c)\wedge\\
\hspace{0pt}\wedge \forall 0<t<l^2, \forall b,c<l,\, Cl^{t}_X(b,c)\iff Cl^{t-1}_X(b,c)\vee\\
\vee\exists b_1,...,b_m,c_1,...,c_m\in A,Cl^{t-1}_X(b_1,c_1)\wedge...\wedge Cl^{t-1}_X(b_m,c_m)\wedge\\
\hspace {0pt}\wedge\Omega(b_1,...,b_m)=b\wedge \Omega(c_1,...,c_m)=c.
\end{gathered}
\end{equation}

The existence of this set follows from $\Sigma^{1,b}_1$-induction. A central subuniverse must be an absorbing subuniverse, namely, a ternary absorbing subuniverse [22]. For any three sets $D,C,S$ the following $\Sigma^{1,b}_0$-definable relation ($D$ and $C$ are bounded by $l$) expresses that the subset $C$ of $D$ is central under ternary term operation $S$:

\begin{equation}
\begin{gathered}
\hspace{0pt}CRsubS(C,D,S)\iff subS(C,D)\wedge\forall c_1,c_2\in C, \forall a\in D, \exists c'_1,c'_2,c'_3\in C,\\
\hspace{0pt}S(c_1,c_2,a)=c'_1\wedge S(c_1,a,c_2)=c'_2\wedge S(a,c_1,c_2)=c'_3\wedge\\
\hspace {0pt}\wedge\bigwedge_{a\in D\backslash C} \bigwedge_{X<\langle l,l\rangle} ((X(a,c)\wedge X(c,a)\leftrightarrow c\in C) \rightarrow \neg Cl^{l^2}_X(a,a)).
\end{gathered}
\end{equation}

Note that for not fixed algebra $\mathbb{B}=(B,\Omega)$, this relation is $\Pi^{1,b}_1$ since the size of $B$ would not be bounded, and therefore we could not use large conjunction. If we want to define a subuniverse, then

\begin{equation}
\begin{gathered}
\hspace{0pt}CRsubU(C,D,S,\Omega)\iff SwNU(\Omega,C)\wedge Pol_2(S,D,\Gamma_{\mathcal{A}})\wedge\\
\hspace {0pt}\wedge CRsubS(C,D,S).
\end{gathered}
\end{equation}

Recall that a central subuniverse can be trivial, i.e. $C=D$.

§.§.§ PC subuniverse

Polynomially complete algebras are necessarily simple [10], i.e. they have no non-trivial congruence relations. The ternary discriminator function is the function $t$ defined by the identities

\[
t(x,y,z) =
\begin{cases}
z, \,x=y, \\
x, \,x\neq y.
\end{cases}
\]

Then Theorem <ref> gives a necessary and sufficient condition of polynomial completeness.

A finite algebra is polynomially complete if and only if it has the ternary discriminator as a polynomial operation.

The clone of all polynomials over $\mathbb{D}$, $Polynom(\mathbb{D})$ is defined as the clone generated by $\Omega$ and all constants on $D$, i.e. nullary operations:

\begin{equation}
Polynom(\mathbb{D}) = Clone(\Omega,a_1,...,a_{|D|}).
\end{equation}

Constants as nullary operations with constant values, composed with $0$-many $n$-ary operations are $n$-ary operations with constant values. Thus, to be preserved by all constant operations, any unary relation has to contain the entire set $D$, and any binary relation has to contain the diagonal relation $\Delta_{D}$. For the algebra $\mathbb{D}=(D,\Omega)$ denote by $\Gamma^{diag}_{\mathcal{D}} = (\Gamma^{1,diag}_{\mathcal{D}}, \Gamma^{2,diag}_{\mathcal{D}})$ the pair of sets such that

\begin{equation}\label{'''''''''''l}
\begin{gathered}
\hspace {0pt}\Gamma^{1,diag}_{\mathcal{D}}(j,a)\iff \Gamma^{1}_{\mathcal{D}}(j,a)\wedge (\forall b\in A, \Gamma^{1}_{\mathcal{D}}(j,b))\\
\Gamma^{2,diag}_{\mathcal{D}}(i,a,b)\iff \Gamma^{2}_{\mathcal{D}}(i,a,b)\wedge (\forall c\in A, \Gamma^{2}_{\mathcal{D}}(j,c,c)).
\end{gathered}
\end{equation}

Note that for some $i,j$, $\Gamma^{1,diag}_{\mathcal{D},j}$ and $\Gamma^{2,diag}_{\mathcal{D},i}$ are empty sets. An $n$-ary operation $P$ on algebra $\mathbb{D}$ is a polynomial operation if it is a polymorphism for relations from $\Gamma^{diag}_{\mathcal{D}}$, i.e.

\begin{equation}
P\in Polynom(\mathbb{D})\iff Pol_{n}(P,D,\Gamma^{diag}_{\mathcal{D}}).
\end{equation}

For any two sets $D$ and $P$ the following $\Sigma^{1,b}_0$-definable relation claims that $P$ is a ternary discriminator on $D$.

\begin{equation}
\begin{gathered}
\hspace{0pt}PCD(D,P)\iff \forall a,b,c\in D, \\
(a=b\wedge P(a,b,c)=c)\vee(a\neq b\wedge P(a,b,c)=a).
\end{gathered}
\end{equation}

To formalize a PC subuniverse we need the following definition.
We say that an algebra $\mathbb{D}=(D,\Omega)$ is polynomially complete if

\begin{equation}
\begin{gathered}
PCA(D,\Omega)\iff \bigvee_{P\in \Pi^{3}_{\mathcal{D}}} Pol_{3}(P,D,\Gamma^{diag}_{\mathcal{D}})\wedge PCD(D,P).
\end{gathered}
\end{equation}

We say that an algebra $\mathbb{D}=(D,\Omega)$ is an algebra without a non-trivial binary absorbing or central subuniverse if it satisfies the following $\Sigma^{1,b}_0$-definable relation:

\begin{equation}
\begin{gathered}
\hspace {0pt}subTA_{\neg BACR}(D,\Omega)\iff subTA(D,A,\Omega)\wedge \\
\wedge\bigwedge_{B<l}\bigwedge_{T<(3l)^{2^3}} PsubS(B)\wedge Pol_2(T,D, \Gamma_{\mathcal{D}})\rightarrow\neg BAsubU(B,D,T)\wedge\\
\hspace {0pt}\wedge\bigwedge_{C<l}\bigwedge_{S<(4l)^{2^4}} PsubS(C)\wedge Pol_3(S,D, \Gamma_{\mathcal{D}})\rightarrow\neg CRsubU(C,D,S).
\end{gathered}
\end{equation}

Note that for a not fixed algebra $\mathbb{B}=(B,\Omega)$, this relation would be $\Pi^{1,b}_2$ since the size of $B$ would not be bounded, and therefore we could not use big conjunctions for sets and $\neg CRsubU(C,D,S)$ would be $\Sigma^{1,b}_1$-formula. We say that an algebra is polynomially complete algebra without a non-trivial binary absorbing or central subuniverse if

\begin{equation}\label{aaaaaaaaa444444}
\begin{gathered}
\hspace{0pt}PCA_{\neg BACR}(D,\Omega)\iff PCA(D,\Omega)\wedge subTA_{\neg BACR}(D,\Omega).
\end{gathered}
\end{equation}

We say that a set $\sigma<\langle l,l\rangle$ is a PC congruence on algebra $\mathbb{D}=(D,\Omega)$ of size bounded by $l$ if

\begin{equation}
\begin{gathered}
PCCong_m(D,\Omega,\sigma)\iff PCA_{\neg BACR}(D/\sigma,\Omega/\sigma).
\end{gathered}
\end{equation}

Note that in this definition we apply notions from (<ref>) to (<ref>) to algebra $(D/\sigma,$ $\Omega/\sigma)$ and relations from $\Gamma_{\mathcal{D}}/\sigma$, recall (<ref>).

Recall that for algebra $\mathbb{A}=(A,\Omega)$ we denoted the set of all congruences on $\mathbb{A}$ and all its subuniverses by $\Sigma_{\mathcal{A}}$. Using this list we can define the list of congruence on $\mathbb{A}$ and all its subuniverses of any type, for example:

\begin{equation}
\begin{gathered}
\Sigma^{max}_{\mathcal{A}}(i,a,b)\iff \Sigma_{\mathcal{A}}(i,a,b)\wedge maxCong_m(A,\Omega,\Sigma_{\mathcal{A},i});\\
\Sigma^{PC}_{\mathcal{D}}(i,a,b)\iff \Sigma_{\mathcal{D}}(i,a,b)\wedge PCCong_m(D,\Omega,\Sigma_{\mathcal{D},i}).
\end{gathered}
\end{equation}

In these definitions we do not enumerate elements in the lists from the beginning, we thin out the existing lists $\Sigma_{\mathcal{A}}$, $\Sigma_{\mathcal{D}}$. That is, for some $i<2^{l^2}$ the new lists can be empty. Then we say that $\sigma$ is an intersection of all PC congruences on $\mathbb{D}$ if it satisfies the following $\Sigma^{1,b}_0$ relation:

\begin{equation}
\begin{gathered}
CongPC(D,\Omega,\sigma)\iff Cong_m(D,\Omega,\sigma)\wedge (\forall i<2^{l^2},\Sigma^{PC}_{{\mathcal{D}},i}\neq\emptyset\rightarrow \sigma\subseteq\Sigma^{PC}_{{\mathcal{D}},i})\wedge\\
\hspace {0pt}\wedge \bigwedge_{\sigma'<\langle l,l\rangle}(Cong_m(D,\Omega,\sigma')\wedge \sigma\subsetneq \sigma')\rightarrow\exists j<2^{l^2}, \Sigma^{PC}_{{\mathcal{D}},j}\neq\emptyset ,\exists a,b\in D,\\
\hspace {0pt}\sigma'(a,b)\wedge \neg \Sigma^{PC}_{{\mathcal{D}},j}(a,b).
\end{gathered}
\end{equation}

A subuniverse $E\subseteq D$ is called a PC subuniverse if $E=E_0\cap...\cap E_{s-1}$ where each $E_i$ is an equivalence class of some PC congruence.

For an algebra $\mathbb{D}=(D,\Omega)$, $E$ is a PC subuniverse if

\begin{equation}
\begin{gathered}
\hspace {0pt}PCsubU(E,D,\Omega)\iff (E=\emptyset)\vee (E=D)\vee\\
\hspace {0pt}\vee\big((\exists j<2^{l^2},\forall a,b\in E, \Sigma^{PC}_{{\mathcal{D}}}(j,a,b))\wedge\\
\wedge (\exists i< 2^{l^2},\forall a\in E,\forall b\in D,\Sigma_{\mathcal{D}}(i,a,b)\leftrightarrow b\in E)\big).
\end{gathered}
\end{equation}

A PC subuniverse can be empty or full ($E=D$). The condition in the second line ensures that the entire $E$ is inside exactly one block of any number of PC congruences (since we do not restrict the number of different $j$'s in any way) and the condition in the third line ensures that $E$ is indeed a block of some congruence (not necessarily PC congruence since due to the maximality, intersection of any number of PC congruences is not a PC congruence).

We give a second definition of a PC subuniverse in this section straightaway. The following lemma is proved in [21].
[Lemma 7.13.1,   [21]]
Suppose that $\sigma_1,...,\sigma_k$ are all PC congruences on $A$. Put $A_i=A/\sigma_i$, and define $\psi:A\to A_1\times...\times A_k$ by $\psi(a)=(a/\sigma_1,...,a/\sigma_k)$. Then

* $\psi$ is surjective, hence $A/\cap_{i}\sigma_i\cong A_1\times...\times A_k$;

* the PC subuniverses are the sets of the form $\psi^{-1}(S)$ where $S\subseteq A_1\times...\times A_k$ is a relation definable by unary constraints of the form $x_i=a_i$;

* for each non-empty PC subuniverse $B$ of $A$ there is a congruence $\theta$ of $A$ such that $B$ is an equivalence class of $\theta$ and $A/\theta$ is isomorphic to a product of PC algebras having no non-trivial binary absorbing subuniverse or center. That is, $A/\theta\cong A_{j_1}\times... \times A_{j_s}$ where each $A_{j_i}$ is a PC algebra that has no non-trivial binary absorbing subuniverse or center.

Since for a fixed algebra $\mathbb{A}=(A,\Omega)$ and all its subalgebras $D$ we know the list of all PC congruences, we do not need to prove this lemma, the algorithm can just check it. Then, since the algebra $\mathbb{A}$ and all its subalgebras are bounded by size $l$, the maximal possible number of quotients in the direct product $D_0\times ...\times D_{k-1}$ is $s=log_2l$.

For an algebra $\mathbb{D}=(D,\Omega)$, $s=log_2l$, $E$ is a PC subuniverse if

\begin{equation}
\begin{gathered}
\hspace{0pt}PCsubU(E,D,\Omega)\iff (E=\emptyset)\vee (E=D)\vee\big((\exists i< 2^{l^2},\forall a\in E,\forall b\in D,\\
\Sigma_{\mathcal{D}}(i,a,b)\leftrightarrow b\in E)\wedge\\
\hspace {0pt}\wedge \bigvee_{\substack{ (\sigma_0\in \Sigma^{PC}_{D}})}\bigvee_{(H\in \mathrm{M}_{D,\Sigma_{D,i},\sigma_0})} ISO_{alg}(D/\Sigma_{D,i},\Omega/\Sigma_{D,i},D/\sigma_0,\Omega/\sigma_0,H) \vee \\
\hspace {0pt}\vee \bigvee_{\substack{ (\sigma_0,\sigma_1\in \Sigma^{PC}_{D}})}\bigvee_{(H\in \mathrm{M}_{D,\Sigma_{D,i},\sigma_0,\sigma_1})} ISO_{alg}(D/\Sigma_{D,i},\Omega/\Sigma_{D,i},D/\sigma_0\times D/\sigma_1,\\
\Omega/\sigma_0\cap \sigma_1,H) \vee ...\\
\hspace{0pt}...\vee \bigvee_{\substack{ (\sigma_0,...,\sigma_{s-1}\in \Sigma^{PC}_{D}})}\bigvee_{(H\in \mathrm{M}_{D,\Sigma_{D,i},\sigma_0,...,\sigma_{s-1}})} ISO_{alg}(D/\Sigma_{D,i},\Omega/\Sigma_{D,i},D/\sigma_0\times...\\
...\times D/\sigma_{s-1},  \Omega/\cap_{i}\sigma_i ,H)\big).
\end{gathered}
\end{equation}

§.§.§ Linear subuniverse

Since the algebra $\mathbb{A}$ and all its subalgebras are bounded by size $l$, the maximal possible number of prime fields in the prime product $\mathbb{Z}_{p_0}\times ...\times \mathbb{Z}_{p_{k-1}}$ is $s=log_2l$. We formalize a finite abelian group $\mathbb{Z}_p=(Z_p,0,+,-)$, where $p$ is prime, as a set $Z_p$, $|Z_p|=p\wedge \forall a<p, Z_p(a)$, and $+_{(mod\,p)}$, $-_{(mod\,p)}$. For any direct product up to $k\leq log_2l$ abelian groups $\mathbb{Z}_{p_0}\times ...\times \mathbb{Z}_{p_{k-1}}$ we define a set $Z_{p_0}\times...\times Z_{p_{k-1}}\leq (p_0+...+p_{k-1}+1)^{2^k}$ such that for all $a_0<p_0,...,a_{k-1}<p_{k-1}$, $(a_0,...,a_{k-1})\in Z_{p_0}\times...\times Z_{p_{k-1}}$ and

\begin{equation}
\begin{gathered}
\hspace {0pt}\forall a_0,b_0<p_0,...,\forall a_{k-1},b_{k-1}<p_{k-1},\\
+((a_0,...,a_{k-1}),(b_0,...,b_{k-1}))=(a_0+_{(mod\,p_0)} b_0,...,a_{k-1}+_{(mod\,p_{k-1})} b_{k-1}),\\
-((a_0,...,a_{k-1}),(b_0,...,b_{k-1}))=(a_0-_{(mod\,p_0)} b_1,...,a_{k-1}-_{(mod\,p_{k-1})} b_{k-1}).
\end{gathered}
\end{equation}

We will denote elements $(a_0,...,a_{k-1})$ of $Z_{p_0}\times...\times Z_{p_{k-1}}$ by $\bar{a}^k$, and will omit index $_{(mod\,p)}$ when it does not lead to confusion. Also, we allow the use of trivial algebras (with one element $0$) in a product, so $Prime'(p)\iff Prime(p)\vee p=1$.

For an algebra $\mathbb{D}=(D,\Omega)$, $s=log_2l$, we say that it is a linear algebra if

\begin{equation}
\begin{gathered}
LinA(D,\Omega)\iff \bigvee_{\substack{p_0\leq l \\ Prime'(p_0)}}\bigvee_{H\in \mathrm{M}_{D,p_0}} ISO_{alg}(D,\Omega,Z_{p_0},\bar{a}^1_1+...+\bar{a}^1_m,H)\vee\\
\hspace {0pt}\vee\bigvee_{\substack{ p_0\cdot p_1\leq l\\ Prime'(p_0),Prime'(p_1)}} \bigvee_{H\in \mathrm{M}_{D,p_{0},p_{1}}} ISO_{alg}(D,\Omega,Z_{p_0}\times Z_{p_1},\bar{a}^2_1+...+\bar{a}^2_m,H)\vee...\\
\hspace {0pt}...\vee\bigvee_{\substack{p_0\cdot...\cdot p_{s-1}\leq l \\ Prime'(p_0),...,Prime'(p_k)\\
s=log_2l}} \bigvee_{H\in \mathrm{M}_{D,p_{0}, ...,p_{s-1}}} ISO_{alg}(D,\Omega,Z_{p_0}\times...\times Z_{p_{s-1}},\\
\bar{a}^s_1+...+\bar{a}^s_m,H).
\end{gathered}
\end{equation}

We say that a set $\sigma<\langle l,l\rangle$ is a linear congruence on algebra $\mathbb{D}=(D,\Omega)$ if

\begin{equation}
\begin{gathered}
LinCong_m(D,\Omega,\sigma)\iff LinA(D/\sigma,\Omega/\sigma).
\end{gathered}
\end{equation}

We can also check that any linear congruence of algebra $\mathbb{A}$ (or its subalgebras) bounded by size $l$ is a linear congruence for any subalgebra of $\mathbb{A}$ (or their subalgebras). Let us define the set of all linear congruences on $\mathbb{D}$ as:

\begin{equation}
\begin{gathered}
\Sigma^{lin}_{\mathcal{D}}(i,a,b)\iff \Sigma_{\mathcal{D}}(i,a,b)\wedge LinCong_m(D,\Omega,\Sigma_{\mathcal{D},i}).
\end{gathered}
\end{equation}

Then we say that $\sigma$ is the minimal linear congruence (an intersection of all linear congruences) on $D$ if

\begin{equation}
\begin{gathered}
CongLin(D,\Omega,\sigma)\iff \exists i<2^{l^2}, \sigma = \Sigma^{lin}_{{\mathcal{D}},i}\wedge \forall j<2^{l^2},\Sigma^{lin}_{{\mathcal{D}},j}\neq\emptyset\rightarrow \sigma\subseteq\Sigma^{lin}_{{\mathcal{D}},j}.
\end{gathered}
\end{equation}

Note that the definition of $CongLin$ differs from the definition of $CongPC$ since any intersection of linear congruences is again a linear congruence.
A subuniverse $L\subseteq D$ is called a linear subuniverse if it is stable under $CongLin$:

\begin{equation}
\begin{gathered}
LNsubU(L,D,\Omega)\iff SwNU(\Omega,L)\wedge\bigwedge_{\sigma\leq \langle l,l\rangle} CongLin(D,\Omega,\sigma) \rightarrow \\
\rightarrow Stable_1(L,\sigma).
\end{gathered}
\end{equation}

A linear subuniverse is a union of classes of $CongLin$. However, not every union of such classes needs to be a subuniverse. For example, for a linear algebra $(D,\Omega)$ that is isomorphic to $(\mathbb{Z}_p,x_1+...+x_m)$, and a minimal linear congruence $\Delta$ every element of $\mathbb{Z}_p$ is a subuniverse (since $\Omega$ is idempotent), but not any other proper subset of $\mathbb{Z}_p$ is a subuniverse. From here, we get that there are no non-trivial congruences on $(D,\Omega)$ (every congruence block must be a subuniverse).

§.§.§ One-of-four and minimal subuniverse

All the following formulas in this section are $\Sigma^{1,b}_0$ (they would not if $\mathbb{A}$ is not fixed). We say that $B$ is one-of-four subuniverse of $D$ if

\begin{equation}
\begin{gathered}
1of4subU(B,D,\Omega)\iff PCsubU(B,D,\Omega)\vee LNsubU(B,D,\Omega)\vee\\
\hspace {0pt}\vee\bigvee_{T<(3l)^8} BAsubU(B,D,T,\Omega)\vee\bigvee_{S<(4l)^{16}}CRsubU(B,D,S,\Omega).\\
\end{gathered}
\end{equation}

We say that a subuniverse is minimal if it is non-trivial and inclusion minimal (does not contain any other subuniverse of the same type). For example,

\begin{equation}
\begin{gathered}
minBAsubU(B,D,T,\Omega)\iff BAsubU(B,D,T,\Omega)\wedge \bigwedge_{B'<l}\bigwedge_{T'<(3l)^8}B'\subsetneq B \rightarrow\\
\hspace {0pt}\rightarrow\neg BAsubU(B',D,T',\Omega);\\
\hspace {0pt}minLNsubU(B,D,\Omega)\iff LNsubU(B,D,\Omega)\wedge \bigwedge_{B'<l} B'\subsetneq B \rightarrow\\
\hspace {0pt}\rightarrow\neg LNsubU(B',D,\Omega).
\end{gathered}
\end{equation}

For linear and PC subuniverses we also will use the fact that a minimal linear/ PC subuniverse is a block of $CongLin$/ $CongPC$. We denote a block $B$ of a congruence $\sigma$ as

\begin{equation}
Block(B,D,\sigma)\iff \forall a\in B,\forall b\in D, \sigma(a,b)\leftrightarrow b\in B.
\end{equation}

\begin{equation}
\begin{gathered}
minPCsubU^B(B,D,\Omega)\iff \bigwedge_{\sigma<(2l)^4}CongPC(D,\Omega, \sigma)\rightarrow\\
\hspace {0pt}\rightarrow Block(B,D,\sigma);\\
minLNsubU^B(B,D,\Omega)\iff \bigwedge_{\sigma<(2l)^4}CongLin(D,\Omega, \sigma)\rightarrow \\
\hspace {0pt}\rightarrow Block(B,D,\sigma).\\
\end{gathered}
\end{equation}

§.§ Reductions

Note that all further definitions for all types of reductions and strategies are $\Sigma^{1,b}_0$-formulas.

For an instance $\Theta=(\mathcal{X},\ddot{\mathcal{A}})$ with domain set $D=(D_0,...,D_{n-1})$ we say that a set $D^{(\bot)}=(D^{(\bot)}_0,...,D^{(\bot)}_{n-1})$ is an absorbing reduction of $D$ if there exists a term operation $T$ such that $D^{(\bot)}_i$ is a binary absorbing subuniverse of $D_i$ with the term operation $T$ for every $i$:

\begin{equation}
\begin{gathered}
BARed(D^{(\bot)},D)\iff Red(D^{(\bot)},D)\wedge \bigvee_{T<(3l)^{8}}Pol_2(T,D, \Gamma_{\mathcal{D}})\wedge\\
\hspace {0pt}\wedge \forall i<n,\,BAsubU(D^{(\bot)}_i,D_i,T,\Omega).
\end{gathered}
\end{equation}

We say that $D^{(\bot)}=(D^{(\bot)}_0,...,D^{(\bot)}_{n-1})$ is a central reduction if $D_i$ is a central subuniverse for every $i$:

\begin{equation}
\begin{gathered}
CRRed(D^{(\bot)},D)\iff Red(D^{(\bot)},D)\wedge \forall i<n, \\
\hspace{0pt}\bigvee_{S_i<(4l)^{16}} Pol_3(S_i,D, \Gamma_{\mathcal{D}})\wedge CRsub(D^{(\bot)}_i,D_i,S_i).
\end{gathered}
\end{equation}

We say that $D^{(\bot)}=(D^{(\bot)}_0,...,D^{(\bot)}_{n-1})$ is a PC reduction if

\begin{equation}
\begin{gathered}
PCRed(D^{(\bot)},D)\iff Red(D^{(\bot)},D)\wedge \forall i<n,\\
\hspace {0pt}PCsubU(D^{(\bot)}_i,D_i,\Omega)\wedge subTA_{\neg BACR}(D_i,\Omega).
\end{gathered}
\end{equation}

We say that $D^{(\bot)}=(D^{(\bot)}_0,...,D^{(\bot)}_{n-1})$ is a linear reduction if

\begin{equation}
\begin{gathered}
LNRed(D^{(\bot)},D)\iff Red(D^{(\bot)},D)\wedge \forall i<n,\\
\hspace {0pt}LNsubU(D^{(\bot)}_i,D_i,\Omega)\wedge subTA_{\neg BACR}(D_i,\Omega).
\end{gathered}
\end{equation}

In an obvious way, we can define a minimal absorbing/ central/ PC/ linear reduction, a non-linear reduction $nonLNRed(D^{(\bot)},D)$ and one-of-four reduction $1of4Red(D^{(\bot)},D)$.

A CSP instance $\Theta=(\mathcal{X},\ddot{\mathcal{A}})$ is a set

$$\Theta(\langle\, \,\underbrace{\langle n,\langle n,n\rangle \rangle}_{\mathcal{X}},\underbrace{\langle \langle n,l\rangle, \langle\langle n,l\rangle,\langle n,l\rangle \rangle \rangle}_{\ddot{\mathcal{A}}} \, \,   \rangle)$$

Let us denote the length of $\Theta$ as a number function $instsize(n,l)=|\Theta|$.

A strategy for a CSP instance $\Theta = (\mathcal{X},\ddot{\mathcal{A}})$ with domain set $D$ is a sequence of reductions $D^{(0)},...,D^{(s)}$, where $D^{(j)}=(D^{(j)}_0,...,D^{(j)}_{n-1})$, such that $D^{(0)}=D$ and $D^{(j)}$ is a one-of-four $1$-consistent reduction of $\Theta^{(j-1)}$ for every $j\geq 1$. A strategy is called minimal if every reduction in the sequence is minimal. Since after any reduction we decrease at least one domain by at least one element, to represent the entire strategy it is enough to consider a set (matrix) with $nl$ rows, each row representing a reduction of the CSP instance. We need to track both domain reductions (the set $V_{\ddot{\mathcal{A}}}$, or $D$) and restrictions of the constraint relations (the set $E_{\ddot{\mathcal{A}}}$). An input digraph $\mathcal{X}$ does not change, but for consistency, we will track it as well.

A strategy for an instance $\Theta$ up to $s\leq nl$ step is a set $\Theta_{Str}< \langle nl,instsize(n,l)\rangle$ such that:

\begin{equation}
\begin{gathered}
Strategy(\Theta,\Theta_{Str},s)\iff \Theta_{Str}^0=\Theta\wedge \forall 1\leq j\leq s,  1C(\Theta^{(j)}_{Str})\wedge \\
\wedge redinst(\Theta^{(j-1)},D^{(j)})=\Theta^{(j)}_{Str}\wedge \forall 1\leq j\leq s,\, 1of4Red(D^{(j)}_{Str},D).
\end{gathered}
\end{equation}

A strategy is called minimal if

\begin{equation}
\begin{gathered}
minStrategy(\Theta,\Theta_{Str},s)\iff Strategy(\Theta,\Theta_{Str},s)\wedge \forall 1\leq j\leq s,\,\\  \hspace {0pt}min1of4Red(D^{(j)}_{Str},D).
\end{gathered}
\end{equation}

When we want to consider the domain strategy separately, we will refer to it as $D_{Str}<\langle nl,\langle n,l\rangle\rangle$, each $j$th row representing $D^{(j)}$.

§.§ Three universal algebra axiom schemes

In this section, we formalize three universal algebra axiom schemes, reflecting the "only if" implications of Theorems <ref>, <ref>, and <ref> in [21] (for the soundness we do not need the "if" implication). These axiom schemes were already introduced in [8], and we echo the formalization because of its importance for the understanding of the paper. The schemes are formulated for a constraint language $\Gamma_{\mathcal{A}}$ over the set $A$ of size $l$, fixed algebra $\mathbb{A}=(A,\Omega)$ with $\Omega$ being a special $m$-ary WNU operation. They consist of finitely many $\forall \Sigma^{1,b}_2$-formulas (for all possible subuniverses of $\mathbb{A}$).

BA$_\mathcal{A}$-axiom scheme reflects that if $\Theta$ is a cycle-consistent irreducible CSP instance, and $B$ is a non-trivial binary absorbing subuniverse of $D_i$, then $\Theta$ has a solution only if $\Theta$ has a solution with $x_i\in B$ (Theorem <ref> in [21]):

\begin{equation}
\begin{gathered}
\hspace {0pt}BA_{\mathcal{A},B,D}=_{def}\forall\mathcal{X}=(V_{\mathcal{X}},E_{\mathcal{X}}),\forall\ddot{\mathcal{A}}=(V_{\ddot{\mathcal{A}}},E_{\ddot{\mathcal{A}}},D_0,...,D_{n-1}),\\
\hspace {0pt}\big(B\subsetneq D\wedge SwNU_m(\Omega,D)\wedge SwNU_m(\Omega,B)\wedge\\
\hspace{0pt}\wedge\exists T <(3l)^{2^3}, Pol_{2}(T,D, \Gamma_{\mathcal{A}})\wedge BAsubS(B,D,T) \wedge\\
\hspace{0pt}\wedge Inst(\Theta,\Gamma_{\mathcal{A}})\wedge CCInst(\mathcal{X},\ddot{\mathcal{A}})\wedge IRDInst(\mathcal{X},\ddot{\mathcal{A}})\wedge \\
\hspace{0pt}\exists i<n, D_i=D\wedge\\
\hspace{0pt}\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}})\big)\implies \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}}=(V_{\ddot{\mathcal{A}}},E_{\ddot{\mathcal{A}}},D_0,...,B,...,D_{n-1})).
\end{gathered}
\end{equation}

CR$_\mathcal{A}$-axiom scheme states that if $\Theta$ is a cycle-consistent irreducible CSP instance, and $C$ is a non-trivial central subuniverse of $D_i$, then $\Theta$ has a solution only if $\Theta$ has a solution with $x_i\in C$ (Theorem <ref> in [21]):

\begin{equation}
\begin{gathered}
\hspace{0pt}CR_{\mathcal{A},D,C}=_{def}\forall \mathcal{X}=(V_{\mathcal{X}},E_{\mathcal{X}}),\forall\ddot{\mathcal{A}}=(V_{\ddot{\mathcal{A}}},E_{\ddot{\mathcal{A}}},D_0,...,D_{n-1}),\\
\hspace{0pt}\big(C\subsetneq D\wedge SwNU_m(\Omega,D)\wedge SwNU_m(\Omega,C)\wedge\\
\hspace {0pt}\ \exists S<(4l)^{2^4},\,Pol_3(S, D,\Gamma_{\mathcal{A}})\wedge CRsubS(C,D,S) \wedge \\
\hspace {0pt}\wedge Inst(\Theta,\Gamma_{\mathcal{A}})\wedge CCInst(\mathcal{X},\ddot{\mathcal{A}})\wedge IRDInst(\mathcal{X},\ddot{\mathcal{A}})\wedge \\
\hspace{0pt}\exists i<n, D_i=D\wedge\\
\hspace {0pt}\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}})\big)\implies \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}}=(V_{\ddot{\mathcal{A}}},E_{\ddot{\mathcal{A}}},D_0,...,C,...,D_{n-1})).
\end{gathered}
\end{equation}

Finally, PC$_\mathcal{A}$-axioms says that
if $\Theta$ is a cycle-consistent irreducible CSP instance, there does not exist a non-trivial binary absorbing subuniverse or a non-trivial center on $D_j$ for every $j$, $(D_i,\Omega)/\sigma_i$ is a polynomially complete algebra, and $E$ is an equivalence class of $\sigma_i$, then $\Theta$ has a solution only if $\Theta$ has a solution with $x_i\in E$ (Theorem <ref> in [21]):

\begin{equation}
\begin{gathered}
\hspace{0pt}PC_{\mathcal{A},D,E}=_{def}\forall \mathcal{X}=(V_{\mathcal{X}},E_{\mathcal{X}}),\forall\ddot{\mathcal{A}}=(V_{\ddot{\mathcal{A}}},E_{\ddot{\mathcal{A}}},D_0,...,D_{n-1}),\\
\hspace {0pt}\big([\forall j<n,\forall B<l,\forall T<(3l)^{2^3}, Pol_2(T,D_j, \Gamma_{\mathcal{A}})\rightarrow\neg BAsubS(B,D_j,T)\wedge\\
\hspace {0pt}\wedge\forall j<n,\forall C<l, \forall S<(4l)^{2^4}, Pol_3(S,D_j, \Gamma_{\mathcal{A}})\rightarrow\neg CRsubS(C,D_j,S)]\\
\hspace {0pt}\wedge \exists \sigma<\langle l,l\rangle, \exists D/\sigma<l,\exists\Omega/\sigma<(ml)^{2^{m+1}}, FA_m(D/\sigma,\Omega/\sigma,D,\Omega,\sigma)\wedge\\
\hspace {0pt}\wedge \exists P<(4l)^{2^4},\, Pol_{3}(P,D/\sigma,\Gamma^{diag}_{\mathcal{D}}/\sigma)\wedge PCD(D/\sigma,P)\wedge \\
\hspace{0pt}SwNU_m(\Omega,D)\wedge E\subsetneq D\wedge (\forall a\in E,\forall b\in D, \sigma(a,b)\leftrightarrow b\in E)\wedge\\
\hspace {0pt}\wedge Inst(\Theta,\Gamma_{\mathcal{A}})\wedge CCInst(\mathcal{X},\ddot{\mathcal{A}})\wedge IRDInst(\mathcal{X},\ddot{\mathcal{A}})\wedge \\
\hspace{0pt}\exists i<n, D_i=D\wedge\\
\hspace {0pt}\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}})\big)\implies \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}}=(V_{\ddot{\mathcal{A}}},E_{\ddot{\mathcal{A}}},D_0,...,E,...,D_{n-1})).
\end{gathered}
\end{equation}

§ FORMALIZATION OF A PROOF OF THREE AXIOM SCHEMES

In this section, we consider solution sets and not their projections to subsets of coordinates. The proofs for both cases do not essentially differ, and we can repeat the same reasoning for any projection. However, since projection increases the complexity of a formula from $\Sigma^{1,b}_0$ to $\Sigma^{1,b}_1$, in any proof using the induction or comprehension axioms of level $i$ for a set of solutions, we need to exchange the level for $i+1$ for a projection to a subset of coordinates.

§.§ Formalization of some auxiliary lemmas and theorems

We will present the formalization of several selected statements and their proofs used in the proof of the soundness of the algorithm. We selected those that genuinely represent various types of arguments encountered in [21], [22]. It should be sufficiently clear that other statements of a similar nature can be formalized analogously.

§.§.§ Properties of a binary absorbing subuniverse on $\mathbb{A}^n$

We say that a solution set to a CSP instance $\Theta$ over $\Gamma_{\mathcal{A}}$ on $n$ variables, $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ is a binary absorbing subuniverse of $D_0\times...\times D_{n-1}$ if there exists a binary term operation $T\in Pol(\Gamma_{\mathcal{A}})$ such that for any two maps $H,H':[n]\to(D_0,...,D_{n-1})$ where $H\notin \mathscr{R}_{\Theta}$ and $H'\in \mathscr{R}_{\Theta}$, the maps $usepol_2(T,H,H')$ and $usepol_2(T,H',H)$ are in $\mathscr{R}_{\Theta}$. An analogous definition can be formulated for any projection of the set of solutions $\mathscr{R}^{i_1,...,i_s}_{\Theta}$.

[Lemma 7.1, [21]] Suppose that $\mathscr{R}_{\Theta}$ is defined by a $pp$-formula $\Theta(x_0,...,x_{n-1})$ and $\Theta'$ is obtained from $\Theta$ by replacing some constraint relations $\rho_1,...,\rho_s$ by constraint relations $\rho'_1,...,\rho'_s$ such that $\rho_k'$
absorbs $\rho_k$ with a term operation $T$ for every $k$. Then $V^0$ proves that the relation $\mathscr{R}_{\Theta'}$ defined by
$\Theta'(x_0,...,x_{n-1})$ absorbs $\mathscr{R}_{\Theta}$ with the term operation $T$.

Let us consider two CSP instances $\Theta = (\mathcal{X},\ddot{\mathcal{A}})$ and $\Theta' = (\mathcal{X}',\ddot{\mathcal{A}}')$, where $\mathcal{X}'=\mathcal{X}$ (the analogous reasoning can be applied to projections). Suppose that there exists a binary term $T\in Pol(\Gamma_{\mathcal{A}})$ such that for each $i<n$, $D'_{i}\subseteq D_i$ binary absorbs $D_i$ and for all $i,j<n$ with $E_{\mathcal{X}}(i,j)$, $E^{ij}_{\ddot{\mathcal{A}}'}\subseteq E^{ij}_{\ddot{\mathcal{A}}}$ binary absorbs $E^{ij}_{\ddot{\mathcal{A}}}$:

\begin{equation}\label{djdjjduuuhs6745ed}
\begin{gathered}
\hspace {0pt}\forall a\in D'_i,\forall b\in D_i,\exists c_1,c_2\in D'_i,\,T(a,b)=c_1\wedge T(b,a)=c_2\wedge\\
\hspace {0pt}\forall a_1,b_1<l,\forall a_2,b_2<l,\,(E^{ij}_{\ddot{\mathcal{A}}}(a_1,b_1)\wedge E^{ij}_{\ddot{\mathcal{A}}'}(a_2,b_2))\rightarrow\\
\hspace {0pt}\rightarrow\exists a_3,a_4<l,\exists b_3,b_4<l,\,E^{ij}_{\ddot{\mathcal{A}}'}(a_3,b_3)\wedge E^{ij}_{\ddot{\mathcal{A}}'}(a_4,b_4)\wedge\\
\wedge T(a_1,a_2)=a_3\wedge T(a_2,a_1)=a_4\wedge T(b_1,b_2)=b_3\wedge T(b_2,b_1)=b_4.
\end{gathered}
\end{equation}

Note that for some $i,j<n$, $D'_i$ and $E^{ij}_{\ddot{\mathcal{A}}'}$ could be equal to $D_i$ and $E^{ij}_{\ddot{\mathcal{A}}}$. If $\mathscr{R}_{\Theta'}$ or/ and $\mathscr{R}_{\Theta}$ are empty, we are done ($\mathscr{R}_{\Theta'}$ is an empty subuniverse). Suppose that both instances have solutions. Every solution to the instance $\Theta'$ is a solution to the instance $\Theta$. Consider any two solutions to $\Theta$ and $\Theta'$, homomorphisms $H$ and $H'$, respectively. Consider two maps $H_1=usepol_2(T,H,H')$ and $H_2=usepol_2(T,H',H)$. We need to prove that these maps are homomorphisms from $\mathcal{X}'$ to $\ddot{\mathcal{A}}'$. Suppose that $H_1$ (or $ H_2$) is not a homomorphism. Then there exists an edge in $\mathcal{X}'$, $E_{\mathcal{X}'}(i,j)$ such that $H_1$ fails to map it to an edge in $\ddot{\mathcal{A}}'$. But this contradicts (<ref>).

Suppose $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ and $B_i$ is an absorbing subuniverse in $A_i$ with a term $T$ for every $i$. Then $V^0$ proves that $(B_0\times...\times B_{n-1})\cap \mathscr{R}_{\Theta}$ is an absorbing subuniverse of $\mathscr{R}_{\Theta}$ with the term $T$.

Suppose that $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ is a relation such that $pr_0(\mathscr{R}_{\Theta})=D_0$ and $B=pr_0((B_0\times...\times B_{n-1})\cap \mathscr{R}_{\Theta})$, where $B_i$ is an absorbing subuniverse in $D_i$ with a term $T$ for every $i$. Then $V^1$ proves that $B$ is an absorbing subuniverse in $D_0$ with the term $T$.

Consider $\mathscr{R}_{\Theta}$ as a solution set to some CSP instance $\Theta=(\mathcal{X},\ddot{\mathcal{A}})$. Since every $B_i$ is an absorbing subuniverse of $D_i$, $(B_0\times...\times B_{n-1})\cap \mathscr{R}_{\Theta}$ is a solution set for an instance $\Theta'$ defined similarly to (<ref>) with a domain set $D'=\{B_0,...,B_{n-1}\}$ (for all $i,j<n$, $E^{ij}_{\ddot{\mathcal{A}}'}=E^{ij}_{\ddot{\mathcal{A}}}$). Then from $pr_0(\mathscr{R}_{\Theta})=D_0$ it follows that $B$ is an absorbing subuniverse of $D_0$.

[Lemma 7.3, [21]]
Suppose that $\mathscr{R}_{\Theta}$ is a non-trivial absorbing subuniverse of $D_0\times...\times D_{n-1}$. Then $V^2$ proves that for some $i$ there exists a non-trivial absorbing subuniverse $B_i$ in $D_i$ with the same term.

The lemma is proved by induction on the arity of $\mathscr{R}_{\Theta}$. $\mathscr{R}_{\Theta}$ is a non-trivial binary absorbing subuniverse of $D_0\times...\times D_{n-1}$ if there exists a solution to $\Theta_{null}$ that is not a solution to $\Theta$, and there exists a binary term $T$ such that for any two homomorphisms $H$ from $\mathcal{X}$ to $\ddot{\mathcal{A}}$ and $H_{null}$ from $\mathcal{X}_{null}$ to $\ddot{\mathcal{A}}_{null}$, both maps $usepol_2(T,H,H_{null})$ and $usepol_2(T,H_{null},H)$ are homomorphisms from $\mathcal{X}$ to $\ddot{\mathcal{A}}$.

Consider the following $\mathfrak{B}(\Sigma^{1,b}_1)$-formula $\phi(t)$. Here, as fixed parameters, we use $\Gamma_{\mathcal{A}}$ and $\mathbb{A}=(A,\Omega)$. Induction goes on the size of the instance, $V_{\mathcal{X}} = V_{\mathcal{X}_{null}}=t$. Witnesses ($\forall$ quantification) in $\Sigma^{1,b}_2$-induction corresponding to $t$ are sets $E_{\mathcal{X}}, E_{\mathcal{X}_{null}}$, $\ddot{\mathcal{A}}$ with the set of vertices of size $\langle t,l\rangle$.

\begin{equation}
\begin{gathered}
\hspace {0pt}\phi(t):=\hspace{0pt} \big(V_{\mathcal{X}} = V_{\mathcal{X}_{null}}=t\wedge DG(\Theta)\wedge DG_{null}(\Theta_{nul}) \wedge \\
\wedge Inst(\Theta,\Gamma_{\mathcal{A}})\wedge Inst(\Theta_{null},\Gamma_{\mathcal{A}})\big) \wedge \\
\wedge \big(\bigvee_{T\in \Pi^2_{\mathcal{A}}}\forall H, H_{null}\leq \langle t,\langle t,l\rangle\rangle,\,\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H)\wedge\ddot{HOM}(\mathcal{X}_{null},\ddot{\mathcal{A}}_{null},H_{null})\rightarrow\\
\hspace {0pt}\rightarrow \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},usepol_2(T,H,H_{null})) \wedge\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},usepol_2(T,H_{null},H)\big)\\
\wedge\big(\exists H'\leq \langle t,\langle t,l\rangle\rangle,\,\ddot{HOM}(\mathcal{X}_{null},\ddot{\mathcal{A}}_{null},H')\wedge \neg \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H')\big)\implies\\
\hspace {0pt}\implies\exists i<t,\bigvee_{B<l} B_i\subsetneq A_i\wedge BAsubU(B_i,A_i,T,\Omega).
\end{gathered}
\end{equation}

The expression in the first brackets says that $\Theta$ and $\Theta_{null}$ are CSP instances over $\Gamma_{\mathcal{A}}$ on $t$ variables, and $\Theta_{null}$ is an empty instance. This is obviously true for $t=1$. Suppose that it is true for $t=s$ and consider $t=s+1$. If the projection of $\mathscr{R}_{\Theta}$ on the $s+1$ coordinate is not $D_{s+1}$, then $\mathscr{R}_{\Theta}^{s+1}$ is a binary absorbing subuniverse due to the definition of a non-trivial absorbing subuniverse. Otherwise, choose any element $a\in D_{s+1}$ such that $\mathscr{R}_{\Theta}$ does not contain all homomorphisms sending $s+1$ to $a$ and consider the new $s$-ary relation $\mathscr{R}_{\Theta'}=\{(a_0,...,a_s)| (a_0,...,a_s,a)\in \mathscr{R}_{\Theta}\}$. Due to Lemma <ref>, it is a non-trivial binary absorbing subuniverse for $D_0\times...\times D_{s}$ ($T$ is idempotent). But note that $\mathscr{R}_{\Theta'}$ is also a solution set to a specific CSP instance $\Theta'$ on $s$ variables: we just remove from $E_{\mathcal{X}}$ of $\Theta$ all edges adjacent to $x_{s+1}$ and for all $j<s+1$ restrict $E^{j(s+1)}_{\ddot{\mathcal{A}}}$ and $E^{(s+1)j}_{\ddot{\mathcal{A}}}$ to pairs ending and starting with $a$. Thus, we can apply the induction hypothesis.

The following lemma from [11] gives us a more precise theory, which we will not define here.
For all $i\geq 1$, the theory $T^i_2$ proves the induction scheme IND for $\mathcal{B}(\Sigma^{b}_i)$-formulas.

[Lemma 7.5, [21]]
Suppose $D^{(1)}$ is an absorbing reduction of a CSP instance $\Theta$ and a relation $\mathscr{R}_{\Theta}\leq D_{0}\times...\times D_{n-1}$ is subdirect. Then $V^0$ proves that $\mathscr{R}_{\Theta}^{(1)}$ is not empty.

Suppose the opposite. Then $\mathscr{R}_{\Theta}\cap D^{(1)}_{0}\times...\times D^{(1)}_{n-1}=\emptyset$, where for each $i<n$, $D^{(1)}_i$ is a binary absorbing subuniverse of $D_i$ with the term $T$. This means that for every homomorphism $H_{i_1}\in \mathscr{R}_{\Theta}$ there exists $i<n$ such that $H_{i_1}(i)=\langle i,a\rangle$, where $a\in D_i\backslash D^{(1)}_{i}$. Since $\mathscr{R}_{\Theta}$ is subdirect, for any $i<n$ and for any $b\in D^{(1)}_{i}$ there exists a homomorphism $H_{i_2}$ such that $H_{i_2}(i)=\langle i,b\rangle$. Composing these homomorphisms, since $T$ is a polymorphism, we again get a homomorphism $H_{i_3}=usepol_2(T,H_{i_1},H_{i_2})$ such that $H_{i_3}(i)=\langle i,c\rangle$ for some $c\in D^{(1)}_{i}$. Consider any $j\neq i <n$ such that $H_{i_3}(j)=\langle j,d\rangle$ with $d\notin D^{(1)}_{j}$. Again, since $\mathscr{R}_{\Theta}$ is subdirect, there must be a homomorphism $H_{i_4}$ such that $H_{i_4}(j)=\langle j,e\rangle$ for some $e\in D^{(1)}_{j}$. We compose these two homomorphisms and get $H_{i_5} =usepol_2(T,H_{i_3},H_{i_4})$ such that $H_{i_5}(i)=\langle i,f\rangle$ and $H_{i_5}(j)=\langle j,g\rangle$ with $f\in D^{(1)}_{i}$ and $g\in D^{(1)}_{j}$. Applying this procedure at most $n$ times, we will get a homomorphism in $\mathscr{R}_{\Theta}^{(1)}$, a contradiction.

§.§.§ Properties of a central subuniverse on $\mathbb{A}^n$

We say that a solution set to a CSP instance $\Theta$ over $\Gamma_{\mathcal{A}}$ on $n$ variables, $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ is a central absorbing subuniverse of $D_0\times...\times D_{n-1}$ if there exists a ternary term operation $S\in Pol(\Gamma_{\mathcal{A}})$ such that $\mathscr{R}_{\Theta}$ absorbs $D_0\times...\times D_{n-1}$ with $S$ and for any map $H\notin \mathscr{R}_{\Theta}$ such that for all $i<n$, $H(i)=\langle i,a_i\rangle$, the following conditions hold. Construct two new CSP instances, $\Theta_L$ and $\Theta_R$ as follows:

* We double the number of variables, $D_{L}=D_R=\{D_0,...,D_{2n-1}\}$ with $D_i=D_{n+i}$ for every $i<n$;

* For the instance $\Theta_L$ we copy digraph $\mathcal{X}$ for the first $n$ variables, and we join it with a path $\mathcal{P}_n$ of length $n$, namely $E_{\mathcal{P}_n}(x_n-1,x_n),...,E_{\mathcal{P}_n}(x_{2n-2},x_{2n-1})$. We copy $\ddot{\mathcal{A}}$ for the first $n$ variables and set the constraints for the path: $E^{x_n-1,x_n}_{\ddot{\mathcal{A}}_n}$ as a full relation and for the next edges $E^{x_n,x_{n+1}}_{\ddot{\mathcal{A}}_n}=\{(a_0,a_1)\}$, $E^{x_{n+1},x_{n+2}}_{\ddot{\mathcal{A}}_n}=\{(a_1,a_2)\}$,..., $E^{x_{2n-2},x_{2n-1}}_{\ddot{\mathcal{A}}_n}=\{(a_{n-2},a_{n-1})\}$. Note that such a CSP instance is a CSP instance over $\Gamma_{\mathcal{A}}$ since $\Omega$ is idempotent and every single element of $D_0\times...\times D_{n-1}$ is a subuniverse;

* For the instance $\Theta_R$ we do the same but in inversed manner (copy $\mathcal{X}$ and $\ddot{\mathcal{A}}$ for the variables $n,...,2n-1$);

Then from solutions to $\Theta_L$ and $\Theta_R$ by applying $\Omega$ we cannot generate the map $H$ such that for $i<n$, $H(i)=H(n+i)=\langle i,a_i\rangle$. Note that to define this fact, we need the third-order induction. The number of maps on $2n$ variables is $l^{2n}$, so to define the generated algebra $\mathscr{Cl}_{\mathscr{R}_{\Theta_L}\cup \mathscr{R}_{\Theta_R}}$ it is needed to consider at most $l^{2n}$ steps which we encode by strings:

\begin{equation}
\begin{gathered}
\hspace{0pt}\forall H\leq\langle 2n\langle 2n,l\rangle \rangle,\,\mathscr{Cl}^{[\emptyset]}_{\mathscr{R}_{\Theta_L}\cup \mathscr{R}_{\Theta_R}}(H)\iff \mathscr{R}_{\Theta_L}(H)\vee \mathscr{R}_{\Theta_R}(H)\wedge\\
\forall \emptyset\leq T<2n\lceil log_2l\rceil, \forall H\leq\langle 2n\langle 2n,l\rangle \rangle,\\
\mathscr{Cl}^{[S(T)]}_{\mathscr{R}_{\Theta_L}\cup \mathscr{R}_{\Theta_R}}(H)\iff\mathscr{Cl}^{[T]}_{\mathscr{R}_{\Theta_L}\cup \mathscr{R}_{\Theta_R}}(H) \vee\\
\hspace {0pt}\vee \exists H_1,...,H_m\leq\langle 2n\langle 2n,l\rangle \rangle,\,\mathscr{Cl}^{[T]}_{\mathscr{R}_{\Theta_L}\cup \mathscr{R}_{\Theta_R}}(H_1)\wedge...\wedge \mathscr{Cl}^{[T]}_{\mathscr{R}_{\Theta_L}\cup \mathscr{R}_{\Theta_R}}(H_m)\wedge \\
\hspace {0pt}\wedge \omega(H_1,...,H_m) = H.
\end{gathered}
\end{equation}

The analogous definition can be formulated for any projection of the solution set $\mathscr{R}^{i_1,...,i_s}_{\Theta}$.

[Composed Lemma 7.6, [21], and Theorem 6.9, [22]]
Suppose $\mathscr{R}_{\Theta}$ is defined by a $pp$-formula $\Theta(x_0,...,$ $x_{n-1})$ and $\Theta'$ is obtained from $\Theta$ by replacement of some constraint relations $\rho_1,...,\rho_s$ by constraint relations $\rho'_1,...,\rho'_s$ such that $\rho_k'$
is a central subuniverse for $\rho_k$ with a term operation $S$ for every $k$. Then $V^1$ proves that the relation $\mathscr{R}_{\Theta'}$ defined by
$\Theta'(x_0,...,x_{n-1})$ is a central subuniverse for $\mathscr{R}_{\Theta}$ with the term operation $S$.

Consider two CSP instances $\Theta = (\mathcal{X},\ddot{\mathcal{A}})$ and $\Theta' = (\mathcal{X}',\ddot{\mathcal{A}}')$, where $\mathcal{X}'=\mathcal{X}$ (again, the analogous reasoning can be applied to projections). Due to the assumption, there exists a ternary term $S\in Pol(\Gamma_{\mathcal{A}})$ such that for each $i<n$, $D'_{i}\subseteq D_i$ ternary absorbs $D_i$ and for all $i,j<n$ with $E_{\mathcal{X}}(i,j)$, $E^{ij}_{\ddot{\mathcal{A}}'}\subseteq E^{ij}_{\ddot{\mathcal{A}}}$ ternary absorbs $E^{ij}_{\ddot{\mathcal{A}}}$. The defining relation is analogous to (<ref>). Also, for each $i<n$, and for any $a\in D_i\backslash D'_i$, $(a,a)\notin Sg(X^{i}_{(a)})$, where

\begin{equation}
X^{i}_{(a)}=\{\{a\}\times D'_i,D'_i\times \{a\}\},
\end{equation}

and for all $i,j<n$ with $E_{\mathcal{X}}(i,j)$, and for every $(a,b)\in E^{ij}_{\ddot{\mathcal{A}}}\backslash E^{ij}_{\ddot{\mathcal{A}}'}$ we have $(a,b,a,b)\notin Sg(X^{ij}_{(a,b)})$, where

\begin{equation}
X^{ij}_{(a,b)}=\{(a,b)\}\times E^{ij}_{\ddot{\mathcal{A}}'}\cup E^{ij}_{\ddot{\mathcal{A}}'}\times \{(a,b)\}.
\end{equation}

We will show how to define $Sg(X^{ij}_{(a,b)})$ analogously to a central subuniverse we defined before, using the closure operator $Cl(X^{ij}_{(a,b)})$. Since $\mathbb{A}$ is finite of size $l$ and $|X^{ij}_{(a,b)}|=2|E^{ij}_{\ddot{\mathcal{A}}'}|$, we do not need more than $(l^4-2|E^{ij}_{\ddot{\mathcal{A}}'}|)$ steps. Not to depend on $E^{ij}_{\ddot{\mathcal{A}}'}$, choose the value $l^4$. For set $X^{ij}_{(a,b)}\leq \langle\langle l,l\rangle, \langle l,l\rangle\rangle$, iteratively define the following set $Cl^{t}_{X^{ij}_{(a,b)}}$ up to $l^4$:

\begin{equation}
\begin{gathered}
\hspace {0pt}\forall c,d,e,f<l,\,Cl^{0}_{X^{ij}_{(a,b)}}(c,d,e,f)\iff X^{ij}_{(a,b)}(c,d,e,f)\wedge\\
\hspace {0pt}\wedge \forall 0<t<l^4, \forall c,d,e,f<l,\, Cl^{t}_{X^{ij}_{(a,b)}}(c,d,e,f)\iff Cl^{t-1}_{X^{ij}_{(a,b)}}(c,d,e,f)\vee\\
\hspace{0pt}\vee\exists c_1,...,c_m,d_1,...,d_m,e_1,...,e_m,f_1,...,f_m\in A,\\
\hspace {0pt}Cl^{t-1}_{X^{ij}_{(a,b)}}(c_1,d_1,e_1,f_1)\wedge...\wedge Cl^{t-1}_{X^{ij}_{(a,b)}}(c_m,d_m,e_m,f_m)\wedge\\
\hspace{0pt}\wedge\Omega(c_1,...,c_m)=c\wedge \Omega(d_1,...,d_m)=d\wedge \Omega(e_1,...,e_m)=e\wedge \Omega(f_1,...,f_m)=f.
\end{gathered}
\end{equation}

\begin{equation}\label{akakudu467763}
\begin{gathered}
\forall i,j<n, \forall a,b<l,\,(E_{\mathcal{X}}(i,j)\wedge E^{ij}_{\ddot{\mathcal{A}}}(a,b)\wedge \neg E^{ij}_{\ddot{\mathcal{A}}'}(a,b))\rightarrow \neg Cl^{l^4}_{X^{ij}_{(a,b)}}(a,b,a,b).
\end{gathered}
\end{equation}

That $\mathscr{R}_{\Theta'}$ absorbs $\mathscr{R}_{\Theta}$ with ternary operation $S$ can be proved as in Lemma <ref>. Suppose that $\mathscr{R}_{\Theta'}$ is not a central subuniverse of $\mathscr{R}_{\Theta}$.
Then there exists a homomorphism $H$ from $\mathcal{X}$ to $\ddot{\mathcal{A}}$, sending each $i<n$ to $\langle i,a_i\rangle$, such that it is not a homomorphism from $\mathcal{X}'$ to $\ddot{\mathcal{A}}'$, and if we construct two instances $\Theta_L'$ and $\Theta_R'$ as above, the subalgebra generated by these two instances contains a homomorphism $H'$ sending both $i$ and $n+i$ to $\langle i,a_i\rangle$ for each $i<n$. It would mean that for all $i,j<n$ such that $E_{\mathcal{X}}(i,j)$, elements of the form $(a_i,a_j,a_i,a_j)\in D_{i}\times D_{j}\times D_{n+i}\times D_{n+j}$ must belong to sets
$Cl^{l^4}_{X^{ij}_{(a_i,a_j)}}$. But at least one $(a_i,a_j)$ must be from $E^{ij}_{\ddot{\mathcal{A}}}\backslash E^{ij}_{\ddot{\mathcal{A}}'}$ (otherwise $H$ is a homomorphism from $\mathcal{X}'$ to $\ddot{\mathcal{A}}'$). That contradicts with (<ref>).

Note that in the above proof, we do not even use the definition of the third-order object. We lowered requirements to second-order objects and showed the contradiction. Thus, we can remain in $V^1$.

Suppose $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ is a relation such that $pr_0(\mathscr{R}_{\Theta})=D_0$ and $C=pr_0((C_0\times...\times C_{n-1})\cap \mathscr{R}_{\Theta})$, where $C_i$ is a central subuniverse in $D_i$ for every $i$. Then $V^1$ proves that $C$ is a central subuniverse in $D_0$.

Suppose $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ and $C_i$ is a central subuniverse for every $i$. Then $V^1$ proves that $(C_0\times...\times C_{n-1})\cap \mathscr{R}_{\Theta}$ is a central subuniverse for $\mathscr{R}_{\Theta}$.

[Lemma 7.7, [21]] Suppose $\mathscr{R}_{\Theta}$ is a non-trivial center of $D_0\times...\times D_{n-1}$. Then $V^2$ proves that for some $i$ there exists a non-trivial center $C_i$ of $D_i$.

§.§.§ Properties of a PC subuniverse on $\mathbb{A}^n$

While considering the properties of a PC subuniverse on $D_0\times...\times D_{n-1}$, we keep in mind that we further use all auxiliary lemmas in the proof of the main statements about the next reduction, and all reductions are constructed based on separate domains upward to subuniverses on their product. That is, there is no need to consider arbitrary PC subuniverses on $D_0\times...\times D_{n-1}$ or on the solution set $\mathscr{R}_{\Theta}$. The problem here is that we have no definition of a PC algebra for an arbitrary product or a PC congruence on that product (recall that in the definition of PC algebra, we use fixed constraint language $\Gamma_{\mathcal{A}}$). Thus, any time in the proofs we consider an arbitrary algebra $\mathbb{D}$ and its arbitrary PC congruence $\sigma$, we may assume that $\mathbb{D}$ is a subuniverse $\mathscr{R}\leq D_0\times...\times D_{n-1}$ and $\sigma$ is an extended congruence for some PC congruence $\sigma_i$ on a domain $D_i$.

[Lemma 6.20, [22]]
Suppose $\mathscr{R}_{\Theta}$ is a subdirect relation on $D_0\times...\times D_{n-1}$ and $E_i$ is a PC subuniverse of $D_i$ for every $i$. Then $W^1_1$ proves that $(E_0\times...\times E_{n-1})\cap \mathscr{R}_{\Theta}$ is a PC subuniverse of $\mathscr{R}_{\Theta}$.

Due to the assumption, there is a PC subuniverse $E_i$ of $D_i$ for every $i$. If some $E_i$ is empty, then we are done. Otherwise, each $E_i$ is a block of some congruence $\delta_i=\cap_j\sigma_{i_j}$ on $D_i$, where $\sigma_{i_1},...,\sigma_{i_s}$ are PC congruences on $D_i$. We can extend every $\sigma_{i_j}$ to the product $D_0\times...\times D_{n-1}$, and consider the congruence $\mathscr{C}_{\theta_i}=\cap_{k\neq i}\mathscr{C}_{\nabla^{ext}_{D_k}}\cap \mathscr{C}_{\sigma_{i_j}^{ext}}$. Since $\mathscr{R}_{\Theta}$ is subdirect, it is easy to check that a third-order map $\mathscr{H}$ that sends every $H\in \mathscr{R}_{\Theta}/\mathscr{C}_{\theta_i}$ to $a\in D_i/\sigma_{ij}$ such that $H(i) = \langle i,a\rangle$, is an isomorphism from $(\mathscr{R}_{\Theta}/\mathscr{C}_{\theta_i}, \mathscr{F}_{\Omega/\theta_i})$ to $(D_i/\sigma_{ij},\Omega/\sigma_{ij})$. So $(\mathscr{R}_{\Theta}/\mathscr{C}_{\theta_i}, \mathscr{F}_{\Omega/\theta_i})$ acts like a PC algebra, and we will call $\mathscr{C}^{\mathscr{R}_{\Theta}}_{\sigma_{i_j}^{ext}}$ restricted to $\mathscr{R}_{\Theta}$ an extended PC congruence for $(\mathscr{R}_{\Theta}, \mathscr{F}_{\Omega})$.

It follows that for each $E_i$, $\mathscr{E}_i^{ext}\cap \mathscr{R}_{\Theta}$ is an intersection of blocks of extended PC congruences restricted to $(\mathscr{R}_{\Theta}, \mathscr{F}_{\Omega})$, as well as $\mathscr{E}_0^{ext}\cap...\cap \mathscr{E}_{n-1}^{ext}\cap \mathscr{R}_{\Theta}$, and we can call it an extended PC subuniverse. By the definition of every $\mathscr{E}_i^{ext}$, it is just $E_0\times...\times E_{n-1}\cap \mathscr{R}_{\Theta}$.

Note that from the same reasoning, it follows that $E_0\times...\times E_{n-1}$ is an extended PC subuniverse of $D_0\times...\times D_{n-1}$.

[Lemma 6.18, [22]]
Suppose that $D$ is a PC algebra and $\mathscr{R}_{\Theta}\leq D^n$ contains all constant tuples $(a,a,...,a)$. Then $V^0$ proves that $\mathscr{R}_{\Theta}$ can be represented as a conjunction of binary relations of the form $x_i=x_j$.

Since $\mathscr{R}_{\Theta}\leq D^n$ contains all constant tuples $(a,a,...,a)$, every domain $D_i$ of a CSP instance $\Theta$ is equal to $D$, and every binary constraint $E^{ij}_{\ddot{\mathcal{D}}}$ contains a diagonal relation $\Delta_{ij}$. Recall that an algebra is PC if there exists a ternary discriminator $P$ such that $Pol_{3}(P,D,\Gamma^{diag}_{\mathcal{D}})$. Therefore, $P$ must preserve $\mathscr{R}_{\Theta}$. We want to show that every $E^{ij}_{\ddot{\mathcal{D}}}$ that is not a full binary relation is equal to relation $\Delta_{ij}$. Suppose that for some $i,j<n$ $E^{ij}_{\ddot{\mathcal{D}}}$ is neither a full nor diagonal relation. Then there must exist some $a\neq b$ such that $E^{ij}_{\ddot{\mathcal{D}}}(a,b)$. But since $P$ preserves $E^{ij}_{\ddot{\mathcal{D}}}$, $(P(a,a,b),P(a,b,b))=(b,a)\in E^{ij}_{\ddot{\mathcal{D}}}$, and for every $c\neq b$, $(P(a,b,c),P(a,a,c))=(a,c)\in E^{ij}_{\ddot{\mathcal{D}}}$. Thus, $E^{ij}_{\ddot{\mathcal{D}}}$ is a full relation.

The following lemma follows from the previous lemma and some additional reasoning.
[Lemma 6.19, [22]]
Suppose that $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ is subdirect, $D_i$ is a PC algebra without non-trivial binary absorbing and central subuniverses for every $i\in\{1,...,n-1\}$, and $D_0$ has no non-trivial central subuniverse. Then $V^1$ proves that $\mathscr{R}_{\Theta}$ can be represented as a conjunction of binary relations $\delta_1(x_{i_1},x_{j_1}),...,\delta_s(x_{i_s},x_{j_s})$, where for every $l\leq s$ the first variable of $\delta_l$ is uniquely determined whenever $i_l\neq 1$ and the
second variable of $\delta_l$ is uniquely determined whenever $j_l\neq 1$.

[Lemma 6.21, [22]]
Suppose that $\mathscr{R}_{\Theta}$ is a subdirect relation on $D_0\times...\times D_{n-1}$, $E_i$ is a PC subuniverse of $D_i$ for all $i$ and $E=pr_0((E_0\times...\times E_{n-1})\cap \mathscr{R}_{\Theta})$.
Then $V^1$ proves that $E_0$ is a PC subuniverse of $D_0$.

We consider $\mathscr{R}_{\Theta}$ to be a solution set to some CSP instance $\Theta$ on $n$ domains such that for all $i,j<n$ there is a constraint $E_{\mathcal{X}}(i,j)$, but for some of them $E^{ij}_{\ddot{\mathcal{A}}}$ are full relations. By Lemma <ref> (or by Definition <ref>) each $E_i$ is a block of congruence $\delta_i$ such that there are PC congruences $\sigma_{i_0},...,\sigma_{i_{k-1}}$ with $k\leq log_2l$ and

$$D_i/\delta_i\cong D_i/\sigma_{i_0}\times...\times D_i/\sigma_{i_{k-1}}.

Then we can consider the factorized instance $\Theta_{PC}$, constructed as follows. The instance digraph $\mathcal{X}_{PC}=\mathcal{X}$ does not change. For a target digraph $\ddot{\mathcal{A}}_{PC}$, the domain set is $D_{PC}=\{D_0,D_1/\delta_1,...,D_{n-1}/\delta_{n-1}\}$, i.e., we factorize every domain except the first one (or equivalently factorize it by $\Delta_0$). Constraint relations are defined by a set
$E_{\ddot{\mathcal{A}}_{PC}}$ such that

\begin{equation}
\begin{gathered}
\hspace{0pt}\forall 0<i,j<n,\, E^{ij}_{\ddot{\mathcal{A}}_{PC}}(a,b)\iff D_i/\delta_i(a)\wedge D_j/\delta_j(b)
\wedge \\
(\exists c,d<l,\,\,\delta_i(a,c)\wedge \delta_j(b,d)\wedge E^{ij}_{\ddot{\mathcal{A}}}(c,d)),\\
\hspace {0pt}\forall i<n,\,E^{1i}_{\ddot{\mathcal{A}}_{PC}}(a,b)\iff D_0(a)\wedge D_i/\delta_i(b)
\wedge (\exists c<l,\,\,\delta_i(b,c)\wedge E^{1i}_{\ddot{\mathcal{A}}}(a,c)),\\
\hspace {0pt}\forall i<n,\,E^{i1}_{\ddot{\mathcal{A}}_{PC}}(a,b)\iff D_0(a)\wedge D_i/\delta_i(b)
\wedge (\exists c<l,\,\,\delta_i(b,c)\wedge E^{i1}_{\ddot{\mathcal{A}}}(c,a)).\\
\end{gathered}
\end{equation}

Then there is a canonical homomorphism $H_c\leq \langle \langle l,n\rangle,\langle l,n\rangle\rangle$ from the target digraph $\ddot{\mathcal{A}}$ to the target digraph $\ddot{\mathcal{A}}_{PC}$ such that for any homomorphism $H$ from $\mathcal{X}$ to $\ddot{\mathcal{A}}$, the map $H_{PC}$ defined as

H_{PC}(i)=\langle i,a\rangle \iff \exists b<l, (H(i)= \langle i,b\rangle\wedge H_c(\langle i,b\rangle)=\langle i,a\rangle),

is a homomorphism from $\mathcal{X}$ to $\ddot{\mathcal{A}}_{PC}$. It is easy to see that $pr_0((E_0\times E_1\times...\times E_{n-1})\cap \mathscr{R}_{\Theta}) = pr_0((E_0\times e_1\times...\times e_{n-1})\cap \mathscr{R}_{\Theta_{PC}})$ where for each $0<i<n$, $e_i$ is the representative of the class $E_i$ and that $\mathscr{R}_{\Theta_{PC}}$ is subdirect.

For any $0<i<n$, we can find $M_i\in \mathrm{M}_{D_i,\delta_i\sigma_{i_0},...,\sigma_{i_{k-1}}}$ such that

$$ISO_{alg}(D_i/\delta_i,\Omega/\delta_i,D_i/\sigma_{i_0}\times...\times D_i/\sigma_{i_{k-1}},\Omega/\cap_{j}\sigma_{i_j} ,M_i).

Let us combine all of these maps into one set $M$. For every $i$ such that $M_i\in \mathrm{M}_{D_i,\delta_i\sigma_{i_0}},...,$ $_{\sigma_{i_{k-1}}}$ for $k<s=log_2l$ we add to the end $s-k$ trivial algebras $D_{i_{k}},...,D_{i_{s-1}}$ (containing one element $0$), set $\sigma_{i_{k}},...,\sigma_{i_{s-1}}$ to be trivial congruences and extend $M_i$ to the $s+1$ -ary set. Then for all $a_0,...,a_{s-1}<l$,

\begin{equation}
\begin{gathered}
\forall 0<i<n,\,\forall a\in D_i/\delta_i,\,M(a)=(a_0,...,a_{s-1})\iff M_i(a)=(a_0,...,a_{s-1})\\
\hspace{0pt}i=0,\,\forall a\in D_0,\,M(a)=(a,0,...,0).
\end{gathered}
\end{equation}

Consider a CSP instance $\Theta'_{PC}$ on $ns$ variables, with domain set

$$D'_{PC}=\{D_0,0,...,0, D_1/\sigma_{1_0},..., D_1/\sigma_{1_{s-1}},..., D_{n-1}/\sigma_{{n-1}_0},...,D_{n-1}/\sigma_{{n-1}_{s-1}}\}$$

such that $H_{PC}'\in \mathscr{R}_{\Theta'_{PC}}$ if and only if $H_{PC}\in \mathscr{R}_{\Theta_{PC}}$ where $H_{PC}'$ is a map from $[ns]$ to $[D'_{PC}]$ defined from a homomorphism $H_{PC}$ as follows:

\begin{equation}\label{alskjdyhrf5564}
\begin{gathered}
\hspace {0pt}i=0,\,H'_{PC}(0) = \langle 0,a\rangle\iff H_{PC}(0) = \langle 0,a\rangle,\\
\hspace {0pt}\forall 0<i<s,\,H'_{PC}(i) = \langle i,0\rangle,\\
\hspace{0pt}\forall 0<j<n,\forall k<s,\,\forall a\in D_j/\sigma_{j_k},\, H'_{PC}(js+k) = \langle js+k,a\rangle\iff\\
\iff \exists b\in D_j/\delta_j,\exists b_0\in D_{j}/\sigma_{j_0},...,\exists b_{k-1}\in D_{j}/\sigma_{j_{k-1}},\\
\exists b_{k+1}\in D_{j}/\sigma_{j_{k+1}},...,\exists b_{s-1}\in D_{j}/\sigma_{j_{s-1}},\\
\hspace {0pt}H_{PC}(j)=\langle j,b\rangle\wedge M(b)=(b_0,...,b_{k-1},a,b_{k+1},...,b_{s-1})
\end{gathered}
\end{equation}

Strictly speaking, the instance $\Theta'$ is not an instance over language $\Gamma_{\mathcal{A}}$, but we still can define every $2s$-ary relation $R^{ij}_{\ddot{\mathcal{A}}'_{PC}}$,

\begin{equation}\label{a00a09s88))(}
\begin{gathered}
R^{ij}_{\ddot{\mathcal{A}}'_{PC}}(a_0,...,a_{s-1}, b_0,...,b_{s-1})\iff \exists a\in D/\delta_i\exists b\in D_j/\delta_j,\,E^{ij}_{\ddot{\mathcal{A}}_{PC}}(a,b)\wedge\\
\hspace {0pt}\wedge M(a)=(a_0,...,a_{s-1})\wedge M(b)=(b_0,...,b_{s-1}).
\end{gathered}
\end{equation}

Moreover, we can apply to $R^{ij}_{\ddot{\mathcal{A}}'_{PC}}$ a similar reasoning as in Lemma <ref>. The solution set $\mathscr{R}_{\Theta'_{PC}}$ is subdirect since $\mathscr{R}_{\Theta_{PC}}$ is subdirect. Since every $D_j/\sigma_{j_k}$ is a PC algebra, it follows that by Lemma <ref>, $\mathscr{R}_{\Theta'_{PC}}$ can be represented as a conjunction of binary relations $\delta_1(x_{i_1},x_{j_1}),...,\delta_s(x_{i_s},x_{j_s})$, where for every $l\leq s$ the first variable of $\delta_l$ is uniquely-determined whenever $i_l\neq 1$ and the second variable of $\delta_l$ is uniquely-determined whenever $j_l\neq 1$. Thus, for all $0<j<n, k<s$, for every $a\in D_0$ there exists a unique $b\in D_j/\delta_{j_{k}}$ such that $E^{1(js+k)}_{\ddot{\mathcal{A}}_{PC}'}(a,b)$ (and analogously for the relation $E^{(js+k)1}_{\ddot{\mathcal{A}}_{PC}'}$). It follows that any such relation divides $D_0$ into $|D_j/\delta_{j_{k}}|$ classes, and we can check that this is a PC congruence on $D_0$. Thus, $pr_0((E_0\times e_1\times...\times e_{n-1})\cap \mathscr{R}_{\Theta_{PC}})$ can be represented as an intersection of blocks of $ns$ PC congruences (some of them can be trivial).

§.§.§ Properties of a linear subuniverse on $\mathbb{A}^n$

It is known that the ability to simulate an affine CSP (or historically the ability to count) adds substantial complexity to the problem. Structures that cannot count are all tractable and can even be solved by a simple constraint propagation algorithm.

For linear algebras, we shall adhere to the following notation. We will continue to denote elements of different domains $D_i,D_j$ by $a_i,a_j$. If we consider several elements of the same domain, we add an index after the index of the domain, for example, $a_{i1},...,a_{im}$. To represent an element $a_{ij}$ as an element of the product of $k\leq log_2l$ prime fields $Z_{p_0},...,Z_{p_{k-1}}$, we add the superscript $\bar{a}^k_{ij} = (a_{ij}^0,...,a_{ij}^{k-1})$.

The proof complexity of linear algebra (in the sense of a branch of mathematics) was well studied in [18], or in [19]. In particular, Gaussian elimination was considered and was shown to be formalizable in theory $V^1$. The detailed proof of the following lemma can be found, for example, in [8]. We show how to formalize it in $V^1$.

[Lemma 7.20, [21]]
Suppose that the relation $\mathscr{R}_{\Theta}\leq (\mathbb{Z}_{p_1})^{n_1}\times ... \times (\mathbb{Z}_{p_k})^{n_k}$ is preserved by $x_1+...+x_m$, where $p_1,...,p_k$ are distinct prime numbers dividing $m-1$ and $\mathbb{Z}_{p_i} = (\mathbb{Z}_{p_i},x_1+...+x_m)$ for every $i$. Then $V^1$ proves that $\mathscr{R}_{\Theta} = L_1\times...\times L_k$, where each $L_i$ is an affine subspace of $(\mathbb{Z}_{p_i})^{n_i}$.

Consider any CSP instance $\Theta$ on $n$ variables such that each $D_i$ is a linear algebra, i.e. $LinA(D_i,\Omega)$. That is, for every $i<n$ there are some $k\leq log_2l$, primes $p_0,...,p_{k-1}<l$, and an isomorphism $M_i\in \mathrm{M}_{A,\Delta_i,p_0,...,p_{k-1}}$ from $(D_i,\Omega)$ to $(Z_{p_0}\times...\times Z_{p_{k-1}},\bar{a}^k_{i1}+...+\bar{a}^k_{im})$ such that

$$M_i(a_{ij}) = \bar{a}^k_{ij}=(a_{ij}^0,...,a_{ij}^{k-1}).

As for the PC subuniverses, to unify all $M_i$, for every $k<s=log_2l$, we add $s-k$ trivial algebras $\mathbb{Z}_{p_{k}},...,\mathbb{Z}_{p_{s-1}}$, representing their elements as $0$'s. Thus, $M_i(a_{ij})=\bar{a}^s_{ij}$. Then we can construct $M$. For all $a_i^0,...,a_i^{s-1}<l$,

\begin{equation}
\begin{gathered}
\forall 0<i<n,\,\forall a_i\in D_i,\,M(a_i)=(a_i^0,...,a_i^{s-1})\iff M_i(a_i)=(a_i^0,...,a_i^{s-1}).  \end{gathered}
\end{equation}

We consider CSP instance $\Theta_L$ on $ns$ domains such that every solution to $\Theta$, translated naturally (analogously to (<ref>)) is a solution to $\Theta_L$ and vice versa. Again, it is not a CSP instance over language $\Gamma_{\mathcal{A}}$, but all $2s$-ary relations $R^{ij}_{\ddot{\mathcal{A}}_{L}}$ can be easily defined; see
(<ref>). The most important thing is that these relations are preserved by $m$-ary sum.

For this proof, we do not need to collect equal $Z_{p_j}$ from different domains to a group. We define a vector space on $Z_{p_0}\times...\times Z_{p_{ns-1}}$ as any subset of maps from $[ns]$ to $[D_L] = [Z_{p_0},...,Z_{p_{ns-1}}]$ such that it contains 'zero map' $H$ sending all $i<ns$ to $0$, and is closed under $+$, i.e. for any two maps $H_1,H_2$, the map $H_3=H_1+H_2$ such that

\begin{equation}
\begin{gathered}
(H_1+H_2)(i)= H_3(i)=\langle i,a\rangle\iff \exists b,c\in D_i,\\
H_1(i)=\langle i,b\rangle\wedge H_2(i)=\langle i,c\rangle\wedge a=b+c,
\end{gathered}
\end{equation}

is also in that set. We define an affine subspace $\mathscr{R}_{\Theta_L}$ of $Z_{p_0}\times...\times Z_{p_{ns-1}}$ as a shift of some linear subspace, i.e. such a set that for any map $H\in \mathscr{R}_{\Theta_L}$, the set of all maps $H'$ such that $H'+H\in\mathscr{R}_{\Theta_L}$ contains zero map and is closed under $+$. Note that when we are talking about solution sets, it is a second-order definition:

\begin{equation}
\begin{gathered}
\hspace {0pt}AffSubS(\mathscr{R}_{\Theta_L})\iff \forall H\leq \langle n\langle n,l\rangle\rangle,\forall H_1,H_2\leq \langle n\langle n,l\rangle\rangle,\,\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H)\wedge \\
\wedge \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H+H_1)\wedge \ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H+H_2)\rightarrow \\
\rightarrow\ddot{HOM}(\mathcal{X},\ddot{\mathcal{A}},H+(H_1+H_2)).
\end{gathered}
\end{equation}

Then it is easy to show that the solution to $\Theta_L$ is an affine subspace defining $x-y+z (mod \,p_j) = \Omega(x,z,y,...,y)$.

To prove some auxiliary lemmas and theorems, in addition to Definition <ref>, we need to define a linear algebra on a product $D_0\times...\times D_{n-1}$ of algebras of size at most $|A|$. We could define a linear algebra $\mathscr{R}_{\Theta}$ on $n$ domains, each of which is isomorphic to a product of $k\leq log_2l$ prime fields, as a solution set to some CSP instance $\Theta$ or as a set of maps closed under $x_1+...+x_m$. This defining relation is second-sorted and it would give us that $V^1$ proves that the set of linear algebras is closed under taking subalgebras. The problem here is that the resulting direct product isomorphic to relation $\mathscr{R}_{\Theta}$ will not be related to the initial CSP instance $\Theta$, it is considered exclusively as an algebra. We know that any relation preserved by $x_1+...+x_m$ can be represented as a system of linear equations over at most $ns$ variables, where $s=log_2l$, and this system can be solved by Gaussian elimination. Different domains $\mathbb{Z}_{p_i}$ cannot be mixed in one subsystem of equations, but variables over the same $\mathbb{Z}_{p_i}$ representing different $x_i,x_j$ can. For example, suppose that domains $D_i,D_j$ are both isomorphic to $\mathbb{Z}_3$, and that the solution to CSP instance $\Theta$ for these two variables contains the affine subspace (coset) $\{(1,1),(2,0),(0,2)\}$. This is isomorphic to $(\mathbb{Z}_3,\Omega)$, but we lose a domain. The same would happen while taking the quotient and in the proofs of some results about linear algebras on $n$ domains, we need the closeness of a set of linear algebras under taking quotients, especially extended ones. So we cannot avoid an isomorphism between third-order objects. Recall that we allow trivial algebras $\mathbb{Z}_1$ and that solution set to any CSP instance $\Theta_{null}$ on $n$ domains is a full relation.

For an algebra $(\mathscr{R},\mathscr{F})$ defined on a set of maps from $[k]$ to $[D'_0,...,D'_{k-1}]$, where $k\leq n$, we say that $\mathscr{R}$ is a linear algebra on $n$ domains if there exists a set of $n$ domains $D$ and the set of $n$ $m$-ary operations $F$ on these domains such that every algebra $(D_i,F_i)$ is linear and there is an isomorphism from $(\mathscr{R},\mathscr{F})$ to an algebra $(\mathscr{D}_0\times...\times \mathscr{D}_{n-1},\mathscr{F}_{F_0,...,F_{n-1}})$, where $\mathscr{D}_0\times...\times \mathscr{D}_{n-1}$ and $\mathscr{F}_{F_0,...,F_{n-1}}$ are defined as in (<ref>)-(<ref>):

\begin{equation}
\begin{gathered}
LinA(\mathscr{R},\mathscr{F})\iff \exists D\leq \langle n,l \rangle ,\exists F\leq \langle n,\underbrace{l,l,...,l}_{m\text{ times}}\rangle,\forall i<n,\ LinA(D_i,F_i) \wedge \\
\hspace{0pt}\wedge ISO_{alg}^{3,3}(\mathscr{R},\mathscr{F}, \mathscr{D}_0\times...\times \mathscr{D}_{n-1},\mathscr{F}_{F_0,...,F_{n-1}}).
\end{gathered}
\end{equation}

Note that the defining relation is third-order because of the relation $ISO_{alg}^{3,3}$. In an obvious way, we can define a linear and a minimal linear congruence $\mathscr{C}_{\theta}$ for any algebra on $n$ domains $(\mathscr{R},\mathscr{F})$.

From Lemma <ref>, Definition <ref>, and Definition <ref>, we conclude the following corollary.

$V^1$ proves that the set of linear algebras is closed under taking subalgebras and quotients. $W^1_1$ proves that the set of linear algebras on a product of algebras of size at most $|A|$ is closed under taking subalgebras and quotients.

In the presence of the third-order definition of linear algebra on $n$ domains, the following lemmas can be proved almost exactly as in [21].

[Lemma 7.21, [21]]
$W^1_1$ proves that a linear algebra has no non-trivial absorbing subuniverse, non-trivial central subuniverse, or non-trivial PC subuniverse.

[Lemma 7.24.1, [21]]
Suppose that $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ is a relation such that $pr_0(\mathscr{R}_{\Theta})=D_0$, there are no non-trivial binary absorbing subuniverses on $D_0$, and $L = pr_0((L_1\times...\times L_{n-1})\cap \mathscr{R}_{\Theta})$ where $L_i$ is a linear subuniverse of $D_i$ for every $i<n$. Then $W_1^1$ proves that $L$ is a linear subuniverse of $D_0$.

The following lemma can be proved similarly to Lemma <ref>.
[Lemma 7.25, [21]]
Suppose $\mathscr{R}_{\Theta}$ is a subdirect relation on $D_0\times...\times D_{n-1}$ and $L_i$ is a linear subuniverse of $D_i$ for every $i$. Then $W^1_1$ proves that $(L_0\times...\times L_{n-1})\cap \mathscr{R}_{\Theta}$ is a linear subuniverse of $\mathscr{R}_{\Theta}$.

§.§.§ Common properties and Interaction between subuniverses

The common property for subuniverses $C_0,...,C_{n-1}$ of a fixed type (any but linear) is that there does not exist $(C_0,...,C_{n-1})$-essential relation $\mathscr{R}$ of any arity greater than $2$. For PC subuniverses we additionally require the relation to be subdirect.

[Lemma 7.27,   [21]]
Suppose $C_i$ is a non-trivial binary absorbing subuniverse of $D_i$ with a term $T$ for all $i\in \{0,1,2,...,n\}$ and $n>1$. Then $V^0$ proves that there does not exist a $(C_0,...,C_{n-1})$-essential solution set $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$.

Suppose that such solution set $\mathscr{R}_{\Theta}$ to some CSP instance over $\Gamma_{\mathcal{A}}$ exists. Consider two solutions, $H_1\in (D_0\times C_1\times...\times C_{n-1})\cap \mathscr{R}_{\Theta}$ and $H_2\in (C_0\times C_1\times...\times D_{n-1})\cap \mathscr{R}_{\Theta}$. Then $usepol_{2}(T,H_1,H_2)$ is a new solution to $\Theta$ and it is in $C_0\times...\times C_{n-1}$.

[Lemma 6.11, [22]]
Suppose $C_i$ is a central subuniverse of $D_i$ for all $i\in \{0,1,2,...,n\}$ and $n>2$. Then $V^1$ proves that there does not exist a $(C_0,...,C_{n-1})$-essential solution set $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$.

[Corollary 7.13.3, [21]]
Suppose $C_i$ is a PC subuniverse of $D_i$ for all $i\in \{0,1,2,...,n\}$ and $n>2$. Then $V^1$ proves that there does not exist a $(C_0,...,C_{n-1})$-essential subdirect solution set $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$.

For our purposes, the last two lemmas can be proved by an exhaustive search. For any subuniverses $D_0,D_1,D_2$ of the fixed algebra $\mathbb{A}=(A,\Omega)$, for any of their central /PC subuniverses $C_0,C_1,C_2$ and for any subalgebras $R$ of $D_0\times D_1\times D_2$ check that $R$ is not $(C_0,C_1,C_2)$-essential or $(C_0,C_1,C_2)$-essential and subdirect. For a relation $\mathscr{R}\leq D_0\times...\times D_{n-1}$ of higher arity note that from $(C_0,...,C_{n-1})$-essential relation we can get $(C_0,C_1,C_{2})$-essential relation $\mathscr{R}'$ by setting

$$\mathscr{R}'=pr_{1,2,3}(\mathscr{R}\cap D_0\times D_1\times D_2\times C_3\times... \times C_{n-1}).

In the case of the solution set $\mathscr{R}_{\Theta}$ to the instance $\Theta$, we consider those homomorphisms that send variables $x_3,...,x_{n-1}$ to sets $C_3,...,C_{n-1}$. The definition of $\mathscr{R}'_{\Theta}$ requires $\Sigma^{1,b}_1$-COMP, this gives us theory $V^1$.

The following three lemmas about the interaction of subuniverses of different types are formulated for an arbitrary algebra $D$, i.e. for example, they can be used for $D=D_0\times...\times D_{n-1}$ and its subuniverses $\mathscr{R}_1$ and $\mathscr{R}_2$. For these cases, we can think about $D$ as of a domain set, and about $B_1$ and $B_2$ as of reductions $D^{(i)}_0\times...\times D^{(i)}_{n-1}$ or solution sets $\mathscr{R}_{\Theta}$. Sometimes we consider $D=\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ and $B_1=\mathscr{R}_{\Theta}\cap D^{(\bot)}_0\times...\times D^{(\bot)}_{n-1}$, $B_2=\mathscr{R}_{\Theta}\cap D^{(\top)}_0\times...\times D^{(\top)}_{n-1}$, where $D^{(\bot)}, D^{(\top)}$ are reductions of some (different) types. The proof of these lemmas is based on simple universal algebra reasoning, and in the presence of all third-order objects, their formalization in $W^1_1$ does not differ much from [21], [22].

[Lemma $7.28$,   [21], Lemma $6.25$]
Suppose $B_1$ is a binary absorbing, central, or linear subuniverse of $D$, $B_2$ is a subuniverse of $D$. Then $W^1_1$ proves that $B_1\cap B_2$ is a binary absorbing, central, or linear subuniverse of $B_2$, respectively.

[Lemma 7.29,   [21]]
Suppose $B_1$ and $B_2$ are non-empty one-of-four subuniverses of $D$, $B_1\cap B_2=\emptyset$.
Then $W^1_1$ proves that $B_1$ and $B_2$ are subuniverses of the same type.

[Theorem 7.30,   [21]]
Suppose $B_1$ and $B_2$ are one-of-four subuniverses of $D$ of types $\mathcal{T}_1$ and $\mathcal{T}_2$. Then $W^1_1$ proves that $B_1\cap B_2$ is a one-of-four subuniverse of $B_2$ of type $\mathcal{T}_1$.

The following lemma is proved by induction and is used for third-order objects, namely for reductions in strategies.

[Lemma 7.31,   [21]]
Suppose $\mathscr{A}_0=\mathscr{B}_0$, $s\geq 1$, $t\geq 0$, $\mathscr{A}_{i}$ is a one-of-four subuniverse of $\mathscr{A}_{i-1}$ for every $i\in\{1,...,s\}$, and $\mathscr{B}_{i}$ is a one-of-four subuniverse of $\mathscr{B}_{i-1}$ for every $i\in\{1,...,t\}$. Then $W_1^1$ proves that $\mathscr{A}_{s}\cap \mathscr{B}_t$ is a one-of-four subuniverse of $\mathscr{A}_{s-1}\cap \mathscr{B}_t$ of the same type as $\mathscr{A}_{s}$.

The proof of the claim goes by induction on $s+t$. If $t=0$, then the claim follows from the statement. If $t\leq 1$, then by the inductive assumption, $\mathscr{A}_{s-1}\cap \mathscr{B}_{t}$ and $\mathscr{A}_{s}\cap \mathscr{B}_{t-1}$ are both one-of-four subuniverses of $\mathscr{A}_{s-1}\cap \mathscr{B}_{t-1}$, and the second one is of type $\mathcal{T}$. Then by Theorem <ref> their intersection $\mathscr{A}_{s}\cap \mathscr{B}_{t}$ is a one-of-four subuniverses of $\mathscr{A}_{s-1}\cap \mathscr{B}_{t}$ of type $\mathcal{T}$.

We will formalize the proof for the specific case that we further need in the proofs of auxiliary lemmas about strategies. Suppose that $\mathscr{A}_0=\mathscr{B}_0=\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ for some CSP instance $\Theta$ with domain set $D$, where $\mathscr{R}_{\Theta}$ is its solution set, and for each $i\in\{1,...,s\}$,

$$\mathscr{A}_{i} = \mathscr{R}_{\Theta}\cap D^{(i)}_0\times...\times D^{(i)}_{n-1}

where $D=D^{(0)}, D^{(1)},...,D^{(s)}$ is some strategy for $\Theta$, and analogously, for each $i\in\{1,...,t\}$,

$$\mathscr{B}_{i} = \mathscr{R}_{\Theta}\cap D^{(i)'}_0\times...\times D^{(i)'}_{n-1}

for some (other) strategy $D=D^{(0)'}, D^{(1)'},...,D^{(t)'}$ for $\Theta$. Recall that we can formalize any strategy by one set $\Theta_{Str}< \langle nl,instsize(n,l)\rangle$. By Corollaries <ref>, <ref> and Lemmas <ref>, <ref> we know that $W_1^1$ proves that $\mathscr{A}_{i}$ is a one-of-four subuniverse of $\mathscr{A}_{i-1}$ and $\mathscr{B}_{i}$ is a one-of-four subuniverse of $\mathscr{B}_{i-1}$. Since in any step we reduce at least one domain, the number of steps $t,s$ cannot be greater than $nl$ and $t+s< 2nl$. This induction is available in $W_1^1$: the formula itself is $\Sigma^{1,b}_0$, but in the proof of the induction step we use the results proved in $W^1_1$.

[Lemma 7.32,   [21]]
Suppose $\mathscr{R}_{\Theta}\subseteq \mathscr{A}_0\times \mathscr{B}_0$ is a subdirect relation, $\mathscr{B}_i$ is a one-of-four subuniverse of $\mathscr{B}_{i-1}$ for every $i\in\{1,2,...,s\}$, $\mathscr{A}_1$ is a one-of-four subuniverse of $\mathscr{A}_0$. Then $W_1^1$ proves that $pr_1(\mathscr{R}_{\Theta}\cap (\mathscr{A}_1\times \mathscr{B}_s))$ is a one-of-four subuniverse of $pr_1(\mathscr{R}_{\Theta}\cap (\mathscr{A}_1\times \mathscr{B}_{s-1}))$ of the same type as $\mathscr{B}_s$.

The statement of this lemma will eventually be used in the proof of Lemma 8.28 [21], which is used further for constraints and subconstraints in proofs of Theorem <ref> and Theorem <ref>. So we will formalize the proof of the lemma for one specific case of Lemma $8.28$ [21]. Consider some subdirect solution set $\mathscr{R}_{\Theta}\leq D_0\times...\times D_{n-1}$ (for constraints and projections the reasoning is similar). Let $D=D^{(0)}, D^{(1)},...,D^{(s)}$ be some strategy for $\Theta$, and set for $i=0,1$

$$\mathscr{A}_i = pr_{0,1,...t-1}(D^{(i)}_0\times...\times D^{(i)}_{t-1}\times D_t\times...\times D_{n-1}),$$

and for $i=0,...,t$

$$\mathscr{B}_i=pr_{t,t+1,...n-1}(D_0\times...\times D_{t-1}\times D^{(i)}_t\times...\times D^{(i)}_{n-1}).$$

Then by Corollaries <ref>, <ref> and Lemmas <ref>, <ref>, $W_1^1$ proves that $\mathscr{R}_{\Theta}\cap(\mathscr{A}_0\times \mathscr{B}_i)$ is a one-of-four subuniverse of $\mathscr{R}_{\Theta}\cap(\mathscr{A}_0\times \mathscr{B}_{i-1})$ of the same type as $\mathscr{B}_i$, and $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{0})$ is a one-of-four subuniverse of $\mathscr{R}_{\Theta}$. By Lemma <ref>, $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{s})$ is a one-of-four subuniverse of $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{s-1})$ of the same type as $\mathscr{B}_{s}$. Consider a congruence $\mathscr{C}_{\sigma}$ on $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{0})$ such that two elements are equivalent whenever their projections on the second coordinate are equal,

$$\mathscr{C}_{\sigma}(H_1,H_2)\iff \forall t\leq i<n,\, H_1(i)=H_2(i).

Note that this is $\Sigma^{1,b}_0$ definition. Then for every coordinate $i=0,1$, $Stable_1(\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{t}),\mathscr{C}_{\sigma})$, which means that if $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{t})$ contains one element of the block of $\mathscr{C}_{\sigma}$, then it contains the entire block. We now need Lemma $7.26$ from [21], which is used just once in this proof. Therefore, we will formalize it only for this specific case as a claim.

Suppose $\mathscr{C}_{\sigma}$ is a congruence on $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{0})$, $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{t})$ is a one-of-four subuniverse of $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{0})$ stable under $\mathscr{C}_{\sigma}$. Then
$W^1_1$ proves that $\{H/\mathscr{C}_{\sigma}|H\in \mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{t})\}$ is a one-of-four subuniverse of $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{0})/\mathscr{C}_{\sigma}$ of the same type as $\mathscr{R}_{\Theta}\cap(\mathscr{A}_1\times \mathscr{B}_{t})$.

The proof of the claim is as in [21]. The statement follows immediately from the claim.

§.§.§ Some technical lemmas

In the following two lemmas, $\Theta(z)$ is the set of all $a\in D_z$ such that there is a solution to $\Theta$ with $z=a$. Analogously, $\Theta^{(1)}(z)$ is the set of all $a\in D^{(1)}_z$ such that there is a solution to $\Theta^{(1)}$ with $z=a$.

[Lemma 8.1,   [21]]
Suppose $D^{(1)}$ is a one-of-four reduction for an instance $\Theta$ of type $\mathcal{T}$, which is not of the PC type. Then $W^1_1$ proves that $\Theta^{(1)}(z)$ is a one-of-four subuniverse of $\Theta(z)$ of type $\mathcal{T}$ for every variable $z$.

Consider a CSP instance $\Theta$ on $n$ domains and its solution set $\mathscr{R}_{\Theta}$. Since $\mathscr{R}_{\Theta}$ is preserved by $\omega$, $\Theta(i)$ is a subuniverse of $D_i$ for every $i$, and by the definition of reductions, $D^{(1)}_i$ is a subuniverse of type $\mathcal{T}$. Thus, by Lemma <ref>, $\Theta(i)\cap D^{(1)}_i$ is a subuniverse of $\Theta(i)$ of type $\mathcal{T}$ for every $i<n$. Consider the reduction $\Theta'$ of $\Theta$ to the domain set $[\Theta(0),...,\Theta(n-1)]$, $\mathscr{R}_{\Theta'}$ is a subdirect relation. Then, by Corollaries <ref>, <ref> and Lemma <ref>, $\Theta^{(1)}(z)$ is a one-of-four subuniverse of $\Theta(z)$ of type $\mathcal{T}$.

[Lemma 8.2,   [21]]
Suppose $D^{(1)}$ is a PC reduction for a $1$-consistent instance $\Theta$, for every variable $y$ appearing at least twice in $\Theta$ the $pp$-formula $\Theta(y)$ defines $D_y$ and $\Theta(z)$ defines $D_z$ for a variable $z$. Then $V^1$ proves that $\Theta^{(1)}(z)$ is a PC subuniverse of $D_z$.

For the proof, we first rename all variables in $\Theta$ so that every variable occurs just once. This instance is denoted as $\Theta_0$. Then, step by step, we identify each two variables back to obtain the original instance, by the sequence $\Theta_0,\Theta_1,...\Theta_s=\Theta$. We show that these transformations can be held in $V^1$.

Recall that we are allowed to have only one constraint relation for any two variables $x,y$ (in that order). That is, for the instance $\Theta$ with $n$ variables, the number of possible constraints that involve one variable is at most $(2n-1)$ (and the number of all possible constraints is at most $n^2$). First, define the set of all variables that occur in $\Theta$ more than once:

\begin{equation}
\begin{gathered}
\forall x<n,\, S(x)\iff \exists y\neq z<n, \, (E_{\mathcal{X}}(x,y)\vee E_{\mathcal{X}}(y,x))\wedge (E_{\mathcal{X}}(x,z)\vee E_{\mathcal{X}}(z,x)).
\end{gathered}
\end{equation}

Note that if we have two edges of the form $E_{\mathcal{X}}(x,y), E_{\mathcal{X}}(y,x)$, we need to rename one $x$ to $x'$ and one $y$ to $y'$, and do it at different steps. To perform this, we further define two sets of variables for any such $x$, $S^{in}, S^{out}$:

\begin{equation}
\begin{gathered}
\forall x,y<n,\, S^{out}(x,y)\iff S(x)\wedge E_{\mathcal{X}}(x,y),\\
\forall x,z<n,\, S^{in}(x,z)\iff S(x)\wedge E_{\mathcal{X}}(z,x).
\end{gathered}
\end{equation}

When we rename every occurrence of a variable $x$, we can get at most $2n$ new variables (there are at most $(2n-1)$ constraints with $x$, and one of them could be a loop $E_{\mathcal{X}}(x,x)$). It works for every of $n$ variables, so the maximal number of steps is $2n^2$. We now set $s=2n^2$, $\Theta_s=\Theta$, $S_s=S, S^{out}_{s}=S^{out}, S^{in}_{s}=S^{in}$, and then for any $t=1,...,2n^2$ we will define a new CSP instance $\Theta_{s-t}$ based on the following rules. If the set $S_{s-(t-1)}$ is empty (neither of the variables occurs at least twice) we just replicate the instance $\Theta_{s-(t-1)}$. Otherwise, for odd $t$, we consider the set $S^{in}_{(s-(t-1))}$ (and for even the set $S^{out}_{(s-(t-1))}$). If it is empty, replicate the instance and move on. If not, choose elements $x,y$ such that $\langle x,y\rangle$ is the minimum element of $S^{in}_{(s-(t-1))}(x,y)$. Rename a variable $x$ in that constraint by the next number after the maximum element in $V_{\mathcal{X}_{s-(t-1)}}$. For this construction,
for each odd step $t$ we consider additional sets $L_{(s-(t-1))}$ and $R_{(s-(t-1))}$, defined as follows:

\begin{equation}
\begin{gathered}
L_{(s-(t-1))}(x)\iff \exists y<max(V_{\mathcal{X}_{s-(t-1)}})+1,\, min(S^{in}_{(s-(t-1))})=\langle x,y\rangle,\\
R_{(s-(t-1))}(y)\iff \exists x<max(V_{\mathcal{X}_{s-(t-1)}})+1,\, min(S^{in}_{(s-(t-1))})=\langle x,y\rangle.
\end{gathered}
\end{equation}

Now we are ready to define an instance digraph for step $t$:

\begin{equation}
\begin{gathered}
\forall x<max(V_{\mathcal{X}_{s-(t-1)}})+1,\,V_{\mathcal{X}_{s-t}}(x)\iff V_{\mathcal{X}_{s-(t-1)}}(x),\\
\forall x,y<max(V_{\mathcal{X}_{s-(t-1)}})+1,\,E_{\mathcal{X}_{s-t}}(x,y)\iff E_{\mathcal{X}_{s-(t-1)}}(y,x)\wedge \\
\wedge (\neg L_{(s-(t-1))}(x)\vee \neg R_{(s-(t-1))}(y))\\
E_{\mathcal{X}_{s-t}}(y,max(V_{\mathcal{X}_{s-(t-1)}})+1)\iff L_{(s-(t-1))}(x)\wedge R_{(s-(t-1))}(y).
\end{gathered}
\end{equation}

In parallel, we define a target digraph $\ddot{\mathcal{A}}_{s-t}$ by adding there a new domain $D_{max(V_{\mathcal{X}_{s-(t-1)}})}$ $_{+1}$ equal to $ D_x$ for a new variable $max(V_{\mathcal{X}_{s-(t-1)}})+1$ and $E^{yx}_{\ddot{\mathcal{A}}}$ as a constraint for a new edge $E_{\mathcal{X}_{s-t}}(y,max(V_{\mathcal{X}_{s-(t-1)}})+1)$. Eventually, we will get an instance $\Theta_0$. Since we consider all sets in a particular order and address only sets from the previous step $t-1$, all of them exist by $\Sigma^{1,b}_1$ induction.

The proof of the statement then goes by induction on $s$, and the implication $s\rightarrow s+1$ follows from the reasoning that can be easily formalized in $V^1$. We refer the reader to the source [21].

For a relation $\mathscr{R}$ of arity $n$ denote by $UnPol^{\mathscr{R}}$ the set of all unary vector functions preserving the relation $\mathscr{R}$. For a solution set $\mathscr{R}_{\Theta}$ for some CSP instance $\Theta$, due to (<ref>)

\begin{equation}
\Psi\in UnPol^{\mathscr{R}_{\Theta}}\iff VecFun(\mathscr{R}_{\Theta},\Psi),
\end{equation}

which is a $\Pi^{1,b}_1$-formula. For every map $H$ from $[n]$ to $[D_0,...,D_{n-1}]$, and every unary vector function $\Psi$, we can define a map $\Psi(H)$ using bit-definition:

\begin{equation}
\begin{gathered}
\Psi(H)(\langle i,\langle i,a\rangle\rangle)=H^{\Psi}(\langle i,\langle i,a\rangle\rangle)\iff \exists b\in D_i,\, H(\langle i,\langle i,b\rangle\rangle)\wedge \Psi(i,b,a).
\end{gathered}
\end{equation}

[Lemma 8.12,   [21]]
Suppose a $pp$-formula $\Lambda(x_0,...,x_{n-1})$ defines a relation $\mathscr{R}_{\Lambda}$, $H\in D_{x_0}\times...\times D_{x_{n-1}}$, and $\mathscr{R}'=\{H^{\Psi}:\Psi\in UnPol^{\mathscr{R}_{\Lambda}}\}$. Then $W^1_1$ proves that there exists $\Upsilon\in Covering(\Lambda)$ such that $\Upsilon(x_0,...,x_{n-1})$ defines $\mathscr{R}'$.

The idea of the universal algebra proof is the following. Consider any relation $\mathscr{R}$ on $n$ variables. Suppose that there are $l$ elements in each domain, $d_0,...,d_{l-1}$. Then the formula

$$\mathscr{S}(x^{d_0}_0,...,x^{d_{l-1}}_0,...,x^{d_0}_{n-1},...,x^{d_{l-1}}_{n-1}) = \bigwedge_{(b_0,...,b_{n-1})\in \mathscr{R}}\mathscr{R}(x^{b_0}_0,...,x^{b_{n-1}}_{n-1})

expresses that the vector-function preserves $\mathscr{R}$ (we think about $x^{b_i}_i$ as about $x_i$ being sending to $b_i$). Then, if we consider any tuple $\alpha = (a_0,...,a_{n-1})$, the projection of $\mathscr{S}$ to $x^{a_0}_0,...,x^{a_{n-1}}_{n-1}$ defines the relation $\{f(\alpha):f\in UnPol^{\mathscr{R}}\}$.

We will consider $\Lambda$ as a CSP instance on $n$ variables, $|V_{\mathcal{X}_{\Lambda}}|=n$ (for projections the reasoning is analogous). Suppose that for some $a_0,...,a_{n-1}$, for all $i<n$, $H(i)=\langle i,a_i\rangle$. We need to define a new CSP instance $\Upsilon$ such that the projection of its solution set to some subset of vertices is exactly $\mathscr{R}'$. Consider a CSP instance $\Upsilon_{null}$ on $nl$ variables, where for $i<n,a<l$ we think about vertex $il+a$ as about vertex $i$ that was sent to $\langle i,a\rangle$ (or if we use labels, $x_i\to a\in D_i$). Then for every $H'\in \mathscr{R}_{\Lambda}$ such that for $i<n,b_i<l,$ $H'(i)=\langle i,b_i\rangle$ we copy instance $\Lambda$ to domains $D_{b_0},D_{l+b_1},D_{2l+b_2},...,D_{(n-1)l+b_{n-1}}$. Denote the resulting instance by $\Upsilon$. It is clear that $\Upsilon\in Covering(\Lambda)$. Then the projection $\mathscr{R}_{\Upsilon}^{a_0,l+a_1,...,(n-1)l+a_{n-1}}$ defines $\mathscr{R}'$.

The algorithm of the construction is clear, but to perform it we need the number of steps that is bounded only by $l^n$ (the number of possible homomorphisms from $[n]$ to $[D_0,...,D_{n-1}]$). Since every homomorphism $H$ is expressed by a string of length $\langle n,\langle n,l\rangle \rangle<n^4$, we encode the number of steps by strings $\emptyset<T<n^4$ of length up to $n^4$, run the algorithm (if $T$ represents some homomorphism to the instance $\Lambda$, copy $\Lambda$ to corresponding domains), and then use $\Sigma^{\mathscr{B}}_1$-induction to show that such instance exists.

Suppose a $pp$-formula $\Lambda(x_0,...,x_{n-1})$ defines a relation $\mathscr{R}_{\Lambda}$ without a tuple $H\in D_{x_0}\times...\times D_{x_{n-1}}$, $\Sigma$ is the set of all relations defined by $\Upsilon(x_0,...,x_{n-1})$ where $\Upsilon\in Covering(\Lambda)$, and $\mathscr{R}_{\Lambda}$ is an inclusion-maximal relation in $\Sigma$ without the tuple $H$. Then $W^1_1$ proves that $H$ is a key tuple for $\mathscr{R}_{\Lambda}$.

Consider $\Lambda$ as a CSP instance on $n$ variables, let $S$ be any map from $[n]$ to $[D_0,...,D_{n-1}]$ that is not in $\mathscr{R}_{\Lambda}$. Then by Lemma <ref> the set of maps $\mathscr{R}'=\{S^{\Psi}:\Psi\in UnPol^{\mathscr{R}_{\Lambda}}\}$ is a projection of the solution set to some $\Upsilon\in Covering(\Lambda)$. Since $\Psi$ can be constant mapping to a homomorphism of $\Lambda$ and identity mapping, $\mathscr{R}_{\Lambda}\subsetneq\mathscr{R}'$, and since $\mathscr{R}_{\Lambda}$ is inclusion-maximal, $H\in \mathscr{R}'$. By the definition, $H$ is a key tuple for $\mathscr{R}_{\Lambda}$.

Lemmas we consider next in this section are

* either related exclusively to binary relations since we consider languages with at most binary constraint relations,

* or are used in the further proofs only for constant arity relations,

* or related to constant arity relations and constant sizes over algebra $\mathbb{A}$.

In the first and the second cases, they can be formalized and proved in $V^1$ exactly as they are proved in [21]. In the third case, such properties must be listed in the $\mathbb{A}$-Monster set. For these reasons, we will mention a few examples, but for the proofs and the rest, we refer the reader to the source [21].

[Lemma 7.19, [21]]
Suppose $R\subseteq D\times B\times B$ is a subdirect relation, $D$ is a PC algebra without a non-trivial binary absorbing or central subuniverse, and for every $b\in B$ there exists $a\in A$ such that $(a,b,b)\in R$. Then $V^1$ proves that for every $a\in A$ there exists $b\in B$ such that $(a,b,b)\in R$.

The following two lemmas are formulated in [21] for $t$ variables, but then they are only used for relations on one and two variables, so instead of using induction on $t$ we can consider just cases $\Theta(x_0)$ and $\Theta(x_0,x_1)$.
[Lemma 8.3,   [21]]
Suppose $D^{(1)}$ is a minimal absorbing, central or linear reduction for an instance $\Theta$, and $\Theta(x_0,x_1)$ defines a full relation. Then $V^1$ proves that $\Theta^{(1)}(x_0,x_1)$ defines a full or empty relation.

[Lemma 8.4,   [21]]
Suppose $D^{(1)}$ is a minimal PC reduction for a $1$-consistent instance $\Theta$. For every variable $y$ appearing at least twice in $\Theta$ the $pp$-formula $\Theta(y)$ defines $D_y$ and $\Theta(x_0,x_1)$ defines a full relation. Then $V^1$ proves that $\Theta^{(1)}(x_0,x_1)$ defines a full or empty relation

The next examples of technical lemmas are the following.

[Lemma 8.10,   [21]]
Suppose $R\leq D_i\times D_j$ is a critical rectangular binary relation, and $R'$ is a cover of $R$. Then $V^1$ proves that $Con_2^{(R,i)}\subsetneq Con_2^{(R,i)}$.

[Theorem 8.15,   [21]]
Suppose $R\leq D^4$ is a strongly rich relation preserved by an idempotent
WNU. Then $V^1$ proves that there exists an abelian group $(D,+)$ and bijective mappings $\phi_0,\phi_1,\phi_2,\phi_3:D\to D$ such that

$$R=\{(x_0,x_1,x_2,x_3): \phi_0(x_0)+ \phi_1(x_1)+\phi_2(x_2)+\phi_3(x_3)=0\}.

[Theorem 8.17,   [21]]
Suppose $\sigma\subseteq D^2$ is a congruence, $\rho$ is a bridge from $\sigma$ to $\sigma$ such that $\tilde{\rho}$ is a full relation, $pr_{1,2}(\rho)=\omega$, $\omega$ is a minimal relation stable under $\sigma$ such that $\sigma\subsetneq \omega$. Then $V^1$ proves that there exists a prime number $p$ and a relation $\zeta\subseteq D\times D\times \mathbb{Z}_p$ such that $pr_{1,2}\zeta = \omega$ and $(a_1,a_2,b)\in \zeta$ implies that $(a_1,a_2)\in \sigma\iff (b=0).$

[Lemma 8.18,   [21]]
Suppose that $\rho\subseteq D^4$ is an optimal bridge from $\sigma_1$ to $\sigma_2$, and $\sigma_1$ and $\sigma_2$ are different irreducible congruences. Then $V^1$ proves that $\sigma_2\subseteq \tilde{\rho}$.

[Lemma 8.20,   [21]]
Suppose $R\leq D_i\times D_j$ is a subdirect rectangular relation and there exists $(b_i,a_j),(a_i,b_j)\in R$ such that $(a_i,a_j)\notin R$. Then $V^1$ proves that there exists a bridge $\delta$ from $Con_2^{(R,i)}$ to $Con_2^{(R,j)}$ such that $\tilde{\delta} = R$.

These and some other lemmas imply the following result about CSP instances.

[Lemma 8.22,   [21]]
Suppose $\Theta$ is a cycle-consistent connected instance. Then $V^1$ proves that for any constraints $C,C'$ with variables $x,x'$ there exists a bridge $\delta$ from $Con^{(C,x)}$ to $Con^{(C',x')}$ such
that $\tilde{\delta}$ contains all pairs of elements linked in $\Theta$. Moreover, if $Con^{(C'',x'')}\neq Linked_{[x'',x'',\Theta]}$
for some constraint $C''\in\Theta$ and a variable $x''$, then $\delta$ can be chosen so that $\tilde{\delta}$ contains all pairs
of elements linked in $\Theta'$, where $\Theta'$ is obtained from $\Theta$ by replacing every constraint relation
by its cover.

The next lemma is easily proved by the application of the definition of a crucial instance and expanded covering. If we replace any constraint in a crucial instance $\Theta$ with all weaker constraints, we get a solution. All relations in the expanded covering $\Theta'$ are diagonal relations or weaker or equivalent to the relations in $\Theta$.

[Lemma 8.24,   [21]]
Suppose $\Theta_{\mathcal{X}}=(\mathcal{X},\ddot{\mathcal{A}})$ is a crucial instance in $D^{(1)}$, $\Theta_{\mathcal{Y}}=(\mathcal{Y},\ddot{\mathcal{B}})\in ExpCov(\Theta_{\mathcal{X}})$ through the homomorphism $H$ from $\mathcal{Y}$ to $\mathcal{X}$, and $\Theta_{\mathcal{Y}}$ has no solution in $D^{(1)}$. Then $V^1$ proves that for every constraint $E^{x_ix_j}_{\ddot{\mathcal{A}}}$ in $\Theta_{\mathcal{X}}$ there exists a constraint $E^{y_ky_p}_{\ddot{\mathcal{B}}}$ such that $H(y_k)=x_i$, $H(y_p)=x_j$ and $E^{x_ix_j}_{\ddot{\mathcal{A}}} = E^{y_ky_p}_{\ddot{\mathcal{B}}}$.

Lemmas <ref> and <ref> imply Lemma <ref>.
[Lemma 8.25,   [21]]
Suppose $\Theta_{\mathcal{X}}=(\mathcal{X},\ddot{\mathcal{A}})$ is a crucial instance in $D^{(1)}$, $\Theta_{\mathcal{Y}}=(\mathcal{Y},\ddot{\mathcal{B}})\in ExpCov(\Theta_{\mathcal{X}})$ has no solution in $D^{(1)}$, every constraint relation of $\Theta_{\mathcal{X}}$ is a critical rectangular relation, and $\Theta_{\mathcal{Y}}$ is connected.
Then $V^1$ proves that $\Theta_{\mathcal{X}}$ is connected.

§.§ Formalization of the main theorems

§.§.§ The existence of the next reduction

[Lemma 9.1, [21]]
Suppose $D^{(0)},D^{(1)},...,D^{(s)}$ is a strategy for a $1$-consistent CSP instance $\Theta$, and $D^{(\bot)}$ is a reduction of $\Theta^{(s)}$. Then $V^1$ proves that:

* if there exists a $1$-consistent reduction contained in $D^{(\bot)}$ and $D^{(s+1)}$ is maximal among such reductions, then for every variable $x$ of $\Theta$ there exists a tree-formula $\Upsilon_x\in Coverings(\Theta)$ such that $\Upsilon^{(\bot)}_x(x)$ defines $D^{(s+1)}_x$;

* otherwise, there exists a tree-formula $\Upsilon\in Coverings(\Theta)$ such that $\Upsilon^{(\bot)}$ has no solutions.

The proof of this theorem is based on constraint propagation. At the beginning for every variable $x$ we consider an empty tree-formula $\Upsilon_x$. Then $\Upsilon^{(\bot)}_x$ defines the reduction $D^{(\bot)}$. Then the recursive algorithm works as follows: if at some step the reduction defined by these tree-formulas is $1$-consistent, it stops. Otherwise, it considers any constraint $C=R(x_1,...,x_t)$ that breaks $1$-consistency. The current restrictions of variables $x_1,...,x_t$ in $C$ imply stronger restriction of some variable $x_i$, and the algorithm changes the formula $\Upsilon_{x_i}$ as follows:

$$\Upsilon_{x_i} =_{def} C\wedge \Upsilon_{x_1}\wedge...\wedge \Upsilon_{x_t}.$$

To keep the formula $\Upsilon_{x_i}$ tree, any time the algorithm joins $\Upsilon_{x_j}$ and $\Upsilon_{x_k}$ it renames the variables so that they do not have common variables. Finally, for each $\Upsilon_{x_j}$ we consider the reduction of this instance on the domain set $D^{(\bot)}$. Projection of the solution set to $\Upsilon^{(\bot)}_{x_j}$ on variable $x_j$, $\Upsilon^{(\bot)}_{x_j}(x_j)$ defines $D^{(s+1)}_{x_j}$. That will be a maximal $1$-consistent reduction since it is defined by

Let us formalize this algorithm. The formalization is based on a $1$-consistency algorithm (see [2]). Recall that any CSP instance can be converted in polynomial time to a $1$-consistent one with the same set of solutions. Moreover, any implementation of a $1$-consistency algorithm derives the same unary constraints. Thus, we can first define recursive sets of edges and vertices, based on which we can construct our tree-formulas.

For the steps $t=0,t=1$ for any $i,j<n$ we set

\begin{equation}\label{88djeu6453}
\begin{gathered}
E^{ij}_{\ddot{\mathcal{A}},0}(a,b) \iff E^{ij}_{\ddot{\mathcal{A}}}(a,b),\\
E^{ij}_{\ddot{\mathcal{A}},1}(a,b) \iff a\in D_i^{(\bot)}\wedge b\in D_j^{(\bot)}\wedge E^{ij}_{\ddot{\mathcal{A}}}(a,b).
\end{gathered}
\end{equation}

For any further step $t>1$ we will propagate constraints recursively until we cannot change any domain further (i.e. until the instance is $1$-consistent) or some domain is empty. For any $i,j<n$ we set:

\begin{equation}\label{dhhjsyu65d}
\begin{gathered}
\hspace {0pt}E^{ij}_{\ddot{\mathcal{A}},t}(a,b) \iff \big[(\forall p,r<n,\exists e,f<l,\, E_{\mathcal{X}}(p,r)\rightarrow E^{pr}_{\ddot{\mathcal{A}},t-1}(e,f)) \wedge \\
\hspace {0pt}\wedge E^{ij}_{\ddot{\mathcal{A}},t-1}(a,b)\wedge \forall q<n,\,E_{\mathcal{X}}(i,q) \rightarrow \exists d \in D^{(\bot)}_{q},\,E^{iq}_{\ddot{\mathcal{A}},t-1}(a,d)\wedge\\
\hspace {0pt}\hspace {0pt}\wedge\forall k<n, \, E_{\mathcal{X}}(k,i) \rightarrow \exists c \in D^{(\bot)}_{k},\,\, E^{ki}_{\ddot{\mathcal{A}},t-1}(c,a)\wedge\\
\hspace{0pt}\wedge\forall q<n,\,E_{\mathcal{X}}(j,q) \rightarrow \exists d \in D^{(\bot)}_{q},\,E^{jq}_{\ddot{\mathcal{A}},t-1}(b,d)\wedge\\
\hspace {0pt}\hspace {0pt}\wedge\forall k<n, \, E_{\mathcal{X}}(k,j) \rightarrow \exists c \in D^{(\bot)}_{k},\,\, E^{kj}_{\ddot{\mathcal{A}},t-1}(c,b)\big] \vee\\
\hspace {0pt}\vee \big[(\exists p,r<n,\forall e,f<l,\,E_{\mathcal{X}}(p,r)\wedge \neg E^{pr}_{\ddot{\mathcal{A}},t-1}(e,f)) \wedge E^{ij}_{\ddot{\mathcal{A}},t-1}(a,b)\big].
\end{gathered}
\end{equation}

The expression in the first square brackets holds when neither of the relations at the previous step is empty, and the expression in the second square brackets holds otherwise (it would mean that some domain of the instance at this step is already empty). In both cases after some step $t$ the relation set $E^{ij}_{\ddot{\mathcal{A}},t-1}$ stops changing. The maximal number of edges in a directed graph with loops on $n$ vertices is $n^2$. Therefore, the maximal number of edges in the instance $\Theta$ is $n^2l^2$ and since at each step we reduce some relation at least by one edge, it is enough to consider at most $n^2l^2$ steps. Moreover, since we remove an edge if at least one of its endpoints $a\in D^{(\bot)}_i$ violates $1$-consistency (so within one step we remove all edges in $E^{ij}_{\ddot{\mathcal{A}},t-1}$ connected with $a$ for all $j<n$), the actual number of steps is $nl$ (the number of elements). The existence of this set is ensured by $\Sigma^{1,b}_1$-induction: consider the formula

\begin{equation}
\begin{gathered}
\phi(t)=\exists E_{\ddot{\mathcal{A}}}<\langle t, \langle\langle n,l \rangle, \langle n,l \rangle\rangle\rangle,\, \forall i,j<n,\forall a,b<l,\,E^{ij}_{\ddot{\mathcal{A}},1}(a,b)\leftrightarrow (\ref{88djeu6453})\wedge\\
\hspace {0pt}\wedge \forall 1<p<t,\forall i,j<n,\forall a,b<l,\,E^{ij}_{\ddot{\mathcal{A}},p}(a,b)\leftrightarrow (\ref{dhhjsyu65d}).
\end{gathered}
\end{equation}

Since (<ref>) is a $\Sigma^{1,b}_0$-formula, to provide the implication $\phi(t)\rightarrow \phi(t+1)$ we can use comprehension axiom $\Sigma^{1,b}_0$-COMP.

Note that in (<ref>) we do not need to track the domain's changes separately (they are all recorded in the relations $E^{ij}_{\ddot{\mathcal{A}},t}$). We will proceed with recursive propagation of the domain set $V_{\ddot{\mathcal{A}}}$ after this procedure based on the resulting relation set. For any $i<n$, for steps $t=0,t=1$ we set

\begin{equation}
\begin{gathered}
V_{\ddot{\mathcal{A}},0}(i,a)\iff D_i(a), \\
V_{\ddot{\mathcal{A}},1}(i,a)\iff D_i^{(\bot)}(a),
\end{gathered}
\end{equation}

and for all $1<t<nl$

\begin{equation}\label{ssskiia8a6yu}
\begin{gathered}
V_{\ddot{\mathcal{A}},t}(i,a)\iff V_{\ddot{\mathcal{A}}^,t-1}(i,a) \wedge (\forall j<n,\,E_{\mathcal{X}}(i,j) \rightarrow (\exists b<l,\, V_{\ddot{\mathcal{A}}^,t-1}(j,b)\wedge\\
\hspace {0pt}\wedge E^{ij}_{\ddot{\mathcal{A}},t}(a,b)))\wedge(\forall k<n, \, E_{\mathcal{X}}(k,i) \rightarrow (\exists c<l,\,V_{\ddot{\mathcal{A}},t-1}(k,c)\wedge \\
\hspace {0pt}\wedge E^{ki}_{\ddot{\mathcal{A}},t}(c,a))).
\end{gathered}
\end{equation}

Again, this set exists due to $\Sigma^{1,b}_1$-induction. Note that in (<ref>) for the step $t<nl$ we use $E_{\ddot{\mathcal{A}},t-1}$ and not $E_{\ddot{\mathcal{A}},nl}$: we need recursive changing of the domains for further reconstruction of the tree-formulas $\Upsilon_i$. We also define a set $C^{list}_i$ that for any step $0<t<nl$ collect elements that were deleted from $V_{\ddot{\mathcal{A}},t,i}$:

\begin{equation}
\begin{gathered}
\forall 0<t<nl,\forall a<l,\, C^{list}_i(t,a)\iff V_{\ddot{\mathcal{A}},t-1}(i,a)\wedge \neg V_{\ddot{\mathcal{A}},t}(i,a).
\end{gathered}
\end{equation}

Further, we need to construct tree-instances $\Upsilon_i$. We want them to be coverings, so for each $i$ we only need to define an instance graph $\mathcal{X}_i$ and remember parents for renamed variables. To do it, we again use recursion. For each $i<n$, we start with an instance $\Upsilon_{i,0}$ with a domain set $D$ and with an empty set of constraints. Then for further steps $u$ we:

* either do nothing with instance $\Upsilon_{i,u}$ - if for any $k<n$ and for some $t$ constraints $E^{ik}_{\ddot{\mathcal{A}},t}$ and $E^{ki}_{\ddot{\mathcal{A}},t}$ that violate $1$-consistency do not imply stronger restriction of a domain $D_i$,

* or we need to consider a union of two CSP instances (that corresponds to the intersection of their constraints) for every constraint $E^{ij}_{\ddot{\mathcal{A}},t}$ (or $E^{ji}_{\ddot{\mathcal{A}}^,t}$) restricting domain $D_i$, namely

$$\Upsilon_{i,u}:= E^{ij}_{\ddot{\mathcal{A}}}\wedge \Upsilon_{i,u-1}\wedge \Upsilon_{j,u-1}.

Note that while our next move depends on reduced by the step constraint $E^{ik}_{\ddot{\mathcal{A}},t}$, to the instance $\Upsilon_{i,u}$ we add original constraint $E^{ik}_{\ddot{\mathcal{A}}}$. After we add enough such constraints and previous instances, the reduction of the resulted instance $\Upsilon_{i,u}$ to $D^{(\bot)}$ will give us the same projection to the coordinate $D_{i}$ as it gives (<ref>).

Also note that if two constraints at step $t$ reduce domain $D_i$ by the same values, we do not need to and we will not construct both intersections. Recall that when joining any two $\Upsilon_{i,t-1}, \Upsilon_{j,t-1}$ we have to rename all variables to retain the instances tree. Since we have at most binary relations and for any two variables there can be only two constraints containing them, namely $E^{ij}_{\ddot{\mathcal{A}}}$ and $E^{ji}_{\ddot{\mathcal{A}}}$, at the first step of the recursion process, we can add to each $\Upsilon_{i,1}$ at most $2n$ new vertices (if for every $j<n$ there are both $E_{\mathcal{X}}(i,j)$ and $E_{\mathcal{X}}(j,i)$). Then for every new constraint restricting at step $t$, we can at most double the number of variables of the largest instance of step $(t-1)$. Still, it will not make sense after the first $l$ intersections for every $\Upsilon_i$ since in this case we will get an empty domain set $D_i$ and thus justify the case $2$ of the theorem. Thus, even if we start with instances $\Upsilon_{i,1}$ on $2n$ variables, after $l$ intersections we will not need more than $2^l2n$ variables.

First, for every $\Upsilon_{i,0}$, define $V_{\mathcal{X}_i,0}$ as a set of length $2^l2n$ that contains only one element $i$, and $E_{\mathcal{X}_i,0}$ as an empty set of length $\langle 2^l2n,2^l2n\rangle$. By $V_{\ddot{\mathcal{A}}_i,0}$ denote the set of length $\langle 2^l2n,l\rangle$, with only one non-empty domain $V_{{\ddot{\mathcal{A}}_i},0} = D_i$. By $E_{{\ddot{\mathcal{A}}_i},0}$ denote an empty set of length $\langle\langle 2^l2n,l\rangle,\langle 2^l2n,l\rangle \rangle$.

Strictly speaking, we are not allowed to use empty sets of some length. But we can bypass it by choosing a set, for example, for $V_{\mathcal{X}_i,0}$ with two elements, $i$, and that we will never properly use $2^l2n+1$. Further, we also consider the number function $max'(V_{\mathcal{X}_i,u})$ with the following value:

\begin{equation}
\begin{gathered}
max'(V_{\mathcal{X}_i,u}) = m \iff m\neq 2^l2n+1\wedge \forall u\in V_{\mathcal{X}_i,u}, (u\neq 2^l2n+1\rightarrow u\leq m).
\end{gathered}
\end{equation}

We construct $\Upsilon_0$,...,$\Upsilon_{n-1}$ simultaneously. The entire construction takes $0<u<2n(nl)$ steps. Each $\Upsilon_{i,u}$ consists of

* set $V_{\mathcal{X}_i,u}$, representing the current number of vertices,

* set $E_{\mathcal{X}_i,u}$, representing the current set of edges,

* set $V_{{\ddot{\mathcal{A}}_i},u}$, representing domains for current variables,

* set $E_{{\ddot{\mathcal{A}}_i},u}$, representing constraint relations for current variables,

* and set $C^{erase}_{i,u}$ that keeps track of elements that must be deleted from the domain $D_i$ during each outer step $t$ and erases them one by one if we need to change the instance $\Upsilon_{i,u}$.

We consider these sets in the above order. The description of the algorithm is as follows. For every $\Upsilon_i$, within any step $1<t<nl$ we run $2n$ internal steps. At the beginning of each new internal iteration, for some $2nt$ step, we check the list $C^{list}_{i,t+1}$ for elements that we will exclude from $D_i$ by adding new constraints to the instance during this internal iteration. We write them down to $C^{erase}_{i,2nt}$. For each step $u=2nt+j$ we consider the constraint $E^{ij}_{{\ddot{\mathcal{A}}},t+1}$ (for step $2nt+j+1$ we consider the opposite constraint $E^{ji}_{{\ddot{\mathcal{A}}},t+1}$) and decide whether it kills any of the elements from $C^{erase}_{i,2nt+j}$.
For any $a\in C^{erase}_{i,2nt+j}$ it happens when there exists at least one edge $(a,b)\in E^{ij}_{{\ddot{\mathcal{A}}},t}$ and no edges connected with $a$ in $E^{ij}_{{\ddot{\mathcal{A}}},t+1}$:

\begin{equation}
\exists a\in C^{erase}_{i,2nt+j} (\exists b<l,\,E^{ij}_{\ddot{\mathcal{A}},t}(a,b) \wedge \forall b<l,\,\neg E^{ij}_{\ddot{\mathcal{A}},t+1}(a,b)) .\,\,\text{[formula (\ref{dhhjsyu65d})]}
\end{equation}

If it is the case, we define our instance $\Upsilon_{i,u+1}$ as follows: we first replicate instance $\Upsilon_{i,u}$ and then add all vertices of $\Upsilon_{j,u}$ to part from $max(V_{\mathcal{X}_i,u})+1$ as well as all edges of $\Upsilon_{j,u}$, and add an edge $E_{\mathcal{X}_i,u+1}(i,max(V_{\mathcal{X}_i,u})+1+j)$.

\begin{equation}
\begin{gathered}
\forall k<max'(V_{\mathcal{X}_i,u})+1,\,V_{\mathcal{X}_i,u+1}(k)\iff V_{\mathcal{X}_i,u}(k),\\
\forall k_1,k_2<max'(V_{\mathcal{X}_i,u})+1,\,E_{\mathcal{X}_i,u+1}(k_1,k_2)\iff E_{\mathcal{X}_i,u}(k_1,k_2),\\
\forall max'(V_{\mathcal{X}_i,u})<k< 2^l2n+1,\,V_{\mathcal{X}_i,u+1}(max'(V_{\mathcal{X}_i,u})+1+k)\iff V_{\mathcal{X}_j,u}(k), \\
\forall max'(V_{\mathcal{X}_i,u})<k_1,k_2< 2^l2n+1,\\
\hspace {0pt}E_{\mathcal{X}_i,u+1}(max'(V_{\mathcal{X}_i,u})+1+k_1,max'(V_{\mathcal{X}_i,u})+1+k_2)\iff E_{\mathcal{X}_j,u}(k_1,k_2),\\
\end{gathered}
\end{equation}

In the same way, we define a target digraph $\ddot{\mathcal{A}}_{i,u+1}$ by adding new domains for new variables (from the list $\{D_0,...,D_{n-1}\}$) and $E^{ij}_{\ddot{\mathcal{A}}}$ as a constraint for the new edge $E_{\mathcal{X}_i,u+1}(i,$ $max(V_{\mathcal{X}_i,u})+1+j)$.

If this is not the case, we just replicate instance $\Upsilon_{i,u}$ to $\Upsilon_{i,u+1}$. Finally, we either replicate the set $C^{erase}_{i,u}$ or change it to $C^{erase}_{i,u+1}$ as follows:

\begin{equation}
\begin{gathered}
\forall a<l,\,C^{erase}_{i,(2nt+j)+1}(a)\iff C^{erase}_{i,2nt+j}(a)\wedge (\exists b<l,\, E^{ij}_{\ddot{\mathcal{A}},t+1}(a,b)).
\end{gathered}
\end{equation}

Thus, after we pass constraint $E^{ji}_{{\ddot{\mathcal{A}}},t+1}$ we leave in $C^{erase}_{i,(2nt+j)+1}$ those elements that will be deleted in $V_{{\ddot{\mathcal{A}}},t+1}$ but because of another constraint that will lose all edges adjacent to them. We keep track of already deleted elements for the outer step $t$ not to intersect the instances with constraints that kill the same set of vertices – because we want to stop after intersection $l$ with an empty domain.

At each step, sets $V_{\mathcal{X}_i,u}$, $V_{{\ddot{\mathcal{A}}_i},u}$,
$E_{\mathcal{X}_i,u}$, $E_{{\ddot{\mathcal{A}}_i},u}$ and $C^{erase}_{i,u}$ address themselves and each other in previous steps. They also address different levels of the already defined set $C^{list}_i(t,a)$ based on $V_{\ddot{\mathcal{A}},t}$ and $E^{ij}_{\ddot{\mathcal{A}},t}$. The existence of them is given by $\Sigma^{1,b}_1$-induction. At some point, we stop with tree-instances $\Upsilon_i$, each of them defining $D^{(s+1)}_i$ on $D^{(\bot)}$.

The next three theorems follow from Lemma <ref> and some previous results, formalized in $W^1_1$.

Suppose $D^{(0)},D^{(1)},...,D^{(s)}$ is a strategy for a cycle-consistent CSP instance $\Theta$. Then $W^1_1$ proves that:

* if $D^{(s)}_x$ has a non-trivial binary absorbing subuniverse $B$ then there exists a $1$-consistent absorbing reduction $D^{(s+1)}$ of $\Theta^{(s)}$ with $D_x^{(s+1)}\subseteq B$;

* if $D^{(s)}_x$ has a non-trivial central subuniverse $C$ then there exists a $1$-consistent central reduction $D^{(s+1)}$ of $\Theta^{(s)}$ with $D_x^{(s+1)}\subseteq B$;

* if $D^{(s)}$ has no non-trivial binary absorbing or central subuniverse for every $y$ but there exists a non-trivial PC subuniverse $B$ in $D^{(s)}_x$ for some $x$,
then there exists a $1$-consistent PC reduction $D^{(s+1)}$ of $\Theta^{(s)}$ with $D_x^{(s+1)}\subseteq B$.

Suppose that $D^{(0)},D^{(1)},...,D^{(s)}$ is a strategy for a $1$-consistent CSP instance $\Theta$, and $D^{(\bot)}$ is a non-linear $1$-consistent reduction of $\Theta^{(s)}$. Then $W^1_1$ proves that there exists a $1$-consistent minimal reduction $D^{(s+1)}$ of $\Theta^{(s)}$ of the same type such that $D_i^{(s+1)}\subseteq D_i^{(\bot)}$ for every variable $i$.

Suppose $D^{(\bot)}$ is a $1$-consistent PC reduction for a cycle-consistent irreducible
CSP instance $\Theta$, $\Theta$ is not linked and not fragmented. Then $W^1_1$ proves that there exist a reduction $D^{(1)}$ of $\Theta$ and a minimal strategy $D^{(1)},...,D^{(s)}$ for $\Theta^{(1)}$ such that the solution set to $\Theta^{(1)}$ is subdirect, the reductions $D^{(2)},...,D^{(s)}$ are non-linear, $D^{(s)}_x\subseteq D^{(\bot)}_x$ for every variable $x$.

§.§.§ Main theorems proved by induction

In this section, we consider the main five theorems, proved simultaneously by induction on the size of the domain set (to be defined further). We will not consider the formalization of their proofs, since it is based on the formalization of previous results. However, some reasoning from the proofs is used for the formalization of the theorems.

We will use the same notation $D^{(s)}$ for the reductions of the initial instance, its subinstances, subconstraints, differences, unions, and both coverings and expanded coverings to avoid unnecessary indices. These, of course, cannot be the same sets of domains, but once given $D^{(s)}$ for an instance $\Theta_{\mathcal{X}}$ we can easily construct a similar reduction for any of these objects, denoted by $\Theta_{\mathcal{Y}}$, under the simple rule

$$\forall x_i\forall y_j,\,\, D_{x_i}=D_{y_j}\implies D^{(s)}_{x_i}=D^{(s)}_{y_j}.

This is well-defined since we can additionally require in the reduction $D^{(s)}$ of instance $\Theta_{\mathcal{X}}$ that equal domains be reduced to equal domains (see <ref>). In a minimal $1$-consistent one-of-four reduction, every $D^{(s)}_{x_i}$ must be minimal by inclusion.

Suppose $D^{(1)}$ is a minimal $1$-consistent one-of-four reduction of a cycle-consistent irreducible CSP instance $\Theta$, $\Lambda(x_0,...,x_{n-1})$ is a subconstraint of $\Theta$, the solution set to $\Lambda^{(1)}$ is subdirect, $\Theta\backslash\Lambda$ has a solution in $D^{(1)}$, and $\Theta$ has no solutions in $D^{(1)}$. Then $W_1^1$ proves that there exist instances $\Upsilon_1,...,\Upsilon_t\in Coverings(\Lambda)$ such that $\Phi = (\Theta\backslash\Lambda)\cup\Upsilon_1\cup...\cup \Upsilon_{t}$ has no solutions in $D^{(1)}$, each $\Upsilon_i(x_0,...,x_{n-1})$ is a subconstraint of $\Phi$, and $\Upsilon^{(1)}_i(x_0,...,x_{n-1})$ defines a subdirect key relation with the parallelogram property for every $i$.

The formalization of the theorem will be based on its proof. Since $\Lambda(x_0,...,x_{n-1})$ is a subconstraint of $\Theta$, it follows that $\Lambda$ is a subinstance of $\Theta$ that involves variables $x_0,...,$ $x_{n-1},$ $y_0,...,y_{k-1}$, and $\Theta$ as an instance on variables $x_0,...,x_{n-1},y_0,...,y_{k-1}, z_0,...,z_{s-1}$ such that $\Theta\backslash\Lambda$ involves variables $x_0,...,x_{n-1},z_0,...,z_{s-1}$. $\Upsilon_i(x_0,...,x_{n-1})$ here denotes all tuples $(a_0,...,a_{n-1})$ such that instance $\Upsilon_i$ has a solution with $x_0=a_0$,...,$x_{n-1}=a_{n-1}$. That is, it is a projection of the solution set to $\Upsilon_i$ onto coordinates $x_0,...,x_{n-1}$, which can be expressed by the formula

$$\exists y^i_0...\exists y_{m_i-1}^i\Upsilon_i(x_0,...,x_{n-1},y_0^i,...,y_{m_i-1}^i).

$\Upsilon^{(1)}_i(x_0,...,x_{n-1})$ thus expressed the projection of the solution set to the instance $\Upsilon_i^{(1)}$ after the reduction $D^{(1)}$. We can denote this projection using a third-order object $\mathscr{R}^{x_0,...,x_{n-1}}_{\Upsilon_i^{(1)}}$. Note that when we talk not about a solution set to an instance but about projection to the solution set, we add to the formula an additional second-sorted existential quantifier, see (<ref>).