(0) Obligation:
Clauses:
append([], L, L).
append(.(H, L1), L2, .(H, L3)) :- append(L1, L2, L3).
append3(A, B, C, D) :- ','(append(A, B, E), append(E, C, D)).
Query: append3(g,g,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(z0, z1, z2) → U1(f6_in(z0, z1, z2), z0, z1, z2)
U1(f6_out1(z0, z1), z2, z3, z4) → f1_out1(z1)
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
f11_in([], z0) → f11_out1(z0)
f11_in(.(z0, z1), z2) → U3(f11_in(z1, z2), .(z0, z1), z2)
U3(f11_out1(z0), .(z1, z2), z3) → f11_out1(.(z1, z0))
f6_in(z0, z1, z2) → U4(f10_in(z0, z1), z0, z1, z2)
U4(f10_out1(z0), z1, z2, z3) → U5(f11_in(z0, z3), z1, z2, z3, z0)
U5(f11_out1(z0), z1, z2, z3, z4) → f6_out1(z4, z0)
Tuples:
F1_IN(z0, z1, z2) → c(U1'(f6_in(z0, z1, z2), z0, z1, z2), F6_IN(z0, z1, z2))
F10_IN(.(z0, z1), z2) → c3(U2'(f10_in(z1, z2), .(z0, z1), z2), F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(U3'(f11_in(z1, z2), .(z0, z1), z2), F11_IN(z1, z2))
F6_IN(z0, z1, z2) → c8(U4'(f10_in(z0, z1), z0, z1, z2), F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c9(U5'(f11_in(z0, z3), z1, z2, z3, z0), F11_IN(z0, z3))
S tuples:
F1_IN(z0, z1, z2) → c(U1'(f6_in(z0, z1, z2), z0, z1, z2), F6_IN(z0, z1, z2))
F10_IN(.(z0, z1), z2) → c3(U2'(f10_in(z1, z2), .(z0, z1), z2), F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(U3'(f11_in(z1, z2), .(z0, z1), z2), F11_IN(z1, z2))
F6_IN(z0, z1, z2) → c8(U4'(f10_in(z0, z1), z0, z1, z2), F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c9(U5'(f11_in(z0, z3), z1, z2, z3, z0), F11_IN(z0, z3))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f10_in, U2, f11_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F1_IN, F10_IN, F11_IN, F6_IN, U4'
Compound Symbols:
c, c3, c6, c8, c9
(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(z0, z1, z2) → U1(f6_in(z0, z1, z2), z0, z1, z2)
U1(f6_out1(z0, z1), z2, z3, z4) → f1_out1(z1)
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
f11_in([], z0) → f11_out1(z0)
f11_in(.(z0, z1), z2) → U3(f11_in(z1, z2), .(z0, z1), z2)
U3(f11_out1(z0), .(z1, z2), z3) → f11_out1(.(z1, z0))
f6_in(z0, z1, z2) → U4(f10_in(z0, z1), z0, z1, z2)
U4(f10_out1(z0), z1, z2, z3) → U5(f11_in(z0, z3), z1, z2, z3, z0)
U5(f11_out1(z0), z1, z2, z3, z4) → f6_out1(z4, z0)
Tuples:
F10_IN(.(z0, z1), z2) → c3(U2'(f10_in(z1, z2), .(z0, z1), z2), F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(U3'(f11_in(z1, z2), .(z0, z1), z2), F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1(U1'(f6_in(z0, z1, z2), z0, z1, z2))
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(U5'(f11_in(z0, z3), z1, z2, z3, z0))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
S tuples:
F10_IN(.(z0, z1), z2) → c3(U2'(f10_in(z1, z2), .(z0, z1), z2), F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(U3'(f11_in(z1, z2), .(z0, z1), z2), F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1(U1'(f6_in(z0, z1, z2), z0, z1, z2))
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(U5'(f11_in(z0, z3), z1, z2, z3, z0))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f10_in, U2, f11_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F10_IN, F11_IN, F1_IN, F6_IN, U4'
Compound Symbols:
c3, c6, c1
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, z1, z2) → U1(f6_in(z0, z1, z2), z0, z1, z2)
U1(f6_out1(z0, z1), z2, z3, z4) → f1_out1(z1)
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
f11_in([], z0) → f11_out1(z0)
f11_in(.(z0, z1), z2) → U3(f11_in(z1, z2), .(z0, z1), z2)
U3(f11_out1(z0), .(z1, z2), z3) → f11_out1(.(z1, z0))
f6_in(z0, z1, z2) → U4(f10_in(z0, z1), z0, z1, z2)
U4(f10_out1(z0), z1, z2, z3) → U5(f11_in(z0, z3), z1, z2, z3, z0)
U5(f11_out1(z0), z1, z2, z3, z4) → f6_out1(z4, z0)
Tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
S tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
K tuples:none
Defined Rule Symbols:
f1_in, U1, f10_in, U2, f11_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F1_IN, F6_IN, U4', F10_IN, F11_IN
Compound Symbols:
c1, c3, c6, c1
(7) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
U4'(f10_out1(z0), z1, z2, z3) → c1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, z1, z2) → U1(f6_in(z0, z1, z2), z0, z1, z2)
U1(f6_out1(z0, z1), z2, z3, z4) → f1_out1(z1)
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
f11_in([], z0) → f11_out1(z0)
f11_in(.(z0, z1), z2) → U3(f11_in(z1, z2), .(z0, z1), z2)
U3(f11_out1(z0), .(z1, z2), z3) → f11_out1(.(z1, z0))
f6_in(z0, z1, z2) → U4(f10_in(z0, z1), z0, z1, z2)
U4(f10_out1(z0), z1, z2, z3) → U5(f11_in(z0, z3), z1, z2, z3, z0)
U5(f11_out1(z0), z1, z2, z3, z4) → f6_out1(z4, z0)
Tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
S tuples:
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
K tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
Defined Rule Symbols:
f1_in, U1, f10_in, U2, f11_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F1_IN, F6_IN, U4', F10_IN, F11_IN
Compound Symbols:
c1, c3, c6, c1
(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.
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
We considered the (Usable) Rules:
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
And the Tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [2] + x2
POL(F10_IN(x1, x2)) = [2] + [2]x1 + [2]x2
POL(F11_IN(x1, x2)) = 0
POL(F1_IN(x1, x2, x3)) = [2] + [2]x1 + [2]x2 + [2]x3
POL(F6_IN(x1, x2, x3)) = [2] + [2]x1 + [2]x2 + x3
POL(U2(x1, x2, x3)) = 0
POL(U4'(x1, x2, x3, x4)) = [2]x2 + [2]x3 + x4
POL([]) = 0
POL(c1) = 0
POL(c1(x1)) = x1
POL(c3(x1)) = x1
POL(c6(x1)) = x1
POL(f10_in(x1, x2)) = 0
POL(f10_out1(x1)) = 0
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, z1, z2) → U1(f6_in(z0, z1, z2), z0, z1, z2)
U1(f6_out1(z0, z1), z2, z3, z4) → f1_out1(z1)
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
f11_in([], z0) → f11_out1(z0)
f11_in(.(z0, z1), z2) → U3(f11_in(z1, z2), .(z0, z1), z2)
U3(f11_out1(z0), .(z1, z2), z3) → f11_out1(.(z1, z0))
f6_in(z0, z1, z2) → U4(f10_in(z0, z1), z0, z1, z2)
U4(f10_out1(z0), z1, z2, z3) → U5(f11_in(z0, z3), z1, z2, z3, z0)
U5(f11_out1(z0), z1, z2, z3, z4) → f6_out1(z4, z0)
Tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
S tuples:
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
K tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
Defined Rule Symbols:
f1_in, U1, f10_in, U2, f11_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F1_IN, F6_IN, U4', F10_IN, F11_IN
Compound Symbols:
c1, c3, c6, c1
(11) 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.
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
We considered the (Usable) Rules:
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
And the Tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [2] + x2
POL(F10_IN(x1, x2)) = [1] + x2
POL(F11_IN(x1, x2)) = [1] + x1
POL(F1_IN(x1, x2, x3)) = [3] + [3]x1 + [2]x2 + x3
POL(F6_IN(x1, x2, x3)) = [2] + [3]x1 + [2]x2
POL(U2(x1, x2, x3)) = [2] + x1
POL(U4'(x1, x2, x3, x4)) = [1] + x1
POL([]) = [1]
POL(c1) = 0
POL(c1(x1)) = x1
POL(c3(x1)) = x1
POL(c6(x1)) = x1
POL(f10_in(x1, x2)) = [1] + [2]x1 + x2
POL(f10_out1(x1)) = x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, z1, z2) → U1(f6_in(z0, z1, z2), z0, z1, z2)
U1(f6_out1(z0, z1), z2, z3, z4) → f1_out1(z1)
f10_in([], z0) → f10_out1(z0)
f10_in(.(z0, z1), z2) → U2(f10_in(z1, z2), .(z0, z1), z2)
U2(f10_out1(z0), .(z1, z2), z3) → f10_out1(.(z1, z0))
f11_in([], z0) → f11_out1(z0)
f11_in(.(z0, z1), z2) → U3(f11_in(z1, z2), .(z0, z1), z2)
U3(f11_out1(z0), .(z1, z2), z3) → f11_out1(.(z1, z0))
f6_in(z0, z1, z2) → U4(f10_in(z0, z1), z0, z1, z2)
U4(f10_out1(z0), z1, z2, z3) → U5(f11_in(z0, z3), z1, z2, z3, z0)
U5(f11_out1(z0), z1, z2, z3, z4) → f6_out1(z4, z0)
Tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
S tuples:none
K tuples:
F1_IN(z0, z1, z2) → c1(F6_IN(z0, z1, z2))
F6_IN(z0, z1, z2) → c1(U4'(f10_in(z0, z1), z0, z1, z2))
F6_IN(z0, z1, z2) → c1(F10_IN(z0, z1))
U4'(f10_out1(z0), z1, z2, z3) → c1(F11_IN(z0, z3))
F1_IN(z0, z1, z2) → c1
U4'(f10_out1(z0), z1, z2, z3) → c1
F10_IN(.(z0, z1), z2) → c3(F10_IN(z1, z2))
F11_IN(.(z0, z1), z2) → c6(F11_IN(z1, z2))
Defined Rule Symbols:
f1_in, U1, f10_in, U2, f11_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F1_IN, F6_IN, U4', F10_IN, F11_IN
Compound Symbols:
c1, c3, c6, c1
(13) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(14) BOUNDS(O(1), O(1))
(15) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([], z0, z1) → U1(f8_in(z0, z1), [], z0, z1)
f2_in(.(z0, z1), z2, z3) → U2(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3)
U1(f8_out1(z0), [], z1, z2) → f2_out1(z0)
U1(f8_out2(z0, z1), [], z2, z3) → f2_out1(z1)
U2(f34_out1(z0, z1), .(z2, z3), z4, z5) → f2_out1(z1)
f12_in([], z0) → f12_out1(z0)
f12_in(.(z0, z1), z2) → U3(f12_in(z1, z2), .(z0, z1), z2)
U3(f12_out1(z0), .(z1, z2), z3) → f12_out1(.(z1, z0))
f37_in([], z0) → f37_out1(z0)
f37_in(.(z0, z1), z2) → U4(f37_in(z1, z2), .(z0, z1), z2)
U4(f37_out1(z0), .(z1, z2), z3) → f37_out1(.(z1, z0))
f34_in(z0, z1, z2, z3) → U5(f37_in(z0, z1), z0, z1, z2, z3)
U5(f37_out1(z0), z1, z2, z3, z4) → U6(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0)
U6(f12_out1(z0), z1, z2, z3, z4, z5) → f34_out1(z5, z0)
f8_in(z0, z1) → U7(f12_in(z0, z1), f14_in(z0, z1), z0, z1)
U7(f12_out1(z0), z1, z2, z3) → f8_out1(z0)
U7(z0, f14_out1(z1, z2), z3, z4) → f8_out2(z1, z2)
Tuples:
F2_IN([], z0, z1) → c(U1'(f8_in(z0, z1), [], z0, z1), F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c1(U2'(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3), F34_IN(z1, z2, z0, z3))
F12_IN(.(z0, z1), z2) → c6(U3'(f12_in(z1, z2), .(z0, z1), z2), F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(U4'(f37_in(z1, z2), .(z0, z1), z2), F37_IN(z1, z2))
F34_IN(z0, z1, z2, z3) → c11(U5'(f37_in(z0, z1), z0, z1, z2, z3), F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c12(U6'(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0), F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c14(U7'(f12_in(z0, z1), f14_in(z0, z1), z0, z1), F12_IN(z0, z1))
S tuples:
F2_IN([], z0, z1) → c(U1'(f8_in(z0, z1), [], z0, z1), F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c1(U2'(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3), F34_IN(z1, z2, z0, z3))
F12_IN(.(z0, z1), z2) → c6(U3'(f12_in(z1, z2), .(z0, z1), z2), F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(U4'(f37_in(z1, z2), .(z0, z1), z2), F37_IN(z1, z2))
F34_IN(z0, z1, z2, z3) → c11(U5'(f37_in(z0, z1), z0, z1, z2, z3), F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c12(U6'(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0), F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c14(U7'(f12_in(z0, z1), f14_in(z0, z1), z0, z1), F12_IN(z0, z1))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f12_in, U3, f37_in, U4, f34_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F12_IN, F37_IN, F34_IN, U5', F8_IN
Compound Symbols:
c, c1, c6, c9, c11, c12, c14
(17) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([], z0, z1) → U1(f8_in(z0, z1), [], z0, z1)
f2_in(.(z0, z1), z2, z3) → U2(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3)
U1(f8_out1(z0), [], z1, z2) → f2_out1(z0)
U1(f8_out2(z0, z1), [], z2, z3) → f2_out1(z1)
U2(f34_out1(z0, z1), .(z2, z3), z4, z5) → f2_out1(z1)
f12_in([], z0) → f12_out1(z0)
f12_in(.(z0, z1), z2) → U3(f12_in(z1, z2), .(z0, z1), z2)
U3(f12_out1(z0), .(z1, z2), z3) → f12_out1(.(z1, z0))
f37_in([], z0) → f37_out1(z0)
f37_in(.(z0, z1), z2) → U4(f37_in(z1, z2), .(z0, z1), z2)
U4(f37_out1(z0), .(z1, z2), z3) → f37_out1(.(z1, z0))
f34_in(z0, z1, z2, z3) → U5(f37_in(z0, z1), z0, z1, z2, z3)
U5(f37_out1(z0), z1, z2, z3, z4) → U6(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0)
U6(f12_out1(z0), z1, z2, z3, z4, z5) → f34_out1(z5, z0)
f8_in(z0, z1) → U7(f12_in(z0, z1), f14_in(z0, z1), z0, z1)
U7(f12_out1(z0), z1, z2, z3) → f8_out1(z0)
U7(z0, f14_out1(z1, z2), z3, z4) → f8_out2(z1, z2)
Tuples:
F12_IN(.(z0, z1), z2) → c6(U3'(f12_in(z1, z2), .(z0, z1), z2), F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(U4'(f37_in(z1, z2), .(z0, z1), z2), F37_IN(z1, z2))
F2_IN([], z0, z1) → c2(U1'(f8_in(z0, z1), [], z0, z1))
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(U2'(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(U6'(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(U7'(f12_in(z0, z1), f14_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
S tuples:
F12_IN(.(z0, z1), z2) → c6(U3'(f12_in(z1, z2), .(z0, z1), z2), F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(U4'(f37_in(z1, z2), .(z0, z1), z2), F37_IN(z1, z2))
F2_IN([], z0, z1) → c2(U1'(f8_in(z0, z1), [], z0, z1))
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(U2'(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(U6'(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(U7'(f12_in(z0, z1), f14_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f12_in, U3, f37_in, U4, f34_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F12_IN, F37_IN, F2_IN, F34_IN, U5', F8_IN
Compound Symbols:
c6, c9, c2
(19) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 6 trailing tuple parts
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([], z0, z1) → U1(f8_in(z0, z1), [], z0, z1)
f2_in(.(z0, z1), z2, z3) → U2(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3)
U1(f8_out1(z0), [], z1, z2) → f2_out1(z0)
U1(f8_out2(z0, z1), [], z2, z3) → f2_out1(z1)
U2(f34_out1(z0, z1), .(z2, z3), z4, z5) → f2_out1(z1)
f12_in([], z0) → f12_out1(z0)
f12_in(.(z0, z1), z2) → U3(f12_in(z1, z2), .(z0, z1), z2)
U3(f12_out1(z0), .(z1, z2), z3) → f12_out1(.(z1, z0))
f37_in([], z0) → f37_out1(z0)
f37_in(.(z0, z1), z2) → U4(f37_in(z1, z2), .(z0, z1), z2)
U4(f37_out1(z0), .(z1, z2), z3) → f37_out1(.(z1, z0))
f34_in(z0, z1, z2, z3) → U5(f37_in(z0, z1), z0, z1, z2, z3)
U5(f37_out1(z0), z1, z2, z3, z4) → U6(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0)
U6(f12_out1(z0), z1, z2, z3, z4, z5) → f34_out1(z5, z0)
f8_in(z0, z1) → U7(f12_in(z0, z1), f14_in(z0, z1), z0, z1)
U7(f12_out1(z0), z1, z2, z3) → f8_out1(z0)
U7(z0, f14_out1(z1, z2), z3, z4) → f8_out2(z1, z2)
Tuples:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F12_IN(.(z0, z1), z2) → c6(F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
S tuples:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F12_IN(.(z0, z1), z2) → c6(F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f12_in, U3, f37_in, U4, f34_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F34_IN, U5', F8_IN, F12_IN, F37_IN
Compound Symbols:
c2, c6, c9, c2
(21) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F8_IN(z0, z1) → c2
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([], z0, z1) → U1(f8_in(z0, z1), [], z0, z1)
f2_in(.(z0, z1), z2, z3) → U2(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3)
U1(f8_out1(z0), [], z1, z2) → f2_out1(z0)
U1(f8_out2(z0, z1), [], z2, z3) → f2_out1(z1)
U2(f34_out1(z0, z1), .(z2, z3), z4, z5) → f2_out1(z1)
f12_in([], z0) → f12_out1(z0)
f12_in(.(z0, z1), z2) → U3(f12_in(z1, z2), .(z0, z1), z2)
U3(f12_out1(z0), .(z1, z2), z3) → f12_out1(.(z1, z0))
f37_in([], z0) → f37_out1(z0)
f37_in(.(z0, z1), z2) → U4(f37_in(z1, z2), .(z0, z1), z2)
U4(f37_out1(z0), .(z1, z2), z3) → f37_out1(.(z1, z0))
f34_in(z0, z1, z2, z3) → U5(f37_in(z0, z1), z0, z1, z2, z3)
U5(f37_out1(z0), z1, z2, z3, z4) → U6(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0)
U6(f12_out1(z0), z1, z2, z3, z4, z5) → f34_out1(z5, z0)
f8_in(z0, z1) → U7(f12_in(z0, z1), f14_in(z0, z1), z0, z1)
U7(f12_out1(z0), z1, z2, z3) → f8_out1(z0)
U7(z0, f14_out1(z1, z2), z3, z4) → f8_out2(z1, z2)
Tuples:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F12_IN(.(z0, z1), z2) → c6(F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
S tuples:
F12_IN(.(z0, z1), z2) → c6(F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
K tuples:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
Defined Rule Symbols:
f2_in, U1, U2, f12_in, U3, f37_in, U4, f34_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F34_IN, U5', F8_IN, F12_IN, F37_IN
Compound Symbols:
c2, c6, c9, c2
(23) 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.
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
We considered the (Usable) Rules:
f37_in([], z0) → f37_out1(z0)
f37_in(.(z0, z1), z2) → U4(f37_in(z1, z2), .(z0, z1), z2)
U4(f37_out1(z0), .(z1, z2), z3) → f37_out1(.(z1, z0))
And the Tuples:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F12_IN(.(z0, z1), z2) → c6(F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [2] + x2
POL(F12_IN(x1, x2)) = [1] + x2
POL(F2_IN(x1, x2, x3)) = [2]x1 + [3]x2 + [3]x3
POL(F34_IN(x1, x2, x3, x4)) = [2] + [2]x1 + [3]x2 + [2]x4
POL(F37_IN(x1, x2)) = [1] + x1 + [2]x2
POL(F8_IN(x1, x2)) = [2] + x1 + [2]x2
POL(U4(x1, x2, x3)) = [2] + x3
POL(U5'(x1, x2, x3, x4, x5)) = [1] + [2]x2 + x5
POL([]) = [2]
POL(c2) = 0
POL(c2(x1)) = x1
POL(c6(x1)) = x1
POL(c9(x1)) = x1
POL(f37_in(x1, x2)) = [3] + x1 + [2]x2
POL(f37_out1(x1)) = [2]
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([], z0, z1) → U1(f8_in(z0, z1), [], z0, z1)
f2_in(.(z0, z1), z2, z3) → U2(f34_in(z1, z2, z0, z3), .(z0, z1), z2, z3)
U1(f8_out1(z0), [], z1, z2) → f2_out1(z0)
U1(f8_out2(z0, z1), [], z2, z3) → f2_out1(z1)
U2(f34_out1(z0, z1), .(z2, z3), z4, z5) → f2_out1(z1)
f12_in([], z0) → f12_out1(z0)
f12_in(.(z0, z1), z2) → U3(f12_in(z1, z2), .(z0, z1), z2)
U3(f12_out1(z0), .(z1, z2), z3) → f12_out1(.(z1, z0))
f37_in([], z0) → f37_out1(z0)
f37_in(.(z0, z1), z2) → U4(f37_in(z1, z2), .(z0, z1), z2)
U4(f37_out1(z0), .(z1, z2), z3) → f37_out1(.(z1, z0))
f34_in(z0, z1, z2, z3) → U5(f37_in(z0, z1), z0, z1, z2, z3)
U5(f37_out1(z0), z1, z2, z3, z4) → U6(f12_in(.(z3, z0), z4), z1, z2, z3, z4, z0)
U6(f12_out1(z0), z1, z2, z3, z4, z5) → f34_out1(z5, z0)
f8_in(z0, z1) → U7(f12_in(z0, z1), f14_in(z0, z1), z0, z1)
U7(f12_out1(z0), z1, z2, z3) → f8_out1(z0)
U7(z0, f14_out1(z1, z2), z3, z4) → f8_out2(z1, z2)
Tuples:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F12_IN(.(z0, z1), z2) → c6(F12_IN(z1, z2))
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
S tuples:
F12_IN(.(z0, z1), z2) → c6(F12_IN(z1, z2))
K tuples:
F2_IN([], z0, z1) → c2(F8_IN(z0, z1))
F2_IN(.(z0, z1), z2, z3) → c2(F34_IN(z1, z2, z0, z3))
F34_IN(z0, z1, z2, z3) → c2(U5'(f37_in(z0, z1), z0, z1, z2, z3))
F34_IN(z0, z1, z2, z3) → c2(F37_IN(z0, z1))
U5'(f37_out1(z0), z1, z2, z3, z4) → c2(F12_IN(.(z3, z0), z4))
F8_IN(z0, z1) → c2(F12_IN(z0, z1))
F2_IN([], z0, z1) → c2
F2_IN(.(z0, z1), z2, z3) → c2
U5'(f37_out1(z0), z1, z2, z3, z4) → c2
F8_IN(z0, z1) → c2
F37_IN(.(z0, z1), z2) → c9(F37_IN(z1, z2))
Defined Rule Symbols:
f2_in, U1, U2, f12_in, U3, f37_in, U4, f34_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F34_IN, U5', F8_IN, F12_IN, F37_IN
Compound Symbols:
c2, c6, c9, c2