MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(X, 0()) -> X , +(X, s(Y)) -> s(+(X, Y)) , double(X) -> +(X, X) , f(0(), s(0()), X) -> f(X, double(X), X) , g(X, Y) -> X , g(X, Y) -> Y } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { +^#(X, 0()) -> c_1() , +^#(X, s(Y)) -> c_2(+^#(X, Y)) , double^#(X) -> c_3(+^#(X, X)) , f^#(0(), s(0()), X) -> c_4(f^#(X, double(X), X), double^#(X)) , g^#(X, Y) -> c_5() , g^#(X, Y) -> c_6() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(X, 0()) -> c_1() , +^#(X, s(Y)) -> c_2(+^#(X, Y)) , double^#(X) -> c_3(+^#(X, X)) , f^#(0(), s(0()), X) -> c_4(f^#(X, double(X), X), double^#(X)) , g^#(X, Y) -> c_5() , g^#(X, Y) -> c_6() } Weak Trs: { +(X, 0()) -> X , +(X, s(Y)) -> s(+(X, Y)) , double(X) -> +(X, X) , f(0(), s(0()), X) -> f(X, double(X), X) , g(X, Y) -> X , g(X, Y) -> Y } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,5,6} by applications of Pre({1,5,6}) = {2,3}. Here rules are labeled as follows: DPs: { 1: +^#(X, 0()) -> c_1() , 2: +^#(X, s(Y)) -> c_2(+^#(X, Y)) , 3: double^#(X) -> c_3(+^#(X, X)) , 4: f^#(0(), s(0()), X) -> c_4(f^#(X, double(X), X), double^#(X)) , 5: g^#(X, Y) -> c_5() , 6: g^#(X, Y) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(X, s(Y)) -> c_2(+^#(X, Y)) , double^#(X) -> c_3(+^#(X, X)) , f^#(0(), s(0()), X) -> c_4(f^#(X, double(X), X), double^#(X)) } Weak DPs: { +^#(X, 0()) -> c_1() , g^#(X, Y) -> c_5() , g^#(X, Y) -> c_6() } Weak Trs: { +(X, 0()) -> X , +(X, s(Y)) -> s(+(X, Y)) , double(X) -> +(X, X) , f(0(), s(0()), X) -> f(X, double(X), X) , g(X, Y) -> X , g(X, Y) -> Y } 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. { +^#(X, 0()) -> c_1() , g^#(X, Y) -> c_5() , g^#(X, Y) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(X, s(Y)) -> c_2(+^#(X, Y)) , double^#(X) -> c_3(+^#(X, X)) , f^#(0(), s(0()), X) -> c_4(f^#(X, double(X), X), double^#(X)) } Weak Trs: { +(X, 0()) -> X , +(X, s(Y)) -> s(+(X, Y)) , double(X) -> +(X, X) , f(0(), s(0()), X) -> f(X, double(X), X) , g(X, Y) -> X , g(X, Y) -> Y } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { +(X, 0()) -> X , +(X, s(Y)) -> s(+(X, Y)) , double(X) -> +(X, X) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(X, s(Y)) -> c_2(+^#(X, Y)) , double^#(X) -> c_3(+^#(X, X)) , f^#(0(), s(0()), X) -> c_4(f^#(X, double(X), X), double^#(X)) } Weak Trs: { +(X, 0()) -> X , +(X, s(Y)) -> s(+(X, Y)) , double(X) -> +(X, X) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..