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