48 *M. Slota and J. Leite and T. Swift* Follows by Lemma 87 and the fact that I ⊕ M = M for any M ∈ M.

Proposition 89 Let U = hUiii<n be a sequence of first-order theories with n > 0 and M be the minimal change update model of U. Then M |= Un−1.

Proof (sketch)
This follows by induction on n, by the fact that M⊕N is a subset of N for any M, N ∈ M.

Proposition 90 Let U = hUiii<n+1 be a nonempty sequence of first-order theories and M be an MKNF
interpretation. Then M is a minimal change update model of U if and only if M = N1⊕N2 where N1 is the minimal change update model of hUiii<n and N2 is the MKNF model of Un.

Proof By Def. 85, M is the minimal change update model of U if and only if M = mod(U) = N1 ⊕ N2 ,
where N1 =Lhmod(Ui)ii<n and N2 = mod(Un). Furthermore, since M is nonempty, it follows by Lemma 84 that both N1 and N2 are nonempty. So N1 is the minimal change update model of hUiii<n by Def. 85 and N2 is the MKNF model of Un by Lemma 87.

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

Proof Suppose J does not belong to I ⊕ N. If J does not belong to N, then since N is sequencesaturated relative to S, there is some **α < µ** such that J
[Sα] does not belong to N[Sα]. But then J
[Sα]also does not belong to I
[Sα] ⊕ N[Sα], so we reached the desired conclusion.

In the principal case, when J belongs to N, we know there exists some J
′ ∈ N such that J
′ <I J. This means that for every predicate symbol P ∈ P,
diff (**P, I, J**′) ⊆ diff (**P, I, J**) (D1)
and for some predicate symbol P0 ∈ P,
diff (P0**, I, J**′) ( diff (P0**, I, J**) . (D2)
Since S is a saturation sequence, there is a unique ordinal α such that P0 belongs to Sα. It follows from (D2) that diff (P0, I[Sα], J′[Sα]) = diff (P0**, I, J**′) ( diff (P0**, I, J**) = diff (P0, I[Sα], J[Sα])
Furthermore, for any predicate symbol P ∈ Sα it follows from (D1) that diff (P, I[Sα], J′[Sα]) = diff (**P, I, J**′) ⊆ diff (**P, I, J**) = diff (P, I[Sα], J[Sα]) .