(0) Obligation:
Clauses:
gopher(nil, nil).
gopher(cons(nil, Y), cons(nil, Y)).
gopher(cons(cons(U, V), W), X) :- gopher(cons(U, cons(V, W)), X).
Query: gopher(g,a)
(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(nil) → f1_out1(nil)
f1_in(cons(nil, z0)) → f1_out1(cons(nil, z0))
f1_in(cons(cons(z0, z1), z2)) → U1(f1_in(cons(z0, cons(z1, z2))), cons(cons(z0, z1), z2))
U1(f1_out1(z0), cons(cons(z1, z2), z3)) → f1_out1(z0)
Tuples:
F1_IN(cons(cons(z0, z1), z2)) → c2(U1'(f1_in(cons(z0, cons(z1, z2))), cons(cons(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
S tuples:
F1_IN(cons(cons(z0, z1), z2)) → c2(U1'(f1_in(cons(z0, cons(z1, z2))), cons(cons(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
K tuples:none
Defined Rule Symbols:
f1_in, U1
Defined Pair Symbols:
F1_IN
Compound Symbols:
c2
(3) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(nil) → f1_out1(nil)
f1_in(cons(nil, z0)) → f1_out1(cons(nil, z0))
f1_in(cons(cons(z0, z1), z2)) → U1(f1_in(cons(z0, cons(z1, z2))), cons(cons(z0, z1), z2))
U1(f1_out1(z0), cons(cons(z1, z2), z3)) → f1_out1(z0)
Tuples:
F1_IN(cons(cons(z0, z1), z2)) → c2(F1_IN(cons(z0, cons(z1, z2))))
S tuples:
F1_IN(cons(cons(z0, z1), z2)) → c2(F1_IN(cons(z0, cons(z1, z2))))
K tuples:none
Defined Rule Symbols:
f1_in, U1
Defined Pair Symbols:
F1_IN
Compound Symbols:
c2
(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.
F1_IN(cons(cons(z0, z1), z2)) → c2(F1_IN(cons(z0, cons(z1, z2))))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(cons(cons(z0, z1), z2)) → c2(F1_IN(cons(z0, cons(z1, z2))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F1_IN(x1)) = [2]x1
POL(c2(x1)) = x1
POL(cons(x1, x2)) = [2] + x1
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(nil) → f1_out1(nil)
f1_in(cons(nil, z0)) → f1_out1(cons(nil, z0))
f1_in(cons(cons(z0, z1), z2)) → U1(f1_in(cons(z0, cons(z1, z2))), cons(cons(z0, z1), z2))
U1(f1_out1(z0), cons(cons(z1, z2), z3)) → f1_out1(z0)
Tuples:
F1_IN(cons(cons(z0, z1), z2)) → c2(F1_IN(cons(z0, cons(z1, z2))))
S tuples:none
K tuples:
F1_IN(cons(cons(z0, z1), z2)) → c2(F1_IN(cons(z0, cons(z1, z2))))
Defined Rule Symbols:
f1_in, U1
Defined Pair Symbols:
F1_IN
Compound Symbols:
c2
(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:
f2_in(nil) → f2_out1(nil)
f2_in(cons(nil, z0)) → f2_out1(cons(nil, z0))
f2_in(cons(cons(nil, z0), z1)) → f2_out1(cons(nil, cons(z0, z1)))
f2_in(cons(cons(cons(z0, z1), z2), z3)) → U1(f2_in(cons(z0, cons(z1, cons(z2, z3)))), cons(cons(cons(z0, z1), z2), z3))
U1(f2_out1(z0), cons(cons(cons(z1, z2), z3), z4)) → f2_out1(z0)
Tuples:
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(U1'(f2_in(cons(z0, cons(z1, cons(z2, z3)))), cons(cons(cons(z0, z1), z2), z3)), F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
S tuples:
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(U1'(f2_in(cons(z0, cons(z1, cons(z2, z3)))), cons(cons(cons(z0, z1), z2), z3)), F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c3
(11) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(nil) → f2_out1(nil)
f2_in(cons(nil, z0)) → f2_out1(cons(nil, z0))
f2_in(cons(cons(nil, z0), z1)) → f2_out1(cons(nil, cons(z0, z1)))
f2_in(cons(cons(cons(z0, z1), z2), z3)) → U1(f2_in(cons(z0, cons(z1, cons(z2, z3)))), cons(cons(cons(z0, z1), z2), z3))
U1(f2_out1(z0), cons(cons(cons(z1, z2), z3), z4)) → f2_out1(z0)
Tuples:
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
S tuples:
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c3
(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.
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F2_IN(x1)) = [2]x1
POL(c3(x1)) = x1
POL(cons(x1, x2)) = [2] + x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(nil) → f2_out1(nil)
f2_in(cons(nil, z0)) → f2_out1(cons(nil, z0))
f2_in(cons(cons(nil, z0), z1)) → f2_out1(cons(nil, cons(z0, z1)))
f2_in(cons(cons(cons(z0, z1), z2), z3)) → U1(f2_in(cons(z0, cons(z1, cons(z2, z3)))), cons(cons(cons(z0, z1), z2), z3))
U1(f2_out1(z0), cons(cons(cons(z1, z2), z3), z4)) → f2_out1(z0)
Tuples:
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
S tuples:none
K tuples:
F2_IN(cons(cons(cons(z0, z1), z2), z3)) → c3(F2_IN(cons(z0, cons(z1, cons(z2, z3)))))
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c3