Transition Systems for Model Generators - A Unifying Approach 21 Proposition 4 A set of literals M is a model of an SM(ASP) theory [F,Π] if and only if M
is a model of an SM(ASP) theory [F,Πo].

Proof Proceeding in each direction, we can assume that M is a complete (over At(F ∪ Π)) and consistent set of literals such that |M| = |At(F ∪Π)|. It follows that to prove the assertion it suffices to show that for every such set M, M+ is an input answer set of Π if and only if M+ is an input answer set of Πo.

We note that Πo = Π∪{a← not not a | a∈At(F∪Π)\*Head*(Π)}. Thus, M+ ⊆ *Head*(Π)
and so, by Proposition 3, M+ is an input answer set of Πoif and only if M+ is an answer set of Πo. It follows that to complete the argument, it suffices to show that under our assumptions about M, M+ is an answer set of Π ∪ (M+ \ *Head*(Π)) if and only if M+ is an answer set of Πo. This statement is evident once we observe that the reducts of Π∪(M+ \ *Head*(Π)) and Πo with respect to M+ are equal (they are both equal to ΠM+∪
(M+ \ *Head*(Π))).

Proposition 5 For any SM(ASP) theory [F,Π] that is Π-safe, a set X of atoms is an answer set of Π if and only if X = M+ ∩At(Π), for some model M of [F,Π].

Proof
(⇒) Let X be an answer set of Π. Since [F,Π] is Π-safe, there is a model M of F such that X = M+ ∩ *Head*(Π). Moreover, again by the Π-safety of [F,Π], {¬a | a ∈ OΠ} ⊆ M. It follows that X = M+ ∩At(Π) and (M+ \*Head*(Π))∩At(Π) = /0. By Proposition 3(b), M+
is an input answer set of Π.

(⇐) Let X = M+ ∩At(Π), where M is a model of [F,Π]. It follows that M is a model of F. By the Π-safety of [F,Π], we have {¬a | a ∈ OΠ} ⊆ M. As above, it follows that (M+ \
Head(Π))∩At(Π) = /0. Since M+ is an input answer set of Π, Proposition 3(b) implies that M+ ∩*Head*(Π) is an answer set of Π. From the identity (M+ \*Head*(Π))∩At(Π) = /0, it follows that M+ ∩*Head*(Π) = M+ ∩At(Π). Thus, X is an answer set of Π.

Corollary 1 follows immediately from Proposition 5. We omit its proof and move on to Proposition 6. We start by proving two simple auxiliary results. Lemma 4 For a logic program Π, and a consistent and complete set M of literals over At(Π), if M = WΠ(M), then M is a model of Π.

Proof It is sufficient to show that for every rule a ← B ∈ Π if s(B) ⊆ M then a ∈ M. This follows from the definition of the operator WΠ and the fact that M = WΠ(M).

Lemma 5 For a logic program Π and a consistent and complete set M of literals over At(Π), if M =
WΠ(M) then M+ does not have any non-empty subset that is unfounded on M with respect to Π.