Finally, we are left to prove the theorem for "non homogeneous" goals where the atoms with maximum height among A1**, . . . , A**k may belong to different strongly connected components. The proof is by induction on k; the induction step relies on Lemma 5.3. ✷
Corollary 5.10 Let P be a program with a recursion pattern π and G0 be an a-goal. Assume that P and G0 are call-safe w.r.t. π. Then G0 has finitely many acyclic a-derivations from P. Moreover, they are all finite.

## 5.3 Acyclic Supports And Stable Models

It is well-known that the stable models of a program P are completely characterized by the supports of P's ground atoms. In our setting, a *support* for an a-goal G with answer substitution θ is a set of negative literals {L1**, . . . , L**n} such that G has a successful aderivation from Ground(P) with answer substitution θ and last goal L1α1**, . . . , L**nαn. A
support for an atom A is a support for the a-goal Aε. The set of (negative) literals occurring in the last a-goal of a successful a-derivation ∆ is called the *support of* ∆. By *acyclic* support we mean a support generated by an acyclic derivation. The first result tells that by adopting acyclic a-derivations, only redundant supports can be lost:
Theorem 5.11 *(Completeness of acyclic derivations w.r.t. supports*)
If G0 has a successful a-derivation ∆ from P with global answer θ, then G0 has a successful acyclic a-derivation ∆afrom P with global answer θ asuch that θ ais more general than θ and the support of ∆ais more general than a subset of the support of ∆.

A-derivations and the related notion of support are in close correspondence with the Pproofs of (Marek and Remmel 2008) and the corresponding supports. By exploiting these relationships and the previous lemma, one can easily prove the following characterization of stable models in terms of the supports of acyclic a-derivations.

Theorem 5.12 Let P be a normal program. A set M of ground atoms is a stable model of P iff M is the set of all ground atoms that have a ground acyclic support in Ground(P) satisfied by M.

## 6 The Class Fp2

We are finally ready to introduce the class of FP2 programs. If π and τ are two selection index mappings, we say that τ *contains* π (in symbols, τ ⊇ π) iff, for each predicate symbol p, it holds that τp ⊇ πp.

Definition 6.1 *(Call patterns*)
A selection index mapping τ for a normal program P is a *call pattern* for P iff (i) τ contains a recursion pattern of P, and (ii) for each rule R ∈ P there exists a permutation L1, L2**, ..., L**n of body(R) such that head(R) ← L1, L2**, ..., L**n is call-safe w.r.t. τ.

Definition 6.2 (FP2)
A normal logic program belongs to the class FP2 iff it has a call pattern.