MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. 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: MAYBE We add following dependency tuples: 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^#(X)) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(length(X)) -> c_21(a__length^#(mark(X)), 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 MAYBE. 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^#(X)) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X)) , 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: MAYBE We estimate the number of application of {1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,19} by applications of Pre({1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,19}) = {4,18,20,21,22}. Here rules are labeled as follows: DPs: { 1: a__eq^#(X, Y) -> c_1() , 2: a__eq^#(X1, X2) -> c_2() , 3: a__eq^#(0(), 0()) -> c_3() , 4: a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , 5: a__inf^#(X) -> c_5() , 6: a__inf^#(X) -> c_6() , 7: a__take^#(X1, X2) -> c_7() , 8: a__take^#(0(), X) -> c_8() , 9: a__take^#(s(X), cons(Y, L)) -> c_9() , 10: a__length^#(X) -> c_10() , 11: a__length^#(cons(X, L)) -> c_11() , 12: a__length^#(nil()) -> c_12() , 13: mark^#(0()) -> c_13() , 14: mark^#(true()) -> c_14() , 15: mark^#(s(X)) -> c_15() , 16: mark^#(false()) -> c_16() , 17: mark^#(cons(X1, X2)) -> c_17() , 18: mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X)) , 19: mark^#(nil()) -> c_19() , 20: mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , 21: mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X)) , 22: mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X)) , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(length(X)) -> c_21(a__length^#(mark(X)), 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^#(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: MAYBE 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^#(nil()) -> c_19() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X)) , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X)) , 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: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { mark^#(inf(X)) -> c_18(a__inf^#(mark(X)), mark^#(X)) , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(length(X)) -> c_21(a__length^#(mark(X)), mark^#(X)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__eq^#(s(X), s(Y)) -> c_1(a__eq^#(X, Y)) , mark^#(inf(X)) -> c_2(mark^#(X)) , mark^#(take(X1, X2)) -> c_3(mark^#(X1), mark^#(X2)) , mark^#(length(X)) -> c_4(mark^#(X)) , mark^#(eq(X1, X2)) -> c_5(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: MAYBE No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__eq^#(s(X), s(Y)) -> c_1(a__eq^#(X, Y)) , mark^#(inf(X)) -> c_2(mark^#(X)) , mark^#(take(X1, X2)) -> c_3(mark^#(X1), mark^#(X2)) , mark^#(length(X)) -> c_4(mark^#(X)) , mark^#(eq(X1, X2)) -> c_5(a__eq^#(X1, X2)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..