by (Πsh )X construction. It follows that |{a1, . . . , ak} ∩ X| ≤ **1. From the fact that** Y ⊆ X and Z ⊂ Y we conclude that |{a1, . . . , ak}∩Y | ≤ 1 and {a1**, . . . , a**k}∩Z = ∅,
so that {ai} ∩ Z = ∅.

For instance, for X = {p, q, r} and (Π3)sh , we have that [(Π3)sh ]X **consists of the**
last two rules in (54). Only the singletons {p}, {q}, and {r} **are elementary loops**
of [(Π3)sh ]X, and clearly they are elementary loops of Π3 **as well.**
We are now ready to show the equivalence between an HEF program and its shifted variant.

Theorem 5 For any HEF program Π and any set X of atoms, X **is a stable model of Π iff** X
is a stable model of Πsh .

Proof. *From left to right:* Assume that X is a stable model of Π. Then X **is a**
model of Πsh such that all its atoms occur in Πsh and also in [Πsh ]X**. Furthermore,**
by Theoremd 1 (d), we have that X satisfies LF Π(Y **) for all elementary loops** Y
of Π. By Proposition 8, the elementary loops of Π include all elementary loops Y
of [Πsh ]X that are contained in X, and, since Π is HEF, it holds that ES Πsh (Y **) and**
ES Π(Y ) as well as LF Πsh (Y ) and LF Π(Y **) are equivalent to each other. This implies**
that X satisfies ES Πsh (Y ) for all elementary loops Y of [Πsh ]X **that are contained**
in X, so that X contains no elementarily unfounded sets for Πsh w.r.t. X**. By**
Theoremd 1 (e′), we conclude that X **is a stable model of Π**sh .

From right to left: Assume that X is a stable model of Πsh . Then X **is a model**
of Π such that all its atoms occur in Π. Furthermore, by Theoremd **1 (d), we have**
that X satisfies LF Πsh (Y ) for all elementary loops Y of Πsh **. By Proposition 7,**
the elementary loops of Πsh include all elementary loops Y **of Π, and, since Π is**
HEF, it holds that ES Π(Y ) and ES Πsh (Y ) as well as LF Π(Y ) and LF Πsh (Y **) are** equivalent to each other. This implies that X satisfies LF Π(Y **) for all elementary**
loops Y of Π. By Theoremd 1 (d), we conclude that X **is a stable model of Π.**
For instance, one can check that both Π2 and (Π2)sh have {p} and {q} **as their**
stable models. It follows that HEF programs are not more expressive than nondisjunctive programs, so that one can regard the use of disjunctive **rules in such programs as a syntactic variant. Furthermore, the problem of deciding whether a model**
is stable for an HEF program is tractable, just as the same problem for a nondisjunctive program. (In the case of arbitrary disjunctive programs, it is coNP**-complete**
(Eiter and Gottlob 1995).) These properties were known for HCF programs, and here we extended them to HEF programs.

In Section 3.4, we defined the notion of an elementary subgraph of a set X of atoms for a disjunctive program Π. Theorem 3 still applies to HEF programs.

Theoremhef 3 For any HEF program Π and any nonempty set X of atoms that occur in Π, X **is an** elementary loop of Π iff the elementary subgraph of X **for Π is strongly connected.**
Proof. *From left to right:* Assume that X **is an elementary loop of Π, and, for**
the sake of contradiction, that the elementary subgraph of X for Π is not strongly