(0) Obligation:
Clauses:
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
app([], Ys, Ys).
reverse(.(X, Xs), Ys) :- ','(reverse(Xs, Zs), app(Zs, .(X, []), Ys)).
reverse([], []).
Query: reverse(g,a)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
app([], Ys, Ys).
reverse([], []).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
reverse(.(X, Xs), Ys) :- ','(reverse(Xs, Zs), app(Zs, .(X, []), Ys)).
Query: reverse(g,a)
(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F2_IN(.(z0, z1)) → c1(U1'(f15_in(z1, z0), .(z0, z1)), F15_IN(z1, z0))
F24_IN(.(z0, z1), z2) → c4(U2'(f24_in(z1, z2), .(z0, z1), z2), F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(U3'(f36_in(z1, z0), .(z0, z1)), F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(U4'(f41_in(z1, z2), .(z0, z1), z2), F41_IN(z1, z2))
F15_IN(z0, z1) → c12(U5'(f22_in(z0), z0, z1), F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c13(U6'(f24_in(z0, z2), z1, z2, z0), F24_IN(z0, z2))
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
U7'(f22_out1(z0), z1, z2) → c16(U8'(f41_in(z0, z2), z1, z2, z0), F41_IN(z0, z2))
S tuples:
F2_IN(.(z0, z1)) → c1(U1'(f15_in(z1, z0), .(z0, z1)), F15_IN(z1, z0))
F24_IN(.(z0, z1), z2) → c4(U2'(f24_in(z1, z2), .(z0, z1), z2), F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(U3'(f36_in(z1, z0), .(z0, z1)), F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(U4'(f41_in(z1, z2), .(z0, z1), z2), F41_IN(z1, z2))
F15_IN(z0, z1) → c12(U5'(f22_in(z0), z0, z1), F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c13(U6'(f24_in(z0, z2), z1, z2, z0), F24_IN(z0, z2))
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
U7'(f22_out1(z0), z1, z2) → c16(U8'(f41_in(z0, z2), z1, z2, z0), F41_IN(z0, z2))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F2_IN, F24_IN, F22_IN, F41_IN, F15_IN, U5', F36_IN, U7'
Compound Symbols:
c1, c4, c7, c10, c12, c13, c15, c16
(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F24_IN(.(z0, z1), z2) → c4(U2'(f24_in(z1, z2), .(z0, z1), z2), F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(U3'(f36_in(z1, z0), .(z0, z1)), F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(U4'(f41_in(z1, z2), .(z0, z1), z2), F41_IN(z1, z2))
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
F2_IN(.(z0, z1)) → c(U1'(f15_in(z1, z0), .(z0, z1)))
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(U6'(f24_in(z0, z2), z1, z2, z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(U8'(f41_in(z0, z2), z1, z2, z0))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
S tuples:
F24_IN(.(z0, z1), z2) → c4(U2'(f24_in(z1, z2), .(z0, z1), z2), F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(U3'(f36_in(z1, z0), .(z0, z1)), F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(U4'(f41_in(z1, z2), .(z0, z1), z2), F41_IN(z1, z2))
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
F2_IN(.(z0, z1)) → c(U1'(f15_in(z1, z0), .(z0, z1)))
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(U6'(f24_in(z0, z2), z1, z2, z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(U8'(f41_in(z0, z2), z1, z2, z0))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F24_IN, F22_IN, F41_IN, F36_IN, F2_IN, F15_IN, U5', U7'
Compound Symbols:
c4, c7, c10, c15, c
(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 6 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c
S tuples:
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F36_IN, F2_IN, F15_IN, U5', U7', F24_IN, F22_IN, F41_IN
Compound Symbols:
c15, c, c4, c7, c10, c
(9) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U5'(f22_out1(z0), z1, z2) → c
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c
S tuples:
F36_IN(z0, z1) → c15(U7'(f22_in(z0), z0, z1), F22_IN(z0))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
U7'(f22_out1(z0), z1, z2) → c
K tuples:
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F36_IN, F2_IN, F15_IN, U5', U7', F24_IN, F22_IN, F41_IN
Compound Symbols:
c15, c, c4, c7, c10, c
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F36_IN(
z0,
z1) →
c15(
U7'(
f22_in(
z0),
z0,
z1),
F22_IN(
z0)) by
F36_IN([], x1) → c15(U7'(f22_out1([]), [], x1), F22_IN([]))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
U7'(f22_out1(z0), z1, z2) → c
F36_IN([], x1) → c15(U7'(f22_out1([]), [], x1), F22_IN([]))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
S tuples:
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
U7'(f22_out1(z0), z1, z2) → c
F36_IN([], x1) → c15(U7'(f22_out1([]), [], x1), F22_IN([]))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
K tuples:
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
F15_IN(z0, z1) → c(F22_IN(z0))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F2_IN, F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c, c15
(13) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 4 of 13 dangling nodes:
F2_IN(.(z0, z1)) → c(F15_IN(z1, z0))
F15_IN(z0, z1) → c(F22_IN(z0))
F2_IN(.(z0, z1)) → c
U5'(f22_out1(z0), z1, z2) → c
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
U7'(f22_out1(z0), z1, z2) → c
F36_IN([], x1) → c15(U7'(f22_out1([]), [], x1), F22_IN([]))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
S tuples:
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
U7'(f22_out1(z0), z1, z2) → c
F36_IN([], x1) → c15(U7'(f22_out1([]), [], x1), F22_IN([]))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c, c15
(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, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1(F22_IN([]))
S tuples:
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1(F22_IN([]))
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c15, c1
(17) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
S tuples:
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c15, c1, c1
(19) 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.
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
We considered the (Usable) Rules:
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
And the Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = x2
POL(F15_IN(x1, x2)) = [2] + [2]x2
POL(F22_IN(x1)) = [2] + [2]x1
POL(F24_IN(x1, x2)) = [1]
POL(F36_IN(x1, x2)) = [2] + [2]x1
POL(F41_IN(x1, x2)) = 0
POL(U3(x1, x2)) = 0
POL(U4(x1, x2, x3)) = 0
POL(U5'(x1, x2, x3)) = [1]
POL(U7(x1, x2, x3)) = 0
POL(U7'(x1, x2, x3)) = 0
POL(U8(x1, x2, x3, x4)) = 0
POL([]) = [3]
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1, x2)) = x1 + x2
POL(c4(x1)) = x1
POL(c7(x1)) = x1
POL(f22_in(x1)) = 0
POL(f22_out1(x1)) = 0
POL(f36_in(x1, x2)) = 0
POL(f36_out1(x1, x2)) = 0
POL(f41_in(x1, x2)) = 0
POL(f41_out1(x1)) = 0
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
S tuples:
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c15, c1, c1
(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.
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
We considered the (Usable) Rules:
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
And the Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F15_IN(x1, x2)) = [2] + [2]x1
POL(F22_IN(x1)) = x1
POL(F24_IN(x1, x2)) = [1]
POL(F36_IN(x1, x2)) = x1
POL(F41_IN(x1, x2)) = 0
POL(U3(x1, x2)) = 0
POL(U4(x1, x2, x3)) = 0
POL(U5'(x1, x2, x3)) = [1] + [2]x2
POL(U7(x1, x2, x3)) = 0
POL(U7'(x1, x2, x3)) = 0
POL(U8(x1, x2, x3, x4)) = 0
POL([]) = 0
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1, x2)) = x1 + x2
POL(c4(x1)) = x1
POL(c7(x1)) = x1
POL(f22_in(x1)) = 0
POL(f22_out1(x1)) = 0
POL(f36_in(x1, x2)) = 0
POL(f36_out1(x1, x2)) = 0
POL(f41_in(x1, x2)) = 0
POL(f41_out1(x1)) = 0
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
S tuples:
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c15, c1, c1
(23) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
S tuples:
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c15, c1, c1
(25) 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.
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
We considered the (Usable) Rules:
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
And the Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [2] + x2
POL(F15_IN(x1, x2)) = [3] + [2]x1 + [2]x2
POL(F22_IN(x1)) = [1] + x1
POL(F24_IN(x1, x2)) = [1] + x1
POL(F36_IN(x1, x2)) = [3] + x1
POL(F41_IN(x1, x2)) = 0
POL(U3(x1, x2)) = x1
POL(U4(x1, x2, x3)) = [2] + x1
POL(U5'(x1, x2, x3)) = [2] + x1 + x2 + x3
POL(U7(x1, x2, x3)) = [2] + x1
POL(U7'(x1, x2, x3)) = 0
POL(U8(x1, x2, x3, x4)) = x1
POL([]) = 0
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1, x2)) = x1 + x2
POL(c4(x1)) = x1
POL(c7(x1)) = x1
POL(f22_in(x1)) = [1] + x1
POL(f22_out1(x1)) = x1
POL(f36_in(x1, x2)) = [3] + x1
POL(f36_out1(x1, x2)) = x2
POL(f41_in(x1, x2)) = [2] + x1
POL(f41_out1(x1)) = x1
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
S tuples:
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c15, c1, c1
(27) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
We considered the (Usable) Rules:
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
And the Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F15_IN(x1, x2)) = x22 + x1·x2 + x12
POL(F22_IN(x1)) = x12
POL(F24_IN(x1, x2)) = 0
POL(F36_IN(x1, x2)) = [1] + x1 + x12
POL(F41_IN(x1, x2)) = x1
POL(U3(x1, x2)) = x1
POL(U4(x1, x2, x3)) = [1] + x1
POL(U5'(x1, x2, x3)) = x2·x3 + x22
POL(U7(x1, x2, x3)) = [1] + x1
POL(U7'(x1, x2, x3)) = x1
POL(U8(x1, x2, x3, x4)) = x1
POL([]) = 0
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c15(x1, x2)) = x1 + x2
POL(c4(x1)) = x1
POL(c7(x1)) = x1
POL(f22_in(x1)) = x1
POL(f22_out1(x1)) = x1
POL(f36_in(x1, x2)) = [1] + x1
POL(f36_out1(x1, x2)) = x2
POL(f41_in(x1, x2)) = [1] + x1
POL(f41_out1(x1)) = x1
(28) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1([])
f2_in(.(z0, z1)) → U1(f15_in(z1, z0), .(z0, z1))
U1(f15_out1(z0, z1), .(z2, z3)) → f2_out1(z1)
f24_in([], z0) → f24_out1(.(z0, []))
f24_in(.(z0, z1), z2) → U2(f24_in(z1, z2), .(z0, z1), z2)
U2(f24_out1(z0), .(z1, z2), z3) → f24_out1(.(z1, z0))
f22_in([]) → f22_out1([])
f22_in(.(z0, z1)) → U3(f36_in(z1, z0), .(z0, z1))
U3(f36_out1(z0, z1), .(z2, z3)) → f22_out1(z1)
f41_in([], z0) → f41_out1(.(z0, []))
f41_in(.(z0, z1), z2) → U4(f41_in(z1, z2), .(z0, z1), z2)
U4(f41_out1(z0), .(z1, z2), z3) → f41_out1(.(z1, z0))
f15_in(z0, z1) → U5(f22_in(z0), z0, z1)
U5(f22_out1(z0), z1, z2) → U6(f24_in(z0, z2), z1, z2, z0)
U6(f24_out1(z0), z1, z2, z3) → f15_out1(z3, z0)
f36_in(z0, z1) → U7(f22_in(z0), z0, z1)
U7(f22_out1(z0), z1, z2) → U8(f41_in(z0, z2), z1, z2, z0)
U8(f41_out1(z0), z1, z2, z3) → f36_out1(z3, z0)
Tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
S tuples:none
K tuples:
F15_IN(z0, z1) → c(U5'(f22_in(z0), z0, z1))
U5'(f22_out1(z0), z1, z2) → c(F24_IN(z0, z2))
F36_IN([], x1) → c1(U7'(f22_out1([]), [], x1))
F36_IN([], x1) → c1
F22_IN(.(z0, z1)) → c7(F36_IN(z1, z0))
F36_IN(.(z0, z1), x1) → c15(U7'(U3(f36_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F22_IN(.(z0, z1)))
U7'(f22_out1(z0), z1, z2) → c(F41_IN(z0, z2))
F24_IN(.(z0, z1), z2) → c4(F24_IN(z1, z2))
F41_IN(.(z0, z1), z2) → c10(F41_IN(z1, z2))
Defined Rule Symbols:
f2_in, U1, f24_in, U2, f22_in, U3, f41_in, U4, f15_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F15_IN, U5', U7', F24_IN, F22_IN, F41_IN, F36_IN
Compound Symbols:
c, c4, c7, c10, c15, c1, c1
(29) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(30) BOUNDS(O(1), O(1))
(31) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(32) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F1_IN(.(z0, [])) → c1(U1'(f18_in(z0), .(z0, [])), F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(U2'(f38_in(z2, z1, z0), .(z0, .(z1, z2))), F38_IN(z2, z1, z0))
F57_IN(.(z0, z1), z2) → c7(U3'(f57_in(z1, z2), .(z0, z1), z2), F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(U4'(f54_in(z1, z0), .(z0, z1)), F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(U5'(f75_in(z1, z2), .(z0, z1), z2), F75_IN(z1, z2))
F38_IN(z0, z1, z2) → c16(U6'(f42_in(z0), z0, z1, z2), F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c17(U7'(f43_in(z0, z2, z3), z1, z2, z3, z0), F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c19(U8'(f57_in(z0, z1), z0, z1, z2), F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c20(U9'(f75_in(z0, z3), z1, z2, z3, z0), F75_IN(z0, z3))
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
U10'(f42_out1(z0), z1, z2) → c23(U11'(f57_in(z0, z2), z1, z2, z0), F57_IN(z0, z2))
F18_IN(z0) → c25(U12'(f20_in(z0), f21_in(z0), z0), F20_IN(z0))
S tuples:
F1_IN(.(z0, [])) → c1(U1'(f18_in(z0), .(z0, [])), F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(U2'(f38_in(z2, z1, z0), .(z0, .(z1, z2))), F38_IN(z2, z1, z0))
F57_IN(.(z0, z1), z2) → c7(U3'(f57_in(z1, z2), .(z0, z1), z2), F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(U4'(f54_in(z1, z0), .(z0, z1)), F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(U5'(f75_in(z1, z2), .(z0, z1), z2), F75_IN(z1, z2))
F38_IN(z0, z1, z2) → c16(U6'(f42_in(z0), z0, z1, z2), F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c17(U7'(f43_in(z0, z2, z3), z1, z2, z3, z0), F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c19(U8'(f57_in(z0, z1), z0, z1, z2), F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c20(U9'(f75_in(z0, z3), z1, z2, z3, z0), F75_IN(z0, z3))
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
U10'(f42_out1(z0), z1, z2) → c23(U11'(f57_in(z0, z2), z1, z2, z0), F57_IN(z0, z2))
F18_IN(z0) → c25(U12'(f20_in(z0), f21_in(z0), z0), F20_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F1_IN, F57_IN, F42_IN, F75_IN, F38_IN, U6', F43_IN, U8', F54_IN, U10', F18_IN
Compound Symbols:
c1, c2, c7, c10, c13, c16, c17, c19, c20, c22, c23, c25
(33) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(34) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F57_IN(.(z0, z1), z2) → c7(U3'(f57_in(z1, z2), .(z0, z1), z2), F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(U4'(f54_in(z1, z0), .(z0, z1)), F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(U5'(f75_in(z1, z2), .(z0, z1), z2), F75_IN(z1, z2))
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
F1_IN(.(z0, [])) → c(U1'(f18_in(z0), .(z0, [])))
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(U2'(f38_in(z2, z1, z0), .(z0, .(z1, z2))))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(U7'(f43_in(z0, z2, z3), z1, z2, z3, z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(U9'(f75_in(z0, z3), z1, z2, z3, z0))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(U11'(f57_in(z0, z2), z1, z2, z0))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F18_IN(z0) → c(U12'(f20_in(z0), f21_in(z0), z0))
F18_IN(z0) → c(F20_IN(z0))
S tuples:
F57_IN(.(z0, z1), z2) → c7(U3'(f57_in(z1, z2), .(z0, z1), z2), F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(U4'(f54_in(z1, z0), .(z0, z1)), F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(U5'(f75_in(z1, z2), .(z0, z1), z2), F75_IN(z1, z2))
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
F1_IN(.(z0, [])) → c(U1'(f18_in(z0), .(z0, [])))
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(U2'(f38_in(z2, z1, z0), .(z0, .(z1, z2))))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(U7'(f43_in(z0, z2, z3), z1, z2, z3, z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(U9'(f75_in(z0, z3), z1, z2, z3, z0))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(U11'(f57_in(z0, z2), z1, z2, z0))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F18_IN(z0) → c(U12'(f20_in(z0), f21_in(z0), z0))
F18_IN(z0) → c(F20_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F57_IN, F42_IN, F75_IN, F54_IN, F1_IN, F38_IN, U6', F43_IN, U8', U10', F18_IN
Compound Symbols:
c7, c10, c13, c22, c
(35) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 10 trailing tuple parts
(36) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F1_IN(.(z0, [])) → c
F1_IN(.(z0, .(z1, z2))) → c
U6'(f42_out1(z0), z1, z2, z3) → c
U8'(f57_out1(z0), z1, z2, z3) → c
U10'(f42_out1(z0), z1, z2) → c
F18_IN(z0) → c
S tuples:
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F1_IN(.(z0, [])) → c
F1_IN(.(z0, .(z1, z2))) → c
U6'(f42_out1(z0), z1, z2, z3) → c
U8'(f57_out1(z0), z1, z2, z3) → c
U10'(f42_out1(z0), z1, z2) → c
F18_IN(z0) → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F54_IN, F1_IN, F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F18_IN
Compound Symbols:
c22, c, c7, c10, c13, c
(37) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
F1_IN(.(z0, [])) → c
F1_IN(.(z0, .(z1, z2))) → c
U6'(f42_out1(z0), z1, z2, z3) → c
U8'(f57_out1(z0), z1, z2, z3) → c
F18_IN(z0) → c
F18_IN(z0) → c
F18_IN(z0) → c
F18_IN(z0) → c
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
U6'(f42_out1(z0), z1, z2, z3) → c
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U8'(f57_out1(z0), z1, z2, z3) → c
(38) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F1_IN(.(z0, [])) → c
F1_IN(.(z0, .(z1, z2))) → c
U6'(f42_out1(z0), z1, z2, z3) → c
U8'(f57_out1(z0), z1, z2, z3) → c
U10'(f42_out1(z0), z1, z2) → c
F18_IN(z0) → c
S tuples:
F54_IN(z0, z1) → c22(U10'(f42_in(z0), z0, z1), F42_IN(z0))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
U10'(f42_out1(z0), z1, z2) → c
K tuples:
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
F1_IN(.(z0, [])) → c
F1_IN(.(z0, .(z1, z2))) → c
U6'(f42_out1(z0), z1, z2, z3) → c
U8'(f57_out1(z0), z1, z2, z3) → c
F18_IN(z0) → c
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F54_IN, F1_IN, F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F18_IN
Compound Symbols:
c22, c, c7, c10, c13, c
(39) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F54_IN(
z0,
z1) →
c22(
U10'(
f42_in(
z0),
z0,
z1),
F42_IN(
z0)) by
F54_IN([], x1) → c22(U10'(f42_out1([]), [], x1), F42_IN([]))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
(40) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F1_IN(.(z0, [])) → c
F1_IN(.(z0, .(z1, z2))) → c
U6'(f42_out1(z0), z1, z2, z3) → c
U8'(f57_out1(z0), z1, z2, z3) → c
U10'(f42_out1(z0), z1, z2) → c
F18_IN(z0) → c
F54_IN([], x1) → c22(U10'(f42_out1([]), [], x1), F42_IN([]))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
S tuples:
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
U10'(f42_out1(z0), z1, z2) → c
F54_IN([], x1) → c22(U10'(f42_out1([]), [], x1), F42_IN([]))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
K tuples:
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
F1_IN(.(z0, [])) → c
F1_IN(.(z0, .(z1, z2))) → c
U6'(f42_out1(z0), z1, z2, z3) → c
U8'(f57_out1(z0), z1, z2, z3) → c
F18_IN(z0) → c
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F1_IN, F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F18_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c, c22
(41) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 8 of 20 dangling nodes:
F1_IN(.(z0, .(z1, z2))) → c(F38_IN(z2, z1, z0))
F38_IN(z0, z1, z2) → c(F42_IN(z0))
U6'(f42_out1(z0), z1, z2, z3) → c
F18_IN(z0) → c
F1_IN(.(z0, .(z1, z2))) → c
U8'(f57_out1(z0), z1, z2, z3) → c
F1_IN(.(z0, [])) → c(F18_IN(z0))
F1_IN(.(z0, [])) → c
(42) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
U10'(f42_out1(z0), z1, z2) → c
F54_IN([], x1) → c22(U10'(f42_out1([]), [], x1), F42_IN([]))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
S tuples:
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
U10'(f42_out1(z0), z1, z2) → c
F54_IN([], x1) → c22(U10'(f42_out1([]), [], x1), F42_IN([]))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
K tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c, c22
(43) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(44) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1(F42_IN([]))
S tuples:
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1(F42_IN([]))
K tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c22, c1
(45) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(46) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
S tuples:
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
K tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c22, c1, c1
(47) 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.
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
We considered the (Usable) Rules:
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
And the Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = x2
POL(F38_IN(x1, x2, x3)) = [1] + [3]x2 + [2]x3
POL(F42_IN(x1)) = [1]
POL(F43_IN(x1, x2, x3)) = x2 + [2]x3
POL(F54_IN(x1, x2)) = [1]
POL(F57_IN(x1, x2)) = 0
POL(F75_IN(x1, x2)) = x2
POL(U10(x1, x2, x3)) = 0
POL(U10'(x1, x2, x3)) = 0
POL(U11(x1, x2, x3, x4)) = 0
POL(U3(x1, x2, x3)) = 0
POL(U4(x1, x2)) = x2
POL(U6'(x1, x2, x3, x4)) = [1] + [2]x3 + [2]x4
POL(U8'(x1, x2, x3, x4)) = x4
POL([]) = [2]
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c13(x1)) = x1
POL(c22(x1, x2)) = x1 + x2
POL(c7(x1)) = x1
POL(f42_in(x1)) = [2]x1
POL(f42_out1(x1)) = x1
POL(f54_in(x1, x2)) = 0
POL(f54_out1(x1, x2)) = 0
POL(f57_in(x1, x2)) = 0
POL(f57_out1(x1)) = 0
(48) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
S tuples:
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
K tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c22, c1, c1
(49) 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.
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
We considered the (Usable) Rules:
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
And the Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F38_IN(x1, x2, x3)) = [1] + [2]x1 + [3]x2 + [3]x3
POL(F42_IN(x1)) = x1
POL(F43_IN(x1, x2, x3)) = [1] + [3]x2 + [3]x3
POL(F54_IN(x1, x2)) = x1
POL(F57_IN(x1, x2)) = 0
POL(F75_IN(x1, x2)) = 0
POL(U10(x1, x2, x3)) = 0
POL(U10'(x1, x2, x3)) = 0
POL(U11(x1, x2, x3, x4)) = 0
POL(U3(x1, x2, x3)) = 0
POL(U4(x1, x2)) = [1]
POL(U6'(x1, x2, x3, x4)) = [1] + x2 + [3]x3 + [3]x4
POL(U8'(x1, x2, x3, x4)) = [1] + [2]x3 + [3]x4
POL([]) = [1]
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c13(x1)) = x1
POL(c22(x1, x2)) = x1 + x2
POL(c7(x1)) = x1
POL(f42_in(x1)) = [2] + [2]x1
POL(f42_out1(x1)) = 0
POL(f54_in(x1, x2)) = 0
POL(f54_out1(x1, x2)) = 0
POL(f57_in(x1, x2)) = 0
POL(f57_out1(x1)) = 0
(50) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
S tuples:
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
K tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c22, c1, c1
(51) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
(52) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
S tuples:
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
K tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c22, c1, c1
(53) 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.
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
We considered the (Usable) Rules:
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
And the Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F38_IN(x1, x2, x3)) = [3] + [2]x1 + [3]x2 + [3]x3
POL(F42_IN(x1)) = 0
POL(F43_IN(x1, x2, x3)) = [2] + x1 + [3]x2 + [2]x3
POL(F54_IN(x1, x2)) = 0
POL(F57_IN(x1, x2)) = 0
POL(F75_IN(x1, x2)) = x1 + x2
POL(U10(x1, x2, x3)) = [1] + x1
POL(U10'(x1, x2, x3)) = 0
POL(U11(x1, x2, x3, x4)) = x1
POL(U3(x1, x2, x3)) = [1] + x1
POL(U4(x1, x2)) = x1
POL(U6'(x1, x2, x3, x4)) = [3] + x1 + [3]x3 + [2]x4
POL(U8'(x1, x2, x3, x4)) = x1 + [3]x3 + [2]x4
POL([]) = 0
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c13(x1)) = x1
POL(c22(x1, x2)) = x1 + x2
POL(c7(x1)) = x1
POL(f42_in(x1)) = x1
POL(f42_out1(x1)) = x1
POL(f54_in(x1, x2)) = [1] + x1
POL(f54_out1(x1, x2)) = x2
POL(f57_in(x1, x2)) = [1] + x1
POL(f57_out1(x1)) = x1
(54) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → U1(f18_in(z0), .(z0, []))
f1_in(.(z0, .(z1, z2))) → U2(f38_in(z2, z1, z0), .(z0, .(z1, z2)))
U1(f18_out1(z0), .(z1, [])) → f1_out1(z0)
U1(f18_out2(z0, z1), .(z2, [])) → f1_out1(z1)
U2(f38_out1(z0, z1, z2), .(z3, .(z4, z5))) → f1_out1(z2)
f57_in([], z0) → f57_out1(.(z0, []))
f57_in(.(z0, z1), z2) → U3(f57_in(z1, z2), .(z0, z1), z2)
U3(f57_out1(z0), .(z1, z2), z3) → f57_out1(.(z1, z0))
f42_in([]) → f42_out1([])
f42_in(.(z0, z1)) → U4(f54_in(z1, z0), .(z0, z1))
U4(f54_out1(z0, z1), .(z2, z3)) → f42_out1(z1)
f75_in([], z0) → f75_out1(.(z0, []))
f75_in(.(z0, z1), z2) → U5(f75_in(z1, z2), .(z0, z1), z2)
U5(f75_out1(z0), .(z1, z2), z3) → f75_out1(.(z1, z0))
f20_in(z0) → f20_out1(.(z0, []))
f38_in(z0, z1, z2) → U6(f42_in(z0), z0, z1, z2)
U6(f42_out1(z0), z1, z2, z3) → U7(f43_in(z0, z2, z3), z1, z2, z3, z0)
U7(f43_out1(z0, z1), z2, z3, z4, z5) → f38_out1(z5, z0, z1)
f43_in(z0, z1, z2) → U8(f57_in(z0, z1), z0, z1, z2)
U8(f57_out1(z0), z1, z2, z3) → U9(f75_in(z0, z3), z1, z2, z3, z0)
U9(f75_out1(z0), z1, z2, z3, z4) → f43_out1(z4, z0)
f54_in(z0, z1) → U10(f42_in(z0), z0, z1)
U10(f42_out1(z0), z1, z2) → U11(f57_in(z0, z2), z1, z2, z0)
U11(f57_out1(z0), z1, z2, z3) → f54_out1(z3, z0)
f18_in(z0) → U12(f20_in(z0), f21_in(z0), z0)
U12(f20_out1(z0), z1, z2) → f18_out1(z0)
U12(z0, f21_out1(z1, z2), z3) → f18_out2(z1, z2)
Tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
S tuples:
F57_IN(.(z0, z1), z2) → c7(F57_IN(z1, z2))
K tuples:
F38_IN(z0, z1, z2) → c(U6'(f42_in(z0), z0, z1, z2))
U6'(f42_out1(z0), z1, z2, z3) → c(F43_IN(z0, z2, z3))
F43_IN(z0, z1, z2) → c(U8'(f57_in(z0, z1), z0, z1, z2))
F43_IN(z0, z1, z2) → c(F57_IN(z0, z1))
U8'(f57_out1(z0), z1, z2, z3) → c(F75_IN(z0, z3))
F54_IN([], x1) → c1(U10'(f42_out1([]), [], x1))
F54_IN([], x1) → c1
F42_IN(.(z0, z1)) → c10(F54_IN(z1, z0))
F54_IN(.(z0, z1), x1) → c22(U10'(U4(f54_in(z1, z0), .(z0, z1)), .(z0, z1), x1), F42_IN(.(z0, z1)))
U10'(f42_out1(z0), z1, z2) → c(F57_IN(z0, z2))
F75_IN(.(z0, z1), z2) → c13(F75_IN(z1, z2))
Defined Rule Symbols:
f1_in, U1, U2, f57_in, U3, f42_in, U4, f75_in, U5, f20_in, f38_in, U6, U7, f43_in, U8, U9, f54_in, U10, U11, f18_in, U12
Defined Pair Symbols:
F38_IN, U6', F43_IN, U8', U10', F57_IN, F42_IN, F75_IN, F54_IN
Compound Symbols:
c, c7, c10, c13, c22, c1, c1