(0) Obligation:
Clauses:
f(c(s(X), Y)) :- f(c(X, s(Y))).
g(c(X, s(Y))) :- g(c(s(X), Y)).
h(X) :- ','(f(X), g(X)).
Query: h(g)
(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
f12_in(c(z0, s(z1))) → U3(f12_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f12_out1, c(z0, s(z1))) → f12_out1
f6_in(z0) → U4(f10_in(z0), z0)
U4(f10_out1, z0) → U5(f12_in(z0), z0)
U5(f12_out1, z0) → f6_out1
Tuples:
F2_IN(z0) → c1(U1'(f6_in(z0), z0), F6_IN(z0))
F10_IN(c(s(z0), z1)) → c3(U2'(f10_in(c(z0, s(z1))), c(s(z0), z1)), F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(U3'(f12_in(c(s(z0), z1)), c(z0, s(z1))), F12_IN(c(s(z0), z1)))
F6_IN(z0) → c7(U4'(f10_in(z0), z0), F10_IN(z0))
U4'(f10_out1, z0) → c8(U5'(f12_in(z0), z0), F12_IN(z0))
S tuples:
F2_IN(z0) → c1(U1'(f6_in(z0), z0), F6_IN(z0))
F10_IN(c(s(z0), z1)) → c3(U2'(f10_in(c(z0, s(z1))), c(s(z0), z1)), F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(U3'(f12_in(c(s(z0), z1)), c(z0, s(z1))), F12_IN(c(s(z0), z1)))
F6_IN(z0) → c7(U4'(f10_in(z0), z0), F10_IN(z0))
U4'(f10_out1, z0) → c8(U5'(f12_in(z0), z0), F12_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f10_in, U2, f12_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F2_IN, F10_IN, F12_IN, F6_IN, U4'
Compound Symbols:
c1, c3, c5, c7, c8
(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
f12_in(c(z0, s(z1))) → U3(f12_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f12_out1, c(z0, s(z1))) → f12_out1
f6_in(z0) → U4(f10_in(z0), z0)
U4(f10_out1, z0) → U5(f12_in(z0), z0)
U5(f12_out1, z0) → f6_out1
Tuples:
F10_IN(c(s(z0), z1)) → c3(U2'(f10_in(c(z0, s(z1))), c(s(z0), z1)), F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(U3'(f12_in(c(s(z0), z1)), c(z0, s(z1))), F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2(U1'(f6_in(z0), z0))
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(U5'(f12_in(z0), z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
S tuples:
F10_IN(c(s(z0), z1)) → c3(U2'(f10_in(c(z0, s(z1))), c(s(z0), z1)), F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(U3'(f12_in(c(s(z0), z1)), c(z0, s(z1))), F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2(U1'(f6_in(z0), z0))
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(U5'(f12_in(z0), z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f10_in, U2, f12_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F10_IN, F12_IN, F2_IN, F6_IN, U4'
Compound Symbols:
c3, c5, c2
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
f12_in(c(z0, s(z1))) → U3(f12_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f12_out1, c(z0, s(z1))) → f12_out1
f6_in(z0) → U4(f10_in(z0), z0)
U4(f10_out1, z0) → U5(f12_in(z0), z0)
U5(f12_out1, z0) → f6_out1
Tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
S tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
K tuples:none
Defined Rule Symbols:
f2_in, U1, f10_in, U2, f12_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F2_IN, F6_IN, U4', F10_IN, F12_IN
Compound Symbols:
c2, c3, c5, c2
(7) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
U4'(f10_out1, z0) → c2
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
f12_in(c(z0, s(z1))) → U3(f12_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f12_out1, c(z0, s(z1))) → f12_out1
f6_in(z0) → U4(f10_in(z0), z0)
U4(f10_out1, z0) → U5(f12_in(z0), z0)
U5(f12_out1, z0) → f6_out1
Tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
S tuples:
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
K tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
Defined Rule Symbols:
f2_in, U1, f10_in, U2, f12_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F2_IN, F6_IN, U4', F10_IN, F12_IN
Compound Symbols:
c2, c3, c5, c2
(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
We considered the (Usable) Rules:
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
And the Tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F10_IN(x1)) = [1] + x1
POL(F12_IN(x1)) = [1]
POL(F2_IN(x1)) = [2] + [2]x1
POL(F6_IN(x1)) = [2] + [2]x1
POL(U2(x1, x2)) = 0
POL(U4'(x1, x2)) = [2]
POL(c(x1, x2)) = x1
POL(c2) = 0
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c5(x1)) = x1
POL(f10_in(x1)) = [2]x1
POL(f10_out1) = 0
POL(s(x1)) = [2] + x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
f12_in(c(z0, s(z1))) → U3(f12_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f12_out1, c(z0, s(z1))) → f12_out1
f6_in(z0) → U4(f10_in(z0), z0)
U4(f10_out1, z0) → U5(f12_in(z0), z0)
U5(f12_out1, z0) → f6_out1
Tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
S tuples:
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
K tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
Defined Rule Symbols:
f2_in, U1, f10_in, U2, f12_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F2_IN, F6_IN, U4', F10_IN, F12_IN
Compound Symbols:
c2, c3, c5, c2
(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.
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
We considered the (Usable) Rules:
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
And the Tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F10_IN(x1)) = 0
POL(F12_IN(x1)) = [1] + x1
POL(F2_IN(x1)) = [3] + x1
POL(F6_IN(x1)) = [3] + x1
POL(U2(x1, x2)) = [2] + [2]x2
POL(U4'(x1, x2)) = [2] + x2
POL(c(x1, x2)) = x2
POL(c2) = 0
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c5(x1)) = x1
POL(f10_in(x1)) = [3] + [2]x1
POL(f10_out1) = 0
POL(s(x1)) = [2] + x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f10_in(c(s(z0), z1)) → U2(f10_in(c(z0, s(z1))), c(s(z0), z1))
U2(f10_out1, c(s(z0), z1)) → f10_out1
f12_in(c(z0, s(z1))) → U3(f12_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f12_out1, c(z0, s(z1))) → f12_out1
f6_in(z0) → U4(f10_in(z0), z0)
U4(f10_out1, z0) → U5(f12_in(z0), z0)
U5(f12_out1, z0) → f6_out1
Tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
S tuples:none
K tuples:
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f10_in(z0), z0))
F6_IN(z0) → c2(F10_IN(z0))
U4'(f10_out1, z0) → c2(F12_IN(z0))
F2_IN(z0) → c2
U4'(f10_out1, z0) → c2
F10_IN(c(s(z0), z1)) → c3(F10_IN(c(z0, s(z1))))
F12_IN(c(z0, s(z1))) → c5(F12_IN(c(s(z0), z1)))
Defined Rule Symbols:
f2_in, U1, f10_in, U2, f12_in, U3, f6_in, U4, U5
Defined Pair Symbols:
F2_IN, F6_IN, U4', F10_IN, F12_IN
Compound Symbols:
c2, c3, c5, c2
(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:
f1_in(c(s(z0), z1)) → U1(f8_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(s(z0), z1)) → f1_out1
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
f13_in(z0, s(z1)) → U3(f13_in(s(z0), z1), z0, s(z1))
U3(f13_out1, z0, s(z1)) → f13_out1
f8_in(z0, z1) → U4(f11_in(z0, z1), z0, z1)
U4(f11_out1, z0, z1) → U5(f13_in(z0, z1), z0, z1)
U5(f13_out1, z0, z1) → f8_out1
Tuples:
F1_IN(c(s(z0), z1)) → c1(U1'(f8_in(z0, z1), c(s(z0), z1)), F8_IN(z0, z1))
F11_IN(s(z0), z1) → c3(U2'(f11_in(z0, s(z1)), s(z0), z1), F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(U3'(f13_in(s(z0), z1), z0, s(z1)), F13_IN(s(z0), z1))
F8_IN(z0, z1) → c7(U4'(f11_in(z0, z1), z0, z1), F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c8(U5'(f13_in(z0, z1), z0, z1), F13_IN(z0, z1))
S tuples:
F1_IN(c(s(z0), z1)) → c1(U1'(f8_in(z0, z1), c(s(z0), z1)), F8_IN(z0, z1))
F11_IN(s(z0), z1) → c3(U2'(f11_in(z0, s(z1)), s(z0), z1), F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(U3'(f13_in(s(z0), z1), z0, s(z1)), F13_IN(s(z0), z1))
F8_IN(z0, z1) → c7(U4'(f11_in(z0, z1), z0, z1), F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c8(U5'(f13_in(z0, z1), z0, z1), F13_IN(z0, z1))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f11_in, U2, f13_in, U3, f8_in, U4, U5
Defined Pair Symbols:
F1_IN, F11_IN, F13_IN, F8_IN, U4'
Compound Symbols:
c1, c3, c5, c7, c8
(17) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(c(s(z0), z1)) → U1(f8_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(s(z0), z1)) → f1_out1
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
f13_in(z0, s(z1)) → U3(f13_in(s(z0), z1), z0, s(z1))
U3(f13_out1, z0, s(z1)) → f13_out1
f8_in(z0, z1) → U4(f11_in(z0, z1), z0, z1)
U4(f11_out1, z0, z1) → U5(f13_in(z0, z1), z0, z1)
U5(f13_out1, z0, z1) → f8_out1
Tuples:
F11_IN(s(z0), z1) → c3(U2'(f11_in(z0, s(z1)), s(z0), z1), F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(U3'(f13_in(s(z0), z1), z0, s(z1)), F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2(U1'(f8_in(z0, z1), c(s(z0), z1)))
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(U5'(f13_in(z0, z1), z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
S tuples:
F11_IN(s(z0), z1) → c3(U2'(f11_in(z0, s(z1)), s(z0), z1), F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(U3'(f13_in(s(z0), z1), z0, s(z1)), F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2(U1'(f8_in(z0, z1), c(s(z0), z1)))
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(U5'(f13_in(z0, z1), z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f11_in, U2, f13_in, U3, f8_in, U4, U5
Defined Pair Symbols:
F11_IN, F13_IN, F1_IN, F8_IN, U4'
Compound Symbols:
c3, c5, c2
(19) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(c(s(z0), z1)) → U1(f8_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(s(z0), z1)) → f1_out1
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
f13_in(z0, s(z1)) → U3(f13_in(s(z0), z1), z0, s(z1))
U3(f13_out1, z0, s(z1)) → f13_out1
f8_in(z0, z1) → U4(f11_in(z0, z1), z0, z1)
U4(f11_out1, z0, z1) → U5(f13_in(z0, z1), z0, z1)
U5(f13_out1, z0, z1) → f8_out1
Tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
S tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
K tuples:none
Defined Rule Symbols:
f1_in, U1, f11_in, U2, f13_in, U3, f8_in, U4, U5
Defined Pair Symbols:
F1_IN, F8_IN, U4', F11_IN, F13_IN
Compound Symbols:
c2, c3, c5, c2
(21) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(c(s(z0), z1)) → U1(f8_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(s(z0), z1)) → f1_out1
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
f13_in(z0, s(z1)) → U3(f13_in(s(z0), z1), z0, s(z1))
U3(f13_out1, z0, s(z1)) → f13_out1
f8_in(z0, z1) → U4(f11_in(z0, z1), z0, z1)
U4(f11_out1, z0, z1) → U5(f13_in(z0, z1), z0, z1)
U5(f13_out1, z0, z1) → f8_out1
Tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
S tuples:
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
K tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
Defined Rule Symbols:
f1_in, U1, f11_in, U2, f13_in, U3, f8_in, U4, U5
Defined Pair Symbols:
F1_IN, F8_IN, U4', F11_IN, F13_IN
Compound Symbols:
c2, c3, c5, c2
(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
We considered the (Usable) Rules:
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
And the Tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F11_IN(x1, x2)) = [2]
POL(F13_IN(x1, x2)) = [2]x2
POL(F1_IN(x1)) = [3] + [3]x1
POL(F8_IN(x1, x2)) = [3] + [3]x2
POL(U2(x1, x2, x3)) = 0
POL(U4'(x1, x2, x3)) = [2]x3
POL(c(x1, x2)) = x2
POL(c2) = 0
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c5(x1)) = x1
POL(f11_in(x1, x2)) = 0
POL(f11_out1) = 0
POL(s(x1)) = [3] + x1
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(c(s(z0), z1)) → U1(f8_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(s(z0), z1)) → f1_out1
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
f13_in(z0, s(z1)) → U3(f13_in(s(z0), z1), z0, s(z1))
U3(f13_out1, z0, s(z1)) → f13_out1
f8_in(z0, z1) → U4(f11_in(z0, z1), z0, z1)
U4(f11_out1, z0, z1) → U5(f13_in(z0, z1), z0, z1)
U5(f13_out1, z0, z1) → f8_out1
Tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
S tuples:
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
K tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
Defined Rule Symbols:
f1_in, U1, f11_in, U2, f13_in, U3, f8_in, U4, U5
Defined Pair Symbols:
F1_IN, F8_IN, U4', F11_IN, F13_IN
Compound Symbols:
c2, c3, c5, c2
(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.
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
We considered the (Usable) Rules:
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
And the Tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F11_IN(x1, x2)) = x1
POL(F13_IN(x1, x2)) = 0
POL(F1_IN(x1)) = [1] + [2]x1
POL(F8_IN(x1, x2)) = x1 + x2
POL(U2(x1, x2, x3)) = 0
POL(U4'(x1, x2, x3)) = x2 + x3
POL(c(x1, x2)) = x1 + x2
POL(c2) = 0
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c5(x1)) = x1
POL(f11_in(x1, x2)) = 0
POL(f11_out1) = 0
POL(s(x1)) = [1] + x1
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(c(s(z0), z1)) → U1(f8_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(s(z0), z1)) → f1_out1
f11_in(s(z0), z1) → U2(f11_in(z0, s(z1)), s(z0), z1)
U2(f11_out1, s(z0), z1) → f11_out1
f13_in(z0, s(z1)) → U3(f13_in(s(z0), z1), z0, s(z1))
U3(f13_out1, z0, s(z1)) → f13_out1
f8_in(z0, z1) → U4(f11_in(z0, z1), z0, z1)
U4(f11_out1, z0, z1) → U5(f13_in(z0, z1), z0, z1)
U5(f13_out1, z0, z1) → f8_out1
Tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
S tuples:none
K tuples:
F1_IN(c(s(z0), z1)) → c2(F8_IN(z0, z1))
F8_IN(z0, z1) → c2(U4'(f11_in(z0, z1), z0, z1))
F8_IN(z0, z1) → c2(F11_IN(z0, z1))
U4'(f11_out1, z0, z1) → c2(F13_IN(z0, z1))
F1_IN(c(s(z0), z1)) → c2
U4'(f11_out1, z0, z1) → c2
F13_IN(z0, s(z1)) → c5(F13_IN(s(z0), z1))
F11_IN(s(z0), z1) → c3(F11_IN(z0, s(z1)))
Defined Rule Symbols:
f1_in, U1, f11_in, U2, f13_in, U3, f8_in, U4, U5
Defined Pair Symbols:
F1_IN, F8_IN, U4', F11_IN, F13_IN
Compound Symbols:
c2, c3, c5, c2