(0) Obligation:
Clauses:
palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse(X1s, [], X2s).
reverse([], Xs, Xs).
reverse(.(X, X1s), X2s, Ys) :- reverse(X1s, .(X, X2s), Ys).
Query: palindrome(g)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
reverse([], Xs, Xs).
palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse(X1s, [], X2s).
reverse(.(X, X1s), X2s, Ys) :- reverse(X1s, .(X, X2s), Ys).
Query: palindrome(g)
(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))
S tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f123_in, U2
Defined Pair Symbols:
F1_IN, F123_IN
Compound Symbols:
c8, c11
(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1
Tuples:
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
S tuples:
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f123_in, U2
Defined Pair Symbols:
F123_IN, F1_IN
Compound Symbols:
c11, c
(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, f123_in, U2
Defined Pair Symbols:
F1_IN, F123_IN
Compound Symbols:
c, c11, c
(9) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
K tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
Defined Rule Symbols:
f1_in, U1, f123_in, U2
Defined Pair Symbols:
F1_IN, F123_IN
Compound Symbols:
c, c11, c
(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.
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [2] + x1 + x2
POL(F123_IN(x1, x2, x3, x4, x5)) = x1 + x4
POL(F1_IN(x1)) = x1
POL([]) = 0
POL(c) = 0
POL(c(x1)) = x1
POL(c11(x1)) = x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:none
K tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
Defined Rule Symbols:
f1_in, U1, f123_in, U2
Defined Pair Symbols:
F1_IN, F123_IN
Compound Symbols:
c, c11, c
(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([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f129_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f129_in([], z0, z1, z0, z1) → f129_out1
f129_in(.(z0, z1), z2, z3, z4, z5) → U2(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f129_out1, .(z0, z1), z2, z3, z4, z5) → f129_out1
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F129_IN(z1, z0, .(z2, z3), z4, z5))
S tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F129_IN(z1, z0, .(z2, z3), z4, z5))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f129_in, U2
Defined Pair Symbols:
F2_IN, F129_IN
Compound Symbols:
c8, c11
(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([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f129_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f129_in([], z0, z1, z0, z1) → f129_out1
f129_in(.(z0, z1), z2, z3, z4, z5) → U2(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f129_out1, .(z0, z1), z2, z3, z4, z5) → f129_out1
Tuples:
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F129_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
S tuples:
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F129_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f129_in, U2
Defined Pair Symbols:
F129_IN, F2_IN
Compound Symbols:
c11, c
(19) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f129_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f129_in([], z0, z1, z0, z1) → f129_out1
f129_in(.(z0, z1), z2, z3, z4, z5) → U2(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f129_out1, .(z0, z1), z2, z3, z4, z5) → f129_out1
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, f129_in, U2
Defined Pair Symbols:
F2_IN, F129_IN
Compound Symbols:
c, c11, c
(21) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f129_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f129_in([], z0, z1, z0, z1) → f129_out1
f129_in(.(z0, z1), z2, z3, z4, z5) → U2(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f129_out1, .(z0, z1), z2, z3, z4, z5) → f129_out1
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
K tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
Defined Rule Symbols:
f2_in, U1, f129_in, U2
Defined Pair Symbols:
F2_IN, F129_IN
Compound Symbols:
c, c11, c
(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.
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [2] + x1 + x2
POL(F129_IN(x1, x2, x3, x4, x5)) = x1 + x4
POL(F2_IN(x1)) = x1
POL([]) = 0
POL(c) = 0
POL(c(x1)) = x1
POL(c11(x1)) = x1
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f129_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f129_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f129_in([], z0, z1, z0, z1) → f129_out1
f129_in(.(z0, z1), z2, z3, z4, z5) → U2(f129_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f129_out1, .(z0, z1), z2, z3, z4, z5) → f129_out1
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:none
K tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F129_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F129_IN(.(z0, z1), z2, z3, z4, z5) → c11(F129_IN(z1, z0, .(z2, z3), z4, z5))
Defined Rule Symbols:
f2_in, U1, f129_in, U2
Defined Pair Symbols:
F2_IN, F129_IN
Compound Symbols:
c, c11, c