MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { a__app^#(X1, X2) -> c_1() , a__app^#(nil(), YS) -> c_2(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_3(mark^#(X)) , mark^#(nil()) -> c_4() , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_7(a__from^#(mark(X)), mark^#(X)) , mark^#(s(X)) -> c_8(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X)), mark^#(X)) , a__from^#(X) -> c_11(mark^#(X)) , a__from^#(X) -> c_12() , a__zWadr^#(X1, X2) -> c_13() , a__zWadr^#(XS, nil()) -> c_14() , a__zWadr^#(nil(), YS) -> c_15() , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), mark^#(Y), mark^#(X)) , a__prefix^#(L) -> c_17() , a__prefix^#(X) -> c_18() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__app^#(X1, X2) -> c_1() , a__app^#(nil(), YS) -> c_2(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_3(mark^#(X)) , mark^#(nil()) -> c_4() , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_7(a__from^#(mark(X)), mark^#(X)) , mark^#(s(X)) -> c_8(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X)), mark^#(X)) , a__from^#(X) -> c_11(mark^#(X)) , a__from^#(X) -> c_12() , a__zWadr^#(X1, X2) -> c_13() , a__zWadr^#(XS, nil()) -> c_14() , a__zWadr^#(nil(), YS) -> c_15() , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), mark^#(Y), mark^#(X)) , a__prefix^#(L) -> c_17() , a__prefix^#(X) -> c_18() } Weak Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,4,12,13,14,15,17,18} by applications of Pre({1,4,12,13,14,15,17,18}) = {2,3,5,6,7,8,9,10,11,16}. Here rules are labeled as follows: DPs: { 1: a__app^#(X1, X2) -> c_1() , 2: a__app^#(nil(), YS) -> c_2(mark^#(YS)) , 3: a__app^#(cons(X, XS), YS) -> c_3(mark^#(X)) , 4: mark^#(nil()) -> c_4() , 5: mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , 6: mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , 7: mark^#(from(X)) -> c_7(a__from^#(mark(X)), mark^#(X)) , 8: mark^#(s(X)) -> c_8(mark^#(X)) , 9: mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , 10: mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X)), mark^#(X)) , 11: a__from^#(X) -> c_11(mark^#(X)) , 12: a__from^#(X) -> c_12() , 13: a__zWadr^#(X1, X2) -> c_13() , 14: a__zWadr^#(XS, nil()) -> c_14() , 15: a__zWadr^#(nil(), YS) -> c_15() , 16: a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), mark^#(Y), mark^#(X)) , 17: a__prefix^#(L) -> c_17() , 18: a__prefix^#(X) -> c_18() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__app^#(nil(), YS) -> c_2(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_3(mark^#(X)) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_7(a__from^#(mark(X)), mark^#(X)) , mark^#(s(X)) -> c_8(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X)), mark^#(X)) , a__from^#(X) -> c_11(mark^#(X)) , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), mark^#(Y), mark^#(X)) } Weak DPs: { a__app^#(X1, X2) -> c_1() , mark^#(nil()) -> c_4() , a__from^#(X) -> c_12() , a__zWadr^#(X1, X2) -> c_13() , a__zWadr^#(XS, nil()) -> c_14() , a__zWadr^#(nil(), YS) -> c_15() , a__prefix^#(L) -> c_17() , a__prefix^#(X) -> c_18() } Weak Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } 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__app^#(X1, X2) -> c_1() , mark^#(nil()) -> c_4() , a__from^#(X) -> c_12() , a__zWadr^#(X1, X2) -> c_13() , a__zWadr^#(XS, nil()) -> c_14() , a__zWadr^#(nil(), YS) -> c_15() , a__prefix^#(L) -> c_17() , a__prefix^#(X) -> c_18() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__app^#(nil(), YS) -> c_2(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_3(mark^#(X)) , mark^#(cons(X1, X2)) -> c_5(mark^#(X1)) , mark^#(app(X1, X2)) -> c_6(a__app^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_7(a__from^#(mark(X)), mark^#(X)) , mark^#(s(X)) -> c_8(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_9(a__zWadr^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(prefix(X)) -> c_10(a__prefix^#(mark(X)), mark^#(X)) , a__from^#(X) -> c_11(mark^#(X)) , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_16(a__app^#(mark(Y), cons(mark(X), nil())), mark^#(Y), mark^#(X)) } Weak Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } 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^#(prefix(X)) -> c_10(a__prefix^#(mark(X)), mark^#(X)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__app^#(nil(), YS) -> c_1(mark^#(YS)) , a__app^#(cons(X, XS), YS) -> c_2(mark^#(X)) , mark^#(cons(X1, X2)) -> c_3(mark^#(X1)) , mark^#(app(X1, X2)) -> c_4(a__app^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_5(a__from^#(mark(X)), mark^#(X)) , mark^#(s(X)) -> c_6(mark^#(X)) , mark^#(zWadr(X1, X2)) -> c_7(a__zWadr^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(prefix(X)) -> c_8(mark^#(X)) , a__from^#(X) -> c_9(mark^#(X)) , a__zWadr^#(cons(X, XS), cons(Y, YS)) -> c_10(a__app^#(mark(Y), cons(mark(X), nil())), mark^#(Y), mark^#(X)) } Weak Trs: { a__app(X1, X2) -> app(X1, X2) , a__app(nil(), YS) -> mark(YS) , a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS)) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(app(X1, X2)) -> a__app(mark(X1), mark(X2)) , mark(from(X)) -> a__from(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2)) , mark(prefix(X)) -> a__prefix(mark(X)) , a__from(X) -> cons(mark(X), from(s(X))) , a__from(X) -> from(X) , a__zWadr(X1, X2) -> zWadr(X1, X2) , a__zWadr(XS, nil()) -> nil() , a__zWadr(nil(), YS) -> nil() , a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil())), zWadr(XS, YS)) , a__prefix(L) -> cons(nil(), zWadr(L, prefix(L))) , a__prefix(X) -> prefix(X) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: Following exception was raised: stack overflow 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..