MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { +(0(), y) -> y , +(s(x), 0()) -> s(x) , +(s(x), s(y)) -> s(+(s(x), +(y, 0()))) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { +^#(0(), y) -> c_1() , +^#(s(x), 0()) -> c_2() , +^#(s(x), s(y)) -> c_3(+^#(s(x), +(y, 0())), +^#(y, 0())) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(0(), y) -> c_1() , +^#(s(x), 0()) -> c_2() , +^#(s(x), s(y)) -> c_3(+^#(s(x), +(y, 0())), +^#(y, 0())) } Weak Trs: { +(0(), y) -> y , +(s(x), 0()) -> s(x) , +(s(x), s(y)) -> s(+(s(x), +(y, 0()))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2} by applications of Pre({1,2}) = {3}. Here rules are labeled as follows: DPs: { 1: +^#(0(), y) -> c_1() , 2: +^#(s(x), 0()) -> c_2() , 3: +^#(s(x), s(y)) -> c_3(+^#(s(x), +(y, 0())), +^#(y, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(x), s(y)) -> c_3(+^#(s(x), +(y, 0())), +^#(y, 0())) } Weak DPs: { +^#(0(), y) -> c_1() , +^#(s(x), 0()) -> c_2() } Weak Trs: { +(0(), y) -> y , +(s(x), 0()) -> s(x) , +(s(x), s(y)) -> s(+(s(x), +(y, 0()))) } 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. { +^#(0(), y) -> c_1() , +^#(s(x), 0()) -> c_2() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(x), s(y)) -> c_3(+^#(s(x), +(y, 0())), +^#(y, 0())) } Weak Trs: { +(0(), y) -> y , +(s(x), 0()) -> s(x) , +(s(x), s(y)) -> s(+(s(x), +(y, 0()))) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { +^#(s(x), s(y)) -> c_3(+^#(s(x), +(y, 0())), +^#(y, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(x), s(y)) -> c_1(+^#(s(x), +(y, 0()))) } Weak Trs: { +(0(), y) -> y , +(s(x), 0()) -> s(x) , +(s(x), s(y)) -> s(+(s(x), +(y, 0()))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..