The Main Theorem in (Lee 2005) implies the following property loop formulas. In its statement we refer to the concept of a program entailing a formula. The notion is defined as follows. A program Π entails a formula F (over the set of atoms in Π) if for every interpretation M (over the set of atoms in Π) such that M+ is an answer set of Π, M is a model of F. Lemma 10 *(Lemma on Loop Formulas*)
For every program Π and every set Y of atoms, Y ⊆ At(Π), Π entails the loop formula (6)
for Y.

For an SM(ASP) theory [F,Π] and a list PlQ of literals, we say that a clause C ∨l is a reason for l to be in PlQ with respect to [F,Π] if 1. P |= ¬C, and 2. F,Πo|= C∨l.

Lemma 11 Let [F,Π] be an SM(ASP) theory. For every state M||Γ reachable from /0||/0 in the graph SML(ASP)F,Π, every literal l in M is either a decision literal or has a reason to be in M with respect to [F,Π].

## Proof

We proceed by induction on the length of a path from /0||/0 to M||Γ in the graph SML(ASP)F,Π.

Since the property trivially holds in the initial state /0||/0, we only need to prove that every transition rule of SML(ASP)F,Π preserves it.

Let us consider an edge M||Γ =⇒ M′||Γ
′, where M is a sequence l1 ... lk such that every li, 1 ≤ i ≤ k, is either a decision literal or has a reason to be in M with respect to [F,Π].

It is evident that transition rules Backjump, Decide, *Learn*, and *Fail* preserve the property (the last one trivially, as *FailState* contains no literals).

Unit Propagate Learn: The edge M||Γ =⇒ M′||Γ
′is justified by the rule Unit Propagate Learn. That is, there is a clause C∨l ∈ F ∪Πcl ∪Γ such that C ⊆ M and M′ = Ml. By the inductive hypothesis, the property holds for every literal in M. We now show that a clause C∨l is a reason for l to be in Ml. By the applicability conditions of *Unit Propagate Learn*,
C ⊆ M. Consequently, M |= C. It remains to show that F,Πo|= C∨l.

Case 1. C∨l ∈ F. Then, clearly, F |= C∨l and, consequently, F,Πo|= C∨l. Case 2. C ∨ l ∈ Πcl. Since Πcl ⊆ (Πo)
cl, C ∨ l ∈ (Πo)
cl. Let M be a model of [F,Πo].

It follows that M+ is an answer set of Πo. Thus, M |= (Πo)
cl and so, M |= C ∨l. Thus, F,Πo|= C∨l.

Case 3. C ∨l ∈ Γ. We recall that F,Πo|= Γ by the definition of an augmented state. Consequently, F,Πo|= C∨l.

Unfounded: We have that M is consistent, and that there is an unfounded set U on M with respect to Πoand a ∈ U such that M′ = M¬a. By the inductive hypothesis, the property holds for every literal in M. We need to show that ¬a has a reason to be in M¬a with respect to [F,Π].

Let B ∈ *Bodies*(Πo,U) be such that U ∩ B
pos = /0. By the definition of an unfounded