MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { -(x, 0()) -> x , -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()) , -(0(), y) -> 0() , p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE We add following weak dependency pairs: Strict DPs: { -^#(x, 0()) -> c_1() , -^#(x, s(y)) -> c_2(-^#(x, p(s(y)))) , -^#(0(), y) -> c_3() , p^#(0()) -> c_4() , p^#(s(x)) -> c_5() } 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() , -^#(x, s(y)) -> c_2(-^#(x, p(s(y)))) , -^#(0(), y) -> c_3() , p^#(0()) -> c_4() , p^#(s(x)) -> c_5() } Strict Trs: { -(x, 0()) -> x , -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()) , -(0(), y) -> 0() , p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Strict Usable Rules: { p(0()) -> 0() , p(s(x)) -> x } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { -^#(x, 0()) -> c_1() , -^#(x, s(y)) -> c_2(-^#(x, p(s(y)))) , -^#(0(), y) -> c_3() , p^#(0()) -> c_4() , p^#(s(x)) -> c_5() } Strict Trs: { p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(-^#) = {2}, Uargs(c_2) = {1} TcT has computed following constructor-restricted matrix interpretation. [0] = [2] [s](x1) = [1] x1 + [0] [p](x1) = [1] x1 + [2] [-^#](x1, x2) = [1] x1 + [2] x2 + [2] [c_1] = [1] [c_2](x1) = [1] x1 + [1] [c_3] = [1] [p^#](x1) = [2] x1 + [2] [c_4] = [1] [c_5] = [1] This order satisfies following ordering constraints: [p(0())] = [4] > [2] = [0()] [p(s(x))] = [1] x + [2] > [1] x + [0] = [x] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { -^#(x, s(y)) -> c_2(-^#(x, p(s(y)))) } Weak DPs: { -^#(x, 0()) -> c_1() , -^#(0(), y) -> c_3() , p^#(0()) -> c_4() , p^#(s(x)) -> c_5() } Weak Trs: { p(0()) -> 0() , p(s(x)) -> 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(), y) -> c_3() , p^#(0()) -> c_4() , p^#(s(x)) -> c_5() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { -^#(x, s(y)) -> c_2(-^#(x, p(s(y)))) } Weak Trs: { p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..