(0) Obligation:
Clauses:
q(X) :- p(X, 0).
p(0, X1).
p(s(X), Y) :- p(X, s(Y)).
Query: q(g)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
p(0, X1).
q(X) :- p(X, 0).
p(s(X), Y) :- p(X, s(Y)).
Query: q(g)
(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(0)) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(s(s(0)))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(s(0)))))) → f2_out1
f2_in(s(s(s(s(s(s(0))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f117_out1, s(s(s(s(s(s(s(s(z0))))))))) → f2_out1
f117_in(0, z0) → f117_out1
f117_in(s(z0), z1) → U2(f117_in(z0, s(z1)), s(z0), z1)
U2(f117_out1, s(z0), z1) → f117_out1
Tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c8(U1'(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))), F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F117_IN(s(z0), z1) → c11(U2'(f117_in(z0, s(z1)), s(z0), z1), F117_IN(z0, s(z1)))
S tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c8(U1'(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))), F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F117_IN(s(z0), z1) → c11(U2'(f117_in(z0, s(z1)), s(z0), z1), F117_IN(z0, s(z1)))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f117_in, U2
Defined Pair Symbols:
F2_IN, F117_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:
f2_in(0) → f2_out1
f2_in(s(0)) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(s(s(0)))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(s(0)))))) → f2_out1
f2_in(s(s(s(s(s(s(0))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f117_out1, s(s(s(s(s(s(s(s(z0))))))))) → f2_out1
f117_in(0, z0) → f117_out1
f117_in(s(z0), z1) → U2(f117_in(z0, s(z1)), s(z0), z1)
U2(f117_out1, s(z0), z1) → f117_out1
Tuples:
F117_IN(s(z0), z1) → c11(U2'(f117_in(z0, s(z1)), s(z0), z1), F117_IN(z0, s(z1)))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(U1'(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
S tuples:
F117_IN(s(z0), z1) → c11(U2'(f117_in(z0, s(z1)), s(z0), z1), F117_IN(z0, s(z1)))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(U1'(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f117_in, U2
Defined Pair Symbols:
F117_IN, F2_IN
Compound Symbols:
c11, c
(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(0)) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(s(s(0)))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(s(0)))))) → f2_out1
f2_in(s(s(s(s(s(s(0))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f117_out1, s(s(s(s(s(s(s(s(z0))))))))) → f2_out1
f117_in(0, z0) → f117_out1
f117_in(s(z0), z1) → U2(f117_in(z0, s(z1)), s(z0), z1)
U2(f117_out1, s(z0), z1) → f117_out1
Tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
S tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, f117_in, U2
Defined Pair Symbols:
F2_IN, F117_IN
Compound Symbols:
c, c11, c
(9) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(0)) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(s(s(0)))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(s(0)))))) → f2_out1
f2_in(s(s(s(s(s(s(0))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f117_out1, s(s(s(s(s(s(s(s(z0))))))))) → f2_out1
f117_in(0, z0) → f117_out1
f117_in(s(z0), z1) → U2(f117_in(z0, s(z1)), s(z0), z1)
U2(f117_out1, s(z0), z1) → f117_out1
Tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
S tuples:
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
K tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
Defined Rule Symbols:
f2_in, U1, f117_in, U2
Defined Pair Symbols:
F2_IN, F117_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.
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = [1]
POL(F117_IN(x1, x2)) = [3]x1 + [2]x2
POL(F2_IN(x1)) = [3] + [3]x1
POL(c) = 0
POL(c(x1)) = x1
POL(c11(x1)) = x1
POL(s(x1)) = [3] + x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(0)) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(s(s(0)))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(s(0)))))) → f2_out1
f2_in(s(s(s(s(s(s(0))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(0)))))))) → f2_out1
f2_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f117_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f117_out1, s(s(s(s(s(s(s(s(z0))))))))) → f2_out1
f117_in(0, z0) → f117_out1
f117_in(s(z0), z1) → U2(f117_in(z0, s(z1)), s(z0), z1)
U2(f117_out1, s(z0), z1) → f117_out1
Tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
S tuples:none
K tuples:
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F117_IN(z0, s(s(s(s(s(s(s(0)))))))))
F2_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F117_IN(s(z0), z1) → c11(F117_IN(z0, s(z1)))
Defined Rule Symbols:
f2_in, U1, f117_in, U2
Defined Pair Symbols:
F2_IN, F117_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:
f1_in(0) → f1_out1
f1_in(s(0)) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(0)))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(s(0)))))) → f1_out1
f1_in(s(s(s(s(s(s(0))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(0)))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f125_out1, s(s(s(s(s(s(s(s(z0))))))))) → f1_out1
f125_in(0, z0) → f125_out1
f125_in(s(z0), z1) → U2(f125_in(z0, s(z1)), s(z0), z1)
U2(f125_out1, s(z0), z1) → f125_out1
Tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c8(U1'(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))), F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F125_IN(s(z0), z1) → c11(U2'(f125_in(z0, s(z1)), s(z0), z1), F125_IN(z0, s(z1)))
S tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c8(U1'(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))), F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F125_IN(s(z0), z1) → c11(U2'(f125_in(z0, s(z1)), s(z0), z1), F125_IN(z0, s(z1)))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f125_in, U2
Defined Pair Symbols:
F1_IN, F125_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:
f1_in(0) → f1_out1
f1_in(s(0)) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(0)))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(s(0)))))) → f1_out1
f1_in(s(s(s(s(s(s(0))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(0)))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f125_out1, s(s(s(s(s(s(s(s(z0))))))))) → f1_out1
f125_in(0, z0) → f125_out1
f125_in(s(z0), z1) → U2(f125_in(z0, s(z1)), s(z0), z1)
U2(f125_out1, s(z0), z1) → f125_out1
Tuples:
F125_IN(s(z0), z1) → c11(U2'(f125_in(z0, s(z1)), s(z0), z1), F125_IN(z0, s(z1)))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(U1'(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
S tuples:
F125_IN(s(z0), z1) → c11(U2'(f125_in(z0, s(z1)), s(z0), z1), F125_IN(z0, s(z1)))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(U1'(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0))))))))))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f125_in, U2
Defined Pair Symbols:
F125_IN, F1_IN
Compound Symbols:
c11, c
(19) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(0)))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(s(0)))))) → f1_out1
f1_in(s(s(s(s(s(s(0))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(0)))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f125_out1, s(s(s(s(s(s(s(s(z0))))))))) → f1_out1
f125_in(0, z0) → f125_out1
f125_in(s(z0), z1) → U2(f125_in(z0, s(z1)), s(z0), z1)
U2(f125_out1, s(z0), z1) → f125_out1
Tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
S tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, f125_in, U2
Defined Pair Symbols:
F1_IN, F125_IN
Compound Symbols:
c, c11, c
(21) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(0)))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(s(0)))))) → f1_out1
f1_in(s(s(s(s(s(s(0))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(0)))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f125_out1, s(s(s(s(s(s(s(s(z0))))))))) → f1_out1
f125_in(0, z0) → f125_out1
f125_in(s(z0), z1) → U2(f125_in(z0, s(z1)), s(z0), z1)
U2(f125_out1, s(z0), z1) → f125_out1
Tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
S tuples:
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
K tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
Defined Rule Symbols:
f1_in, U1, f125_in, U2
Defined Pair Symbols:
F1_IN, F125_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.
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = [1]
POL(F125_IN(x1, x2)) = [3]x1 + [2]x2
POL(F1_IN(x1)) = [3] + [3]x1
POL(c) = 0
POL(c(x1)) = x1
POL(c11(x1)) = x1
POL(s(x1)) = [3] + x1
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(0)) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(0)))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(s(0)))))) → f1_out1
f1_in(s(s(s(s(s(s(0))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(0)))))))) → f1_out1
f1_in(s(s(s(s(s(s(s(s(z0))))))))) → U1(f125_in(z0, s(s(s(s(s(s(s(0)))))))), s(s(s(s(s(s(s(s(z0)))))))))
U1(f125_out1, s(s(s(s(s(s(s(s(z0))))))))) → f1_out1
f125_in(0, z0) → f125_out1
f125_in(s(z0), z1) → U2(f125_in(z0, s(z1)), s(z0), z1)
U2(f125_out1, s(z0), z1) → f125_out1
Tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
S tuples:none
K tuples:
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F125_IN(z0, s(s(s(s(s(s(s(0)))))))))
F1_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F125_IN(s(z0), z1) → c11(F125_IN(z0, s(z1)))
Defined Rule Symbols:
f1_in, U1, f125_in, U2
Defined Pair Symbols:
F1_IN, F125_IN
Compound Symbols:
c, c11, c