(0) Obligation:

Clauses:

rev(L, R) :- rev(L, [], R).
rev([], Y, Y).
rev(L, S, R) :- ','(no(empty(L)), ','(head(L, X), ','(tail(L, T), rev(T, .(X, S), R)))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, Xs), Xs).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: rev(g,a)

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

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f545_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f545_in([], z0, z1) → f545_out1
f545_in(.(z0, z1), z2, z3) → U2(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f545_out1, .(z0, z1), z2, z3) → f545_out1
Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F545_IN(.(z0, z1), z2, z3) → c11(U2'(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F545_IN(z1, z0, .(z2, z3)))
S tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F545_IN(.(z0, z1), z2, z3) → c11(U2'(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F545_IN(z1, z0, .(z2, z3)))
K tuples:none
Defined Rule Symbols:

f1_in, U1, f545_in, U2

Defined Pair Symbols:

F1_IN, F545_IN

Compound Symbols:

c8, c11

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f545_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f545_in([], z0, z1) → f545_out1
f545_in(.(z0, z1), z2, z3) → U2(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f545_out1, .(z0, z1), z2, z3) → f545_out1
Tuples:

F545_IN(.(z0, z1), z2, z3) → c11(U2'(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F545_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
S tuples:

F545_IN(.(z0, z1), z2, z3) → c11(U2'(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F545_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
K tuples:none
Defined Rule Symbols:

f1_in, U1, f545_in, U2

Defined Pair Symbols:

F545_IN, F1_IN

Compound Symbols:

c11, c

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

Removed 2 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f545_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f545_in([], z0, z1) → f545_out1
f545_in(.(z0, z1), z2, z3) → U2(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f545_out1, .(z0, z1), z2, z3) → f545_out1
Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
K tuples:none
Defined Rule Symbols:

f1_in, U1, f545_in, U2

Defined Pair Symbols:

F1_IN, F545_IN

Compound Symbols:

c, c11, c

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f545_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f545_in([], z0, z1) → f545_out1
f545_in(.(z0, z1), z2, z3) → U2(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f545_out1, .(z0, z1), z2, z3) → f545_out1
Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:

F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
K tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
Defined Rule Symbols:

f1_in, U1, f545_in, U2

Defined Pair Symbols:

F1_IN, F545_IN

Compound Symbols:

c, c11, c

(9) 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.

F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
We considered the (Usable) Rules:none
And the Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [3] + x2   
POL(F1_IN(x1)) = [3]x1   
POL(F545_IN(x1, x2, x3)) = [3]x1 + x3   
POL([]) = [2]   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c11(x1)) = x1   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f545_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f545_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f545_in([], z0, z1) → f545_out1
f545_in(.(z0, z1), z2, z3) → U2(f545_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f545_out1, .(z0, z1), z2, z3) → f545_out1
Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:none
K tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F545_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F545_IN(.(z0, z1), z2, z3) → c11(F545_IN(z1, z0, .(z2, z3)))
Defined Rule Symbols:

f1_in, U1, f545_in, U2

Defined Pair Symbols:

F1_IN, F545_IN

Compound Symbols:

c, c11, c

(11) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(12) BOUNDS(O(1), O(1))

(13) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f532_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f532_in([], z0, z1) → f532_out1
f532_in(.(z0, z1), z2, z3) → U2(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f532_out1, .(z0, z1), z2, z3) → f532_out1
Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F532_IN(.(z0, z1), z2, z3) → c11(U2'(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F532_IN(z1, z0, .(z2, z3)))
S tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F532_IN(.(z0, z1), z2, z3) → c11(U2'(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F532_IN(z1, z0, .(z2, z3)))
K tuples:none
Defined Rule Symbols:

f2_in, U1, f532_in, U2

Defined Pair Symbols:

F2_IN, F532_IN

Compound Symbols:

c8, c11

(15) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f532_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f532_in([], z0, z1) → f532_out1
f532_in(.(z0, z1), z2, z3) → U2(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f532_out1, .(z0, z1), z2, z3) → f532_out1
Tuples:

F532_IN(.(z0, z1), z2, z3) → c11(U2'(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F532_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
S tuples:

F532_IN(.(z0, z1), z2, z3) → c11(U2'(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F532_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
K tuples:none
Defined Rule Symbols:

f2_in, U1, f532_in, U2

Defined Pair Symbols:

F532_IN, F2_IN

Compound Symbols:

c11, c

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

Removed 2 trailing tuple parts

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f532_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f532_in([], z0, z1) → f532_out1
f532_in(.(z0, z1), z2, z3) → U2(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f532_out1, .(z0, z1), z2, z3) → f532_out1
Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
K tuples:none
Defined Rule Symbols:

f2_in, U1, f532_in, U2

Defined Pair Symbols:

F2_IN, F532_IN

Compound Symbols:

c, c11, c

(19) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f532_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f532_in([], z0, z1) → f532_out1
f532_in(.(z0, z1), z2, z3) → U2(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f532_out1, .(z0, z1), z2, z3) → f532_out1
Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:

F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
K tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
Defined Rule Symbols:

f2_in, U1, f532_in, U2

Defined Pair Symbols:

F2_IN, F532_IN

Compound Symbols:

c, c11, c

(21) 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.

F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
We considered the (Usable) Rules:none
And the Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [3] + x2   
POL(F2_IN(x1)) = [3]x1   
POL(F532_IN(x1, x2, x3)) = [3]x1 + x3   
POL([]) = [2]   
POL(c) = 0   
POL(c(x1)) = x1   
POL(c11(x1)) = x1   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f532_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f532_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f532_in([], z0, z1) → f532_out1
f532_in(.(z0, z1), z2, z3) → U2(f532_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f532_out1, .(z0, z1), z2, z3) → f532_out1
Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:none
K tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F532_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F532_IN(.(z0, z1), z2, z3) → c11(F532_IN(z1, z0, .(z2, z3)))
Defined Rule Symbols:

f2_in, U1, f532_in, U2

Defined Pair Symbols:

F2_IN, F532_IN

Compound Symbols:

c, c11, c