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