YES(?,O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict Trs: { and(tt(), X) -> activate(X) , activate(X) -> X , plus(N, 0()) -> N , plus(N, s(M)) -> s(plus(N, M)) , x(N, 0()) -> 0() , x(N, s(M)) -> plus(x(N, M), N) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We add following dependency tuples: Strict DPs: { and^#(tt(), X) -> c_1(activate^#(X)) , activate^#(X) -> c_2() , plus^#(N, 0()) -> c_3() , plus^#(N, s(M)) -> c_4(plus^#(N, M)) , x^#(N, 0()) -> c_5() , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) } 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: { and^#(tt(), X) -> c_1(activate^#(X)) , activate^#(X) -> c_2() , plus^#(N, 0()) -> c_3() , plus^#(N, s(M)) -> c_4(plus^#(N, M)) , x^#(N, 0()) -> c_5() , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) } Weak Trs: { and(tt(), X) -> activate(X) , activate(X) -> X , plus(N, 0()) -> N , plus(N, s(M)) -> s(plus(N, M)) , x(N, 0()) -> 0() , x(N, s(M)) -> plus(x(N, M), N) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We estimate the number of application of {2,3,5} by applications of Pre({2,3,5}) = {1,4,6}. Here rules are labeled as follows: DPs: { 1: and^#(tt(), X) -> c_1(activate^#(X)) , 2: activate^#(X) -> c_2() , 3: plus^#(N, 0()) -> c_3() , 4: plus^#(N, s(M)) -> c_4(plus^#(N, M)) , 5: x^#(N, 0()) -> c_5() , 6: x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { and^#(tt(), X) -> c_1(activate^#(X)) , plus^#(N, s(M)) -> c_4(plus^#(N, M)) , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) } Weak DPs: { activate^#(X) -> c_2() , plus^#(N, 0()) -> c_3() , x^#(N, 0()) -> c_5() } Weak Trs: { and(tt(), X) -> activate(X) , activate(X) -> X , plus(N, 0()) -> N , plus(N, s(M)) -> s(plus(N, M)) , x(N, 0()) -> 0() , x(N, s(M)) -> plus(x(N, M), N) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We estimate the number of application of {1} by applications of Pre({1}) = {}. Here rules are labeled as follows: DPs: { 1: and^#(tt(), X) -> c_1(activate^#(X)) , 2: plus^#(N, s(M)) -> c_4(plus^#(N, M)) , 3: x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) , 4: activate^#(X) -> c_2() , 5: plus^#(N, 0()) -> c_3() , 6: x^#(N, 0()) -> c_5() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { plus^#(N, s(M)) -> c_4(plus^#(N, M)) , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) } Weak DPs: { and^#(tt(), X) -> c_1(activate^#(X)) , activate^#(X) -> c_2() , plus^#(N, 0()) -> c_3() , x^#(N, 0()) -> c_5() } Weak Trs: { and(tt(), X) -> activate(X) , activate(X) -> X , plus(N, 0()) -> N , plus(N, s(M)) -> s(plus(N, M)) , x(N, 0()) -> 0() , x(N, s(M)) -> plus(x(N, M), N) } 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. { and^#(tt(), X) -> c_1(activate^#(X)) , activate^#(X) -> c_2() , plus^#(N, 0()) -> c_3() , x^#(N, 0()) -> c_5() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { plus^#(N, s(M)) -> c_4(plus^#(N, M)) , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) } Weak Trs: { and(tt(), X) -> activate(X) , activate(X) -> X , plus(N, 0()) -> N , plus(N, s(M)) -> s(plus(N, M)) , x(N, 0()) -> 0() , x(N, s(M)) -> plus(x(N, M), N) } Obligation: innermost runtime complexity Answer: YES(?,O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { plus(N, 0()) -> N , plus(N, s(M)) -> s(plus(N, M)) , x(N, 0()) -> 0() , x(N, s(M)) -> plus(x(N, M), N) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^2)). Strict DPs: { plus^#(N, s(M)) -> c_4(plus^#(N, M)) , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N), x^#(N, M)) } Weak Trs: { plus(N, 0()) -> N , plus(N, s(M)) -> s(plus(N, M)) , x(N, 0()) -> 0() , x(N, s(M)) -> plus(x(N, M), N) } 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(plus) = {}, safe(0) = {}, safe(s) = {1}, safe(x) = {}, safe(plus^#) = {1}, safe(c_4) = {}, safe(x^#) = {}, safe(c_6) = {} and precedence x > plus, x > plus^#, x^# > plus, x^# > plus^#, plus ~ plus^#, x ~ x^# . Following symbols are considered recursive: {plus, x, plus^#, x^#} The recursion depth is 2. Further, following argument filtering is employed: pi(plus) = [2], pi(0) = [], pi(s) = [1], pi(x) = [2], pi(plus^#) = [2], pi(c_4) = [1], pi(x^#) = [1, 2], pi(c_6) = [1, 2] Usable defined function symbols are a subset of: {plus^#, x^#} For your convenience, here are the satisfied ordering constraints: pi(plus^#(N, s(M))) = plus^#(s(; M);) > c_4(plus^#(M;);) = pi(c_4(plus^#(N, M))) pi(x^#(N, s(M))) = x^#(N, s(; M);) > c_6(plus^#(N;), x^#(N, M;);) = pi(c_6(plus^#(x(N, M), N), x^#(N, M))) Hurray, we answered YES(?,O(n^2))