and by another application of Proposition 90 we obtain that σ(M′, Sα) is the minimal change update model of bSα(U
′).

It remains to show that M′is sequence-saturated relative to S. Suppose that J is a Herbrand interpretation such that J
[Sα] belongs to M′[Sα]. We conclude by Proposition 93 that for any **α < µ**, J
[Sα] belongs to M[Sα] ⊕ N[Sα]. Thus, by Proposition 92, J belongs to M ⊕ N = M′as desired.

## Proposition 103

Let U = hUii be a finite sequence of first-order theories, U be a splitting sequence for U
and S = hSαiα<µ be the saturation sequence induced by U. If for every ordinal **α < µ**, Xα is the minimal change update model of bSα(U), then Tα<µ Xα is the minimal change update model of U.

## Proof

We prove by induction on n.

1
◦If n = 0, then U = h i and for every **α < µ**, bSα(U) = h i, so Xα = I and M =Tα<µ Xα = I, so M is indeed the minimal change update model of U.

2
◦ We assume the claim holds for n and prove it for n+1. Suppose that for every ordinal α < µ, X′α is the minimal change update model of bSα(U
′) where U
′ = hUiii<n+1.

We need to show that Tα<µ X′α is the minimal change update model of U
′.

It follows from Proposition 90 that X′α = Xα ⊕ Yα where Xα is the minimal change update model of bSα(U), where U = hUiii<n, and Yα is the MKNF model of bSα(Un). Thus, by the inductive assumption, M =Tα<µ Xα is the minimal change update model of U. Also, by Proposition 98, N =Tα<µ Yα is the MKNF model of Un. Moreover, we know from Proposition 101 that both Xα and Yα are saturated relative to Sα. Thus, we can use Proposition 48 to conclude that Xα = σ(**M, S**α) and Yα = σ(**N, S**α) and that both M and N are nonempty and by Proposition 47 they are also sequence-saturated relative to S. We can thus apply Propositions 92 and 94 to obtain

$$M\oplus N=\bigcap_{\alpha<\mu}\sigma(M,S_{\alpha})\oplus\sigma(N,S_{\alpha})=\bigcap_{\alpha<\mu}X_{\alpha}\oplus Y_{\alpha}=\bigcap_{\alpha<\mu}X_{\alpha}^{\prime}\;\;.$$

Thus, by Proposition 90 it follows that Tα<µ X′α is the minimal change update model of U
′.

## Appendix E Splitting Theorem For Dynamic Logic Programs

Proposition 104 *(Positive Support*)
Let I be a dynamic stable model of a dynamic logic program P. Then for every p ∈ I there exists a rule r from ρ(P)P such that H(r) = p and I |= B(r).

Proof Follows by definition and the fact that the least model of a definite logic program satisfies support.