YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following innermost weak dependency pairs: Strict DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(X1, X2) -> c_2() , a__eq^#(0(), 0()) -> c_3() , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , a__inf^#(X) -> c_5() , a__inf^#(X) -> c_6() , a__take^#(X1, X2) -> c_7() , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9() , a__length^#(X) -> c_10() , a__length^#(cons(X, L)) -> c_11() , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15() , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17() , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(X1, X2) -> c_2() , a__eq^#(0(), 0()) -> c_3() , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , a__inf^#(X) -> c_5() , a__inf^#(X) -> c_6() , a__take^#(X1, X2) -> c_7() , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9() , a__length^#(X) -> c_10() , a__length^#(cons(X, L)) -> c_11() , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15() , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17() , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } Strict Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(a__inf) = {1}, Uargs(a__take) = {1, 2}, Uargs(a__length) = {1}, Uargs(c_4) = {1}, Uargs(a__inf^#) = {1}, Uargs(a__take^#) = {1, 2}, Uargs(a__length^#) = {1}, Uargs(c_18) = {1}, Uargs(c_20) = {1}, Uargs(c_21) = {1}, Uargs(c_22) = {1} TcT has computed the following constructor-restricted matrix interpretation. [a__eq](x1, x2) = [0 1] x2 + [1] [0 1] [2] [0] = [0] [0] [true] = [0] [0] [s](x1) = [0 0] x1 + [0] [0 1] [1] [false] = [0] [0] [a__inf](x1) = [1 0] x1 + [1] [0 1] [2] [cons](x1, x2) = [0 0] x2 + [0] [0 1] [0] [inf](x1) = [0 0] x1 + [0] [0 1] [1] [a__take](x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 1] [0 1] [2] [nil] = [0] [2] [take](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [2] [a__length](x1) = [1 0] x1 + [1] [0 1] [2] [length](x1) = [1 0] x1 + [0] [0 1] [1] [mark](x1) = [0 2] x1 + [1] [0 2] [0] [eq](x1, x2) = [0 0] x2 + [0] [0 1] [2] [a__eq^#](x1, x2) = [0 0] x1 + [2] [1 0] [2] [c_1] = [1] [1] [c_2] = [2] [1] [c_3] = [1] [1] [c_4](x1) = [1 0] x1 + [1] [0 1] [1] [a__inf^#](x1) = [1 0] x1 + [1] [0 0] [2] [c_5] = [0] [1] [c_6] = [0] [1] [a__take^#](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_7] = [1] [1] [c_8] = [1] [0] [c_9] = [1] [0] [a__length^#](x1) = [1 0] x1 + [0] [0 0] [0] [c_10] = [1] [1] [c_11] = [1] [0] [c_12] = [1] [0] [mark^#](x1) = [0 2] x1 + [0] [0 0] [0] [c_13] = [1] [0] [c_14] = [1] [0] [c_15] = [1] [1] [c_16] = [1] [0] [c_17] = [1] [0] [c_18](x1) = [1 0] x1 + [2] [0 1] [2] [c_19] = [1] [0] [c_20](x1) = [1 0] x1 + [2] [0 1] [2] [c_21](x1) = [1 0] x1 + [1] [0 1] [2] [c_22](x1) = [1 0] x1 + [1] [0 1] [1] The following symbols are considered usable {a__eq, a__inf, a__take, a__length, mark, a__eq^#, a__inf^#, a__take^#, a__length^#, mark^#} The order satisfies the following ordering constraints: [a__eq(X, Y)] = [0 1] Y + [1] [0 1] [2] > [0] [0] = [false()] [a__eq(X1, X2)] = [0 1] X2 + [1] [0 1] [2] > [0 0] X2 + [0] [0 1] [2] = [eq(X1, X2)] [a__eq(0(), 0())] = [1] [2] > [0] [0] = [true()] [a__eq(s(X), s(Y))] = [0 1] Y + [2] [0 1] [3] > [0 1] Y + [1] [0 1] [2] = [a__eq(X, Y)] [a__inf(X)] = [1 0] X + [1] [0 1] [2] > [0 0] X + [0] [0 1] [2] = [cons(X, inf(s(X)))] [a__inf(X)] = [1 0] X + [1] [0 1] [2] > [0 0] X + [0] [0 1] [1] = [inf(X)] [a__take(X1, X2)] = [1 0] X1 + [1 0] X2 + [1] [0 1] [0 1] [2] > [1 0] X1 + [1 0] X2 + [0] [0 1] [0 1] [2] = [take(X1, X2)] [a__take(0(), X)] = [1 0] X + [1] [0 1] [2] > [0] [2] = [nil()] [a__take(s(X), cons(Y, L))] = [0 0] X + [0 0] L + [1] [0 1] [0 1] [3] > [0 0] X + [0 0] L + [0] [0 1] [0 1] [2] = [cons(Y, take(X, L))] [a__length(X)] = [1 0] X + [1] [0 1] [2] > [1 0] X + [0] [0 1] [1] = [length(X)] [a__length(cons(X, L))] = [0 0] L + [1] [0 1] [2] > [0 0] L + [0] [0 1] [2] = [s(length(L))] [a__length(nil())] = [1] [4] > [0] [0] = [0()] [mark(0())] = [1] [0] > [0] [0] = [0()] [mark(true())] = [1] [0] > [0] [0] = [true()] [mark(s(X))] = [0 2] X + [3] [0 2] [2] > [0 0] X + [0] [0 1] [1] = [s(X)] [mark(false())] = [1] [0] > [0] [0] = [false()] [mark(cons(X1, X2))] = [0 2] X2 + [1] [0 2] [0] > [0 0] X2 + [0] [0 1] [0] = [cons(X1, X2)] [mark(inf(X))] = [0 2] X + [3] [0 2] [2] > [0 2] X + [2] [0 2] [2] = [a__inf(mark(X))] [mark(nil())] = [5] [4] > [0] [2] = [nil()] [mark(take(X1, X2))] = [0 2] X1 + [0 2] X2 + [5] [0 2] [0 2] [4] > [0 2] X1 + [0 2] X2 + [3] [0 2] [0 2] [2] = [a__take(mark(X1), mark(X2))] [mark(length(X))] = [0 2] X + [3] [0 2] [2] > [0 2] X + [2] [0 2] [2] = [a__length(mark(X))] [mark(eq(X1, X2))] = [0 2] X2 + [5] [0 2] [4] > [0 1] X2 + [1] [0 1] [2] = [a__eq(X1, X2)] [a__eq^#(X, Y)] = [0 0] X + [2] [1 0] [2] > [1] [1] = [c_1()] [a__eq^#(X1, X2)] = [0 0] X1 + [2] [1 0] [2] >= [2] [1] = [c_2()] [a__eq^#(0(), 0())] = [2] [2] > [1] [1] = [c_3()] [a__eq^#(s(X), s(Y))] = [2] [2] ? [0 0] X + [3] [1 0] [3] = [c_4(a__eq^#(X, Y))] [a__inf^#(X)] = [1 0] X + [1] [0 0] [2] > [0] [1] = [c_5()] [a__inf^#(X)] = [1 0] X + [1] [0 0] [2] > [0] [1] = [c_6()] [a__take^#(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] [0 0] [0 0] [0] ? [1] [1] = [c_7()] [a__take^#(0(), X)] = [1 0] X + [0] [0 0] [0] ? [1] [0] = [c_8()] [a__take^#(s(X), cons(Y, L))] = [0] [0] ? [1] [0] = [c_9()] [a__length^#(X)] = [1 0] X + [0] [0 0] [0] ? [1] [1] = [c_10()] [a__length^#(cons(X, L))] = [0] [0] ? [1] [0] = [c_11()] [a__length^#(nil())] = [0] [0] ? [1] [0] = [c_12()] [mark^#(0())] = [0] [0] ? [1] [0] = [c_13()] [mark^#(true())] = [0] [0] ? [1] [0] = [c_14()] [mark^#(s(X))] = [0 2] X + [2] [0 0] [0] ? [1] [1] = [c_15()] [mark^#(false())] = [0] [0] ? [1] [0] = [c_16()] [mark^#(cons(X1, X2))] = [0 2] X2 + [0] [0 0] [0] ? [1] [0] = [c_17()] [mark^#(inf(X))] = [0 2] X + [2] [0 0] [0] ? [0 2] X + [4] [0 0] [4] = [c_18(a__inf^#(mark(X)))] [mark^#(nil())] = [4] [0] > [1] [0] = [c_19()] [mark^#(take(X1, X2))] = [0 2] X1 + [0 2] X2 + [4] [0 0] [0 0] [0] ? [0 2] X1 + [0 2] X2 + [4] [0 0] [0 0] [2] = [c_20(a__take^#(mark(X1), mark(X2)))] [mark^#(length(X))] = [0 2] X + [2] [0 0] [0] ? [0 2] X + [2] [0 0] [2] = [c_21(a__length^#(mark(X)))] [mark^#(eq(X1, X2))] = [0 2] X2 + [4] [0 0] [0] ? [0 0] X1 + [3] [1 0] [3] = [c_22(a__eq^#(X1, X2))] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a__eq^#(X1, X2) -> c_2() , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , a__take^#(X1, X2) -> c_7() , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9() , a__length^#(X) -> c_10() , a__length^#(cons(X, L)) -> c_11() , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15() , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17() , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } Weak DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(0(), 0()) -> c_3() , a__inf^#(X) -> c_5() , a__inf^#(X) -> c_6() , mark^#(nil()) -> c_19() } Weak Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {1,3,4,5,6,7,8,9,10,11,12,13,14} by applications of Pre({1,3,4,5,6,7,8,9,10,11,12,13,14}) = {2,15,16,17}. Here rules are labeled as follows: DPs: { 1: a__eq^#(X1, X2) -> c_2() , 2: a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , 3: a__take^#(X1, X2) -> c_7() , 4: a__take^#(0(), X) -> c_8() , 5: a__take^#(s(X), cons(Y, L)) -> c_9() , 6: a__length^#(X) -> c_10() , 7: a__length^#(cons(X, L)) -> c_11() , 8: a__length^#(nil()) -> c_12() , 9: mark^#(0()) -> c_13() , 10: mark^#(true()) -> c_14() , 11: mark^#(s(X)) -> c_15() , 12: mark^#(false()) -> c_16() , 13: mark^#(cons(X1, X2)) -> c_17() , 14: mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , 15: mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , 16: mark^#(length(X)) -> c_21(a__length^#(mark(X))) , 17: mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) , 18: a__eq^#(X, Y) -> c_1() , 19: a__eq^#(0(), 0()) -> c_3() , 20: a__inf^#(X) -> c_5() , 21: a__inf^#(X) -> c_6() , 22: mark^#(nil()) -> c_19() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } Weak DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(X1, X2) -> c_2() , a__eq^#(0(), 0()) -> c_3() , a__inf^#(X) -> c_5() , a__inf^#(X) -> c_6() , a__take^#(X1, X2) -> c_7() , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9() , a__length^#(X) -> c_10() , a__length^#(cons(X, L)) -> c_11() , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15() , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17() , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(nil()) -> c_19() } Weak Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {2,3} by applications of Pre({2,3}) = {}. Here rules are labeled as follows: DPs: { 1: a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , 2: mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , 3: mark^#(length(X)) -> c_21(a__length^#(mark(X))) , 4: mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) , 5: a__eq^#(X, Y) -> c_1() , 6: a__eq^#(X1, X2) -> c_2() , 7: a__eq^#(0(), 0()) -> c_3() , 8: a__inf^#(X) -> c_5() , 9: a__inf^#(X) -> c_6() , 10: a__take^#(X1, X2) -> c_7() , 11: a__take^#(0(), X) -> c_8() , 12: a__take^#(s(X), cons(Y, L)) -> c_9() , 13: a__length^#(X) -> c_10() , 14: a__length^#(cons(X, L)) -> c_11() , 15: a__length^#(nil()) -> c_12() , 16: mark^#(0()) -> c_13() , 17: mark^#(true()) -> c_14() , 18: mark^#(s(X)) -> c_15() , 19: mark^#(false()) -> c_16() , 20: mark^#(cons(X1, X2)) -> c_17() , 21: mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , 22: mark^#(nil()) -> c_19() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } Weak DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(X1, X2) -> c_2() , a__eq^#(0(), 0()) -> c_3() , a__inf^#(X) -> c_5() , a__inf^#(X) -> c_6() , a__take^#(X1, X2) -> c_7() , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9() , a__length^#(X) -> c_10() , a__length^#(cons(X, L)) -> c_11() , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15() , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17() , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) } Weak Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { a__eq^#(X, Y) -> c_1() , a__eq^#(X1, X2) -> c_2() , a__eq^#(0(), 0()) -> c_3() , a__inf^#(X) -> c_5() , a__inf^#(X) -> c_6() , a__take^#(X1, X2) -> c_7() , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9() , a__length^#(X) -> c_10() , a__length^#(cons(X, L)) -> c_11() , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15() , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17() , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } Weak Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Consider the dependency graph 1: a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) -->_1 a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) :1 2: mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) -->_1 a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) :1 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) } Weak Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(a__eq) = {}, safe(0) = {}, safe(true) = {}, safe(s) = {1}, safe(false) = {}, safe(a__inf) = {}, safe(cons) = {1, 2}, safe(inf) = {1}, safe(a__take) = {}, safe(nil) = {}, safe(take) = {1, 2}, safe(a__length) = {}, safe(length) = {1}, safe(mark) = {}, safe(eq) = {1, 2}, safe(a__eq^#) = {2}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(a__inf^#) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(a__take^#) = {}, safe(c_7) = {}, safe(c_8) = {}, safe(c_9) = {}, safe(a__length^#) = {}, safe(c_10) = {}, safe(c_11) = {}, safe(c_12) = {}, safe(mark^#) = {}, safe(c_13) = {}, safe(c_14) = {}, safe(c_15) = {}, safe(c_16) = {}, safe(c_17) = {}, safe(c_18) = {}, safe(c_19) = {}, safe(c_20) = {}, safe(c_21) = {}, safe(c_22) = {} and precedence empty . Following symbols are considered recursive: {a__eq^#} The recursion depth is 1. Further, following argument filtering is employed: pi(a__eq) = [], pi(0) = [], pi(true) = [], pi(s) = [1], pi(false) = [], pi(a__inf) = [], pi(cons) = [], pi(inf) = [], pi(a__take) = [], pi(nil) = [], pi(take) = [], pi(a__length) = [], pi(length) = [], pi(mark) = [], pi(eq) = [], pi(a__eq^#) = [1, 2], pi(c_1) = [], pi(c_2) = [], pi(c_3) = [], pi(c_4) = [1], pi(a__inf^#) = [], pi(c_5) = [], pi(c_6) = [], pi(a__take^#) = [], pi(c_7) = [], pi(c_8) = [], pi(c_9) = [], pi(a__length^#) = [], pi(c_10) = [], pi(c_11) = [], pi(c_12) = [], pi(mark^#) = [], pi(c_13) = [], pi(c_14) = [], pi(c_15) = [], pi(c_16) = [], pi(c_17) = [], pi(c_18) = [], pi(c_19) = [], pi(c_20) = [], pi(c_21) = [], pi(c_22) = [] Usable defined function symbols are a subset of: {a__eq^#, a__inf^#, a__take^#, a__length^#, mark^#} For your convenience, here are the satisfied ordering constraints: pi(a__eq^#(s(X), s(Y))) = a__eq^#(s(; X); s(; Y)) > c_4(a__eq^#(X; Y);) = pi(c_4(a__eq^#(X, Y))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))