and thus

$F(X,X)\cap F(X,X_{2})\cap F(X_{1},X)\cap F(X_{1},X_{2})=$  $$F(X,X)\cap F(X,Y_{2})\cap F(Y_{1},X)\cap F(Y_{1},Y_{2}).$$
Since, by normality of F,

$$\begin{array}{r c l}{{F(X,X)\cap F(X,X_{2})\cap F(X_{1},X)}}&{{\supseteq}}&{{t_{f}^{\mathfrak{M}}(X),}}\\ {{}}&{{F(X,X)\cap F(X,Y_{2})\cap F(Y_{1},X)}}&{{\supseteq}}&{{t_{f}^{\mathfrak{M}}(X),}}\end{array}$$
$${\mathrm{this~implies~}}t_{f}^{\mathfrak{M}}(X)\cap F(X_{1},X_{2})=t_{f}^{\mathfrak{M}}(X)\cap F(Y_{1},Y_{2}).$$
$\square$
4.2.3 THE TRANSFER RESULT
Using covering normal terms, we can now formulate the second transfer theorem, which is concerned with the transfer of decidability of (non-relativized) satisfiability.

Theorem 29. Let S 1 and S 2 be local ADSs having covering normal terms, and suppose that the satisfiability problems for S1 and S2 are decidable. Then the satisfiability problem for S1 8 S2 is also decidable.

As in the proof of Theorem 17, we fix two local ADSs Si = ( Li, Mi), i E {1, 2}, in which L is based on the set of function symbols F and relation symbols R , and L 2 is based on G
and Q. Let L = L 1 8 L 2 and M = M 1 8 M 2 .

The proof of Theorem 29 follows the same general ideas as the proof of Theorem 17.

There are, however, notable differences in the way satisfiability in S 1 & S 2 is reduced to stisfiability in S 1 and S 2 . In Theorem 20 we had to "guess" a set D of types, and then based on this set and some additional guesses, a pair of satisfiability problems Γ 1 and Γ 2 in S 1 and S 2 , respectively, was generated. In the proof of Theorem 29, we do not need to guess D. Instead, we can compute the right set. However, this computation requires us to solve additional satisfiability problems in the fusion S 1 & S 2 . Nevertheless, this yields a reduction since the alternation depth (i.e., number of alternations between function symbols of S 1 and S 2 ) decreases when going from the input set Γ to these additional mixed satisfiability problems.

Before we can describe this reduction in more detail, we must introduce some new notation. In the case of relativized satisfiability, term assertions of the form T E sur i ( V D )
were used to assert that all elements of the domain belong to suri(VD). Now, we use covering normal terms to "propagate" suri( VD ) into terms up to a certain depth. For a set of function symbols E , define the E -depth d E ( t ) of a term t inductively:

$d_{E}\left[\left.x_{i}\right.\right]$
dE(xi) = 0

$$d_{E}\left(\neg t\right)=d_{E}\left(t\right)$$ $$d_{E}\left(t_{1}\lor t_{2}\right)=d_{E}\left(t_{1}\wedge t_{2}\right)=max\{d_{E}\left(t_{1}\right),d_{E}\left(t_{2}\right)\}$$ $$d_{E}\left(f\left(t_{1},\ldots,t_{n}\right)\right)=max\{d_{E}\left(t_{1}\right),\ldots,d_{E}\left(t_{n}\right)\}+1\ \ \mbox{if}\ \ f\in E$$ $$d_{E}\left(f\left(t_{1},\ldots,t_{n}\right)\right)=max\{d_{E}\left(t_{1}\right),\ldots,d_{E}\left(t_{n}\right)\}\ \ \mbox{if}\ \ f\not\in E$$
