(0) Obligation:
Clauses:
even(s(s(X))) :- even(X).
even(0).
lte(s(X), s(Y)) :- lte(X, Y).
lte(0, Y).
goal :- ','(lte(X, s(s(s(s(0))))), even(X)).
Query: goal()
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
even(0).
lte(0, Y).
even(s(s(X))) :- even(X).
lte(s(X), s(Y)) :- lte(X, Y).
goal :- ','(lte(X, s(s(s(s(0))))), even(X)).
Query: goal()
(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in → U1(f6_in)
U1(f6_out1(z0)) → f1_out1
f16_in(0) → f16_out1
f16_in(s(s(z0))) → U2(f16_in(z0), s(s(z0)))
U2(f16_out1, s(s(z0))) → f16_out1
f15_in → f15_out1(0)
f15_in → f15_out1(s(0))
f15_in → f15_out1(s(s(0)))
f15_in → f15_out1(s(s(s(0))))
f15_in → f15_out1(s(s(s(s(0)))))
f6_in → U3(f15_in)
U3(f15_out1(z0)) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f6_out1(z0)
Tuples:
F1_IN → c(U1'(f6_in), F6_IN)
F16_IN(s(s(z0))) → c3(U2'(f16_in(z0), s(s(z0))), F16_IN(z0))
F6_IN → c10(U3'(f15_in), F15_IN)
U3'(f15_out1(z0)) → c11(U4'(f16_in(z0), z0), F16_IN(z0))
S tuples:
F1_IN → c(U1'(f6_in), F6_IN)
F16_IN(s(s(z0))) → c3(U2'(f16_in(z0), s(s(z0))), F16_IN(z0))
F6_IN → c10(U3'(f15_in), F15_IN)
U3'(f15_out1(z0)) → c11(U4'(f16_in(z0), z0), F16_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f16_in, U2, f15_in, f6_in, U3, U4
Defined Pair Symbols:
F1_IN, F16_IN, F6_IN, U3'
Compound Symbols:
c, c3, c10, c11
(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in → U1(f6_in)
U1(f6_out1(z0)) → f1_out1
f16_in(0) → f16_out1
f16_in(s(s(z0))) → U2(f16_in(z0), s(s(z0)))
U2(f16_out1, s(s(z0))) → f16_out1
f15_in → f15_out1(0)
f15_in → f15_out1(s(0))
f15_in → f15_out1(s(s(0)))
f15_in → f15_out1(s(s(s(0))))
f15_in → f15_out1(s(s(s(s(0)))))
f6_in → U3(f15_in)
U3(f15_out1(z0)) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f6_out1(z0)
Tuples:
F16_IN(s(s(z0))) → c3(U2'(f16_in(z0), s(s(z0))), F16_IN(z0))
F1_IN → c1(U1'(f6_in))
F1_IN → c1(F6_IN)
F6_IN → c1(U3'(f15_in))
F6_IN → c1(F15_IN)
U3'(f15_out1(z0)) → c1(U4'(f16_in(z0), z0))
U3'(f15_out1(z0)) → c1(F16_IN(z0))
S tuples:
F16_IN(s(s(z0))) → c3(U2'(f16_in(z0), s(s(z0))), F16_IN(z0))
F1_IN → c1(U1'(f6_in))
F1_IN → c1(F6_IN)
F6_IN → c1(U3'(f15_in))
F6_IN → c1(F15_IN)
U3'(f15_out1(z0)) → c1(U4'(f16_in(z0), z0))
U3'(f15_out1(z0)) → c1(F16_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f16_in, U2, f15_in, f6_in, U3, U4
Defined Pair Symbols:
F16_IN, F1_IN, F6_IN, U3'
Compound Symbols:
c3, c1
(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in → U1(f6_in)
U1(f6_out1(z0)) → f1_out1
f16_in(0) → f16_out1
f16_in(s(s(z0))) → U2(f16_in(z0), s(s(z0)))
U2(f16_out1, s(s(z0))) → f16_out1
f15_in → f15_out1(0)
f15_in → f15_out1(s(0))
f15_in → f15_out1(s(s(0)))
f15_in → f15_out1(s(s(s(0))))
f15_in → f15_out1(s(s(s(s(0)))))
f6_in → U3(f15_in)
U3(f15_out1(z0)) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f6_out1(z0)
Tuples:
F1_IN → c1(F6_IN)
F6_IN → c1(U3'(f15_in))
U3'(f15_out1(z0)) → c1(F16_IN(z0))
F16_IN(s(s(z0))) → c3(F16_IN(z0))
F1_IN → c1
F6_IN → c1
U3'(f15_out1(z0)) → c1
S tuples:
F1_IN → c1(F6_IN)
F6_IN → c1(U3'(f15_in))
U3'(f15_out1(z0)) → c1(F16_IN(z0))
F16_IN(s(s(z0))) → c3(F16_IN(z0))
F1_IN → c1
F6_IN → c1
U3'(f15_out1(z0)) → c1
K tuples:none
Defined Rule Symbols:
f1_in, U1, f16_in, U2, f15_in, f6_in, U3, U4
Defined Pair Symbols:
F1_IN, F6_IN, U3', F16_IN
Compound Symbols:
c1, c3, c1
(9) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN → c1(F6_IN)
F6_IN → c1(U3'(f15_in))
U3'(f15_out1(z0)) → c1(F16_IN(z0))
F1_IN → c1
F6_IN → c1
U3'(f15_out1(z0)) → c1
F6_IN → c1(U3'(f15_in))
F6_IN → c1
U3'(f15_out1(z0)) → c1(F16_IN(z0))
U3'(f15_out1(z0)) → c1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in → U1(f6_in)
U1(f6_out1(z0)) → f1_out1
f16_in(0) → f16_out1
f16_in(s(s(z0))) → U2(f16_in(z0), s(s(z0)))
U2(f16_out1, s(s(z0))) → f16_out1
f15_in → f15_out1(0)
f15_in → f15_out1(s(0))
f15_in → f15_out1(s(s(0)))
f15_in → f15_out1(s(s(s(0))))
f15_in → f15_out1(s(s(s(s(0)))))
f6_in → U3(f15_in)
U3(f15_out1(z0)) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f6_out1(z0)
Tuples:
F1_IN → c1(F6_IN)
F6_IN → c1(U3'(f15_in))
U3'(f15_out1(z0)) → c1(F16_IN(z0))
F16_IN(s(s(z0))) → c3(F16_IN(z0))
F1_IN → c1
F6_IN → c1
U3'(f15_out1(z0)) → c1
S tuples:
F16_IN(s(s(z0))) → c3(F16_IN(z0))
K tuples:
F1_IN → c1(F6_IN)
F6_IN → c1(U3'(f15_in))
U3'(f15_out1(z0)) → c1(F16_IN(z0))
F1_IN → c1
F6_IN → c1
U3'(f15_out1(z0)) → c1
Defined Rule Symbols:
f1_in, U1, f16_in, U2, f15_in, f6_in, U3, U4
Defined Pair Symbols:
F1_IN, F6_IN, U3', F16_IN
Compound Symbols:
c1, c3, c1
(11) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f8_in)
U1(f8_out1) → f2_out1
U1(f8_out2(z0)) → f2_out1
f58_in(0) → f58_out1
f58_in(s(s(z0))) → U2(f58_in(z0), s(s(z0)))
U2(f58_out1, s(s(z0))) → f58_out1
f21_in → f21_out1(0)
f21_in → f21_out1(s(0))
f21_in → f21_out1(s(s(0)))
f21_in → f21_out1(s(s(s(0))))
f22_in(s(z0)) → U3(f58_in(z0), s(z0))
U3(f58_out1, s(z0)) → f22_out1
f9_in → f9_out1
f10_in → U4(f18_in)
U4(f18_out1(z0)) → f10_out1(s(z0))
f18_in → U5(f21_in)
U5(f21_out1(z0)) → U6(f22_in(z0), z0)
U6(f22_out1, z0) → f18_out1(z0)
f8_in → U7(f9_in, f10_in)
U7(f9_out1, z0) → f8_out1
U7(z0, f10_out1(z1)) → f8_out2(z1)
Tuples:
F2_IN → c(U1'(f8_in), F8_IN)
F58_IN(s(s(z0))) → c4(U2'(f58_in(z0), s(s(z0))), F58_IN(z0))
F22_IN(s(z0)) → c10(U3'(f58_in(z0), s(z0)), F58_IN(z0))
F10_IN → c13(U4'(f18_in), F18_IN)
F18_IN → c15(U5'(f21_in), F21_IN)
U5'(f21_out1(z0)) → c16(U6'(f22_in(z0), z0), F22_IN(z0))
F8_IN → c18(U7'(f9_in, f10_in), F9_IN, F10_IN)
S tuples:
F2_IN → c(U1'(f8_in), F8_IN)
F58_IN(s(s(z0))) → c4(U2'(f58_in(z0), s(s(z0))), F58_IN(z0))
F22_IN(s(z0)) → c10(U3'(f58_in(z0), s(z0)), F58_IN(z0))
F10_IN → c13(U4'(f18_in), F18_IN)
F18_IN → c15(U5'(f21_in), F21_IN)
U5'(f21_out1(z0)) → c16(U6'(f22_in(z0), z0), F22_IN(z0))
F8_IN → c18(U7'(f9_in, f10_in), F9_IN, F10_IN)
K tuples:none
Defined Rule Symbols:
f2_in, U1, f58_in, U2, f21_in, f22_in, U3, f9_in, f10_in, U4, f18_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F58_IN, F22_IN, F10_IN, F18_IN, U5', F8_IN
Compound Symbols:
c, c4, c10, c13, c15, c16, c18
(13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f8_in)
U1(f8_out1) → f2_out1
U1(f8_out2(z0)) → f2_out1
f58_in(0) → f58_out1
f58_in(s(s(z0))) → U2(f58_in(z0), s(s(z0)))
U2(f58_out1, s(s(z0))) → f58_out1
f21_in → f21_out1(0)
f21_in → f21_out1(s(0))
f21_in → f21_out1(s(s(0)))
f21_in → f21_out1(s(s(s(0))))
f22_in(s(z0)) → U3(f58_in(z0), s(z0))
U3(f58_out1, s(z0)) → f22_out1
f9_in → f9_out1
f10_in → U4(f18_in)
U4(f18_out1(z0)) → f10_out1(s(z0))
f18_in → U5(f21_in)
U5(f21_out1(z0)) → U6(f22_in(z0), z0)
U6(f22_out1, z0) → f18_out1(z0)
f8_in → U7(f9_in, f10_in)
U7(f9_out1, z0) → f8_out1
U7(z0, f10_out1(z1)) → f8_out2(z1)
Tuples:
F58_IN(s(s(z0))) → c4(U2'(f58_in(z0), s(s(z0))), F58_IN(z0))
F2_IN → c1(U1'(f8_in))
F2_IN → c1(F8_IN)
F22_IN(s(z0)) → c1(U3'(f58_in(z0), s(z0)))
F22_IN(s(z0)) → c1(F58_IN(z0))
F10_IN → c1(U4'(f18_in))
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
F18_IN → c1(F21_IN)
U5'(f21_out1(z0)) → c1(U6'(f22_in(z0), z0))
U5'(f21_out1(z0)) → c1(F22_IN(z0))
F8_IN → c1(U7'(f9_in, f10_in))
F8_IN → c1(F9_IN)
F8_IN → c1(F10_IN)
S tuples:
F58_IN(s(s(z0))) → c4(U2'(f58_in(z0), s(s(z0))), F58_IN(z0))
F2_IN → c1(U1'(f8_in))
F2_IN → c1(F8_IN)
F22_IN(s(z0)) → c1(U3'(f58_in(z0), s(z0)))
F22_IN(s(z0)) → c1(F58_IN(z0))
F10_IN → c1(U4'(f18_in))
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
F18_IN → c1(F21_IN)
U5'(f21_out1(z0)) → c1(U6'(f22_in(z0), z0))
U5'(f21_out1(z0)) → c1(F22_IN(z0))
F8_IN → c1(U7'(f9_in, f10_in))
F8_IN → c1(F9_IN)
F8_IN → c1(F10_IN)
K tuples:none
Defined Rule Symbols:
f2_in, U1, f58_in, U2, f21_in, f22_in, U3, f9_in, f10_in, U4, f18_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F58_IN, F2_IN, F22_IN, F10_IN, F18_IN, U5', F8_IN
Compound Symbols:
c4, c1
(15) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 8 trailing tuple parts
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f8_in)
U1(f8_out1) → f2_out1
U1(f8_out2(z0)) → f2_out1
f58_in(0) → f58_out1
f58_in(s(s(z0))) → U2(f58_in(z0), s(s(z0)))
U2(f58_out1, s(s(z0))) → f58_out1
f21_in → f21_out1(0)
f21_in → f21_out1(s(0))
f21_in → f21_out1(s(s(0)))
f21_in → f21_out1(s(s(s(0))))
f22_in(s(z0)) → U3(f58_in(z0), s(z0))
U3(f58_out1, s(z0)) → f22_out1
f9_in → f9_out1
f10_in → U4(f18_in)
U4(f18_out1(z0)) → f10_out1(s(z0))
f18_in → U5(f21_in)
U5(f21_out1(z0)) → U6(f22_in(z0), z0)
U6(f22_out1, z0) → f18_out1(z0)
f8_in → U7(f9_in, f10_in)
U7(f9_out1, z0) → f8_out1
U7(z0, f10_out1(z1)) → f8_out2(z1)
Tuples:
F2_IN → c1(F8_IN)
F22_IN(s(z0)) → c1(F58_IN(z0))
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
U5'(f21_out1(z0)) → c1(F22_IN(z0))
F8_IN → c1(F10_IN)
F58_IN(s(s(z0))) → c4(F58_IN(z0))
F2_IN → c1
F22_IN(s(z0)) → c1
F10_IN → c1
F18_IN → c1
U5'(f21_out1(z0)) → c1
F8_IN → c1
S tuples:
F2_IN → c1(F8_IN)
F22_IN(s(z0)) → c1(F58_IN(z0))
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
U5'(f21_out1(z0)) → c1(F22_IN(z0))
F8_IN → c1(F10_IN)
F58_IN(s(s(z0))) → c4(F58_IN(z0))
F2_IN → c1
F22_IN(s(z0)) → c1
F10_IN → c1
F18_IN → c1
U5'(f21_out1(z0)) → c1
F8_IN → c1
K tuples:none
Defined Rule Symbols:
f2_in, U1, f58_in, U2, f21_in, f22_in, U3, f9_in, f10_in, U4, f18_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F22_IN, F10_IN, F18_IN, U5', F8_IN, F58_IN
Compound Symbols:
c1, c4, c1
(17) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN → c1(F8_IN)
F8_IN → c1(F10_IN)
F2_IN → c1
F10_IN → c1
F8_IN → c1
F8_IN → c1
F8_IN → c1(F10_IN)
F8_IN → c1
F8_IN → c1
F10_IN → c1(F18_IN)
F10_IN → c1
F18_IN → c1(U5'(f21_in))
F18_IN → c1
U5'(f21_out1(z0)) → c1(F22_IN(z0))
U5'(f21_out1(z0)) → c1
F22_IN(s(z0)) → c1(F58_IN(z0))
F22_IN(s(z0)) → c1
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f8_in)
U1(f8_out1) → f2_out1
U1(f8_out2(z0)) → f2_out1
f58_in(0) → f58_out1
f58_in(s(s(z0))) → U2(f58_in(z0), s(s(z0)))
U2(f58_out1, s(s(z0))) → f58_out1
f21_in → f21_out1(0)
f21_in → f21_out1(s(0))
f21_in → f21_out1(s(s(0)))
f21_in → f21_out1(s(s(s(0))))
f22_in(s(z0)) → U3(f58_in(z0), s(z0))
U3(f58_out1, s(z0)) → f22_out1
f9_in → f9_out1
f10_in → U4(f18_in)
U4(f18_out1(z0)) → f10_out1(s(z0))
f18_in → U5(f21_in)
U5(f21_out1(z0)) → U6(f22_in(z0), z0)
U6(f22_out1, z0) → f18_out1(z0)
f8_in → U7(f9_in, f10_in)
U7(f9_out1, z0) → f8_out1
U7(z0, f10_out1(z1)) → f8_out2(z1)
Tuples:
F2_IN → c1(F8_IN)
F22_IN(s(z0)) → c1(F58_IN(z0))
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
U5'(f21_out1(z0)) → c1(F22_IN(z0))
F8_IN → c1(F10_IN)
F58_IN(s(s(z0))) → c4(F58_IN(z0))
F2_IN → c1
F22_IN(s(z0)) → c1
F10_IN → c1
F18_IN → c1
U5'(f21_out1(z0)) → c1
F8_IN → c1
S tuples:
F58_IN(s(s(z0))) → c4(F58_IN(z0))
K tuples:
F2_IN → c1(F8_IN)
F8_IN → c1(F10_IN)
F2_IN → c1
F10_IN → c1
F8_IN → c1
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
F18_IN → c1
U5'(f21_out1(z0)) → c1(F22_IN(z0))
U5'(f21_out1(z0)) → c1
F22_IN(s(z0)) → c1(F58_IN(z0))
F22_IN(s(z0)) → c1
Defined Rule Symbols:
f2_in, U1, f58_in, U2, f21_in, f22_in, U3, f9_in, f10_in, U4, f18_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F22_IN, F10_IN, F18_IN, U5', F8_IN, F58_IN
Compound Symbols:
c1, c4, c1
(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.
F58_IN(s(s(z0))) → c4(F58_IN(z0))
We considered the (Usable) Rules:
f21_in → f21_out1(0)
f21_in → f21_out1(s(0))
f21_in → f21_out1(s(s(0)))
f21_in → f21_out1(s(s(s(0))))
And the Tuples:
F2_IN → c1(F8_IN)
F22_IN(s(z0)) → c1(F58_IN(z0))
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
U5'(f21_out1(z0)) → c1(F22_IN(z0))
F8_IN → c1(F10_IN)
F58_IN(s(s(z0))) → c4(F58_IN(z0))
F2_IN → c1
F22_IN(s(z0)) → c1
F10_IN → c1
F18_IN → c1
U5'(f21_out1(z0)) → c1
F8_IN → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(F10_IN) = [3]
POL(F18_IN) = [3]
POL(F22_IN(x1)) = x1
POL(F2_IN) = [3]
POL(F58_IN(x1)) = x1
POL(F8_IN) = [3]
POL(U5'(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c4(x1)) = x1
POL(f21_in) = [3]
POL(f21_out1(x1)) = x1
POL(s(x1)) = [1] + x1
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f8_in)
U1(f8_out1) → f2_out1
U1(f8_out2(z0)) → f2_out1
f58_in(0) → f58_out1
f58_in(s(s(z0))) → U2(f58_in(z0), s(s(z0)))
U2(f58_out1, s(s(z0))) → f58_out1
f21_in → f21_out1(0)
f21_in → f21_out1(s(0))
f21_in → f21_out1(s(s(0)))
f21_in → f21_out1(s(s(s(0))))
f22_in(s(z0)) → U3(f58_in(z0), s(z0))
U3(f58_out1, s(z0)) → f22_out1
f9_in → f9_out1
f10_in → U4(f18_in)
U4(f18_out1(z0)) → f10_out1(s(z0))
f18_in → U5(f21_in)
U5(f21_out1(z0)) → U6(f22_in(z0), z0)
U6(f22_out1, z0) → f18_out1(z0)
f8_in → U7(f9_in, f10_in)
U7(f9_out1, z0) → f8_out1
U7(z0, f10_out1(z1)) → f8_out2(z1)
Tuples:
F2_IN → c1(F8_IN)
F22_IN(s(z0)) → c1(F58_IN(z0))
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
U5'(f21_out1(z0)) → c1(F22_IN(z0))
F8_IN → c1(F10_IN)
F58_IN(s(s(z0))) → c4(F58_IN(z0))
F2_IN → c1
F22_IN(s(z0)) → c1
F10_IN → c1
F18_IN → c1
U5'(f21_out1(z0)) → c1
F8_IN → c1
S tuples:none
K tuples:
F2_IN → c1(F8_IN)
F8_IN → c1(F10_IN)
F2_IN → c1
F10_IN → c1
F8_IN → c1
F10_IN → c1(F18_IN)
F18_IN → c1(U5'(f21_in))
F18_IN → c1
U5'(f21_out1(z0)) → c1(F22_IN(z0))
U5'(f21_out1(z0)) → c1
F22_IN(s(z0)) → c1(F58_IN(z0))
F22_IN(s(z0)) → c1
F58_IN(s(s(z0))) → c4(F58_IN(z0))
Defined Rule Symbols:
f2_in, U1, f58_in, U2, f21_in, f22_in, U3, f9_in, f10_in, U4, f18_in, U5, U6, f8_in, U7
Defined Pair Symbols:
F2_IN, F22_IN, F10_IN, F18_IN, U5', F8_IN, F58_IN
Compound Symbols:
c1, c4, c1
(21) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(22) BOUNDS(O(1), O(1))