1. all R ∈ C are decreasing w.r.t. π; 2. all R ∈ C are almost never increasing w.r.t. π and C does not contain any odd-cycles.

As we anticipated, the existence of recursion patterns implies bounds on recursion depth and odd-cycle freedom.

Lemma 4.3 If a program P has a recursion pattern then all paths in DGa(P) contain finitely many different atoms.2 Lemma 4.4 If a normal program P has a recursion pattern then DGa(P) is odd-cycle-free.

Example 4.5 Consider the classical program for appending lists:
append([ ], L, L). append([X|Xs], L, [X|Ys]) ← append(Xs**, L, Y**s).

Let µ be a selection index mapping for this program. If µappend = {1} then µ is a recursion pattern; indeed, the first rule is vacuously decreasing because it has an empty body, and the second rule is decreasing because the selected argument is decreasing: Xs ≺ [X|Xs]. Similarly, if µappend = {3} then µ is a recursion pattern. On the contrary µappend = {2} does not yield a recursion pattern; we have L - L, but µappend is not complete. Finally, µappend = {1, 2, 3} yields a recursion pattern (both rules are decreasing w.r.t. µ).

## 5 Acyclic Derivations, Supports, And Stable Models

By analogy with the theory of finitary programs, a query G over an FP2 program P is answered by computing in a top-down fashion a representative, partially evaluated fragment of Ground(P) that suffices to answer G. FP2 programs will be defined so that such topdown computations are finite and finitely many, therefore a complete enumeration thereof is possible. Note that Lemma 4.3 is not enough for this purpose for two reasons. First, a loop-checking mechanism should be set up to avoid infinite cyclic derivations. Second, there could still be infinitely many bounded, acyclic derivations (a situation that commonly arises in the presence of local variables, that make DGp(P) infinitely branching). We shall constrain queries and rule bodies to be *call safe* (see below) so that the selected, almost never increasing arguments of each predicate are bound whenever the predicate is called; we shall prove that, as a consequence, every subgoal yields finitely many answer substitutions that are all grounding. In this section, we set up the technical machinery for the acyclic top-down computations which is based on annotating each goal with the history of previously resolved atoms in order to check for loops.