(0) Obligation:
Clauses:
minimum(tree(X, void, X1), X).
minimum(tree(X2, Left, X3), X) :- minimum(Left, X).
Query: minimum(g,a)
(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(tree(z0, void, z1)) → f2_out1(z0)
f2_in(tree(z0, z1, z2)) → U1(f2_in(z1), tree(z0, z1, z2))
U1(f2_out1(z0), tree(z1, z2, z3)) → f2_out1(z0)
Tuples:
F2_IN(tree(z0, z1, z2)) → c1(U1'(f2_in(z1), tree(z0, z1, z2)), F2_IN(z1))
S tuples:
F2_IN(tree(z0, z1, z2)) → c1(U1'(f2_in(z1), tree(z0, z1, z2)), F2_IN(z1))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c1
(3) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(tree(z0, void, z1)) → f2_out1(z0)
f2_in(tree(z0, z1, z2)) → U1(f2_in(z1), tree(z0, z1, z2))
U1(f2_out1(z0), tree(z1, z2, z3)) → f2_out1(z0)
Tuples:
F2_IN(tree(z0, z1, z2)) → c1(F2_IN(z1))
S tuples:
F2_IN(tree(z0, z1, z2)) → c1(F2_IN(z1))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c1
(5) 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(tree(z0, z1, z2)) → c1(F2_IN(z1))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(tree(z0, z1, z2)) → c1(F2_IN(z1))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F2_IN(x1)) = x1
POL(c1(x1)) = x1
POL(tree(x1, x2, x3)) = [1] + x2
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(tree(z0, void, z1)) → f2_out1(z0)
f2_in(tree(z0, z1, z2)) → U1(f2_in(z1), tree(z0, z1, z2))
U1(f2_out1(z0), tree(z1, z2, z3)) → f2_out1(z0)
Tuples:
F2_IN(tree(z0, z1, z2)) → c1(F2_IN(z1))
S tuples:none
K tuples:
F2_IN(tree(z0, z1, z2)) → c1(F2_IN(z1))
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c1
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))
(9) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(tree(z0, void, z1)) → f1_out1(z0)
f1_in(tree(z0, void, z1)) → U1(f11_in, tree(z0, void, z1))
f1_in(tree(z0, tree(z1, void, z2), z3)) → f1_out1(z1)
f1_in(tree(z0, tree(z1, void, z2), z3)) → U2(f11_in, tree(z0, tree(z1, void, z2), z3))
f1_in(tree(z0, tree(z1, z2, z3), z4)) → U3(f1_in(z2), tree(z0, tree(z1, z2, z3), z4))
U1(f11_out1(z0), tree(z1, void, z2)) → f1_out1(z0)
U2(f11_out1(z0), tree(z1, tree(z2, void, z3), z4)) → f1_out1(z0)
U3(f1_out1(z0), tree(z1, tree(z2, z3, z4), z5)) → f1_out1(z0)
Tuples:
F1_IN(tree(z0, void, z1)) → c1(U1'(f11_in, tree(z0, void, z1)))
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3(U2'(f11_in, tree(z0, tree(z1, void, z2), z3)))
F1_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(U3'(f1_in(z2), tree(z0, tree(z1, z2, z3), z4)), F1_IN(z2))
S tuples:
F1_IN(tree(z0, void, z1)) → c1(U1'(f11_in, tree(z0, void, z1)))
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3(U2'(f11_in, tree(z0, tree(z1, void, z2), z3)))
F1_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(U3'(f1_in(z2), tree(z0, tree(z1, z2, z3), z4)), F1_IN(z2))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, U3
Defined Pair Symbols:
F1_IN
Compound Symbols:
c1, c3, c4
(11) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing tuple parts
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(tree(z0, void, z1)) → f1_out1(z0)
f1_in(tree(z0, void, z1)) → U1(f11_in, tree(z0, void, z1))
f1_in(tree(z0, tree(z1, void, z2), z3)) → f1_out1(z1)
f1_in(tree(z0, tree(z1, void, z2), z3)) → U2(f11_in, tree(z0, tree(z1, void, z2), z3))
f1_in(tree(z0, tree(z1, z2, z3), z4)) → U3(f1_in(z2), tree(z0, tree(z1, z2, z3), z4))
U1(f11_out1(z0), tree(z1, void, z2)) → f1_out1(z0)
U2(f11_out1(z0), tree(z1, tree(z2, void, z3), z4)) → f1_out1(z0)
U3(f1_out1(z0), tree(z1, tree(z2, z3, z4), z5)) → f1_out1(z0)
Tuples:
F1_IN(tree(z0, void, z1)) → c1
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3
F1_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F1_IN(z2))
S tuples:
F1_IN(tree(z0, void, z1)) → c1
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3
F1_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F1_IN(z2))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, U3
Defined Pair Symbols:
F1_IN
Compound Symbols:
c1, c3, c4
(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.
F1_IN(tree(z0, void, z1)) → c1
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(tree(z0, void, z1)) → c1
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3
F1_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F1_IN(z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F1_IN(x1)) = [2]
POL(c1) = 0
POL(c3) = 0
POL(c4(x1)) = x1
POL(tree(x1, x2, x3)) = 0
POL(void) = 0
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(tree(z0, void, z1)) → f1_out1(z0)
f1_in(tree(z0, void, z1)) → U1(f11_in, tree(z0, void, z1))
f1_in(tree(z0, tree(z1, void, z2), z3)) → f1_out1(z1)
f1_in(tree(z0, tree(z1, void, z2), z3)) → U2(f11_in, tree(z0, tree(z1, void, z2), z3))
f1_in(tree(z0, tree(z1, z2, z3), z4)) → U3(f1_in(z2), tree(z0, tree(z1, z2, z3), z4))
U1(f11_out1(z0), tree(z1, void, z2)) → f1_out1(z0)
U2(f11_out1(z0), tree(z1, tree(z2, void, z3), z4)) → f1_out1(z0)
U3(f1_out1(z0), tree(z1, tree(z2, z3, z4), z5)) → f1_out1(z0)
Tuples:
F1_IN(tree(z0, void, z1)) → c1
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3
F1_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F1_IN(z2))
S tuples:
F1_IN(tree(z0, tree(z1, z2, z3), z4)) → c4(F1_IN(z2))
K tuples:
F1_IN(tree(z0, void, z1)) → c1
F1_IN(tree(z0, tree(z1, void, z2), z3)) → c3
Defined Rule Symbols:
f1_in, U1, U2, U3
Defined Pair Symbols:
F1_IN
Compound Symbols:
c1, c3, c4