Transition Systems for Model Generators - A Unifying Approach 23 set of Πo. it follows that a ∈/ M+. By the completeness of M, ¬a ∈ M. Thus, WoΠ
(M) ⊆ M
and, consequently, WΠo (MO
Π) ⊆ M. By iterating, we obtain that W
fix Πo (MO
Π) ⊆ M. Since
(F,Π) is total, W
fix Πo (MO
Π) = M. Thus, (a) follows.

(b)⇔(c) It is sufficient to show that M is a model of F if and only if M is a model of Comp(Πo) ∪ F given that M+ is an input answer set of Π or, equivalently, that M+ is an answer set of Π ∪ M+ \ *Head*(Π). The "if" part is obvious. For the "only if" part, we proceed as follows. First, reasoning as above we observe that M+ is an answer set of Πo.

Thus, M is the model of the completion *Comp*(Πo) and so, M is a model of *Comp*(Πo)∪F,
which we needed to show.

(b)⇔(d) The equivalence follows from the fact that *ED-Comp*(ΠAt(Π)) is a conservative extension of *Comp*(ΠAt(Π)).

We now proceed to the proof of Proposition 7. We first recall a result proved by Lierler
(2011) (using a slightly modified notation)..

Lemma 6 (*Lemma 4 (Lierler 2011)*)
For any unfounded set U on a consistent set M of literals with respect to a program Π, and any assignment N, if N |= M and N ∩U 6= /0, then N
+ is not an answer set for Π.

It is well known that for any consistent and complete set M of literals over At(Π) (assignment on At(Π)), if M+ is an answer set for a program Π, then M is a model of Πcl.

The property has a counterpart for SM(ASP) theories. The proof is straightforward and we omit it. Lemma 7 For every SM(ASP) theory [F,Π], if M is a model of [F,Π], then M is a model of F ∪Πcl.

Next, we prove the following auxiliary result.

Lemma 8 For every SM(ASP) theory [F,Π], every state M other than *FailState* reachable from /0 in SM(ASP)F,Π, and every model N of [F,Π], if N satisfies all decision literals in M, then N
satisfies M.

Proof We proceed by induction on n = |M|. The property trivially holds for n = 0. Let us assume that the property holds for all states with k
′ ≤ k elements that are reachable from /0. For the inductive step, let us consider a state M = l1 ... lk such that every model N of [F,Π] that satisfies all decision literals lj with j ≤ j satisfies M. We need to prove that applying any transition rule of SM(ASP)F,Π in the state l1 ... lk, leads to a state M′ = l1 ... lk, lk+1 such that if N is a model of [F,Π] and N satisfies every decision literal lj with j ≤ k +1, then N
satisfies M′.

Unit Propagate: By the definition of *Unit Propagate*, there is a clause C∨l ∈ F ∪Πcl such that C ⊆ M and M′ = Ml. Let N be any model of [F,Π] that satisfies all decision literals lj ∈ Ml. It follows that N satisfies all decision literals in M. By the induction hypothesis, N |= M. Since N |= C∨l and C ⊆ M, Lemma 7 implies that N |= l.

Decide: In this case, M′ = Mld(l is a decision literal). If N is a model of the theory [F,Π]