We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) , a() -> n__a() , g(X) -> n__g(X) , activate(X) -> X , activate(n__f(X)) -> f(X) , activate(n__a()) -> a() , activate(n__g(X)) -> g(X) } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) The input is overlay and right-linear. Switching to innermost rewriting. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) , a() -> n__a() , g(X) -> n__g(X) , activate(X) -> X , activate(n__f(X)) -> f(X) , activate(n__a()) -> a() , activate(n__g(X)) -> g(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following weak dependency pairs: Strict DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) , a^#() -> c_3() , g^#(X) -> c_4() , activate^#(X) -> c_5() , activate^#(n__f(X)) -> c_6(f^#(X)) , activate^#(n__a()) -> c_7(a^#()) , activate^#(n__g(X)) -> c_8(g^#(X)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) , a^#() -> c_3() , g^#(X) -> c_4() , activate^#(X) -> c_5() , activate^#(n__f(X)) -> c_6(f^#(X)) , activate^#(n__a()) -> c_7(a^#()) , activate^#(n__g(X)) -> c_8(g^#(X)) } Strict Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) , a() -> n__a() , g(X) -> n__g(X) , activate(X) -> X , activate(n__f(X)) -> f(X) , activate(n__a()) -> a() , activate(n__g(X)) -> g(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Strict Usable Rules: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) , a^#() -> c_3() , g^#(X) -> c_4() , activate^#(X) -> c_5() , activate^#(n__f(X)) -> c_6(f^#(X)) , activate^#(n__a()) -> c_7(a^#()) , activate^#(n__g(X)) -> c_8(g^#(X)) } Strict Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(f) = {1}, Uargs(n__g) = {1}, Uargs(f^#) = {1}, Uargs(c_2) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1} TcT has computed the following constructor-restricted matrix interpretation. [f](x1) = [1 2] x1 + [2] [0 0] [1] [n__f](x1) = [1 1] x1 + [1] [0 0] [1] [n__a] = [0] [0] [n__g](x1) = [1 0] x1 + [0] [0 0] [0] [f^#](x1) = [1 0] x1 + [0] [0 0] [0] [c_1] = [0] [0] [c_2](x1) = [1 0] x1 + [0] [0 1] [0] [a^#] = [1] [1] [c_3] = [0] [0] [g^#](x1) = [1] [1] [c_4] = [0] [0] [activate^#](x1) = [1 0] x1 + [0] [0 0] [0] [c_5] = [0] [0] [c_6](x1) = [1 0] x1 + [0] [0 1] [0] [c_7](x1) = [1 0] x1 + [1] [0 1] [1] [c_8](x1) = [1 0] x1 + [1] [0 1] [1] The order satisfies the following ordering constraints: [f(X)] = [1 2] X + [2] [0 0] [1] > [1 1] X + [1] [0 0] [1] = [n__f(X)] [f(n__f(n__a()))] = [5] [1] > [4] [1] = [f(n__g(f(n__a())))] [f^#(X)] = [1 0] X + [0] [0 0] [0] >= [0] [0] = [c_1()] [f^#(n__f(n__a()))] = [1] [0] ? [2] [0] = [c_2(f^#(n__g(f(n__a()))))] [a^#()] = [1] [1] > [0] [0] = [c_3()] [g^#(X)] = [1] [1] > [0] [0] = [c_4()] [activate^#(X)] = [1 0] X + [0] [0 0] [0] >= [0] [0] = [c_5()] [activate^#(n__f(X))] = [1 1] X + [1] [0 0] [0] > [1 0] X + [0] [0 0] [0] = [c_6(f^#(X))] [activate^#(n__a())] = [0] [0] ? [2] [2] = [c_7(a^#())] [activate^#(n__g(X))] = [1 0] X + [0] [0 0] [0] ? [2] [2] = [c_8(g^#(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 YES(O(1),O(1)). Strict DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) , activate^#(X) -> c_5() , activate^#(n__a()) -> c_7(a^#()) , activate^#(n__g(X)) -> c_8(g^#(X)) } Weak DPs: { a^#() -> c_3() , g^#(X) -> c_4() , activate^#(n__f(X)) -> c_6(f^#(X)) } Weak Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {3,4,5} by applications of Pre({3,4,5}) = {}. Here rules are labeled as follows: DPs: { 1: f^#(X) -> c_1() , 2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) , 3: activate^#(X) -> c_5() , 4: activate^#(n__a()) -> c_7(a^#()) , 5: activate^#(n__g(X)) -> c_8(g^#(X)) , 6: a^#() -> c_3() , 7: g^#(X) -> c_4() , 8: activate^#(n__f(X)) -> c_6(f^#(X)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) } Weak DPs: { a^#() -> c_3() , g^#(X) -> c_4() , activate^#(X) -> c_5() , activate^#(n__f(X)) -> c_6(f^#(X)) , activate^#(n__a()) -> c_7(a^#()) , activate^#(n__g(X)) -> c_8(g^#(X)) } Weak Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { a^#() -> c_3() , g^#(X) -> c_4() , activate^#(X) -> c_5() , activate^#(n__a()) -> c_7(a^#()) , activate^#(n__g(X)) -> c_8(g^#(X)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) } Weak DPs: { activate^#(n__f(X)) -> c_6(f^#(X)) } Weak Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Consider the dependency graph 1: f^#(X) -> c_1() 2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) -->_1 f^#(X) -> c_1() :1 3: activate^#(n__f(X)) -> c_6(f^#(X)) -->_1 f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) :2 -->_1 f^#(X) -> c_1() :1 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). { activate^#(n__f(X)) -> c_6(f^#(X)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) } Weak Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1} by applications of Pre({1}) = {2}. Here rules are labeled as follows: DPs: { 1: f^#(X) -> c_1() , 2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) } Weak DPs: { f^#(X) -> c_1() } Weak Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1} by applications of Pre({1}) = {}. Here rules are labeled as follows: DPs: { 1: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) , 2: f^#(X) -> c_1() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) } Weak Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f^#(X) -> c_1() , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { f(X) -> n__f(X) , f(n__f(n__a())) -> f(n__g(f(n__a()))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))