Proof Let us assume that U is a non-empty subset of M+ that is unfounded on M with respect to Π. It follows that U ⊆ M. Since U 6= /0, M is inconsistent, a contradiction.

Next, we recall the following generalization of a well-known characterization of answer sets in terms of unfounded sets due to Leone et al. (1997). The generalization extended the characterization to the case of programs with double negation. Theorem on Unfounded Sets(Lee 2005)
For a set M of literals, M+ is an answer set of a program Π if and only if M is a model of Π and M+ does not have any non-empty subset that is unfounded on M with respect to Π.

Proposition 6 For a total PC(ID) theory (F,Π) *and a set M of literals over the set At*(F∪ Π) of atoms, the following conditions are equivalent:
(a) M is a model of (F,Π)
(b) M is a model of an SM(ASP) theory [F,Π]
(c) M is a model of an SM(ASP) theory [*Comp*(ΠAt(Π))∪F,Π]
(d) for some model M′ of an SM(ASP) theory [ED-Comp(ΠAt(Π))∪F,Π], M = M′ ∩
At(F ∩Π).

Proof
(a)⇒(b) It is sufficient to show that M+ is an input answer set of Π, that is, an answer set of Π∪(M+ \*Head*(Π)). Since M is a model of the PC(ID) theory (F,Π), M is a complete and consistent set of literals over At(F ∪ Π) and M = W
fix Πo (MOΠ). It follows that M =
WΠo (M). Since At(Πo) = At(F ∪ Π), by Lemma 4 it follows that M is a model of Πo.

Consequently, M is a model of Π∪(M+ \*Head*(Π)). By Theorem on Unfounded Sets, it is sufficient to show that M+ does not have any non-empty subset that is unfounded on M with respect to Π∪(M+ \*Head*(Π)). For a contradiction, let us assume that there is a nonempty set U ⊆ M+ that is unfounded on M with respect to Π ∪(M+ \ *Head*(Π)). Let a ∈ U. It follows that a ∈ M+. If a ∈/ *Head*(Π), then a is a fact in Π ∪(M+ \ *Head*(Π)). This is a contradiction with the unfoundedness of U. Thus, a ∈ *Head*(Π). By the definition of Πo, Bodies(Πo,a) = *Bodies*(Π,a). It follows that for every B ∈ *Bodies*(Πo,a), s(B)∩ M 6= /0 or U ∩B
+ 6= /0. This shows that U is unfounded on M with respect to Πo. This contradicts Lemma 5.

(a)⇐(b) Since M is a model of [F,Π], M is a complete and consistent set of literals over At(F ∪Π). By the assumption, M+ is an answer set of Π′ = Π ∪(M+ \ *Head*(Π)). Since Π′and Π have the same reducts with respect to M+, M+ is an answer set of Πo.

Since MOΠ⊆ M, WΠo (MOΠ) ⊆ WoΠ
(M). Let l ∈ WoΠ
(M). If l = a, where a is an atom in Πo, then there is a rule a ← B in Πosuch that s(B) ⊆ M. Since M is a model of Πo(it is so since M+ is an answer set of Πo), a ∈ M. If l = ¬a, then a ∈ GUS(M,Πo).

Let us assume that a ∈ M+ and let us define U = M+ ∩GUS(M,Πo). Clearly, U 6= /0 and U ⊆ GUS(M,Πo). Let b ∈ U and let B ∈ *Bodies*(Πo,b). Let us assume that s(B)M =
/0. By the completeness of M, s(B) ⊆ M. Since b ∈ GUS(M,Πo), there is an element GUS(M,Πo)∩B
+ 6= /0. Let us assume that c ∈ GUS(M,Πo)∩B
+. It follows that c ∈ M+
and so, c ∈ U. Thus, U is a nonempty set contained in M+ and unfounded on M with respect to Πo. By Theorem on Unfounded Sets, this contradicts the fact that M+ is an answer