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