The assertions in (2e) and (2i) state (again in surrogated versions) that the object interpreting the variable a has type tg. This ensures that, in the models of Γ 1 and Γ 2
(given when showing (2 → 1)), the objects interpreting a have the same type t α from D .

Otherwise, these models could not be combined into a common one for F.

The sets (2f) and (2j) are obtained from Γ by distributing its relationship assertions between Γ 1 and Γ 2 , depending on the relation symbol used in the assertion.

The set (2g) contains (in surrogated version) the term assertions of the form t 1 ⊂ t 2 and the membership assertions of the form a : s of Γ .

Condition 2 is asymmetric in two respects. First, it guesses a subset of C 1 (Γ) rather than a subset of C 2 (F).  Of course this is arbitrary, we could also have chosen index 2 instead of 1 here.  Second, the set Γ 2 neither contains the assertions { sur 2 ( t 1 ) ⊆  sur 2 ( t 2 ) │ t 1  ⊆
t2 E Γ } nor { a : sur2(s) | (a : s) E Γ }. If we added these assertions, the theorem would still be true, but this would unnecessarily increase the amount of work to be done by the combined decision procedure. In fact, since the other assertions in Γ 1 and Γ 2 enforce a tight coordination between the models of Γ 1 and Γ 2 , the fact that the membership assertions and term assertions of Γ are satisfied in the models of Γ 1 implies that they are also satisfied in the models of F2 (see the appendix for details).

To prove Theorem 17, we must show how Theorem 20 can be used to construct a decision procedure for relativized satisfiability in S 1 8 S 2 from such decision procedures for the component systems S 1 and S 2 . For a given finite set of assertions Γ of S 1 ⊗ S 2 , the set C 1 (Γ) is also finite, and thus there are finitely many sets D in (2a) and choices of types for object variables in (2c).  Consequently, we can enumerate all of them and check whether one of these choices leads to satisfiable sets Γ 1 and Γ 2 . By definition of the sets Γ i and of the functions sur i , the assertions in Γ i are indeed assertions of L i , and thus the satisfiability algorithm for ( Li, Mi) can be applied to Γj. This proves Theorem 17.

Regarding the complexity of the obtained decision procedure, the costly step is guessing the right set D. Since the cardinality of the set sub 1 ( Γ ) is linear in the size of Γ , the cardinality of C 1 ( Γ ) is exponential in the size of Γ (and each element of it has size quadratic in Γ). Thus, there are doubly exponentially many different subsets to be chosen from.  Since the cardinality of the chosen set D may be exponential in the size of Γ , also the size of Γ 1 and Γ 2 may be exponential in Γ (because of the big disjunction over D ). From this, the following corollary follows. Corollary 21. Let S 1 and S 2 be local ADSs, and suppose that the relativized satisfiability problems for S1 and S2 are decidable in EXPTIME (PSPACE). Then the relativized satisfiability problem for S 1 8 S 2 is decidable in 2 E XP T I ME (E XP S PACE).

Proof. Assume that Γ has size π . Then we must consider 2 P t ( x ) (for some polynomial p 1 )
different sets D in (2a). Each such set has size 2 P t ( n ) and thus we have of 2 P 2 ( n ) choices in (2c) (for some polynomial p 2 ).  Overall, this still leaves us with doubly exponentially many choices. Now assume that the relativized satisfiability problems for S 1 and S 2 are decidable in EXPTIME. Since each call of these procedures is applied to a set of assertions of exponential size, it may take double exponential time, say 22 p 3 ( n ) and 22 p 4 ( n ) (for polynomials p3 and p4). Overall, we thus have a time complexity of 72p, (n) + 2 p 2 (n) + 2 p 3 (n) + 2 2p 4 (n)),