and it satisfies all decision literals in M′, then N satisfies l (by the assumption) and N
satisfies every decision literal in M. By the induction hypothesis, the latter implies that N |= M. Thus, N |= M′.

Fail: If this rule is applicable, M has no decision literals and is inconsistent. If [F,Π] has a model N, then by the induction hypothesis, N |= M, a contradiction. It follows that [F,Π]
has no models and the assertion is trivially true.

Backtrack: If this rule is applied, it follows that M has the form Pld i Q, where Q contains no decision literals, and M′ = Pli. Let N be a model of [F,Π] such that N satisfies all decision literals in Pli. It follows that N satisfies all decision literals in P and so, by the induction hypothesis, N |= P. Let us assume that N |=li. Then, N satisfies all decision literals in M and, consequently, N |= M, a contradiction as M is inconsistent. Thus, N |= li and so, N |= M′.

Unfounded: If M′is obtained from M by an application of the *Unfounded* rule, then M is consistent and M′ = M¬a, for some a ∈ U, where U is an unfounded set on M with respect to Πo. Let N be any model N of [F,Π] such that N satisfies all decision literals in M′. It follows that N satisfies all decision literals in M and so, by the inductive hypothesis, N |=
M. By the definition of a model of [F,Π], N
+ is an input answer set of Π. Consequently, N
+ is an answer set of Π∪(N
+ \ *Head*(Π)). Arguing as as before, we obtain that N
+ is an answer set of Πo. By Lemma 6, a ∈/ N
+, that is, N |= ¬a.

## Proposition 7 For Any Sm(Asp) Theory [F,Π],

(a) graph SM(ASP)F,Π is finite and acyclic,
(b) for any terminal state M of SM(ASP)F,Π *other than FailState, M is a model of* [F,Π]
(c) FailState is reachable from /0 in SM(ASP)F,Π if and only if [F,Π] *has no models.*
Proof Parts (a) and (c) are proved as in the proof of Proposition 1 (Lierler 2011, Proposition 1)
using Lemma 8.

(b) Let M be a terminal state. It follows that none of the rules are applicable. From the fact that *Decide* is not applicable, we derive that M assigns all literals. Since neither *Backtrack* nor *Fail* are applicable, M is consistent. Since *Unit Propagate* is not applicable, it follows that for every clause C ∨a ∈ F ∪Πcl if C ⊆ M then a ∈ M. Consequently, if M |= C then M |= a. Thus, M is a model of F ∪Πcl. Consequently, M is a model of F.

Next, we show that M+ is an input answer set of Π, that is, that M+ is an answer set of Π ∪(M+ \ *Head*(Π)). To this end, it is sufficient to show that M+ is an answer set of Πo
(we again exploit here the fact that M+ is an answer set of Π∪(M+ \*Head*(Π)) if and only if M+ is an answer set of Πo). Since M is a model of F ∪Πcl, M is a model of Πo.

Let us assume that M+ is not an answer set of Πo. By Theorem on Unfounded Sets, it follows that there is a non-empty unfounded set U on M with respect to Πosuch that U ⊆ M+. Then *Unfounded* can be applied for some a ∈ U. If ¬a ∈/ M, M is not terminal, a contradiction. Thus, ¬a ∈ M. Since M is consistent, a ∈/ M+, a contradiction (as U ⊆ M+).

It follows that M+ is an answer set of Πo, as required.

Finally, we sketch a proof for Proposition 8 Proposition 8 For every program Π*, the graphs* SM−
Π
and SM(ASP)
−Comp(Π),Π are equal.