(0) Obligation:

Clauses:

p(val_i, val_j).
map(.(X, Xs), .(Y, Ys)) :- ','(p(X, Y), map(Xs, Ys)).
map([], []).

Query: map(g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

p(val_i, val_j).
map([], []).
map(.(X, Xs), .(Y, Ys)) :- ','(p(X, Y), map(Xs, Ys)).

Query: map(g,a)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1([])
f1_in(.(val_i, z0)) → U1(f1_in(z0), .(val_i, z0))
U1(f1_out1(z0), .(val_i, z1)) → f1_out1(.(val_j, z0))
Tuples:

F1_IN(.(val_i, z0)) → c1(U1'(f1_in(z0), .(val_i, z0)), F1_IN(z0))
S tuples:

F1_IN(.(val_i, z0)) → c1(U1'(f1_in(z0), .(val_i, z0)), F1_IN(z0))
K tuples:none
Defined Rule Symbols:

f1_in, U1

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1

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

Removed 1 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1([])
f1_in(.(val_i, z0)) → U1(f1_in(z0), .(val_i, z0))
U1(f1_out1(z0), .(val_i, z1)) → f1_out1(.(val_j, z0))
Tuples:

F1_IN(.(val_i, z0)) → c1(F1_IN(z0))
S tuples:

F1_IN(.(val_i, z0)) → c1(F1_IN(z0))
K tuples:none
Defined Rule Symbols:

f1_in, U1

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1

(7) 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(.(val_i, z0)) → c1(F1_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:

F1_IN(.(val_i, z0)) → c1(F1_IN(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [1] + x2   
POL(F1_IN(x1)) = x1   
POL(c1(x1)) = x1   
POL(val_i) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1([])
f1_in(.(val_i, z0)) → U1(f1_in(z0), .(val_i, z0))
U1(f1_out1(z0), .(val_i, z1)) → f1_out1(.(val_j, z0))
Tuples:

F1_IN(.(val_i, z0)) → c1(F1_IN(z0))
S tuples:none
K tuples:

F1_IN(.(val_i, z0)) → c1(F1_IN(z0))
Defined Rule Symbols:

f1_in, U1

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1

(9) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(10) BOUNDS(O(1), O(1))

(11) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1([])
f2_in(.(val_i, z0)) → U1(f2_in(z0), .(val_i, z0))
U1(f2_out1(z0), .(val_i, z1)) → f2_out1(.(val_j, z0))
Tuples:

F2_IN(.(val_i, z0)) → c1(U1'(f2_in(z0), .(val_i, z0)), F2_IN(z0))
S tuples:

F2_IN(.(val_i, z0)) → c1(U1'(f2_in(z0), .(val_i, z0)), F2_IN(z0))
K tuples:none
Defined Rule Symbols:

f2_in, U1

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1

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

Removed 1 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1([])
f2_in(.(val_i, z0)) → U1(f2_in(z0), .(val_i, z0))
U1(f2_out1(z0), .(val_i, z1)) → f2_out1(.(val_j, z0))
Tuples:

F2_IN(.(val_i, z0)) → c1(F2_IN(z0))
S tuples:

F2_IN(.(val_i, z0)) → c1(F2_IN(z0))
K tuples:none
Defined Rule Symbols:

f2_in, U1

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1

(15) 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(.(val_i, z0)) → c1(F2_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:

F2_IN(.(val_i, z0)) → c1(F2_IN(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [1] + x2   
POL(F2_IN(x1)) = x1   
POL(c1(x1)) = x1   
POL(val_i) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1([])
f2_in(.(val_i, z0)) → U1(f2_in(z0), .(val_i, z0))
U1(f2_out1(z0), .(val_i, z1)) → f2_out1(.(val_j, z0))
Tuples:

F2_IN(.(val_i, z0)) → c1(F2_IN(z0))
S tuples:none
K tuples:

F2_IN(.(val_i, z0)) → c1(F2_IN(z0))
Defined Rule Symbols:

f2_in, U1

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1