(0) Obligation:
Clauses:
even(0).
even(s(s(0))).
even(s(s(s(X)))) :- odd(X).
odd(s(0)).
odd(s(X)) :- even(s(s(X))).
Query: even(g)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
even(0).
even(s(s(0))).
odd(s(0)).
even(s(s(s(X)))) :- odd(X).
odd(s(X)) :- even(s(s(X))).
Query: even(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(s(0))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(z0))))) → U1(f2_in(s(s(z0))), s(s(s(s(z0)))))
U1(f2_out1, s(s(s(s(z0))))) → f2_out1
Tuples:
F2_IN(s(s(s(s(z0))))) → c3(U1'(f2_in(s(s(z0))), s(s(s(s(z0))))), F2_IN(s(s(z0))))
S tuples:
F2_IN(s(s(s(s(z0))))) → c3(U1'(f2_in(s(s(z0))), s(s(s(s(z0))))), F2_IN(s(s(z0))))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c3
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(z0))))) → U1(f2_in(s(s(z0))), s(s(s(s(z0)))))
U1(f2_out1, s(s(s(s(z0))))) → f2_out1
Tuples:
F2_IN(s(s(s(s(z0))))) → c3(F2_IN(s(s(z0))))
S tuples:
F2_IN(s(s(s(s(z0))))) → c3(F2_IN(s(s(z0))))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c3
(7) 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(s(s(s(z0))))) → c3(F2_IN(s(s(z0))))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(s(s(s(s(z0))))) → c3(F2_IN(s(s(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F2_IN(x1)) = [2]x1
POL(c3(x1)) = x1
POL(s(x1)) = [1] + x1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(s(s(s(0))))) → f2_out1
f2_in(s(s(s(s(z0))))) → U1(f2_in(s(s(z0))), s(s(s(s(z0)))))
U1(f2_out1, s(s(s(s(z0))))) → f2_out1
Tuples:
F2_IN(s(s(s(s(z0))))) → c3(F2_IN(s(s(z0))))
S tuples:none
K tuples:
F2_IN(s(s(s(s(z0))))) → c3(F2_IN(s(s(z0))))
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c3
(9) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(10) BOUNDS(O(1), O(1))
(11) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(z0))))) → U1(f1_in(s(s(z0))), s(s(s(s(z0)))))
U1(f1_out1, s(s(s(s(z0))))) → f1_out1
Tuples:
F1_IN(s(s(s(s(z0))))) → c3(U1'(f1_in(s(s(z0))), s(s(s(s(z0))))), F1_IN(s(s(z0))))
S tuples:
F1_IN(s(s(s(s(z0))))) → c3(U1'(f1_in(s(s(z0))), s(s(s(s(z0))))), F1_IN(s(s(z0))))
K tuples:none
Defined Rule Symbols:
f1_in, U1
Defined Pair Symbols:
F1_IN
Compound Symbols:
c3
(13) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(z0))))) → U1(f1_in(s(s(z0))), s(s(s(s(z0)))))
U1(f1_out1, s(s(s(s(z0))))) → f1_out1
Tuples:
F1_IN(s(s(s(s(z0))))) → c3(F1_IN(s(s(z0))))
S tuples:
F1_IN(s(s(s(s(z0))))) → c3(F1_IN(s(s(z0))))
K tuples:none
Defined Rule Symbols:
f1_in, U1
Defined Pair Symbols:
F1_IN
Compound Symbols:
c3
(15) 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.
F1_IN(s(s(s(s(z0))))) → c3(F1_IN(s(s(z0))))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(s(s(s(s(z0))))) → c3(F1_IN(s(s(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F1_IN(x1)) = [2]x1
POL(c3(x1)) = x1
POL(s(x1)) = [1] + x1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(s(s(s(0))))) → f1_out1
f1_in(s(s(s(s(z0))))) → U1(f1_in(s(s(z0))), s(s(s(s(z0)))))
U1(f1_out1, s(s(s(s(z0))))) → f1_out1
Tuples:
F1_IN(s(s(s(s(z0))))) → c3(F1_IN(s(s(z0))))
S tuples:none
K tuples:
F1_IN(s(s(s(s(z0))))) → c3(F1_IN(s(s(z0))))
Defined Rule Symbols:
f1_in, U1
Defined Pair Symbols:
F1_IN
Compound Symbols:
c3