(0) Obligation:

Clauses:

bin_tree(void) :- !.
bin_tree(T) :- ','(left(T, L), ','(right(T, R), ','(bin_tree(L), bin_tree(R)))).
left(void, void).
left(tree(X1, L, X2), L).
right(void, void).
right(tree(X3, X4, R), R).

Query: bin_tree(g)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f28_in(z1, z2), tree(z0, z1, z2))
U1(f28_out1, tree(z0, z1, z2)) → f2_out1
f28_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f28_out1
Tuples:

F2_IN(tree(z0, z1, z2)) → c1(U1'(f28_in(z1, z2), tree(z0, z1, z2)), F28_IN(z1, z2))
F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
U2'(f2_out1, z0, z1) → c4(U3'(f2_in(z1), z0, z1), F2_IN(z1))
S tuples:

F2_IN(tree(z0, z1, z2)) → c1(U1'(f28_in(z1, z2), tree(z0, z1, z2)), F28_IN(z1, z2))
F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
U2'(f2_out1, z0, z1) → c4(U3'(f2_in(z1), z0, z1), F2_IN(z1))
K tuples:none
Defined Rule Symbols:

f2_in, U1, f28_in, U2, U3

Defined Pair Symbols:

F2_IN, F28_IN, U2'

Compound Symbols:

c1, c3, c4

(3) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f28_in(z1, z2), tree(z0, z1, z2))
U1(f28_out1, tree(z0, z1, z2)) → f2_out1
f28_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f28_out1
Tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
S tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
K tuples:none
Defined Rule Symbols:

f2_in, U1, f28_in, U2, U3

Defined Pair Symbols:

F28_IN, F2_IN, U2'

Compound Symbols:

c3, c1, c4

(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.

U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
We considered the (Usable) Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f28_in(z1, z2), tree(z0, z1, z2))
f28_in(z0, z1) → U2(f2_in(z0), z0, z1)
U1(f28_out1, tree(z0, z1, z2)) → f2_out1
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f28_out1
And the Tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F28_IN(x1, x2)) = [2] + x1 + x2   
POL(F2_IN(x1)) = x1   
POL(U1(x1, x2)) = 0   
POL(U2(x1, x2, x3)) = 0   
POL(U2'(x1, x2, x3)) = [2] + x3   
POL(U3(x1, x2, x3)) = 0   
POL(c1(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(f28_in(x1, x2)) = 0   
POL(f28_out1) = 0   
POL(f2_in(x1)) = 0   
POL(f2_out1) = 0   
POL(tree(x1, x2, x3)) = [2] + x2 + x3   
POL(void) = 0   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f28_in(z1, z2), tree(z0, z1, z2))
U1(f28_out1, tree(z0, z1, z2)) → f2_out1
f28_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f28_out1
Tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
S tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
K tuples:

U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
Defined Rule Symbols:

f2_in, U1, f28_in, U2, U3

Defined Pair Symbols:

F28_IN, F2_IN, U2'

Compound Symbols:

c3, c1, c4

(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(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
We considered the (Usable) Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f28_in(z1, z2), tree(z0, z1, z2))
f28_in(z0, z1) → U2(f2_in(z0), z0, z1)
U1(f28_out1, tree(z0, z1, z2)) → f2_out1
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f28_out1
And the Tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F28_IN(x1, x2)) = [2]x1 + [2]x2   
POL(F2_IN(x1)) = [2]x1   
POL(U1(x1, x2)) = 0   
POL(U2(x1, x2, x3)) = [3] + [3]x1 + x3   
POL(U2'(x1, x2, x3)) = [2]x3   
POL(U3(x1, x2, x3)) = x3   
POL(c1(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(f28_in(x1, x2)) = [3] + x1 + [2]x2   
POL(f28_out1) = 0   
POL(f2_in(x1)) = 0   
POL(f2_out1) = [2]   
POL(tree(x1, x2, x3)) = [1] + x2 + x3   
POL(void) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(void) → f2_out1
f2_in(tree(z0, z1, z2)) → U1(f28_in(z1, z2), tree(z0, z1, z2))
U1(f28_out1, tree(z0, z1, z2)) → f2_out1
f28_in(z0, z1) → U2(f2_in(z0), z0, z1)
U2(f2_out1, z0, z1) → U3(f2_in(z1), z0, z1)
U3(f2_out1, z0, z1) → f28_out1
Tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
S tuples:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
K tuples:

U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
Defined Rule Symbols:

f2_in, U1, f28_in, U2, U3

Defined Pair Symbols:

F28_IN, F2_IN, U2'

Compound Symbols:

c3, c1, c4

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F28_IN(z0, z1) → c3(U2'(f2_in(z0), z0, z1), F2_IN(z0))
F2_IN(tree(z0, z1, z2)) → c1(F28_IN(z1, z2))
U2'(f2_out1, z0, z1) → c4(F2_IN(z1))
Now 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(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f27_in(z1, z2), tree(z0, z1, z2))
U1(f27_out1, tree(z0, z1, z2)) → f1_out1
f27_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f27_out1
Tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f27_in(z1, z2), tree(z0, z1, z2)), F27_IN(z1, z2))
F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
U2'(f1_out1, z0, z1) → c4(U3'(f1_in(z1), z0, z1), F1_IN(z1))
S tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f27_in(z1, z2), tree(z0, z1, z2)), F27_IN(z1, z2))
F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
U2'(f1_out1, z0, z1) → c4(U3'(f1_in(z1), z0, z1), F1_IN(z1))
K tuples:none
Defined Rule Symbols:

f1_in, U1, f27_in, U2, U3

Defined Pair Symbols:

F1_IN, F27_IN, U2'

Compound Symbols:

c1, c3, c4

(13) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f27_in(z1, z2), tree(z0, z1, z2))
U1(f27_out1, tree(z0, z1, z2)) → f1_out1
f27_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f27_out1
Tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
S tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
K tuples:none
Defined Rule Symbols:

f1_in, U1, f27_in, U2, U3

Defined Pair Symbols:

F27_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

(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.

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
We considered the (Usable) Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f27_in(z1, z2), tree(z0, z1, z2))
f27_in(z0, z1) → U2(f1_in(z0), z0, z1)
U1(f27_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f27_out1
And the Tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F1_IN(x1)) = x1   
POL(F27_IN(x1, x2)) = [2] + x1 + x2   
POL(U1(x1, x2)) = 0   
POL(U2(x1, x2, x3)) = 0   
POL(U2'(x1, x2, x3)) = [2] + x3   
POL(U3(x1, x2, x3)) = 0   
POL(c1(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(f1_in(x1)) = 0   
POL(f1_out1) = 0   
POL(f27_in(x1, x2)) = 0   
POL(f27_out1) = 0   
POL(tree(x1, x2, x3)) = [2] + x2 + x3   
POL(void) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f27_in(z1, z2), tree(z0, z1, z2))
U1(f27_out1, tree(z0, z1, z2)) → f1_out1
f27_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f27_out1
Tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
S tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
K tuples:

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
Defined Rule Symbols:

f1_in, U1, f27_in, U2, U3

Defined Pair Symbols:

F27_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

(17) 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, z1, z2)) → c1(F27_IN(z1, z2))
We considered the (Usable) Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f27_in(z1, z2), tree(z0, z1, z2))
f27_in(z0, z1) → U2(f1_in(z0), z0, z1)
U1(f27_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f27_out1
And the Tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F1_IN(x1)) = [2]x1   
POL(F27_IN(x1, x2)) = [2]x1 + [2]x2   
POL(U1(x1, x2)) = 0   
POL(U2(x1, x2, x3)) = [3] + [3]x1 + x3   
POL(U2'(x1, x2, x3)) = [2]x3   
POL(U3(x1, x2, x3)) = x3   
POL(c1(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(f1_in(x1)) = 0   
POL(f1_out1) = [2]   
POL(f27_in(x1, x2)) = [3] + x1 + [2]x2   
POL(f27_out1) = 0   
POL(tree(x1, x2, x3)) = [1] + x2 + x3   
POL(void) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f27_in(z1, z2), tree(z0, z1, z2))
U1(f27_out1, tree(z0, z1, z2)) → f1_out1
f27_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f27_out1
Tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
S tuples:

F27_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
K tuples:

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c1(F27_IN(z1, z2))
Defined Rule Symbols:

f1_in, U1, f27_in, U2, U3

Defined Pair Symbols:

F27_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4