(0) Obligation:
Clauses:
reverse(X1s, X2s) :- reverse(X1s, [], X2s).
reverse([], Xs, Xs).
reverse(.(X, X1s), X2s, Ys) :- reverse(X1s, .(X, X2s), Ys).
Query: reverse(g,a)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
reverse([], Xs, Xs).
reverse(X1s, X2s) :- reverse(X1s, [], X2s).
reverse(.(X, X1s), X2s, Ys) :- reverse(X1s, .(X, X2s), 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:
f1_in([]) → f1_out1([])
f1_in(.(z0, [])) → f1_out1(.(z0, []))
f1_in(.(z0, .(z1, []))) → f1_out1(.(z1, .(z0, [])))
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1(.(z2, .(z1, .(z0, []))))
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f120_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f120_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f1_out1(z0)
f120_in([], z0, z1) → f120_out1(.(z0, z1))
f120_in(.(z0, z1), z2, z3) → U2(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f120_out1(z0), .(z1, z2), z3, z4) → f120_out1(z0)
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f120_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F120_IN(.(z0, z1), z2, z3) → c11(U2'(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F120_IN(z1, z0, .(z2, z3)))
S tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f120_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F120_IN(.(z0, z1), z2, z3) → c11(U2'(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F120_IN(z1, z0, .(z2, z3)))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f120_in, U2
Defined Pair Symbols:
F1_IN, F120_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(.(z0, []))
f1_in(.(z0, .(z1, []))) → f1_out1(.(z1, .(z0, [])))
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1(.(z2, .(z1, .(z0, []))))
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f120_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f120_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f1_out1(z0)
f120_in([], z0, z1) → f120_out1(.(z0, z1))
f120_in(.(z0, z1), z2, z3) → U2(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f120_out1(z0), .(z1, z2), z3, z4) → f120_out1(z0)
Tuples:
F120_IN(.(z0, z1), z2, z3) → c11(U2'(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F120_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f120_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(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
S tuples:
F120_IN(.(z0, z1), z2, z3) → c11(U2'(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F120_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f120_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(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f120_in, U2
Defined Pair Symbols:
F120_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(.(z0, []))
f1_in(.(z0, .(z1, []))) → f1_out1(.(z1, .(z0, [])))
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1(.(z2, .(z1, .(z0, []))))
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f120_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f120_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f1_out1(z0)
f120_in([], z0, z1) → f120_out1(.(z0, z1))
f120_in(.(z0, z1), z2, z3) → U2(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f120_out1(z0), .(z1, z2), z3, z4) → f120_out1(z0)
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, f120_in, U2
Defined Pair Symbols:
F1_IN, F120_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(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
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(.(z0, []))
f1_in(.(z0, .(z1, []))) → f1_out1(.(z1, .(z0, [])))
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1(.(z2, .(z1, .(z0, []))))
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f120_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f120_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f1_out1(z0)
f120_in([], z0, z1) → f120_out1(.(z0, z1))
f120_in(.(z0, z1), z2, z3) → U2(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f120_out1(z0), .(z1, z2), z3, z4) → f120_out1(z0)
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
K tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
Defined Rule Symbols:
f1_in, U1, f120_in, U2
Defined Pair Symbols:
F1_IN, F120_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.
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [3] + x2
POL(F120_IN(x1, x2, x3)) = [3]x1 + x3
POL(F1_IN(x1)) = [3]x1
POL([]) = [2]
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(.(z0, []))
f1_in(.(z0, .(z1, []))) → f1_out1(.(z1, .(z0, [])))
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1(.(z2, .(z1, .(z0, []))))
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f120_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f120_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f1_out1(z0)
f120_in([], z0, z1) → f120_out1(.(z0, z1))
f120_in(.(z0, z1), z2, z3) → U2(f120_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f120_out1(z0), .(z1, z2), z3, z4) → f120_out1(z0)
Tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:none
K tuples:
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F120_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F120_IN(.(z0, z1), z2, z3) → c11(F120_IN(z1, z0, .(z2, z3)))
Defined Rule Symbols:
f1_in, U1, f120_in, U2
Defined Pair Symbols:
F1_IN, F120_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(.(z0, []))
f2_in(.(z0, .(z1, []))) → f2_out1(.(z1, .(z0, [])))
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1(.(z2, .(z1, .(z0, []))))
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f119_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f119_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f2_out1(z0)
f119_in([], z0, z1) → f119_out1(.(z0, z1))
f119_in(.(z0, z1), z2, z3) → U2(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f119_out1(z0), .(z1, z2), z3, z4) → f119_out1(z0)
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f119_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F119_IN(.(z0, z1), z2, z3) → c11(U2'(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F119_IN(z1, z0, .(z2, z3)))
S tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f119_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F119_IN(.(z0, z1), z2, z3) → c11(U2'(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F119_IN(z1, z0, .(z2, z3)))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f119_in, U2
Defined Pair Symbols:
F2_IN, F119_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(.(z0, []))
f2_in(.(z0, .(z1, []))) → f2_out1(.(z1, .(z0, [])))
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1(.(z2, .(z1, .(z0, []))))
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f119_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f119_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f2_out1(z0)
f119_in([], z0, z1) → f119_out1(.(z0, z1))
f119_in(.(z0, z1), z2, z3) → U2(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f119_out1(z0), .(z1, z2), z3, z4) → f119_out1(z0)
Tuples:
F119_IN(.(z0, z1), z2, z3) → c11(U2'(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F119_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f119_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(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
S tuples:
F119_IN(.(z0, z1), z2, z3) → c11(U2'(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F119_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f119_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(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f119_in, U2
Defined Pair Symbols:
F119_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(.(z0, []))
f2_in(.(z0, .(z1, []))) → f2_out1(.(z1, .(z0, [])))
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1(.(z2, .(z1, .(z0, []))))
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f119_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f119_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f2_out1(z0)
f119_in([], z0, z1) → f119_out1(.(z0, z1))
f119_in(.(z0, z1), z2, z3) → U2(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f119_out1(z0), .(z1, z2), z3, z4) → f119_out1(z0)
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, f119_in, U2
Defined Pair Symbols:
F2_IN, F119_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(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
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(.(z0, []))
f2_in(.(z0, .(z1, []))) → f2_out1(.(z1, .(z0, [])))
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1(.(z2, .(z1, .(z0, []))))
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f119_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f119_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f2_out1(z0)
f119_in([], z0, z1) → f119_out1(.(z0, z1))
f119_in(.(z0, z1), z2, z3) → U2(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f119_out1(z0), .(z1, z2), z3, z4) → f119_out1(z0)
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
K tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
Defined Rule Symbols:
f2_in, U1, f119_in, U2
Defined Pair Symbols:
F2_IN, F119_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.
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [3] + x2
POL(F119_IN(x1, x2, x3)) = [3]x1 + x3
POL(F2_IN(x1)) = [3]x1
POL([]) = [2]
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(.(z0, []))
f2_in(.(z0, .(z1, []))) → f2_out1(.(z1, .(z0, [])))
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1(.(z2, .(z1, .(z0, []))))
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1(.(z3, .(z2, .(z1, .(z0, [])))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1(.(z4, .(z3, .(z2, .(z1, .(z0, []))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1(.(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1(.(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))))
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f119_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f119_out1(z0), .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, .(z8, z9))))))))) → f2_out1(z0)
f119_in([], z0, z1) → f119_out1(.(z0, z1))
f119_in(.(z0, z1), z2, z3) → U2(f119_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f119_out1(z0), .(z1, z2), z3, z4) → f119_out1(z0)
Tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
S tuples:none
K tuples:
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F119_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F119_IN(.(z0, z1), z2, z3) → c11(F119_IN(z1, z0, .(z2, z3)))
Defined Rule Symbols:
f2_in, U1, f119_in, U2
Defined Pair Symbols:
F2_IN, F119_IN
Compound Symbols:
c, c11, c