From (74) and (75), we conclude that (71) does not hold. Furthermore, since Z ⊆ RωΠ,X(Y **), (72) implies that (70) does not hold. Hence, (69) must hold, which,**
in combination with (73), gives us that |A ∩ Z| > 1 .

But since Z **is an elementary loop of Π, this contradicts that Π is HEF.**
We are now ready to generalize Proposition 15 to HEF programs.

Theorem 7 For any HEF program Π and any set X of atoms that occur in Π, X **contains no**
nonempty unfounded sets for Π w.r.t. X iff RωΠ,X(X) = ∅.

Proof**. From left to right follows immediately from Proposition 16.**
From right to left follows immediately from Proposition 14.

Regarding the models of HEF programs, we derive the following corollary.

Corollary 2 For any HEF program Π and any set X of atoms that occur in Π, X **is a stable**
model of Π iff X is a model of Π such that RωΠ,X(X) = ∅.

Proof. Both directions follow immediately from Theoremd 1 (b′**) and Theorem 7.**
For instance, reconsider Π2 **from Section 4, which is HEF, but not HCF. Hence,**
Corollary 2 applies, but Proposition 15 does not apply. Indeed, since RωΠ2,X(X) = X
for (non-stable) model X = {p, q, r} of Π2**, Corollary 2 allows us to conclude that** X is not a stable model of Π2. On the other hand, for model {p} of Π2**, we have**
that RωΠ2,{p}
({p}) = ∅, which implies that {p} **is a stable model of Π**2.

In Section 3.3, we defined the notion of an elementarily unfounded set and showed that it coincides with a minimal nonempty unfounded set. Thus stability checking can be cast into the problem of ensuring the absence of elementarily **unfounded sets.** Since every elementarily unfounded set is a loop, it is clearly contained **in a maximal**
loop, which allows us to modularize the consideration of (elementarily) **unfounded**
sets. The idea of using maximal loops for partitioning a program and confining stability checking to subprograms was already exploited by Leone *et al.* **(1997) and**
Koch *et al.* (2003). In fact, for a disjunctive program Π and a set X **of atoms, Leone** et al. (1997) showed how stability can be checked separately for maximal **loops of Π,** and Koch *et al.* **(2003) developed this idea further by considering maximal loops**
of the smaller program ΠX,RωΠ,X(X)**. We below describe a notion called "bounding**
loops," which go beyond such maximal loops.

For a disjunctive program Π and a set X **of atoms, we say that a subset** Y of X is a *bounding loop* of Π w.r.t. X if Y is maximal among all subsets Z of X **such that**
Z is a loop of ΠX,Z and RωΠ,X(Z) = Z**. Note that there are two crucial differences**
between bounding loops and elementarily unfounded sets. First, a bounding loop Y
of Π w.r.t. X is not necessarily an elementary loop of ΠX,Y **. Next, it does not**
need to be unfounded by Π w.r.t. X. To see this, observe that X = {p, q, r} is a