YES(?,O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict Trs: { f(0()) -> 1() , f(s(x)) -> g(x, s(x)) , g(0(), y) -> y , g(s(x), y) -> g(x, s(+(y, x))) , g(s(x), y) -> g(x, +(y, s(x))) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We add following dependency tuples: Strict DPs: { f^#(0()) -> c_1() , f^#(s(x)) -> c_2(g^#(x, s(x))) , g^#(0(), y) -> c_3() , g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) , g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) , +^#(x, 0()) -> c_6() , +^#(x, s(y)) -> c_7(+^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { f^#(0()) -> c_1() , f^#(s(x)) -> c_2(g^#(x, s(x))) , g^#(0(), y) -> c_3() , g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) , g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) , +^#(x, 0()) -> c_6() , +^#(x, s(y)) -> c_7(+^#(x, y)) } Weak Trs: { f(0()) -> 1() , f(s(x)) -> g(x, s(x)) , g(0(), y) -> y , g(s(x), y) -> g(x, s(+(y, x))) , g(s(x), y) -> g(x, +(y, s(x))) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We estimate the number of application of {1,3,6} by applications of Pre({1,3,6}) = {2,4,5,7}. Here rules are labeled as follows: DPs: { 1: f^#(0()) -> c_1() , 2: f^#(s(x)) -> c_2(g^#(x, s(x))) , 3: g^#(0(), y) -> c_3() , 4: g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) , 5: g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) , 6: +^#(x, 0()) -> c_6() , 7: +^#(x, s(y)) -> c_7(+^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { f^#(s(x)) -> c_2(g^#(x, s(x))) , g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) , g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) , +^#(x, s(y)) -> c_7(+^#(x, y)) } Weak DPs: { f^#(0()) -> c_1() , g^#(0(), y) -> c_3() , +^#(x, 0()) -> c_6() } Weak Trs: { f(0()) -> 1() , f(s(x)) -> g(x, s(x)) , g(0(), y) -> y , g(s(x), y) -> g(x, s(+(y, x))) , g(s(x), y) -> g(x, +(y, s(x))) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f^#(0()) -> c_1() , g^#(0(), y) -> c_3() , +^#(x, 0()) -> c_6() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { f^#(s(x)) -> c_2(g^#(x, s(x))) , g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) , g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) , +^#(x, s(y)) -> c_7(+^#(x, y)) } Weak Trs: { f(0()) -> 1() , f(s(x)) -> g(x, s(x)) , g(0(), y) -> y , g(s(x), y) -> g(x, s(+(y, x))) , g(s(x), y) -> g(x, +(y, s(x))) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) Consider the dependency graph 1: f^#(s(x)) -> c_2(g^#(x, s(x))) -->_1 g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) :3 -->_1 g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) :2 2: g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) -->_2 +^#(x, s(y)) -> c_7(+^#(x, y)) :4 -->_1 g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) :3 -->_1 g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) :2 3: g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) -->_2 +^#(x, s(y)) -> c_7(+^#(x, y)) :4 -->_1 g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) :3 -->_1 g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) :2 4: +^#(x, s(y)) -> c_7(+^#(x, y)) -->_1 +^#(x, s(y)) -> c_7(+^#(x, y)) :4 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { f^#(s(x)) -> c_2(g^#(x, s(x))) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) , g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) , +^#(x, s(y)) -> c_7(+^#(x, y)) } Weak Trs: { f(0()) -> 1() , f(s(x)) -> g(x, s(x)) , g(0(), y) -> y , g(s(x), y) -> g(x, s(+(y, x))) , g(s(x), y) -> g(x, +(y, s(x))) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { g^#(s(x), y) -> c_4(g^#(x, s(+(y, x))), +^#(y, x)) , g^#(s(x), y) -> c_5(g^#(x, +(y, s(x))), +^#(y, s(x))) , +^#(x, s(y)) -> c_7(+^#(x, y)) } Weak Trs: { +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) The input was oriented with the instance of 'Small Polynomial Path Order (PS)' as induced by the safe mapping safe(0) = {}, safe(s) = {1}, safe(+) = {1}, safe(g^#) = {2}, safe(c_4) = {}, safe(+^#) = {1}, safe(c_5) = {}, safe(c_7) = {} and precedence g^# > +, g^# > +^#, + ~ +^# . Following symbols are considered recursive: {+, g^#, +^#} The recursion depth is 2. Further, following argument filtering is employed: pi(0) = [], pi(s) = [1], pi(+) = [1, 2], pi(g^#) = [1, 2], pi(c_4) = [1, 2], pi(+^#) = [1, 2], pi(c_5) = [1, 2], pi(c_7) = [1] Usable defined function symbols are a subset of: {+, g^#, +^#} For your convenience, here are the satisfied ordering constraints: pi(g^#(s(x), y)) = g^#(s(; x); y) > c_4(g^#(x; s(; +(x; y))), +^#(x; y);) = pi(c_4(g^#(x, s(+(y, x))), +^#(y, x))) pi(g^#(s(x), y)) = g^#(s(; x); y) > c_5(g^#(x; +(s(; x); y)), +^#(s(; x); y);) = pi(c_5(g^#(x, +(y, s(x))), +^#(y, s(x)))) pi(+^#(x, s(y))) = +^#(s(; y); x) > c_7(+^#(y; x);) = pi(c_7(+^#(x, y))) pi(+(x, 0())) = +(0(); x) > x = pi(x) pi(+(x, s(y))) = +(s(; y); x) > s(; +(y; x)) = pi(s(+(x, y))) Hurray, we answered YES(?,O(n^2))