Lemma 5.2 *(Decomposition 1*)
∆ is an embedded a-derivation of G0 from P with degree 1 iff either (i) G0 is failed and
∆ = G0, or (ii) G0 has an annotated resolvent G1 with rule R and mgu θ, and ∆ = G0 ·∆′,
where ∆′is an embedded a-derivation of G1 with degree k and k is the number of positive literals in the body of Rθ.

Given two a-derivations ∆ = G0**, . . . , G**m and ∆′ = G′0
, . . . , G′n such that Gm = G′0
,
the *join* of ∆ and ∆′is G0, . . . , Gm, G′1
, . . . , G′n
.

Lemma 5.3 *(Decomposition 2*)
∆ is an embedded a-derivation of G0 from P with degree k iff either (i) ∆ is the join of an embedded a-derivation ∆′ of G0 from P with degree 1 and an embedded a-derivation of Gn from P with degree k − 1, where Gn is the last a-goal of ∆′; or (ii) ∆ is an infinite embedded a-derivation for G0 of degree 1.

## 5.2 Finiteness And Groundness Properties Of Call-Safe, Acyclic A-Derivations

The good finiteness and termination properties we need acyclic derivations to enjoy in order to prove the termination of our algorithms can be enforced by a "call safeness" property that ensures that the arguments selected by recursion pattern are always bound when a predicate is called. Definition 5.4 (*Call-safeness*)
An a-goal L1α1**, ..., L**nαn is *call-safe* w.r.t. a selection index mapping µ iff for all variables X occurring in some Li[µ] or in a negative literal Li (1 ≤ i ≤ n), X occurs also in a positive literal Lj, with 1 ≤ **j < i**. Similarly, a rule R : A ← L1, L2**, ..., L**n is *call-safe* w.r.t. µ iff for each variable X occurring in R, some of the following conditions hold:
1. X occurs in A[µ];
2. X occurs in body(R); moreover, if X occurs in Li[µ] or in a negative literal Li, for some i = 1**, . . . , n**, then X occurs also in a positive literal Lj , with 1 ≤ **j < i**.

Finally, a program P is *call-safe* w.r.t. µ iff for all R ∈ P, R is call-safe w.r.t. µ.

Example 5.5 Consider the following program for reversing a list:
reverse([ ], **[ ])**. reverse([X|Y ], Z) ← reverse(**Y, W**), append(W, [X], Z).

The first rule is trivially call safe w.r.t. any selection index mapping. If µreverse = {1} and µappend = {1} then the second rule is call-safe w.r.t. µ. To see this, note that: (i) X
and Y satisfy condition (1); (ii) Z satisfies (2) because it occurs in the body but not in any selected argument nor in any negative literal; (iii) W, the selected argument of the second subgoal, satisfies condition (2) because it occurs also in the first subgoal.

If both P and G are call-safe, then call-safeness is preserved along all the steps of a derivation: