(0) Obligation:
Clauses:
countstack(empty, 0).
countstack(push(nil, T), X) :- countstack(T, X).
countstack(push(cons(U, V), T), s(X)) :- countstack(push(U, push(V, T)), X).
Query: countstack(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(empty) → f1_out1(0)
f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0), z1) → f1_out1(z0)
U1(f7_out2(z0), z1) → f1_out1(z0)
f18_in(push(nil, z0)) → U2(f1_in(z0), push(nil, z0))
U2(f1_out1(z0), push(nil, z1)) → f18_out1(z0)
f19_in(push(cons(z0, z1), z2)) → U3(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U3(f1_out1(z0), push(cons(z1, z2), z3)) → f19_out1(s(z0))
f7_in(z0) → U4(f18_in(z0), f19_in(z0), z0)
U4(f18_out1(z0), z1, z2) → f7_out1(z0)
U4(z0, f19_out1(z1), z2) → f7_out2(z1)
Tuples:
F1_IN(z0) → c1(U1'(f7_in(z0), z0), F7_IN(z0))
F18_IN(push(nil, z0)) → c4(U2'(f1_in(z0), push(nil, z0)), F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(U3'(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F1_IN(push(z0, push(z1, z2))))
F7_IN(z0) → c8(U4'(f18_in(z0), f19_in(z0), z0), F18_IN(z0), F19_IN(z0))
S tuples:
F1_IN(z0) → c1(U1'(f7_in(z0), z0), F7_IN(z0))
F18_IN(push(nil, z0)) → c4(U2'(f1_in(z0), push(nil, z0)), F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(U3'(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F1_IN(push(z0, push(z1, z2))))
F7_IN(z0) → c8(U4'(f18_in(z0), f19_in(z0), z0), F18_IN(z0), F19_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f18_in, U2, f19_in, U3, f7_in, U4
Defined Pair Symbols:
F1_IN, F18_IN, F19_IN, F7_IN
Compound Symbols:
c1, c4, c6, c8
(3) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(empty) → f1_out1(0)
f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0), z1) → f1_out1(z0)
U1(f7_out2(z0), z1) → f1_out1(z0)
f18_in(push(nil, z0)) → U2(f1_in(z0), push(nil, z0))
U2(f1_out1(z0), push(nil, z1)) → f18_out1(z0)
f19_in(push(cons(z0, z1), z2)) → U3(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U3(f1_out1(z0), push(cons(z1, z2), z3)) → f19_out1(s(z0))
f7_in(z0) → U4(f18_in(z0), f19_in(z0), z0)
U4(f18_out1(z0), z1, z2) → f7_out1(z0)
U4(z0, f19_out1(z1), z2) → f7_out2(z1)
Tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(z0) → c8(F18_IN(z0), F19_IN(z0))
S tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(z0) → c8(F18_IN(z0), F19_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f18_in, U2, f19_in, U3, f7_in, U4
Defined Pair Symbols:
F1_IN, F18_IN, F19_IN, F7_IN
Compound Symbols:
c1, c4, c6, c8
(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F7_IN(
z0) →
c8(
F18_IN(
z0),
F19_IN(
z0)) by
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)), F19_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F18_IN(push(cons(y0, y1), y2)), F19_IN(push(cons(y0, y1), y2)))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(empty) → f1_out1(0)
f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0), z1) → f1_out1(z0)
U1(f7_out2(z0), z1) → f1_out1(z0)
f18_in(push(nil, z0)) → U2(f1_in(z0), push(nil, z0))
U2(f1_out1(z0), push(nil, z1)) → f18_out1(z0)
f19_in(push(cons(z0, z1), z2)) → U3(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U3(f1_out1(z0), push(cons(z1, z2), z3)) → f19_out1(s(z0))
f7_in(z0) → U4(f18_in(z0), f19_in(z0), z0)
U4(f18_out1(z0), z1, z2) → f7_out1(z0)
U4(z0, f19_out1(z1), z2) → f7_out2(z1)
Tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)), F19_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F18_IN(push(cons(y0, y1), y2)), F19_IN(push(cons(y0, y1), y2)))
S tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)), F19_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F18_IN(push(cons(y0, y1), y2)), F19_IN(push(cons(y0, y1), y2)))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f18_in, U2, f19_in, U3, f7_in, U4
Defined Pair Symbols:
F1_IN, F18_IN, F19_IN, F7_IN
Compound Symbols:
c1, c4, c6, c8
(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(empty) → f1_out1(0)
f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0), z1) → f1_out1(z0)
U1(f7_out2(z0), z1) → f1_out1(z0)
f18_in(push(nil, z0)) → U2(f1_in(z0), push(nil, z0))
U2(f1_out1(z0), push(nil, z1)) → f18_out1(z0)
f19_in(push(cons(z0, z1), z2)) → U3(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U3(f1_out1(z0), push(cons(z1, z2), z3)) → f19_out1(s(z0))
f7_in(z0) → U4(f18_in(z0), f19_in(z0), z0)
U4(f18_out1(z0), z1, z2) → f7_out1(z0)
U4(z0, f19_out1(z1), z2) → f7_out2(z1)
Tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
S tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f18_in, U2, f19_in, U3, f7_in, U4
Defined Pair Symbols:
F1_IN, F18_IN, F19_IN, F7_IN
Compound Symbols:
c1, c4, c6, c8
(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.
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F18_IN(x1)) = x1
POL(F19_IN(x1)) = x1
POL(F1_IN(x1)) = x1
POL(F7_IN(x1)) = x1
POL(c1(x1)) = x1
POL(c4(x1)) = x1
POL(c6(x1)) = x1
POL(c8(x1)) = x1
POL(cons(x1, x2)) = x1 + x2
POL(nil) = [1]
POL(push(x1, x2)) = x1 + x2
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(empty) → f1_out1(0)
f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0), z1) → f1_out1(z0)
U1(f7_out2(z0), z1) → f1_out1(z0)
f18_in(push(nil, z0)) → U2(f1_in(z0), push(nil, z0))
U2(f1_out1(z0), push(nil, z1)) → f18_out1(z0)
f19_in(push(cons(z0, z1), z2)) → U3(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U3(f1_out1(z0), push(cons(z1, z2), z3)) → f19_out1(s(z0))
f7_in(z0) → U4(f18_in(z0), f19_in(z0), z0)
U4(f18_out1(z0), z1, z2) → f7_out1(z0)
U4(z0, f19_out1(z1), z2) → f7_out2(z1)
Tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
S tuples:
F1_IN(z0) → c1(F7_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
K tuples:
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
Defined Rule Symbols:
f1_in, U1, f18_in, U2, f19_in, U3, f7_in, U4
Defined Pair Symbols:
F1_IN, F18_IN, F19_IN, F7_IN
Compound Symbols:
c1, c4, c6, c8
(11) 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(z0) → c1(F7_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F18_IN(x1)) = [2]x1
POL(F19_IN(x1)) = [2]x1
POL(F1_IN(x1)) = [3] + [2]x1
POL(F7_IN(x1)) = [2]x1
POL(c1(x1)) = x1
POL(c4(x1)) = x1
POL(c6(x1)) = x1
POL(c8(x1)) = x1
POL(cons(x1, x2)) = [2] + x1 + x2
POL(nil) = [2]
POL(push(x1, x2)) = x1 + x2
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(empty) → f1_out1(0)
f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0), z1) → f1_out1(z0)
U1(f7_out2(z0), z1) → f1_out1(z0)
f18_in(push(nil, z0)) → U2(f1_in(z0), push(nil, z0))
U2(f1_out1(z0), push(nil, z1)) → f18_out1(z0)
f19_in(push(cons(z0, z1), z2)) → U3(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U3(f1_out1(z0), push(cons(z1, z2), z3)) → f19_out1(s(z0))
f7_in(z0) → U4(f18_in(z0), f19_in(z0), z0)
U4(f18_out1(z0), z1, z2) → f7_out1(z0)
U4(z0, f19_out1(z1), z2) → f7_out2(z1)
Tuples:
F1_IN(z0) → c1(F7_IN(z0))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
S tuples:
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
K tuples:
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F1_IN(z0) → c1(F7_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
Defined Rule Symbols:
f1_in, U1, f18_in, U2, f19_in, U3, f7_in, U4
Defined Pair Symbols:
F1_IN, F18_IN, F19_IN, F7_IN
Compound Symbols:
c1, c4, c6, c8
(13) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F7_IN(push(nil, y0)) → c8(F18_IN(push(nil, y0)))
F7_IN(push(cons(y0, y1), y2)) → c8(F19_IN(push(cons(y0, y1), y2)))
F18_IN(push(nil, z0)) → c4(F1_IN(z0))
F19_IN(push(cons(z0, z1), z2)) → c6(F1_IN(push(z0, push(z1, z2))))
Now S is empty
(14) BOUNDS(O(1), O(1))
(15) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(empty) → f2_out1(0)
f2_in(push(nil, empty)) → f2_out1(0)
f2_in(push(nil, z0)) → U1(f21_in(z0), push(nil, z0))
f2_in(push(cons(z0, z1), z2)) → U2(f44_in(z0, z1, z2), push(cons(z0, z1), z2))
U1(f21_out1(z0), push(nil, z1)) → f2_out1(z0)
U1(f21_out2(z0), push(nil, z1)) → f2_out1(z0)
U1(f21_out4(z0), push(nil, z1)) → f2_out1(z0)
U2(f44_out1(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))
U2(f44_out2(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))
f27_in(push(nil, z0)) → U3(f2_in(z0), push(nil, z0))
U3(f2_out1(z0), push(nil, z1)) → f27_out1(z0)
f33_in(push(cons(z0, z1), z2)) → U4(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U4(f2_out1(z0), push(cons(z1, z2), z3)) → f33_out1(s(z0))
f45_in(nil, z0, z1) → U5(f2_in(push(z0, z1)), nil, z0, z1)
U5(f2_out1(z0), nil, z1, z2) → f45_out1(z0)
f46_in(cons(z0, z1), z2, z3) → U6(f2_in(push(z0, push(z1, push(z2, z3)))), cons(z0, z1), z2, z3)
U6(f2_out1(z0), cons(z1, z2), z3, z4) → f46_out1(s(z0))
f21_in(z0) → U7(f27_in(z0), f28_in(z0), z0)
U7(f27_out1(z0), z1, z2) → f21_out1(z0)
U7(z0, f28_out1(z1), z2) → f21_out2(z1)
U7(z0, f28_out3(z1), z2) → f21_out4(z1)
f28_in(z0) → U8(f33_in(z0), f34_in(z0), z0)
U8(f33_out1(z0), z1, z2) → f28_out1(z0)
U8(z0, f34_out2(z1), z2) → f28_out3(z1)
f44_in(z0, z1, z2) → U9(f45_in(z0, z1, z2), f46_in(z0, z1, z2), z0, z1, z2)
U9(f45_out1(z0), z1, z2, z3, z4) → f44_out1(z0)
U9(z0, f46_out1(z1), z2, z3, z4) → f44_out2(z1)
Tuples:
F2_IN(push(nil, z0)) → c2(U1'(f21_in(z0), push(nil, z0)), F21_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c3(U2'(f44_in(z0, z1, z2), push(cons(z0, z1), z2)), F44_IN(z0, z1, z2))
F27_IN(push(nil, z0)) → c9(U3'(f2_in(z0), push(nil, z0)), F2_IN(z0))
F33_IN(push(cons(z0, z1), z2)) → c11(U4'(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F2_IN(push(z0, push(z1, z2))))
F45_IN(nil, z0, z1) → c13(U5'(f2_in(push(z0, z1)), nil, z0, z1), F2_IN(push(z0, z1)))
F46_IN(cons(z0, z1), z2, z3) → c15(U6'(f2_in(push(z0, push(z1, push(z2, z3)))), cons(z0, z1), z2, z3), F2_IN(push(z0, push(z1, push(z2, z3)))))
F21_IN(z0) → c17(U7'(f27_in(z0), f28_in(z0), z0), F27_IN(z0), F28_IN(z0))
F28_IN(z0) → c21(U8'(f33_in(z0), f34_in(z0), z0), F33_IN(z0))
F44_IN(z0, z1, z2) → c24(U9'(f45_in(z0, z1, z2), f46_in(z0, z1, z2), z0, z1, z2), F45_IN(z0, z1, z2), F46_IN(z0, z1, z2))
S tuples:
F2_IN(push(nil, z0)) → c2(U1'(f21_in(z0), push(nil, z0)), F21_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c3(U2'(f44_in(z0, z1, z2), push(cons(z0, z1), z2)), F44_IN(z0, z1, z2))
F27_IN(push(nil, z0)) → c9(U3'(f2_in(z0), push(nil, z0)), F2_IN(z0))
F33_IN(push(cons(z0, z1), z2)) → c11(U4'(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F2_IN(push(z0, push(z1, z2))))
F45_IN(nil, z0, z1) → c13(U5'(f2_in(push(z0, z1)), nil, z0, z1), F2_IN(push(z0, z1)))
F46_IN(cons(z0, z1), z2, z3) → c15(U6'(f2_in(push(z0, push(z1, push(z2, z3)))), cons(z0, z1), z2, z3), F2_IN(push(z0, push(z1, push(z2, z3)))))
F21_IN(z0) → c17(U7'(f27_in(z0), f28_in(z0), z0), F27_IN(z0), F28_IN(z0))
F28_IN(z0) → c21(U8'(f33_in(z0), f34_in(z0), z0), F33_IN(z0))
F44_IN(z0, z1, z2) → c24(U9'(f45_in(z0, z1, z2), f46_in(z0, z1, z2), z0, z1, z2), F45_IN(z0, z1, z2), F46_IN(z0, z1, z2))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f27_in, U3, f33_in, U4, f45_in, U5, f46_in, U6, f21_in, U7, f28_in, U8, f44_in, U9
Defined Pair Symbols:
F2_IN, F27_IN, F33_IN, F45_IN, F46_IN, F21_IN, F28_IN, F44_IN
Compound Symbols:
c2, c3, c9, c11, c13, c15, c17, c21, c24
(17) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 9 trailing tuple parts
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(empty) → f2_out1(0)
f2_in(push(nil, empty)) → f2_out1(0)
f2_in(push(nil, z0)) → U1(f21_in(z0), push(nil, z0))
f2_in(push(cons(z0, z1), z2)) → U2(f44_in(z0, z1, z2), push(cons(z0, z1), z2))
U1(f21_out1(z0), push(nil, z1)) → f2_out1(z0)
U1(f21_out2(z0), push(nil, z1)) → f2_out1(z0)
U1(f21_out4(z0), push(nil, z1)) → f2_out1(z0)
U2(f44_out1(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))
U2(f44_out2(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))
f27_in(push(nil, z0)) → U3(f2_in(z0), push(nil, z0))
U3(f2_out1(z0), push(nil, z1)) → f27_out1(z0)
f33_in(push(cons(z0, z1), z2)) → U4(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U4(f2_out1(z0), push(cons(z1, z2), z3)) → f33_out1(s(z0))
f45_in(nil, z0, z1) → U5(f2_in(push(z0, z1)), nil, z0, z1)
U5(f2_out1(z0), nil, z1, z2) → f45_out1(z0)
f46_in(cons(z0, z1), z2, z3) → U6(f2_in(push(z0, push(z1, push(z2, z3)))), cons(z0, z1), z2, z3)
U6(f2_out1(z0), cons(z1, z2), z3, z4) → f46_out1(s(z0))
f21_in(z0) → U7(f27_in(z0), f28_in(z0), z0)
U7(f27_out1(z0), z1, z2) → f21_out1(z0)
U7(z0, f28_out1(z1), z2) → f21_out2(z1)
U7(z0, f28_out3(z1), z2) → f21_out4(z1)
f28_in(z0) → U8(f33_in(z0), f34_in(z0), z0)
U8(f33_out1(z0), z1, z2) → f28_out1(z0)
U8(z0, f34_out2(z1), z2) → f28_out3(z1)
f44_in(z0, z1, z2) → U9(f45_in(z0, z1, z2), f46_in(z0, z1, z2), z0, z1, z2)
U9(f45_out1(z0), z1, z2, z3, z4) → f44_out1(z0)
U9(z0, f46_out1(z1), z2, z3, z4) → f44_out2(z1)
Tuples:
F2_IN(push(nil, z0)) → c2(F21_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c3(F44_IN(z0, z1, z2))
F27_IN(push(nil, z0)) → c9(F2_IN(z0))
F33_IN(push(cons(z0, z1), z2)) → c11(F2_IN(push(z0, push(z1, z2))))
F45_IN(nil, z0, z1) → c13(F2_IN(push(z0, z1)))
F46_IN(cons(z0, z1), z2, z3) → c15(F2_IN(push(z0, push(z1, push(z2, z3)))))
F21_IN(z0) → c17(F27_IN(z0), F28_IN(z0))
F28_IN(z0) → c21(F33_IN(z0))
F44_IN(z0, z1, z2) → c24(F45_IN(z0, z1, z2), F46_IN(z0, z1, z2))
S tuples:
F2_IN(push(nil, z0)) → c2(F21_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c3(F44_IN(z0, z1, z2))
F27_IN(push(nil, z0)) → c9(F2_IN(z0))
F33_IN(push(cons(z0, z1), z2)) → c11(F2_IN(push(z0, push(z1, z2))))
F45_IN(nil, z0, z1) → c13(F2_IN(push(z0, z1)))
F46_IN(cons(z0, z1), z2, z3) → c15(F2_IN(push(z0, push(z1, push(z2, z3)))))
F21_IN(z0) → c17(F27_IN(z0), F28_IN(z0))
F28_IN(z0) → c21(F33_IN(z0))
F44_IN(z0, z1, z2) → c24(F45_IN(z0, z1, z2), F46_IN(z0, z1, z2))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f27_in, U3, f33_in, U4, f45_in, U5, f46_in, U6, f21_in, U7, f28_in, U8, f44_in, U9
Defined Pair Symbols:
F2_IN, F27_IN, F33_IN, F45_IN, F46_IN, F21_IN, F28_IN, F44_IN
Compound Symbols:
c2, c3, c9, c11, c13, c15, c17, c21, c24
(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F27_IN(
push(
nil,
z0)) →
c9(
F2_IN(
z0)) by
F27_IN(push(nil, push(nil, y0))) → c9(F2_IN(push(nil, y0)))
F27_IN(push(nil, push(cons(y0, y1), y2))) → c9(F2_IN(push(cons(y0, y1), y2)))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(empty) → f2_out1(0)
f2_in(push(nil, empty)) → f2_out1(0)
f2_in(push(nil, z0)) → U1(f21_in(z0), push(nil, z0))
f2_in(push(cons(z0, z1), z2)) → U2(f44_in(z0, z1, z2), push(cons(z0, z1), z2))
U1(f21_out1(z0), push(nil, z1)) → f2_out1(z0)
U1(f21_out2(z0), push(nil, z1)) → f2_out1(z0)
U1(f21_out4(z0), push(nil, z1)) → f2_out1(z0)
U2(f44_out1(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))
U2(f44_out2(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))
f27_in(push(nil, z0)) → U3(f2_in(z0), push(nil, z0))
U3(f2_out1(z0), push(nil, z1)) → f27_out1(z0)
f33_in(push(cons(z0, z1), z2)) → U4(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U4(f2_out1(z0), push(cons(z1, z2), z3)) → f33_out1(s(z0))
f45_in(nil, z0, z1) → U5(f2_in(push(z0, z1)), nil, z0, z1)
U5(f2_out1(z0), nil, z1, z2) → f45_out1(z0)
f46_in(cons(z0, z1), z2, z3) → U6(f2_in(push(z0, push(z1, push(z2, z3)))), cons(z0, z1), z2, z3)
U6(f2_out1(z0), cons(z1, z2), z3, z4) → f46_out1(s(z0))
f21_in(z0) → U7(f27_in(z0), f28_in(z0), z0)
U7(f27_out1(z0), z1, z2) → f21_out1(z0)
U7(z0, f28_out1(z1), z2) → f21_out2(z1)
U7(z0, f28_out3(z1), z2) → f21_out4(z1)
f28_in(z0) → U8(f33_in(z0), f34_in(z0), z0)
U8(f33_out1(z0), z1, z2) → f28_out1(z0)
U8(z0, f34_out2(z1), z2) → f28_out3(z1)
f44_in(z0, z1, z2) → U9(f45_in(z0, z1, z2), f46_in(z0, z1, z2), z0, z1, z2)
U9(f45_out1(z0), z1, z2, z3, z4) → f44_out1(z0)
U9(z0, f46_out1(z1), z2, z3, z4) → f44_out2(z1)
Tuples:
F2_IN(push(nil, z0)) → c2(F21_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c3(F44_IN(z0, z1, z2))
F33_IN(push(cons(z0, z1), z2)) → c11(F2_IN(push(z0, push(z1, z2))))
F45_IN(nil, z0, z1) → c13(F2_IN(push(z0, z1)))
F46_IN(cons(z0, z1), z2, z3) → c15(F2_IN(push(z0, push(z1, push(z2, z3)))))
F21_IN(z0) → c17(F27_IN(z0), F28_IN(z0))
F28_IN(z0) → c21(F33_IN(z0))
F44_IN(z0, z1, z2) → c24(F45_IN(z0, z1, z2), F46_IN(z0, z1, z2))
F27_IN(push(nil, push(nil, y0))) → c9(F2_IN(push(nil, y0)))
F27_IN(push(nil, push(cons(y0, y1), y2))) → c9(F2_IN(push(cons(y0, y1), y2)))
S tuples:
F2_IN(push(nil, z0)) → c2(F21_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c3(F44_IN(z0, z1, z2))
F33_IN(push(cons(z0, z1), z2)) → c11(F2_IN(push(z0, push(z1, z2))))
F45_IN(nil, z0, z1) → c13(F2_IN(push(z0, z1)))
F46_IN(cons(z0, z1), z2, z3) → c15(F2_IN(push(z0, push(z1, push(z2, z3)))))
F21_IN(z0) → c17(F27_IN(z0), F28_IN(z0))
F28_IN(z0) → c21(F33_IN(z0))
F44_IN(z0, z1, z2) → c24(F45_IN(z0, z1, z2), F46_IN(z0, z1, z2))
F27_IN(push(nil, push(nil, y0))) → c9(F2_IN(push(nil, y0)))
F27_IN(push(nil, push(cons(y0, y1), y2))) → c9(F2_IN(push(cons(y0, y1), y2)))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f27_in, U3, f33_in, U4, f45_in, U5, f46_in, U6, f21_in, U7, f28_in, U8, f44_in, U9
Defined Pair Symbols:
F2_IN, F33_IN, F45_IN, F46_IN, F21_IN, F28_IN, F44_IN, F27_IN
Compound Symbols:
c2, c3, c11, c13, c15, c17, c21, c24, c9