(0) Obligation:
Clauses:
app1(.(X, Xs), Ys, .(X, Zs)) :- app1(Xs, Ys, Zs).
app1([], Ys, Ys).
app2(.(X, Xs), Ys, .(X, Zs)) :- app2(Xs, Ys, Zs).
app2([], Ys, Ys).
Query: app2(a,g,g)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
app1([], Ys, Ys).
app2([], Ys, Ys).
app1(.(X, Xs), Ys, .(X, Zs)) :- app1(Xs, Ys, Zs).
app2(.(X, Xs), Ys, .(X, Zs)) :- app2(Xs, Ys, Zs).
Query: app2(a,g,g)
(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0, z0) → f2_out1([])
f2_in(.(z0, z1), .(z0, z1)) → U1(f2_in(.(z0, z1), z1), .(z0, z1), .(z0, z1))
f2_in(z0, .(z1, z2)) → U2(f2_in(z0, z2), z0, .(z1, z2))
U1(f2_out1(z0), .(z1, z2), .(z1, z2)) → f2_out1(.(z1, z0))
U2(f2_out1(z0), z1, .(z2, z3)) → f2_out1(.(z2, z0))
Tuples:
F2_IN(.(z0, z1), .(z0, z1)) → c1(U1'(f2_in(.(z0, z1), z1), .(z0, z1), .(z0, z1)), F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(U2'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
S tuples:
F2_IN(.(z0, z1), .(z0, z1)) → c1(U1'(f2_in(.(z0, z1), z1), .(z0, z1), .(z0, z1)), F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(U2'(f2_in(z0, z2), z0, .(z1, z2)), F2_IN(z0, z2))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c1, c2
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0, z0) → f2_out1([])
f2_in(.(z0, z1), .(z0, z1)) → U1(f2_in(.(z0, z1), z1), .(z0, z1), .(z0, z1))
f2_in(z0, .(z1, z2)) → U2(f2_in(z0, z2), z0, .(z1, z2))
U1(f2_out1(z0), .(z1, z2), .(z1, z2)) → f2_out1(.(z1, z0))
U2(f2_out1(z0), z1, .(z2, z3)) → f2_out1(.(z2, z0))
Tuples:
F2_IN(.(z0, z1), .(z0, z1)) → c1(F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(F2_IN(z0, z2))
S tuples:
F2_IN(.(z0, z1), .(z0, z1)) → c1(F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(F2_IN(z0, z2))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c1, c2
(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(.(z0, z1), .(z0, z1)) → c1(F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(F2_IN(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(.(z0, z1), .(z0, z1)) → c1(F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(F2_IN(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F2_IN(x1, x2)) = x2
POL(c1(x1)) = x1
POL(c2(x1)) = x1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0, z0) → f2_out1([])
f2_in(.(z0, z1), .(z0, z1)) → U1(f2_in(.(z0, z1), z1), .(z0, z1), .(z0, z1))
f2_in(z0, .(z1, z2)) → U2(f2_in(z0, z2), z0, .(z1, z2))
U1(f2_out1(z0), .(z1, z2), .(z1, z2)) → f2_out1(.(z1, z0))
U2(f2_out1(z0), z1, .(z2, z3)) → f2_out1(.(z2, z0))
Tuples:
F2_IN(.(z0, z1), .(z0, z1)) → c1(F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(F2_IN(z0, z2))
S tuples:none
K tuples:
F2_IN(.(z0, z1), .(z0, z1)) → c1(F2_IN(.(z0, z1), z1))
F2_IN(z0, .(z1, z2)) → c2(F2_IN(z0, z2))
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c1, c2
(9) SIsEmptyProof (EQUIVALENT transformation)
The set 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(z0, z0) → f1_out1([])
f1_in(.(z0, .(z1, z2)), .(z0, .(z1, z2))) → U1(f1_in(.(z0, .(z1, z2)), z2), .(z0, .(z1, z2)), .(z0, .(z1, z2)))
f1_in(z0, .(z1, z0)) → f1_out1(.(z1, []))
f1_in(.(z0, z1), .(z2, .(z0, z1))) → U2(f1_in(.(z0, z1), z1), .(z0, z1), .(z2, .(z0, z1)))
f1_in(z0, .(z1, .(z2, z3))) → U3(f1_in(z0, z3), z0, .(z1, .(z2, z3)))
U1(f1_out1(z0), .(z1, .(z2, z3)), .(z1, .(z2, z3))) → f1_out1(.(z1, .(z2, z0)))
U2(f1_out1(z0), .(z1, z2), .(z3, .(z1, z2))) → f1_out1(.(z3, .(z1, z0)))
U3(f1_out1(z0), z1, .(z2, .(z3, z4))) → f1_out1(.(z2, .(z3, z0)))
Tuples:
F1_IN(.(z0, .(z1, z2)), .(z0, .(z1, z2))) → c1(U1'(f1_in(.(z0, .(z1, z2)), z2), .(z0, .(z1, z2)), .(z0, .(z1, z2))), F1_IN(.(z0, .(z1, z2)), z2))
F1_IN(.(z0, z1), .(z2, .(z0, z1))) → c3(U2'(f1_in(.(z0, z1), z1), .(z0, z1), .(z2, .(z0, z1))), F1_IN(.(z0, z1), z1))
F1_IN(z0, .(z1, .(z2, z3))) → c4(U3'(f1_in(z0, z3), z0, .(z1, .(z2, z3))), F1_IN(z0, z3))
S tuples:
F1_IN(.(z0, .(z1, z2)), .(z0, .(z1, z2))) → c1(U1'(f1_in(.(z0, .(z1, z2)), z2), .(z0, .(z1, z2)), .(z0, .(z1, z2))), F1_IN(.(z0, .(z1, z2)), z2))
F1_IN(.(z0, z1), .(z2, .(z0, z1))) → c3(U2'(f1_in(.(z0, z1), z1), .(z0, z1), .(z2, .(z0, z1))), F1_IN(.(z0, z1), z1))
F1_IN(z0, .(z1, .(z2, z3))) → c4(U3'(f1_in(z0, z3), z0, .(z1, .(z2, z3))), F1_IN(z0, z3))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, U3
Defined Pair Symbols:
F1_IN
Compound Symbols:
c1, c3, c4
(13) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing tuple parts
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0, z0) → f1_out1([])
f1_in(.(z0, .(z1, z2)), .(z0, .(z1, z2))) → U1(f1_in(.(z0, .(z1, z2)), z2), .(z0, .(z1, z2)), .(z0, .(z1, z2)))
f1_in(z0, .(z1, z0)) → f1_out1(.(z1, []))
f1_in(.(z0, z1), .(z2, .(z0, z1))) → U2(f1_in(.(z0, z1), z1), .(z0, z1), .(z2, .(z0, z1)))
f1_in(z0, .(z1, .(z2, z3))) → U3(f1_in(z0, z3), z0, .(z1, .(z2, z3)))
U1(f1_out1(z0), .(z1, .(z2, z3)), .(z1, .(z2, z3))) → f1_out1(.(z1, .(z2, z0)))
U2(f1_out1(z0), .(z1, z2), .(z3, .(z1, z2))) → f1_out1(.(z3, .(z1, z0)))
U3(f1_out1(z0), z1, .(z2, .(z3, z4))) → f1_out1(.(z2, .(z3, z0)))
Tuples:
F1_IN(.(z0, .(z1, z2)), .(z0, .(z1, z2))) → c1(F1_IN(.(z0, .(z1, z2)), z2))
F1_IN(.(z0, z1), .(z2, .(z0, z1))) → c3(F1_IN(.(z0, z1), z1))
F1_IN(z0, .(z1, .(z2, z3))) → c4(F1_IN(z0, z3))
S tuples:
F1_IN(.(z0, .(z1, z2)), .(z0, .(z1, z2))) → c1(F1_IN(.(z0, .(z1, z2)), z2))
F1_IN(.(z0, z1), .(z2, .(z0, z1))) → c3(F1_IN(.(z0, z1), z1))
F1_IN(z0, .(z1, .(z2, z3))) → c4(F1_IN(z0, z3))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, U3
Defined Pair Symbols:
F1_IN
Compound Symbols:
c1, c3, c4