(0) Obligation:
Clauses:
p(s(0), 0).
p(s(s(X)), s(s(Y))) :- p(s(X), s(Y)).
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- ','(p(s(X), U), plus(U, Y, Z)).
Query: plus(g,a,a)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
p(s(0), 0).
plus(0, Y, Y).
p(s(s(X)), s(s(Y))) :- p(s(X), s(Y)).
plus(s(X), Y, s(Z)) :- ','(p(s(X), U), plus(U, Y, Z)).
Query: plus(g,a,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(0) → f2_out1
f2_in(s(z0)) → U1(f17_in(z0), s(z0))
U1(f17_out1(z0), s(z1)) → f2_out1
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
f17_in(z0) → U4(f23_in(z0), z0)
U4(f23_out1(z0), z1) → U5(f2_in(z0), z1, z0)
U5(f2_out1, z0, z1) → f17_out1(z1)
Tuples:
F2_IN(s(z0)) → c1(U1'(f17_in(z0), s(z0)), F17_IN(z0))
F38_IN(s(z0)) → c3(U2'(f38_in(z0), s(z0)), F38_IN(z0))
F23_IN(s(z0)) → c6(U3'(f38_in(z0), s(z0)), F38_IN(z0))
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
U4'(f23_out1(z0), z1) → c9(U5'(f2_in(z0), z1, z0), F2_IN(z0))
S tuples:
F2_IN(s(z0)) → c1(U1'(f17_in(z0), s(z0)), F17_IN(z0))
F38_IN(s(z0)) → c3(U2'(f38_in(z0), s(z0)), F38_IN(z0))
F23_IN(s(z0)) → c6(U3'(f38_in(z0), s(z0)), F38_IN(z0))
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
U4'(f23_out1(z0), z1) → c9(U5'(f2_in(z0), z1, z0), F2_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f38_in, U2, f23_in, U3, f17_in, U4, U5
Defined Pair Symbols:
F2_IN, F38_IN, F23_IN, F17_IN, U4'
Compound Symbols:
c1, c3, c6, c8, c9
(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(0) → f2_out1
f2_in(s(z0)) → U1(f17_in(z0), s(z0))
U1(f17_out1(z0), s(z1)) → f2_out1
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
f17_in(z0) → U4(f23_in(z0), z0)
U4(f23_out1(z0), z1) → U5(f2_in(z0), z1, z0)
U5(f2_out1, z0, z1) → f17_out1(z1)
Tuples:
F2_IN(s(z0)) → c1(U1'(f17_in(z0), s(z0)), F17_IN(z0))
F38_IN(s(z0)) → c3(U2'(f38_in(z0), s(z0)), F38_IN(z0))
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
U4'(f23_out1(z0), z1) → c9(U5'(f2_in(z0), z1, z0), F2_IN(z0))
F23_IN(s(z0)) → c(U3'(f38_in(z0), s(z0)))
F23_IN(s(z0)) → c(F38_IN(z0))
S tuples:
F2_IN(s(z0)) → c1(U1'(f17_in(z0), s(z0)), F17_IN(z0))
F38_IN(s(z0)) → c3(U2'(f38_in(z0), s(z0)), F38_IN(z0))
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
U4'(f23_out1(z0), z1) → c9(U5'(f2_in(z0), z1, z0), F2_IN(z0))
F23_IN(s(z0)) → c(U3'(f38_in(z0), s(z0)))
F23_IN(s(z0)) → c(F38_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f38_in, U2, f23_in, U3, f17_in, U4, U5
Defined Pair Symbols:
F2_IN, F38_IN, F17_IN, U4', F23_IN
Compound Symbols:
c1, c3, c8, c9, c
(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f17_in(z0), s(z0))
U1(f17_out1(z0), s(z1)) → f2_out1
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
f17_in(z0) → U4(f23_in(z0), z0)
U4(f23_out1(z0), z1) → U5(f2_in(z0), z1, z0)
U5(f2_out1, z0, z1) → f17_out1(z1)
Tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F2_IN(s(z0)) → c1(F17_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
S tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F2_IN(s(z0)) → c1(F17_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, f38_in, U2, f23_in, U3, f17_in, U4, U5
Defined Pair Symbols:
F17_IN, F23_IN, F2_IN, F38_IN, U4'
Compound Symbols:
c8, c, c1, c3, c9, c
(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.
F2_IN(s(z0)) → c1(F17_IN(z0))
We considered the (Usable) Rules:
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
And the Tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F2_IN(s(z0)) → c1(F17_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(F17_IN(x1)) = 0
POL(F23_IN(x1)) = 0
POL(F2_IN(x1)) = x1
POL(F38_IN(x1)) = 0
POL(U2(x1, x2)) = [2]x1
POL(U3(x1, x2)) = x1
POL(U4'(x1, x2)) = [2]x1
POL(c) = 0
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c3(x1)) = x1
POL(c8(x1, x2)) = x1 + x2
POL(c9(x1)) = x1
POL(f23_in(x1)) = 0
POL(f23_out1(x1)) = x1
POL(f38_in(x1)) = 0
POL(f38_out1(x1)) = [1] + x1
POL(s(x1)) = [1]
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f17_in(z0), s(z0))
U1(f17_out1(z0), s(z1)) → f2_out1
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
f17_in(z0) → U4(f23_in(z0), z0)
U4(f23_out1(z0), z1) → U5(f2_in(z0), z1, z0)
U5(f2_out1, z0, z1) → f17_out1(z1)
Tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F2_IN(s(z0)) → c1(F17_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
S tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
K tuples:
F2_IN(s(z0)) → c1(F17_IN(z0))
Defined Rule Symbols:
f2_in, U1, f38_in, U2, f23_in, U3, f17_in, U4, U5
Defined Pair Symbols:
F17_IN, F23_IN, F2_IN, F38_IN, U4'
Compound Symbols:
c8, c, c1, c3, c9, c
(11) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
F23_IN(s(z0)) → c(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
F2_IN(s(z0)) → c1(F17_IN(z0))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f17_in(z0), s(z0))
U1(f17_out1(z0), s(z1)) → f2_out1
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
f17_in(z0) → U4(f23_in(z0), z0)
U4(f23_out1(z0), z1) → U5(f2_in(z0), z1, z0)
U5(f2_out1, z0, z1) → f17_out1(z1)
Tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F2_IN(s(z0)) → c1(F17_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
S tuples:
F38_IN(s(z0)) → c3(F38_IN(z0))
K tuples:
F2_IN(s(z0)) → c1(F17_IN(z0))
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
Defined Rule Symbols:
f2_in, U1, f38_in, U2, f23_in, U3, f17_in, U4, U5
Defined Pair Symbols:
F17_IN, F23_IN, F2_IN, F38_IN, U4'
Compound Symbols:
c8, c, c1, c3, c9, c
(13) 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.
F38_IN(s(z0)) → c3(F38_IN(z0))
We considered the (Usable) Rules:
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
And the Tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F2_IN(s(z0)) → c1(F17_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = [1]
POL(F17_IN(x1)) = [2] + x1
POL(F23_IN(x1)) = x1
POL(F2_IN(x1)) = [2]x1
POL(F38_IN(x1)) = [2] + x1
POL(U2(x1, x2)) = [2]x1
POL(U3(x1, x2)) = [1] + x1
POL(U4'(x1, x2)) = [2]x1
POL(c) = 0
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c3(x1)) = x1
POL(c8(x1, x2)) = x1 + x2
POL(c9(x1)) = x1
POL(f23_in(x1)) = [1]
POL(f23_out1(x1)) = x1
POL(f38_in(x1)) = 0
POL(f38_out1(x1)) = [3] + x1
POL(s(x1)) = [2] + x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f17_in(z0), s(z0))
U1(f17_out1(z0), s(z1)) → f2_out1
f38_in(s(z0)) → U2(f38_in(z0), s(z0))
U2(f38_out1(z0), s(z1)) → f38_out1(s(z0))
f23_in(0) → f23_out1(0)
f23_in(s(z0)) → U3(f38_in(z0), s(z0))
U3(f38_out1(z0), s(z1)) → f23_out1(s(s(z0)))
f17_in(z0) → U4(f23_in(z0), z0)
U4(f23_out1(z0), z1) → U5(f2_in(z0), z1, z0)
U5(f2_out1, z0, z1) → f17_out1(z1)
Tuples:
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
F2_IN(s(z0)) → c1(F17_IN(z0))
F38_IN(s(z0)) → c3(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
S tuples:none
K tuples:
F2_IN(s(z0)) → c1(F17_IN(z0))
F17_IN(z0) → c8(U4'(f23_in(z0), z0), F23_IN(z0))
F23_IN(s(z0)) → c(F38_IN(z0))
U4'(f23_out1(z0), z1) → c9(F2_IN(z0))
F23_IN(s(z0)) → c
F38_IN(s(z0)) → c3(F38_IN(z0))
Defined Rule Symbols:
f2_in, U1, f38_in, U2, f23_in, U3, f17_in, U4, U5
Defined Pair Symbols:
F17_IN, F23_IN, F2_IN, F38_IN, U4'
Compound Symbols:
c8, c, c1, c3, c9, c
(15) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(16) BOUNDS(O(1), O(1))
(17) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → U1(f16_in, s(0))
f1_in(s(s(z0))) → U2(f36_in(z0), s(s(z0)))
U1(f16_out1, s(0)) → f1_out1
U1(f16_out2(z0), s(0)) → f1_out1
U2(f36_out1(z0), s(s(z1))) → f1_out1
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
f20_in → f20_out1
f36_in(z0) → U4(f40_in(z0), z0)
U4(f40_out1(z0), z1) → U5(f1_in(s(s(z0))), z1, z0)
U5(f1_out1, z0, z1) → f36_out1(z1)
f16_in → U6(f20_in, f21_in)
U6(f20_out1, z0) → f16_out1
U6(z0, f21_out1(z1)) → f16_out2(z1)
Tuples:
F1_IN(s(0)) → c1(U1'(f16_in, s(0)), F16_IN)
F1_IN(s(s(z0))) → c2(U2'(f36_in(z0), s(s(z0))), F36_IN(z0))
F40_IN(s(z0)) → c6(U3'(f40_in(z0), s(z0)), F40_IN(z0))
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(U5'(f1_in(s(s(z0))), z1, z0), F1_IN(s(s(z0))))
F16_IN → c12(U6'(f20_in, f21_in), F20_IN)
S tuples:
F1_IN(s(0)) → c1(U1'(f16_in, s(0)), F16_IN)
F1_IN(s(s(z0))) → c2(U2'(f36_in(z0), s(s(z0))), F36_IN(z0))
F40_IN(s(z0)) → c6(U3'(f40_in(z0), s(z0)), F40_IN(z0))
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(U5'(f1_in(s(s(z0))), z1, z0), F1_IN(s(s(z0))))
F16_IN → c12(U6'(f20_in, f21_in), F20_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f40_in, U3, f20_in, f36_in, U4, U5, f16_in, U6
Defined Pair Symbols:
F1_IN, F40_IN, F36_IN, U4', F16_IN
Compound Symbols:
c1, c2, c6, c9, c10, c12
(19) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → U1(f16_in, s(0))
f1_in(s(s(z0))) → U2(f36_in(z0), s(s(z0)))
U1(f16_out1, s(0)) → f1_out1
U1(f16_out2(z0), s(0)) → f1_out1
U2(f36_out1(z0), s(s(z1))) → f1_out1
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
f20_in → f20_out1
f36_in(z0) → U4(f40_in(z0), z0)
U4(f40_out1(z0), z1) → U5(f1_in(s(s(z0))), z1, z0)
U5(f1_out1, z0, z1) → f36_out1(z1)
f16_in → U6(f20_in, f21_in)
U6(f20_out1, z0) → f16_out1
U6(z0, f21_out1(z1)) → f16_out2(z1)
Tuples:
F1_IN(s(s(z0))) → c2(U2'(f36_in(z0), s(s(z0))), F36_IN(z0))
F40_IN(s(z0)) → c6(U3'(f40_in(z0), s(z0)), F40_IN(z0))
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(U5'(f1_in(s(s(z0))), z1, z0), F1_IN(s(s(z0))))
F1_IN(s(0)) → c(U1'(f16_in, s(0)))
F1_IN(s(0)) → c(F16_IN)
F16_IN → c(U6'(f20_in, f21_in))
F16_IN → c(F20_IN)
S tuples:
F1_IN(s(s(z0))) → c2(U2'(f36_in(z0), s(s(z0))), F36_IN(z0))
F40_IN(s(z0)) → c6(U3'(f40_in(z0), s(z0)), F40_IN(z0))
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(U5'(f1_in(s(s(z0))), z1, z0), F1_IN(s(s(z0))))
F1_IN(s(0)) → c(U1'(f16_in, s(0)))
F1_IN(s(0)) → c(F16_IN)
F16_IN → c(U6'(f20_in, f21_in))
F16_IN → c(F20_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f40_in, U3, f20_in, f36_in, U4, U5, f16_in, U6
Defined Pair Symbols:
F1_IN, F40_IN, F36_IN, U4', F16_IN
Compound Symbols:
c2, c6, c9, c10, c
(21) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 6 trailing tuple parts
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → U1(f16_in, s(0))
f1_in(s(s(z0))) → U2(f36_in(z0), s(s(z0)))
U1(f16_out1, s(0)) → f1_out1
U1(f16_out2(z0), s(0)) → f1_out1
U2(f36_out1(z0), s(s(z1))) → f1_out1
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
f20_in → f20_out1
f36_in(z0) → U4(f40_in(z0), z0)
U4(f40_out1(z0), z1) → U5(f1_in(s(s(z0))), z1, z0)
U5(f1_out1, z0, z1) → f36_out1(z1)
f16_in → U6(f20_in, f21_in)
U6(f20_out1, z0) → f16_out1
U6(z0, f21_out1(z1)) → f16_out2(z1)
Tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
S tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f40_in, U3, f20_in, f36_in, U4, U5, f16_in, U6
Defined Pair Symbols:
F36_IN, F1_IN, F40_IN, U4', F16_IN
Compound Symbols:
c9, c, c2, c6, c10, c
(23) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(0)) → c
F16_IN → c
F16_IN → c
F16_IN → c
F16_IN → c
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → U1(f16_in, s(0))
f1_in(s(s(z0))) → U2(f36_in(z0), s(s(z0)))
U1(f16_out1, s(0)) → f1_out1
U1(f16_out2(z0), s(0)) → f1_out1
U2(f36_out1(z0), s(s(z1))) → f1_out1
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
f20_in → f20_out1
f36_in(z0) → U4(f40_in(z0), z0)
U4(f40_out1(z0), z1) → U5(f1_in(s(s(z0))), z1, z0)
U5(f1_out1, z0, z1) → f36_out1(z1)
f16_in → U6(f20_in, f21_in)
U6(f20_out1, z0) → f16_out1
U6(z0, f21_out1(z1)) → f16_out2(z1)
Tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
S tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
K tuples:
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(0)) → c
F16_IN → c
Defined Rule Symbols:
f1_in, U1, U2, f40_in, U3, f20_in, f36_in, U4, U5, f16_in, U6
Defined Pair Symbols:
F36_IN, F1_IN, F40_IN, U4', F16_IN
Compound Symbols:
c9, c, c2, c6, c10, c
(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.
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
We considered the (Usable) Rules:
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
And the Tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(F16_IN) = [1]
POL(F1_IN(x1)) = [1] + x1
POL(F36_IN(x1)) = [2]
POL(F40_IN(x1)) = [1]
POL(U3(x1, x2)) = x1
POL(U4'(x1, x2)) = [2]x1
POL(c) = 0
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c2(x1)) = x1
POL(c6(x1)) = x1
POL(c9(x1, x2)) = x1 + x2
POL(f40_in(x1)) = 0
POL(f40_out1(x1)) = [1]
POL(s(x1)) = [1]
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → U1(f16_in, s(0))
f1_in(s(s(z0))) → U2(f36_in(z0), s(s(z0)))
U1(f16_out1, s(0)) → f1_out1
U1(f16_out2(z0), s(0)) → f1_out1
U2(f36_out1(z0), s(s(z1))) → f1_out1
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
f20_in → f20_out1
f36_in(z0) → U4(f40_in(z0), z0)
U4(f40_out1(z0), z1) → U5(f1_in(s(s(z0))), z1, z0)
U5(f1_out1, z0, z1) → f36_out1(z1)
f16_in → U6(f20_in, f21_in)
U6(f20_out1, z0) → f16_out1
U6(z0, f21_out1(z1)) → f16_out2(z1)
Tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
S tuples:
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
K tuples:
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(0)) → c
F16_IN → c
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
Defined Rule Symbols:
f1_in, U1, U2, f40_in, U3, f20_in, f36_in, U4, U5, f16_in, U6
Defined Pair Symbols:
F36_IN, F1_IN, F40_IN, U4', F16_IN
Compound Symbols:
c9, c, c2, c6, c10, c
(27) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
(28) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → U1(f16_in, s(0))
f1_in(s(s(z0))) → U2(f36_in(z0), s(s(z0)))
U1(f16_out1, s(0)) → f1_out1
U1(f16_out2(z0), s(0)) → f1_out1
U2(f36_out1(z0), s(s(z1))) → f1_out1
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
f20_in → f20_out1
f36_in(z0) → U4(f40_in(z0), z0)
U4(f40_out1(z0), z1) → U5(f1_in(s(s(z0))), z1, z0)
U5(f1_out1, z0, z1) → f36_out1(z1)
f16_in → U6(f20_in, f21_in)
U6(f20_out1, z0) → f16_out1
U6(z0, f21_out1(z1)) → f16_out2(z1)
Tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
S tuples:
F40_IN(s(z0)) → c6(F40_IN(z0))
K tuples:
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(0)) → c
F16_IN → c
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(s(z0))) → c2(F36_IN(z0))
Defined Rule Symbols:
f1_in, U1, U2, f40_in, U3, f20_in, f36_in, U4, U5, f16_in, U6
Defined Pair Symbols:
F36_IN, F1_IN, F40_IN, U4', F16_IN
Compound Symbols:
c9, c, c2, c6, c10, c
(29) 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.
F40_IN(s(z0)) → c6(F40_IN(z0))
We considered the (Usable) Rules:
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
And the Tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = [1]
POL(F16_IN) = 0
POL(F1_IN(x1)) = x1
POL(F36_IN(x1)) = [3] + x1
POL(F40_IN(x1)) = x1
POL(U3(x1, x2)) = [3]x1
POL(U4'(x1, x2)) = [3] + x1
POL(c) = 0
POL(c(x1)) = x1
POL(c10(x1)) = x1
POL(c2(x1)) = x1
POL(c6(x1)) = x1
POL(c9(x1, x2)) = x1 + x2
POL(f40_in(x1)) = 0
POL(f40_out1(x1)) = [2] + x1
POL(s(x1)) = [2] + x1
(30) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → U1(f16_in, s(0))
f1_in(s(s(z0))) → U2(f36_in(z0), s(s(z0)))
U1(f16_out1, s(0)) → f1_out1
U1(f16_out2(z0), s(0)) → f1_out1
U2(f36_out1(z0), s(s(z1))) → f1_out1
f40_in(s(z0)) → U3(f40_in(z0), s(z0))
U3(f40_out1(z0), s(z1)) → f40_out1(s(z0))
f20_in → f20_out1
f36_in(z0) → U4(f40_in(z0), z0)
U4(f40_out1(z0), z1) → U5(f1_in(s(s(z0))), z1, z0)
U5(f1_out1, z0, z1) → f36_out1(z1)
f16_in → U6(f20_in, f21_in)
U6(f20_out1, z0) → f16_out1
U6(z0, f21_out1(z1)) → f16_out2(z1)
Tuples:
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(0)) → c
F16_IN → c
S tuples:none
K tuples:
F1_IN(s(0)) → c(F16_IN)
F1_IN(s(0)) → c
F16_IN → c
F36_IN(z0) → c9(U4'(f40_in(z0), z0), F40_IN(z0))
U4'(f40_out1(z0), z1) → c10(F1_IN(s(s(z0))))
F1_IN(s(s(z0))) → c2(F36_IN(z0))
F40_IN(s(z0)) → c6(F40_IN(z0))
Defined Rule Symbols:
f1_in, U1, U2, f40_in, U3, f20_in, f36_in, U4, U5, f16_in, U6
Defined Pair Symbols:
F36_IN, F1_IN, F40_IN, U4', F16_IN
Compound Symbols:
c9, c, c2, c6, c10, c