stability of a model by loop formulas, is a part of the main theorem from (Lee 2005) for the nondisjunctive case.

## Theorem 1 (**(Lee 2005)**)

For any nondisjunctive program Π and any set X **of atoms that occur in Π, if** X is a model of Π, then the following conditions are equivalent:
(a) X **is a stable model of Π;**
(b) X satisfies LF Π(Y ) for all nonempty sets Y **of atoms that occur in Π;**
(c) X satisfies LF Π(Y ) for all loops Y **of Π.**
According to the equivalence between conditions (a) and (b) in Theorem 1, a model of Π1 **is stable iff it satisfies the loop formulas of all fifteen nonempty sets**
of atoms formed from the atoms occurring in Π1**. On the other hand, condition (c)**
tells us that it is sufficient to restrict attention to the following loop formulas of the seven loops of Π1:
p → ¬s ∨ r q → r

$$\begin{array}{l}r\to p\wedge q\\ s\to\bot\\ p\wedge r\to\neg s\\ q\wedge r\to\bot\\ p\wedge q\wedge r\to\neg s\ .\end{array}\tag{5}$$
$\mathbf{a}$
Program Π1 has six models: {p}, {s}, {p, s}, {q, s}, {p, q, r}, and {p, q, r, s}**. Among** them, {p} is the only stable model of Π1, which is also the only model of Π1 **that**
satisfies all loop formulas in (5).

As noted in (Lee 2005), the equivalence between conditions (a) and **(c) is a reformulation of the theorem by Lin and Zhao; the equivalence between conditions (a)**
and (b) is a reformulation of Corollary 2 from (Sacc´a and Zaniolo 1990) and Theorem 4.6 from (Leone et al. 1997) (in the nondisjunctive case), which characterizes the stability of a model in terms of unfounded sets. For any sets X, Y **of atoms,** we say that Y is *unfounded* by Π w.r.t. X if Y **is not externally supported by Π**
w.r.t. X**. Condition (b) can be stated in terms of unfounded sets as follows:**
(b′) X **contains no nonempty unfounded sets for Π w.r.t.** X.

## 2.2 Elementary Loops Of Nondisjunctive Programs

Gebser and Schaub (2005) showed that Y in LF Π(Y **) in Theorem 1 can be restricted**
to "elementary" loops only. In this section, we present a reformulation of their definition of an elementary loop and investigate its properties. We compare our reformulation with the original definition by Gebser and Schaub in Section 2.5.

To begin with, the following proposition tells us that a loop can be defined without mentioning a dependency graph.