Splitting and Updating Hybrid Knowledge Bases (Extended Version) 49 Finally, for any predicate symbol P that does not belong to Sα, I
[Sα], J
[Sα]and J
′[Sα] do not contain any atoms with the predicate symbol P, so diff (P, I[Sα], J′[Sα]) = ∅ = diff (P, I[Sα], J[Sα]) .

Thus, we can conclude that J
′[Sα] <I
[Sα] J
[Sα],
so J
[Sα] does not belong to I
[Sα] ⊕ N[Sα], which finishes this part of the proof.

For the converse implication, suppose that for some ordinal **α < µ**, J
[Sα] does not belong to I
[Sα] ⊕ N[Sα]. If J
[Sα] does not belong to N[Sα], we immediately obtain that J
does not belong to N. Consequently, J cannot belong to I ⊕ N.

It remains to consider the principal case when J
[Sα] belongs to N[Sα]. Then there must be some interpretation J
′ ∈ N[Sα]such that J
′ <I
[Sα] J
[Sα]. Thus, for all predicate symbols P ∈ P we know that diff (P, I[Sα], J′) ⊆ diff (P, I[Sα], J[Sα]) . (D3)
We also know that there is some predicate symbol P0 ∈ P such that diff (P0, I[Sα], J′) ( diff (P0, I[Sα], J[Sα]) . (D4)
Additionally, for every predicate symbol P from P \ Sα it holds that I
[Sα], J
[Sα]and J
′
contain no atoms with the predicate symbol P, so that diff (P, I[Sα], J′) = ∅ = diff (P, I[Sα], J[Sα]) .

Consequently, P0 must belong to Sα. Now let J
′′ = J
′ ∪ J
[P\Sα]. It is easy to see that J
′′[Sα] = J
′ ∈ N[Sα]and for every ordinal **β < µ** such that β 6= α, J
′′[Sβ] = J
[Sβ] ∈
N[Sβ], so since N is sequence-saturated relative to S, J
′′ belongs to N. Now take some predicate symbol P ∈ P and consider the following two cases:
a) If P belongs to Sα, then from (D3) we obtain diff (**P, I, J**′′) = diff (P, I[Sα], J′) ⊆ diff (P, I[Sα], J[Sα]) .

b) If P belongs to P \ Sα, then since J
′′[P\Sα] = J
[P\Sα],
diff (**P, I, J**′′) = diff (**P, I, J**) .

In both cases we see that diff (**P, I, J**′′) is a subset of diff (**P, I, J**). Moreover, from (D4)
we obtain diff (P0**, I, J**′′) = diff (P0, I[Sα], J′) ( diff (P0, I[Sα], J[Sα]) .

It follows from the above considerations that J
′′ <I J. Consequently, J does not belong to I ⊕ N.

Proposition 92 Let S = hSαiα<µ be a saturation sequence, M, N ∈ M be both sequence-saturated relative to S and J be a Herbrand interpretation. Then J ∈ M ⊕ N ⇐⇒ (∀**α < µ**)(J
[Sα] ∈ M[Sα] ⊕ N
[Sα]) .

Proof