YES(O(1),O(1)) 2.51/1.26 YES(O(1),O(1)) 2.51/1.26 2.51/1.26 We are left with following problem, upon which TcT provides the 2.51/1.26 certificate YES(O(1),O(1)). 2.51/1.26 2.51/1.26 Strict Trs: 2.51/1.26 { f(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())) 2.51/1.26 , f(g(h(a(), b()), c()), d()) -> 2.51/1.26 if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) } 2.51/1.26 Obligation: 2.51/1.26 innermost runtime complexity 2.51/1.26 Answer: 2.51/1.26 YES(O(1),O(1)) 2.51/1.26 2.51/1.26 We add the following weak dependency pairs: 2.51/1.26 2.51/1.26 Strict DPs: 2.51/1.26 { f^#(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) 2.51/1.26 , f^#(g(h(a(), b()), c()), d()) -> 2.51/1.26 c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) } 2.51/1.26 2.51/1.26 and mark the set of starting terms. 2.51/1.26 2.51/1.26 We are left with following problem, upon which TcT provides the 2.51/1.26 certificate YES(O(1),O(1)). 2.51/1.26 2.51/1.26 Strict DPs: 2.51/1.26 { f^#(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) 2.51/1.26 , f^#(g(h(a(), b()), c()), d()) -> 2.51/1.26 c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) } 2.51/1.26 Strict Trs: 2.51/1.26 { f(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())) 2.51/1.26 , f(g(h(a(), b()), c()), d()) -> 2.51/1.26 if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) } 2.51/1.26 Obligation: 2.51/1.26 innermost runtime complexity 2.51/1.26 Answer: 2.51/1.26 YES(O(1),O(1)) 2.51/1.26 2.51/1.26 No rule is usable, rules are removed from the input problem. 2.51/1.26 2.51/1.26 We are left with following problem, upon which TcT provides the 2.51/1.26 certificate YES(O(1),O(1)). 2.51/1.26 2.51/1.26 Strict DPs: 2.51/1.26 { f^#(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) 2.51/1.26 , f^#(g(h(a(), b()), c()), d()) -> 2.51/1.26 c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) } 2.51/1.26 Obligation: 2.51/1.26 innermost runtime complexity 2.51/1.26 Answer: 2.51/1.26 YES(O(1),O(1)) 2.51/1.26 2.51/1.26 The weightgap principle applies (using the following constant 2.51/1.26 growth matrix-interpretation) 2.51/1.26 2.51/1.26 The following argument positions are usable: 2.51/1.26 none 2.51/1.26 2.51/1.26 TcT has computed the following constructor-restricted matrix 2.51/1.26 interpretation. 2.51/1.26 2.51/1.26 [g](x1, x2) = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [i](x1, x2, x3) = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [a] = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [b] = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [b'] = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [c] = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [d] = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [.](x1, x2) = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [d'] = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [h](x1, x2) = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [f^#](x1, x2) = [1] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [c_1](x1, x2) = [1] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 [c_2](x1, x2) = [0] 2.51/1.26 [0] 2.51/1.26 2.51/1.26 The order satisfies the following ordering constraints: 2.51/1.26 2.51/1.26 [f^#(g(i(a(), b(), b'()), c()), d())] = [1] 2.51/1.26 [0] 2.51/1.26 >= [1] 2.51/1.26 [0] 2.51/1.26 = [c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))] 2.51/1.26 2.51/1.26 [f^#(g(h(a(), b()), c()), d())] = [1] 2.51/1.26 [0] 2.51/1.26 > [0] 2.51/1.26 [0] 2.51/1.26 = [c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))] 2.51/1.26 2.51/1.26 2.51/1.26 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 2.51/1.26 2.51/1.26 We are left with following problem, upon which TcT provides the 2.51/1.26 certificate YES(O(1),O(1)). 2.51/1.26 2.51/1.26 Strict DPs: 2.51/1.26 { f^#(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) } 2.51/1.26 Weak DPs: 2.51/1.26 { f^#(g(h(a(), b()), c()), d()) -> 2.51/1.26 c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) } 2.51/1.26 Obligation: 2.51/1.26 innermost runtime complexity 2.51/1.26 Answer: 2.51/1.26 YES(O(1),O(1)) 2.51/1.26 2.51/1.26 We estimate the number of application of {1} by applications of 2.51/1.26 Pre({1}) = {}. Here rules are labeled as follows: 2.51/1.26 2.51/1.26 DPs: 2.51/1.26 { 1: f^#(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) 2.51/1.26 , 2: f^#(g(h(a(), b()), c()), d()) -> 2.51/1.26 c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) } 2.51/1.26 2.51/1.26 We are left with following problem, upon which TcT provides the 2.51/1.26 certificate YES(O(1),O(1)). 2.51/1.26 2.51/1.26 Weak DPs: 2.51/1.26 { f^#(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) 2.51/1.26 , f^#(g(h(a(), b()), c()), d()) -> 2.51/1.26 c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) } 2.51/1.26 Obligation: 2.51/1.26 innermost runtime complexity 2.51/1.26 Answer: 2.51/1.26 YES(O(1),O(1)) 2.51/1.26 2.51/1.26 The following weak DPs constitute a sub-graph of the DG that is 2.51/1.26 closed under successors. The DPs are removed. 2.51/1.26 2.51/1.26 { f^#(g(i(a(), b(), b'()), c()), d()) -> 2.51/1.26 c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) 2.51/1.26 , f^#(g(h(a(), b()), c()), d()) -> 2.51/1.26 c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) } 2.51/1.26 2.51/1.26 We are left with following problem, upon which TcT provides the 2.51/1.26 certificate YES(O(1),O(1)). 2.51/1.26 2.51/1.26 Rules: Empty 2.51/1.26 Obligation: 2.51/1.26 innermost runtime complexity 2.51/1.26 Answer: 2.51/1.26 YES(O(1),O(1)) 2.51/1.26 2.51/1.26 Empty rules are trivially bounded 2.51/1.26 2.51/1.26 Hurray, we answered YES(O(1),O(1)) 2.51/1.27 EOF