(0) Obligation:
Clauses:
fold(X, [], Z) :- ','(!, eq(X, Z)).
fold(X, Y, Z) :- ','(head(Y, H), ','(tail(Y, T), ','(myop(X, H, V), fold(V, T, Z)))).
myop(a, b, a).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
eq(X, X).
Query: fold(g,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(z0, []) → f2_out1(z0)
f2_in(a, .(b, z0)) → U1(f39_in(z0), a, .(b, z0))
U1(f39_out1(z0), a, .(b, z1)) → f2_out1(z0)
f39_in([]) → f39_out1(a)
f39_in(.(b, z0)) → U2(f39_in(z0), .(b, z0))
U2(f39_out1(z0), .(b, z1)) → f39_out1(z0)
Tuples:
F2_IN(a, .(b, z0)) → c1(U1'(f39_in(z0), a, .(b, z0)), F39_IN(z0))
F39_IN(.(b, z0)) → c4(U2'(f39_in(z0), .(b, z0)), F39_IN(z0))
S tuples:
F2_IN(a, .(b, z0)) → c1(U1'(f39_in(z0), a, .(b, z0)), F39_IN(z0))
F39_IN(.(b, z0)) → c4(U2'(f39_in(z0), .(b, z0)), F39_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f39_in, U2
Defined Pair Symbols:
F2_IN, F39_IN
Compound Symbols:
c1, c4
(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0, []) → f2_out1(z0)
f2_in(a, .(b, z0)) → U1(f39_in(z0), a, .(b, z0))
U1(f39_out1(z0), a, .(b, z1)) → f2_out1(z0)
f39_in([]) → f39_out1(a)
f39_in(.(b, z0)) → U2(f39_in(z0), .(b, z0))
U2(f39_out1(z0), .(b, z1)) → f39_out1(z0)
Tuples:
F39_IN(.(b, z0)) → c4(U2'(f39_in(z0), .(b, z0)), F39_IN(z0))
F2_IN(a, .(b, z0)) → c(U1'(f39_in(z0), a, .(b, z0)))
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
S tuples:
F39_IN(.(b, z0)) → c4(U2'(f39_in(z0), .(b, z0)), F39_IN(z0))
F2_IN(a, .(b, z0)) → c(U1'(f39_in(z0), a, .(b, z0)))
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, f39_in, U2
Defined Pair Symbols:
F39_IN, F2_IN
Compound Symbols:
c4, c
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0, []) → f2_out1(z0)
f2_in(a, .(b, z0)) → U1(f39_in(z0), a, .(b, z0))
U1(f39_out1(z0), a, .(b, z1)) → f2_out1(z0)
f39_in([]) → f39_out1(a)
f39_in(.(b, z0)) → U2(f39_in(z0), .(b, z0))
U2(f39_out1(z0), .(b, z1)) → f39_out1(z0)
Tuples:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F39_IN(.(b, z0)) → c4(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
S tuples:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F39_IN(.(b, z0)) → c4(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, f39_in, U2
Defined Pair Symbols:
F2_IN, F39_IN
Compound Symbols:
c, c4, c
(7) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0, []) → f2_out1(z0)
f2_in(a, .(b, z0)) → U1(f39_in(z0), a, .(b, z0))
U1(f39_out1(z0), a, .(b, z1)) → f2_out1(z0)
f39_in([]) → f39_out1(a)
f39_in(.(b, z0)) → U2(f39_in(z0), .(b, z0))
U2(f39_out1(z0), .(b, z1)) → f39_out1(z0)
Tuples:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F39_IN(.(b, z0)) → c4(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
S tuples:
F39_IN(.(b, z0)) → c4(F39_IN(z0))
K tuples:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
Defined Rule Symbols:
f2_in, U1, f39_in, U2
Defined Pair Symbols:
F2_IN, F39_IN
Compound Symbols:
c, c4, 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.
F39_IN(.(b, z0)) → c4(F39_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F39_IN(.(b, z0)) → c4(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F2_IN(x1, x2)) = x1 + [2]x2
POL(F39_IN(x1)) = [3] + x1
POL(a) = [2]
POL(b) = 0
POL(c) = 0
POL(c(x1)) = x1
POL(c4(x1)) = x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0, []) → f2_out1(z0)
f2_in(a, .(b, z0)) → U1(f39_in(z0), a, .(b, z0))
U1(f39_out1(z0), a, .(b, z1)) → f2_out1(z0)
f39_in([]) → f39_out1(a)
f39_in(.(b, z0)) → U2(f39_in(z0), .(b, z0))
U2(f39_out1(z0), .(b, z1)) → f39_out1(z0)
Tuples:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F39_IN(.(b, z0)) → c4(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
S tuples:none
K tuples:
F2_IN(a, .(b, z0)) → c(F39_IN(z0))
F2_IN(a, .(b, z0)) → c
F39_IN(.(b, z0)) → c4(F39_IN(z0))
Defined Rule Symbols:
f2_in, U1, f39_in, U2
Defined Pair Symbols:
F2_IN, F39_IN
Compound Symbols:
c, c4, 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:
f1_in(z0, []) → f1_out1(z0)
f1_in(a, .(b, z0)) → U1(f35_in(z0), a, .(b, z0))
U1(f35_out1(z0), a, .(b, z1)) → f1_out1(z0)
f35_in([]) → f35_out1(a)
f35_in(.(b, z0)) → U2(f35_in(z0), .(b, z0))
U2(f35_out1(z0), .(b, z1)) → f35_out1(z0)
Tuples:
F1_IN(a, .(b, z0)) → c1(U1'(f35_in(z0), a, .(b, z0)), F35_IN(z0))
F35_IN(.(b, z0)) → c4(U2'(f35_in(z0), .(b, z0)), F35_IN(z0))
S tuples:
F1_IN(a, .(b, z0)) → c1(U1'(f35_in(z0), a, .(b, z0)), F35_IN(z0))
F35_IN(.(b, z0)) → c4(U2'(f35_in(z0), .(b, z0)), F35_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f35_in, U2
Defined Pair Symbols:
F1_IN, F35_IN
Compound Symbols:
c1, c4
(15) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, []) → f1_out1(z0)
f1_in(a, .(b, z0)) → U1(f35_in(z0), a, .(b, z0))
U1(f35_out1(z0), a, .(b, z1)) → f1_out1(z0)
f35_in([]) → f35_out1(a)
f35_in(.(b, z0)) → U2(f35_in(z0), .(b, z0))
U2(f35_out1(z0), .(b, z1)) → f35_out1(z0)
Tuples:
F35_IN(.(b, z0)) → c4(U2'(f35_in(z0), .(b, z0)), F35_IN(z0))
F1_IN(a, .(b, z0)) → c(U1'(f35_in(z0), a, .(b, z0)))
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
S tuples:
F35_IN(.(b, z0)) → c4(U2'(f35_in(z0), .(b, z0)), F35_IN(z0))
F1_IN(a, .(b, z0)) → c(U1'(f35_in(z0), a, .(b, z0)))
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f35_in, U2
Defined Pair Symbols:
F35_IN, F1_IN
Compound Symbols:
c4, c
(17) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, []) → f1_out1(z0)
f1_in(a, .(b, z0)) → U1(f35_in(z0), a, .(b, z0))
U1(f35_out1(z0), a, .(b, z1)) → f1_out1(z0)
f35_in([]) → f35_out1(a)
f35_in(.(b, z0)) → U2(f35_in(z0), .(b, z0))
U2(f35_out1(z0), .(b, z1)) → f35_out1(z0)
Tuples:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F35_IN(.(b, z0)) → c4(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
S tuples:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F35_IN(.(b, z0)) → c4(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, f35_in, U2
Defined Pair Symbols:
F1_IN, F35_IN
Compound Symbols:
c, c4, c
(19) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, []) → f1_out1(z0)
f1_in(a, .(b, z0)) → U1(f35_in(z0), a, .(b, z0))
U1(f35_out1(z0), a, .(b, z1)) → f1_out1(z0)
f35_in([]) → f35_out1(a)
f35_in(.(b, z0)) → U2(f35_in(z0), .(b, z0))
U2(f35_out1(z0), .(b, z1)) → f35_out1(z0)
Tuples:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F35_IN(.(b, z0)) → c4(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
S tuples:
F35_IN(.(b, z0)) → c4(F35_IN(z0))
K tuples:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
Defined Rule Symbols:
f1_in, U1, f35_in, U2
Defined Pair Symbols:
F1_IN, F35_IN
Compound Symbols:
c, c4, 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.
F35_IN(.(b, z0)) → c4(F35_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F35_IN(.(b, z0)) → c4(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F1_IN(x1, x2)) = x1 + [2]x2
POL(F35_IN(x1)) = [3] + x1
POL(a) = [2]
POL(b) = 0
POL(c) = 0
POL(c(x1)) = x1
POL(c4(x1)) = x1
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, []) → f1_out1(z0)
f1_in(a, .(b, z0)) → U1(f35_in(z0), a, .(b, z0))
U1(f35_out1(z0), a, .(b, z1)) → f1_out1(z0)
f35_in([]) → f35_out1(a)
f35_in(.(b, z0)) → U2(f35_in(z0), .(b, z0))
U2(f35_out1(z0), .(b, z1)) → f35_out1(z0)
Tuples:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F35_IN(.(b, z0)) → c4(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
S tuples:none
K tuples:
F1_IN(a, .(b, z0)) → c(F35_IN(z0))
F1_IN(a, .(b, z0)) → c
F35_IN(.(b, z0)) → c4(F35_IN(z0))
Defined Rule Symbols:
f1_in, U1, f35_in, U2
Defined Pair Symbols:
F1_IN, F35_IN
Compound Symbols:
c, c4, c