Proposition 6 For any nondisjunctive program Π and any set L of atoms, L **is a GS-elementary**
loop of Π iff L **is a nontrivial elementary loop of Π.**
Proof. *From left to right:* Assume that L **is a GS-elementary loop of Π. If** L is a singleton, it is a (nontrivial) elementary loop according to our definition. If L is not a singleton, we have that R
−
Π(L
′) ∩ R
+
Π(L) 6= ∅ **for any proper subset** L
′ of L
that is a nontrivial loop of Π. In other words, there is a rule (3) in Π such that

$$a_{1}\in L^{\prime},$$
$$\left(7\right)$$
$\left(\mathfrak{S}\right)_{\text{}}$
′, (7)
$$B\cap L^{\prime}=\varnothing,$$
′ = ∅, (8)
and

$B\cap(L\setminus L')\neq\emptyset$. 
′) 6= ∅. (9)
We thus have that L
′is outbound in L **for Π. Furthermore, for any trivial loop** {a1}
of Π contained in L, there must be a rule (3) in Π such that B ∩ (L \ {a1}) 6= ∅, as L cannot be a loop of Π otherwise. Since {a1} is trivial, B ∩ {a1} = ∅**, so that** {a1} is outbound in L for Π. By Proposition 3, it follows that L **is a (nontrivial)**
elementary loop of Π. From right to left: Assume that L **is a nontrivial elementary loop of Π. From the** definition of an elementary loop, it follows that any proper subset L
′ of L **that is a**
nontrivial loop of Π is outbound in L **for Π. That is, there is a rule (3) in Π such** that (7), (8), and (9) hold, so that L **is a GS-elementary loop of Π.**
For a nondisjunctive program Π and a set X of atoms, a loop L of ΠX **is a**
GS-elementary loop of ΠX iff L is a nontrivial elementary loop of ΠX **. Thus an**
active elementary loop **of Π according to (Gebser and Schaub 2005) is a nontrivial**
elementary loop of ΠX that is unfounded by Π w.r.t. X. Hence, any active elementary loop L of Π is an elementarily unfounded set for Π w.r.t. X**, while the converse**
does not hold in general if L **is a singleton.**
In fact, there are a few differences between Definition 1 and our definition of an elementary loop. First, our definition of an elementary loop does not a priori assume that its atoms form a loop. Rather, the fact that an elementary loop is a loop follows from its definition in view of Proposition 1. Second, the two **definitions**
do not agree on trivial loops: a trivial loop is an elementary loop, but not a GSelementary loop. This originates from the difference between the definition of a loop in (Lin and Zhao 2004) and its reformulation given in (Lee 2005). As shown in the main theorem from (Lee 2005), identifying a trivial loop as a loop admits a simpler reformulation of the Lin-Zhao theorem by allowing us to view completion formulas (Clark 1978) as a special case of loop formulas. Furthermore, the reformulated definition of an elementary loop enables us to identify a close relationship between maximal elementary loops (elementarily unfounded sets) and minimal **nonempty** unfounded sets.

Importantly, trivial loops allow us to extend the notion of an elementary loop to disjunctive programs without producing counterintuitive results. For instance,