(0) Obligation:

Clauses:

q(X) :- ','(not_zero(X), ','(p(X, Y), q(Y))).
p(0, 0).
p(s(X), X).
zero(0).
not_zero(X) :- ','(zero(X), ','(!, failure(a))).
not_zero(X1).
failure(b).

Query: q(g)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(s(z0)) → U1(f2_in(z0), s(z0))
U1(f2_out1, s(z0)) → f2_out1
Tuples:

F2_IN(s(z0)) → c(U1'(f2_in(z0), s(z0)), F2_IN(z0))
S tuples:

F2_IN(s(z0)) → c(U1'(f2_in(z0), s(z0)), F2_IN(z0))
K tuples:none
Defined Rule Symbols:

f2_in, U1

Defined Pair Symbols:

F2_IN

Compound Symbols:

c

(3) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(s(z0)) → U1(f2_in(z0), s(z0))
U1(f2_out1, s(z0)) → f2_out1
Tuples:

F2_IN(s(z0)) → c(F2_IN(z0))
S tuples:

F2_IN(s(z0)) → c(F2_IN(z0))
K tuples:none
Defined Rule Symbols:

f2_in, U1

Defined Pair Symbols:

F2_IN

Compound Symbols:

c

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F2_IN(s(z0)) → c(F2_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:

F2_IN(s(z0)) → c(F2_IN(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F2_IN(x1)) = x1   
POL(c(x1)) = x1   
POL(s(x1)) = [1] + x1   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(s(z0)) → U1(f2_in(z0), s(z0))
U1(f2_out1, s(z0)) → f2_out1
Tuples:

F2_IN(s(z0)) → c(F2_IN(z0))
S tuples:none
K tuples:

F2_IN(s(z0)) → c(F2_IN(z0))
Defined Rule Symbols:

f2_in, U1

Defined Pair Symbols:

F2_IN

Compound Symbols:

c

(7) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(8) BOUNDS(O(1), O(1))

(9) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(s(z0)) → U1(f1_in(z0), s(z0))
U1(f1_out1, s(z0)) → f1_out1
Tuples:

F1_IN(s(z0)) → c(U1'(f1_in(z0), s(z0)), F1_IN(z0))
S tuples:

F1_IN(s(z0)) → c(U1'(f1_in(z0), s(z0)), F1_IN(z0))
K tuples:none
Defined Rule Symbols:

f1_in, U1

Defined Pair Symbols:

F1_IN

Compound Symbols:

c

(11) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(s(z0)) → U1(f1_in(z0), s(z0))
U1(f1_out1, s(z0)) → f1_out1
Tuples:

F1_IN(s(z0)) → c(F1_IN(z0))
S tuples:

F1_IN(s(z0)) → c(F1_IN(z0))
K tuples:none
Defined Rule Symbols:

f1_in, U1

Defined Pair Symbols:

F1_IN

Compound Symbols:

c

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F1_IN(s(z0)) → c(F1_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:

F1_IN(s(z0)) → c(F1_IN(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F1_IN(x1)) = x1   
POL(c(x1)) = x1   
POL(s(x1)) = [1] + x1   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(s(z0)) → U1(f1_in(z0), s(z0))
U1(f1_out1, s(z0)) → f1_out1
Tuples:

F1_IN(s(z0)) → c(F1_IN(z0))
S tuples:none
K tuples:

F1_IN(s(z0)) → c(F1_IN(z0))
Defined Rule Symbols:

f1_in, U1

Defined Pair Symbols:

F1_IN

Compound Symbols:

c