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