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