(0) Obligation:
Clauses:
even(0) :- !.
even(N) :- ','(p(N, P), odd(P)).
odd(s(0)) :- !.
odd(N) :- ','(p(N, P), even(P)).
p(0, 0).
p(s(X), X).
Query: even(g)
(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(0)) → U1(f38_in, s(0))
f1_in(s(s(z0))) → U2(f1_in(z0), s(s(z0)))
U1(f38_out1, s(0)) → f1_out1
U1(f38_out2(z0), s(0)) → f1_out1
U2(f1_out1, s(s(z0))) → f1_out1
f41_in → f41_out1
f38_in → U3(f41_in, f43_in)
U3(f41_out1, z0) → f38_out1
U3(z0, f43_out1(z1)) → f38_out2(z1)
Tuples:
F1_IN(s(0)) → c2(U1'(f38_in, s(0)), F38_IN)
F1_IN(s(s(z0))) → c3(U2'(f1_in(z0), s(s(z0))), F1_IN(z0))
F38_IN → c8(U3'(f41_in, f43_in), F41_IN)
S tuples:
F1_IN(s(0)) → c2(U1'(f38_in, s(0)), F38_IN)
F1_IN(s(s(z0))) → c3(U2'(f1_in(z0), s(s(z0))), F1_IN(z0))
F38_IN → c8(U3'(f41_in, f43_in), F41_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f41_in, f38_in, U3
Defined Pair Symbols:
F1_IN, F38_IN
Compound Symbols:
c2, c3, c8
(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(0)) → U1(f38_in, s(0))
f1_in(s(s(z0))) → U2(f1_in(z0), s(s(z0)))
U1(f38_out1, s(0)) → f1_out1
U1(f38_out2(z0), s(0)) → f1_out1
U2(f1_out1, s(s(z0))) → f1_out1
f41_in → f41_out1
f38_in → U3(f41_in, f43_in)
U3(f41_out1, z0) → f38_out1
U3(z0, f43_out1(z1)) → f38_out2(z1)
Tuples:
F1_IN(s(s(z0))) → c3(U2'(f1_in(z0), s(s(z0))), F1_IN(z0))
F1_IN(s(0)) → c(U1'(f38_in, s(0)))
F1_IN(s(0)) → c(F38_IN)
F38_IN → c(U3'(f41_in, f43_in))
F38_IN → c(F41_IN)
S tuples:
F1_IN(s(s(z0))) → c3(U2'(f1_in(z0), s(s(z0))), F1_IN(z0))
F1_IN(s(0)) → c(U1'(f38_in, s(0)))
F1_IN(s(0)) → c(F38_IN)
F38_IN → c(U3'(f41_in, f43_in))
F38_IN → c(F41_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f41_in, f38_in, U3
Defined Pair Symbols:
F1_IN, F38_IN
Compound Symbols:
c3, c
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(0)) → U1(f38_in, s(0))
f1_in(s(s(z0))) → U2(f1_in(z0), s(s(z0)))
U1(f38_out1, s(0)) → f1_out1
U1(f38_out2(z0), s(0)) → f1_out1
U2(f1_out1, s(s(z0))) → f1_out1
f41_in → f41_out1
f38_in → U3(f41_in, f43_in)
U3(f41_out1, z0) → f38_out1
U3(z0, f43_out1(z1)) → f38_out2(z1)
Tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(s(z0))) → c3(F1_IN(z0))
F1_IN(s(0)) → c
F38_IN → c
S tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(s(z0))) → c3(F1_IN(z0))
F1_IN(s(0)) → c
F38_IN → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f41_in, f38_in, U3
Defined Pair Symbols:
F1_IN, F38_IN
Compound Symbols:
c, c3, c
(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.
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(0)) → c
F38_IN → c
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(s(z0))) → c3(F1_IN(z0))
F1_IN(s(0)) → c
F38_IN → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(F1_IN(x1)) = [3]
POL(F38_IN) = [2]
POL(c) = 0
POL(c(x1)) = x1
POL(c3(x1)) = x1
POL(s(x1)) = 0
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(0)) → U1(f38_in, s(0))
f1_in(s(s(z0))) → U2(f1_in(z0), s(s(z0)))
U1(f38_out1, s(0)) → f1_out1
U1(f38_out2(z0), s(0)) → f1_out1
U2(f1_out1, s(s(z0))) → f1_out1
f41_in → f41_out1
f38_in → U3(f41_in, f43_in)
U3(f41_out1, z0) → f38_out1
U3(z0, f43_out1(z1)) → f38_out2(z1)
Tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(s(z0))) → c3(F1_IN(z0))
F1_IN(s(0)) → c
F38_IN → c
S tuples:
F1_IN(s(s(z0))) → c3(F1_IN(z0))
K tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(0)) → c
F38_IN → c
Defined Rule Symbols:
f1_in, U1, U2, f41_in, f38_in, U3
Defined Pair Symbols:
F1_IN, F38_IN
Compound Symbols:
c, c3, 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.
F1_IN(s(s(z0))) → c3(F1_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(s(z0))) → c3(F1_IN(z0))
F1_IN(s(0)) → c
F38_IN → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(F1_IN(x1)) = [3] + x1
POL(F38_IN) = [3]
POL(c) = 0
POL(c(x1)) = x1
POL(c3(x1)) = x1
POL(s(x1)) = [1] + x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(0) → f1_out1
f1_in(s(s(0))) → f1_out1
f1_in(s(0)) → U1(f38_in, s(0))
f1_in(s(s(z0))) → U2(f1_in(z0), s(s(z0)))
U1(f38_out1, s(0)) → f1_out1
U1(f38_out2(z0), s(0)) → f1_out1
U2(f1_out1, s(s(z0))) → f1_out1
f41_in → f41_out1
f38_in → U3(f41_in, f43_in)
U3(f41_out1, z0) → f38_out1
U3(z0, f43_out1(z1)) → f38_out2(z1)
Tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(s(z0))) → c3(F1_IN(z0))
F1_IN(s(0)) → c
F38_IN → c
S tuples:none
K tuples:
F1_IN(s(0)) → c(F38_IN)
F1_IN(s(0)) → c
F38_IN → c
F1_IN(s(s(z0))) → c3(F1_IN(z0))
Defined Rule Symbols:
f1_in, U1, U2, f41_in, f38_in, U3
Defined Pair Symbols:
F1_IN, F38_IN
Compound Symbols:
c, c3, c
(11) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(12) BOUNDS(O(1), O(1))
(13) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(0)) → U1(f37_in, s(0))
f2_in(s(s(z0))) → U2(f2_in(z0), s(s(z0)))
U1(f37_out1, s(0)) → f2_out1
U1(f37_out2(z0), s(0)) → f2_out1
U2(f2_out1, s(s(z0))) → f2_out1
f42_in → f42_out1
f37_in → U3(f42_in, f44_in)
U3(f42_out1, z0) → f37_out1
U3(z0, f44_out1(z1)) → f37_out2(z1)
Tuples:
F2_IN(s(0)) → c2(U1'(f37_in, s(0)), F37_IN)
F2_IN(s(s(z0))) → c3(U2'(f2_in(z0), s(s(z0))), F2_IN(z0))
F37_IN → c8(U3'(f42_in, f44_in), F42_IN)
S tuples:
F2_IN(s(0)) → c2(U1'(f37_in, s(0)), F37_IN)
F2_IN(s(s(z0))) → c3(U2'(f2_in(z0), s(s(z0))), F2_IN(z0))
F37_IN → c8(U3'(f42_in, f44_in), F42_IN)
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f42_in, f37_in, U3
Defined Pair Symbols:
F2_IN, F37_IN
Compound Symbols:
c2, c3, c8
(15) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(0)) → U1(f37_in, s(0))
f2_in(s(s(z0))) → U2(f2_in(z0), s(s(z0)))
U1(f37_out1, s(0)) → f2_out1
U1(f37_out2(z0), s(0)) → f2_out1
U2(f2_out1, s(s(z0))) → f2_out1
f42_in → f42_out1
f37_in → U3(f42_in, f44_in)
U3(f42_out1, z0) → f37_out1
U3(z0, f44_out1(z1)) → f37_out2(z1)
Tuples:
F2_IN(s(s(z0))) → c3(U2'(f2_in(z0), s(s(z0))), F2_IN(z0))
F2_IN(s(0)) → c(U1'(f37_in, s(0)))
F2_IN(s(0)) → c(F37_IN)
F37_IN → c(U3'(f42_in, f44_in))
F37_IN → c(F42_IN)
S tuples:
F2_IN(s(s(z0))) → c3(U2'(f2_in(z0), s(s(z0))), F2_IN(z0))
F2_IN(s(0)) → c(U1'(f37_in, s(0)))
F2_IN(s(0)) → c(F37_IN)
F37_IN → c(U3'(f42_in, f44_in))
F37_IN → c(F42_IN)
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f42_in, f37_in, U3
Defined Pair Symbols:
F2_IN, F37_IN
Compound Symbols:
c3, c
(17) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(0)) → U1(f37_in, s(0))
f2_in(s(s(z0))) → U2(f2_in(z0), s(s(z0)))
U1(f37_out1, s(0)) → f2_out1
U1(f37_out2(z0), s(0)) → f2_out1
U2(f2_out1, s(s(z0))) → f2_out1
f42_in → f42_out1
f37_in → U3(f42_in, f44_in)
U3(f42_out1, z0) → f37_out1
U3(z0, f44_out1(z1)) → f37_out2(z1)
Tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(s(z0))) → c3(F2_IN(z0))
F2_IN(s(0)) → c
F37_IN → c
S tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(s(z0))) → c3(F2_IN(z0))
F2_IN(s(0)) → c
F37_IN → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f42_in, f37_in, U3
Defined Pair Symbols:
F2_IN, F37_IN
Compound Symbols:
c, c3, c
(19) 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(0)) → c(F37_IN)
F2_IN(s(0)) → c
F37_IN → c
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(s(z0))) → c3(F2_IN(z0))
F2_IN(s(0)) → c
F37_IN → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(F2_IN(x1)) = [3]
POL(F37_IN) = [2]
POL(c) = 0
POL(c(x1)) = x1
POL(c3(x1)) = x1
POL(s(x1)) = 0
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(0)) → U1(f37_in, s(0))
f2_in(s(s(z0))) → U2(f2_in(z0), s(s(z0)))
U1(f37_out1, s(0)) → f2_out1
U1(f37_out2(z0), s(0)) → f2_out1
U2(f2_out1, s(s(z0))) → f2_out1
f42_in → f42_out1
f37_in → U3(f42_in, f44_in)
U3(f42_out1, z0) → f37_out1
U3(z0, f44_out1(z1)) → f37_out2(z1)
Tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(s(z0))) → c3(F2_IN(z0))
F2_IN(s(0)) → c
F37_IN → c
S tuples:
F2_IN(s(s(z0))) → c3(F2_IN(z0))
K tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(0)) → c
F37_IN → c
Defined Rule Symbols:
f2_in, U1, U2, f42_in, f37_in, U3
Defined Pair Symbols:
F2_IN, F37_IN
Compound Symbols:
c, c3, c
(21) 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(z0))) → c3(F2_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(s(z0))) → c3(F2_IN(z0))
F2_IN(s(0)) → c
F37_IN → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(F2_IN(x1)) = [3] + x1
POL(F37_IN) = [3]
POL(c) = 0
POL(c(x1)) = x1
POL(c3(x1)) = x1
POL(s(x1)) = [1] + x1
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(0) → f2_out1
f2_in(s(s(0))) → f2_out1
f2_in(s(0)) → U1(f37_in, s(0))
f2_in(s(s(z0))) → U2(f2_in(z0), s(s(z0)))
U1(f37_out1, s(0)) → f2_out1
U1(f37_out2(z0), s(0)) → f2_out1
U2(f2_out1, s(s(z0))) → f2_out1
f42_in → f42_out1
f37_in → U3(f42_in, f44_in)
U3(f42_out1, z0) → f37_out1
U3(z0, f44_out1(z1)) → f37_out2(z1)
Tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(s(z0))) → c3(F2_IN(z0))
F2_IN(s(0)) → c
F37_IN → c
S tuples:none
K tuples:
F2_IN(s(0)) → c(F37_IN)
F2_IN(s(0)) → c
F37_IN → c
F2_IN(s(s(z0))) → c3(F2_IN(z0))
Defined Rule Symbols:
f2_in, U1, U2, f42_in, f37_in, U3
Defined Pair Symbols:
F2_IN, F37_IN
Compound Symbols:
c, c3, c