Lemma 5.6 Let P be a normal logic program and G an a-goal. If P and G are call-safe w.r.t. a selection index mapping µ, then all resolvents of G and a rule R ∈ P are call-safe w.r.t. µ, too.

Proof. Let G′ be an annotated resolvent of the first positive a-literal Lα in G and a rule R = A ← L1**, ..., L**k in P with a substitution θ = mgu(**L, A**). Since G is call-safe, L[µ] is ground, and so must be Aθ[µ]. It follows - since P is call-safe - that the a-goal L1(L · α)**, ..., L**k(L · α) must be call-safe w.r.t. µ. Then G′is call-safe w.r.t. µ, too. ✷
Furthermore, the binding propagation schema imposed by call-safeness ensures that global answers are grounding:

## Lemma 5.7

Let P be a normal logic program and G0 an a-goal. Assume that P and G0 are call-safe w.r.t. a selection index mapping µ. If G0 has a successful a-derivation ∆ = G0**, ..., G**n from P with global answer θ, then for all i = 0**, ..., n**, the a-goal Giθ is ground.

Proof. By induction on the length of ∆.

Base case (the length of ∆ **is 0):** Let ∆ = G0. Since G0 is call-safe, all its a-literals have to be negative and ground. Then, G0θ is ground.

Inductive step (the length of ∆ is n + 1): Let ∆ = G0, G1**, ..., G**n+1. By Lemma 5.6, G1 is call-safe w.r.t. µ. Moreover, ∆′ = G1**, ..., G**n+1 is a successful a-derivation of length n for G1 with global answer θ
′ more general than θ. By inductive hypohesis, for all i = 1, ..., n + 1, the a-goal Giθ
′
is ground. Since G1 is a resolvent of G0 and both goals are call-safe, all variables in G0θ must be also in G1θ
′
. Consequently, G0θ is ground. ✷

The proof of the main theorem - that we need to prove the termination of our reasoning algorithm - will be based on inductions over the three indices defined below.

Let the height of a predicate q be the cardinality of the set of predicates reachable from q in DGp(P). The *height* of an atom A is the height of pred(A). Note that (i) height(A) ≥ 1;
(ii) if pred(A) depends on pred(A′) but not viceversa, then height(A) > height(A′); (iii)
if pred(A) and pred(A′) belong to the same strongly connected component of DGp(P),
then height(A) = height(A′). By convention, the height of a negative literal is 0.

Let π be a recursion pattern for P, and A be an atom such that A[π] is ground. The call size of A is |A[π]| (the norm of A[π]).

For the strongly connected components C of DGp(P) in which the call size does not decrease during recursion, we adopt a "loop saturation" index. Let a C*-atom* be an atom A with pred(A) ∈ C. Given a ground C-atom A, let maxA be the number of ground Catoms B such that A depends on B. Such an integer maxA exists due to the following lemma (that shows why π should be complete over such C):

## Lemma 5.8

Let P be a program with a recursion pattern π and C be a strongly connected component of DGp(P) s.t. π is complete for predicates in C. Every ground C-atom A depends on finitely many C-atoms in P.