Proposition 3 For any nondisjunctive program Π and any nonempty set X **of atoms that occur**
in Π, X is an elementary loop of Π iff all proper subsets of X **that are elementary**
loops of Π are outbound in X **for Π.**
The following proposition describes an important relationship between loop formulas of elementary loops and loop formulas of arbitrary sets of atoms.

Proposition 4 For any nondisjunctive program Π and any nonempty set Y **of atoms that occur**
in Π, there is an elementary loop Z of Π such that Z is a subset of Y and LF Π(Z)
entails LF Π(Y ).

Proposition 4 allows us to limit attention to loop formulas of elementary **loops**
only. This yields the following theorem, which is a reformulation of Theorem 3 from (Gebser and Schaub 2005).

Theorem 1 (d)
The following condition is equivalent to each of conditions (a)–(c) in Theorem 1:
(d) X satisfies LF Π(Y ) for all elementary loops Y **of Π.**
For instance, according to Theorem 1 (d), a model of Π1 **is stable iff it satisfies the**
first six loop formulas in (5); the loop formula of the non-elementary loop {**p, q, r**} (the last one in (5)) can be disregarded.

## 2.3 Elementarily Unfounded Sets For Nondisjunctive Programs

If we modify condition (c) in Theorem 1 by replacing "loops" in its statement with "maximal loops," the condition becomes weaker, and the modified **statement**
of Theorem 1 is incorrect. For instance, Π1 has only two maximal loops, {**p, q, r**}
and {s}, and their loop formulas are satisfied by a non-stable model {p, q, r}**. In**
fact, maximal loop {p, q, r} is not even an elementary loop of Π1**. Similarly, it is**
not sufficient to consider maximal elementary loops only. If we replace "elementary loops" in the statement of Theorem 1 (d) with "maximal elementary loops," then the modified statement is incorrect. For instance, the program

$\sum_{n\in\mathbb{N}}q_{n}n_{n}$
p ← q, **not p** q ← p, **not p** p ← .

has two models, {p} and {p, q}**, among which the latter is not stable. On the other** hand, the only maximal elementary loop of the program is {p, q}**, and its loop** formula p ∧ q → ⊤ **is satisfied by both models, so that this loop formula alone is**
not sufficient to refute the stability of {p, q}. (Model {p, q} **does not satisfy the loop**
formula of {q}, which is q → p ∧ ¬p.)
However, in the following we show that, if we consider the "relevant" **part of a**
program w.r.t. a given interpretation, it is sufficient to restrict attention to maximal elementary loops. For any nondisjunctive program Π and any set X of atoms, by