YES(O(1),O(n^3)) 256.06/90.15 YES(O(1),O(n^3)) 256.06/90.15 256.06/90.15 We are left with following problem, upon which TcT provides the 256.06/90.15 certificate YES(O(1),O(n^3)). 256.06/90.15 256.06/90.15 Strict Trs: 256.06/90.15 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.15 , +(x, 0()) -> x 256.06/90.15 , +(x, s(y)) -> s(+(x, y)) 256.06/90.15 , +(0(), y) -> y 256.06/90.15 , +(s(x), y) -> s(+(x, y)) 256.06/90.15 , f(g(f(x))) -> f(h(s(0()), x)) 256.06/90.15 , f(g(h(x, y))) -> f(h(s(x), y)) 256.06/90.15 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 256.06/90.15 Obligation: 256.06/90.15 innermost runtime complexity 256.06/90.15 Answer: 256.06/90.15 YES(O(1),O(n^3)) 256.06/90.15 256.06/90.15 We add the following dependency tuples: 256.06/90.15 256.06/90.15 Strict DPs: 256.06/90.15 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 , +^#(x, 0()) -> c_2() 256.06/90.15 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.15 , +^#(0(), y) -> c_4() 256.06/90.15 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.15 , f^#(g(f(x))) -> c_6(f^#(h(s(0()), x))) 256.06/90.15 , f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.15 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.15 256.06/90.15 and mark the set of starting terms. 256.06/90.15 256.06/90.15 We are left with following problem, upon which TcT provides the 256.06/90.15 certificate YES(O(1),O(n^3)). 256.06/90.15 256.06/90.15 Strict DPs: 256.06/90.15 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 , +^#(x, 0()) -> c_2() 256.06/90.15 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.15 , +^#(0(), y) -> c_4() 256.06/90.15 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.15 , f^#(g(f(x))) -> c_6(f^#(h(s(0()), x))) 256.06/90.15 , f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.15 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.15 Weak Trs: 256.06/90.15 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.15 , +(x, 0()) -> x 256.06/90.15 , +(x, s(y)) -> s(+(x, y)) 256.06/90.15 , +(0(), y) -> y 256.06/90.15 , +(s(x), y) -> s(+(x, y)) 256.06/90.15 , f(g(f(x))) -> f(h(s(0()), x)) 256.06/90.15 , f(g(h(x, y))) -> f(h(s(x), y)) 256.06/90.15 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 256.06/90.15 Obligation: 256.06/90.15 innermost runtime complexity 256.06/90.15 Answer: 256.06/90.15 YES(O(1),O(n^3)) 256.06/90.15 256.06/90.15 Consider the dependency graph: 256.06/90.15 256.06/90.15 1: +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 -->_2 +^#(s(x), y) -> c_5(+^#(x, y)) :5 256.06/90.15 -->_1 +^#(s(x), y) -> c_5(+^#(x, y)) :5 256.06/90.15 -->_2 +^#(0(), y) -> c_4() :4 256.06/90.15 -->_1 +^#(0(), y) -> c_4() :4 256.06/90.15 -->_2 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.15 256.06/90.15 2: +^#(x, 0()) -> c_2() 256.06/90.15 256.06/90.15 3: +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.15 -->_1 +^#(s(x), y) -> c_5(+^#(x, y)) :5 256.06/90.15 -->_1 +^#(0(), y) -> c_4() :4 256.06/90.15 -->_1 +^#(x, s(y)) -> c_3(+^#(x, y)) :3 256.06/90.15 -->_1 +^#(x, 0()) -> c_2() :2 256.06/90.15 -->_1 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.15 256.06/90.15 4: +^#(0(), y) -> c_4() 256.06/90.15 256.06/90.15 5: +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.15 -->_1 +^#(s(x), y) -> c_5(+^#(x, y)) :5 256.06/90.15 -->_1 +^#(0(), y) -> c_4() :4 256.06/90.15 -->_1 +^#(x, s(y)) -> c_3(+^#(x, y)) :3 256.06/90.15 -->_1 +^#(x, 0()) -> c_2() :2 256.06/90.15 -->_1 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.15 256.06/90.15 6: f^#(g(f(x))) -> c_6(f^#(h(s(0()), x))) 256.06/90.15 -->_1 f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) :8 256.06/90.15 256.06/90.15 7: f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.15 -->_1 f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) :8 256.06/90.15 256.06/90.15 8: f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) 256.06/90.15 -->_1 f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) :8 256.06/90.15 -->_2 +^#(s(x), y) -> c_5(+^#(x, y)) :5 256.06/90.15 -->_2 +^#(0(), y) -> c_4() :4 256.06/90.15 -->_2 +^#(x, s(y)) -> c_3(+^#(x, y)) :3 256.06/90.15 -->_2 +^#(x, 0()) -> c_2() :2 256.06/90.15 -->_2 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.15 256.06/90.15 256.06/90.15 Only the nodes {2,3,5,4,1,7,8} are reachable from nodes 256.06/90.15 {2,3,4,5,7,8} that start derivation from marked basic terms. The 256.06/90.15 nodes not reachable are removed from the problem. 256.06/90.15 256.06/90.15 We are left with following problem, upon which TcT provides the 256.06/90.15 certificate YES(O(1),O(n^3)). 256.06/90.15 256.06/90.15 Strict DPs: 256.06/90.15 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 , +^#(x, 0()) -> c_2() 256.06/90.15 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.15 , +^#(0(), y) -> c_4() 256.06/90.15 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.15 , f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.15 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.15 Weak Trs: 256.06/90.15 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.15 , +(x, 0()) -> x 256.06/90.15 , +(x, s(y)) -> s(+(x, y)) 256.06/90.15 , +(0(), y) -> y 256.06/90.15 , +(s(x), y) -> s(+(x, y)) 256.06/90.15 , f(g(f(x))) -> f(h(s(0()), x)) 256.06/90.15 , f(g(h(x, y))) -> f(h(s(x), y)) 256.06/90.15 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 256.06/90.15 Obligation: 256.06/90.15 innermost runtime complexity 256.06/90.15 Answer: 256.06/90.15 YES(O(1),O(n^3)) 256.06/90.15 256.06/90.15 We estimate the number of application of {2,4} by applications of 256.06/90.15 Pre({2,4}) = {1,3,5,7}. Here rules are labeled as follows: 256.06/90.15 256.06/90.15 DPs: 256.06/90.15 { 1: +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 , 2: +^#(x, 0()) -> c_2() 256.06/90.15 , 3: +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.15 , 4: +^#(0(), y) -> c_4() 256.06/90.15 , 5: +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.15 , 6: f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.15 , 7: f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.15 256.06/90.15 We are left with following problem, upon which TcT provides the 256.06/90.15 certificate YES(O(1),O(n^3)). 256.06/90.15 256.06/90.15 Strict DPs: 256.06/90.15 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.15 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.15 , f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.15 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.15 Weak DPs: 256.06/90.15 { +^#(x, 0()) -> c_2() 256.06/90.15 , +^#(0(), y) -> c_4() } 256.06/90.15 Weak Trs: 256.06/90.15 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.15 , +(x, 0()) -> x 256.06/90.15 , +(x, s(y)) -> s(+(x, y)) 256.06/90.15 , +(0(), y) -> y 256.06/90.15 , +(s(x), y) -> s(+(x, y)) 256.06/90.15 , f(g(f(x))) -> f(h(s(0()), x)) 256.06/90.15 , f(g(h(x, y))) -> f(h(s(x), y)) 256.06/90.15 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 256.06/90.15 Obligation: 256.06/90.15 innermost runtime complexity 256.06/90.15 Answer: 256.06/90.15 YES(O(1),O(n^3)) 256.06/90.15 256.06/90.15 The following weak DPs constitute a sub-graph of the DG that is 256.06/90.15 closed under successors. The DPs are removed. 256.06/90.15 256.06/90.15 { +^#(x, 0()) -> c_2() 256.06/90.15 , +^#(0(), y) -> c_4() } 256.06/90.15 256.06/90.15 We are left with following problem, upon which TcT provides the 256.06/90.15 certificate YES(O(1),O(n^3)). 256.06/90.15 256.06/90.15 Strict DPs: 256.06/90.15 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.15 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.15 , f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.15 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.15 Weak Trs: 256.06/90.15 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.15 , +(x, 0()) -> x 256.06/90.15 , +(x, s(y)) -> s(+(x, y)) 256.06/90.15 , +(0(), y) -> y 256.06/90.15 , +(s(x), y) -> s(+(x, y)) 256.06/90.15 , f(g(f(x))) -> f(h(s(0()), x)) 256.06/90.15 , f(g(h(x, y))) -> f(h(s(x), y)) 256.06/90.15 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 256.06/90.15 Obligation: 256.06/90.15 innermost runtime complexity 256.06/90.15 Answer: 256.06/90.15 YES(O(1),O(n^3)) 256.06/90.15 256.06/90.15 Consider the dependency graph 256.06/90.15 256.06/90.15 1: +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.15 -->_2 +^#(s(x), y) -> c_5(+^#(x, y)) :3 256.06/90.15 -->_1 +^#(s(x), y) -> c_5(+^#(x, y)) :3 256.06/90.16 -->_2 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.16 256.06/90.16 2: +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 -->_1 +^#(s(x), y) -> c_5(+^#(x, y)) :3 256.06/90.16 -->_1 +^#(x, s(y)) -> c_3(+^#(x, y)) :2 256.06/90.16 -->_1 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.16 256.06/90.16 3: +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 -->_1 +^#(s(x), y) -> c_5(+^#(x, y)) :3 256.06/90.16 -->_1 +^#(x, s(y)) -> c_3(+^#(x, y)) :2 256.06/90.16 -->_1 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.16 256.06/90.16 4: f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) 256.06/90.16 -->_1 f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) :5 256.06/90.16 256.06/90.16 5: f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) 256.06/90.16 -->_1 f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) :5 256.06/90.16 -->_2 +^#(s(x), y) -> c_5(+^#(x, y)) :3 256.06/90.16 -->_2 +^#(x, s(y)) -> c_3(+^#(x, y)) :2 256.06/90.16 -->_2 +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) :1 256.06/90.16 256.06/90.16 256.06/90.16 Following roots of the dependency graph are removed, as the 256.06/90.16 considered set of starting terms is closed under reduction with 256.06/90.16 respect to these rules (modulo compound contexts). 256.06/90.16 256.06/90.16 { f^#(g(h(x, y))) -> c_7(f^#(h(s(x), y))) } 256.06/90.16 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(n^3)). 256.06/90.16 256.06/90.16 Strict DPs: 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) 256.06/90.16 , f(g(f(x))) -> f(h(s(0()), x)) 256.06/90.16 , f(g(h(x, y))) -> f(h(s(x), y)) 256.06/90.16 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(n^3)) 256.06/90.16 256.06/90.16 We replace rewrite rules by usable rules: 256.06/90.16 256.06/90.16 Weak Usable Rules: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(n^3)). 256.06/90.16 256.06/90.16 Strict DPs: 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(n^3)) 256.06/90.16 256.06/90.16 We use the processor 'matrix interpretation of dimension 2' to 256.06/90.16 orient following rules strictly. 256.06/90.16 256.06/90.16 DPs: 256.06/90.16 { 2: +^#(x, s(y)) -> c_3(+^#(x, y)) } 256.06/90.16 256.06/90.16 Sub-proof: 256.06/90.16 ---------- 256.06/90.16 The following argument positions are usable: 256.06/90.16 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1}, 256.06/90.16 Uargs(c_8) = {1, 2} 256.06/90.16 256.06/90.16 TcT has computed the following constructor-based matrix 256.06/90.16 interpretation satisfying not(EDA) and not(IDA(1)). 256.06/90.16 256.06/90.16 [+](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 256.06/90.16 [0 1] [0 1] [0] 256.06/90.16 256.06/90.16 [0] = [0] 256.06/90.16 [0] 256.06/90.16 256.06/90.16 [s](x1) = [0 0] x1 + [0] 256.06/90.16 [0 1] [3] 256.06/90.16 256.06/90.16 [h](x1, x2) = [0 0] x1 + [0 2] x2 + [0] 256.06/90.16 [0 1] [0 1] [0] 256.06/90.16 256.06/90.16 [+^#](x1, x2) = [0 3] x2 + [0] 256.06/90.16 [4 0] [4] 256.06/90.16 256.06/90.16 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 256.06/90.16 [0 0] [0 0] [3] 256.06/90.16 256.06/90.16 [c_3](x1) = [1 0] x1 + [5] 256.06/90.16 [0 0] [3] 256.06/90.16 256.06/90.16 [c_5](x1) = [1 0] x1 + [0] 256.06/90.16 [0 0] [3] 256.06/90.16 256.06/90.16 [f^#](x1) = [4 0] x1 + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 256.06/90.16 [c_8](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 256.06/90.16 [0 0] [0 0] [0] 256.06/90.16 256.06/90.16 The order satisfies the following ordering constraints: 256.06/90.16 256.06/90.16 [+(x, +(y, z))] = [1 0] x + [2 0] y + [4 0] z + [0] 256.06/90.16 [0 1] [0 1] [0 1] [0] 256.06/90.16 >= [1 0] x + [2 0] y + [2 0] z + [0] 256.06/90.16 [0 1] [0 1] [0 1] [0] 256.06/90.16 = [+(+(x, y), z)] 256.06/90.16 256.06/90.16 [+(x, 0())] = [1 0] x + [0] 256.06/90.16 [0 1] [0] 256.06/90.16 >= [1 0] x + [0] 256.06/90.16 [0 1] [0] 256.06/90.16 = [x] 256.06/90.16 256.06/90.16 [+(x, s(y))] = [1 0] x + [0 0] y + [0] 256.06/90.16 [0 1] [0 1] [3] 256.06/90.16 >= [0 0] x + [0 0] y + [0] 256.06/90.16 [0 1] [0 1] [3] 256.06/90.16 = [s(+(x, y))] 256.06/90.16 256.06/90.16 [+(0(), y)] = [2 0] y + [0] 256.06/90.16 [0 1] [0] 256.06/90.16 >= [1 0] y + [0] 256.06/90.16 [0 1] [0] 256.06/90.16 = [y] 256.06/90.16 256.06/90.16 [+(s(x), y)] = [0 0] x + [2 0] y + [0] 256.06/90.16 [0 1] [0 1] [3] 256.06/90.16 >= [0 0] x + [0 0] y + [0] 256.06/90.16 [0 1] [0 1] [3] 256.06/90.16 = [s(+(x, y))] 256.06/90.16 256.06/90.16 [+^#(x, +(y, z))] = [0 3] y + [0 3] z + [0] 256.06/90.16 [4 0] [8 0] [4] 256.06/90.16 >= [0 3] y + [0 3] z + [0] 256.06/90.16 [0 0] [0 0] [3] 256.06/90.16 = [c_1(+^#(+(x, y), z), +^#(x, y))] 256.06/90.16 256.06/90.16 [+^#(x, s(y))] = [0 3] y + [9] 256.06/90.16 [0 0] [4] 256.06/90.16 > [0 3] y + [5] 256.06/90.16 [0 0] [3] 256.06/90.16 = [c_3(+^#(x, y))] 256.06/90.16 256.06/90.16 [+^#(s(x), y)] = [0 3] y + [0] 256.06/90.16 [4 0] [4] 256.06/90.16 >= [0 3] y + [0] 256.06/90.16 [0 0] [3] 256.06/90.16 = [c_5(+^#(x, y))] 256.06/90.16 256.06/90.16 [f^#(h(x, h(y, z)))] = [0 8] y + [0 8] z + [0] 256.06/90.16 [0 0] [0 0] [0] 256.06/90.16 >= [0 6] y + [0 8] z + [0] 256.06/90.16 [0 0] [0 0] [0] 256.06/90.16 = [c_8(f^#(h(+(x, y), z)), +^#(x, y))] 256.06/90.16 256.06/90.16 256.06/90.16 The strictly oriented rules are moved into the weak component. 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(n^3)). 256.06/90.16 256.06/90.16 Strict DPs: 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 Weak DPs: { +^#(x, s(y)) -> c_3(+^#(x, y)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(n^3)) 256.06/90.16 256.06/90.16 We use the processor 'matrix interpretation of dimension 2' to 256.06/90.16 orient following rules strictly. 256.06/90.16 256.06/90.16 DPs: 256.06/90.16 { 1: +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) } 256.06/90.16 256.06/90.16 Sub-proof: 256.06/90.16 ---------- 256.06/90.16 The following argument positions are usable: 256.06/90.16 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1}, 256.06/90.16 Uargs(c_8) = {1, 2} 256.06/90.16 256.06/90.16 TcT has computed the following constructor-based matrix 256.06/90.16 interpretation satisfying not(EDA) and not(IDA(1)). 256.06/90.16 256.06/90.16 [+](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 256.06/90.16 [0 1] [0 2] [1] 256.06/90.16 256.06/90.16 [0] = [0] 256.06/90.16 [0] 256.06/90.16 256.06/90.16 [s](x1) = [0 0] x1 + [0] 256.06/90.16 [0 1] [0] 256.06/90.16 256.06/90.16 [h](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 256.06/90.16 [0 1] [0 0] [0] 256.06/90.16 256.06/90.16 [+^#](x1, x2) = [0 4] x2 + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 256.06/90.16 [c_1](x1, x2) = [2 0] x1 + [1 0] x2 + [1] 256.06/90.16 [0 0] [0 0] [0] 256.06/90.16 256.06/90.16 [c_3](x1) = [1 0] x1 + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 256.06/90.16 [c_5](x1) = [1 0] x1 + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 256.06/90.16 [f^#](x1) = [4 0] x1 + [0] 256.06/90.16 [0 0] [4] 256.06/90.16 256.06/90.16 [c_8](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 256.06/90.16 [0 0] [0 0] [3] 256.06/90.16 256.06/90.16 The order satisfies the following ordering constraints: 256.06/90.16 256.06/90.16 [+(x, +(y, z))] = [1 0] x + [1 0] y + [1 0] z + [0] 256.06/90.16 [0 1] [0 2] [0 4] [3] 256.06/90.16 >= [1 0] x + [1 0] y + [1 0] z + [0] 256.06/90.16 [0 1] [0 2] [0 2] [2] 256.06/90.16 = [+(+(x, y), z)] 256.06/90.16 256.06/90.16 [+(x, 0())] = [1 0] x + [0] 256.06/90.16 [0 1] [1] 256.06/90.16 >= [1 0] x + [0] 256.06/90.16 [0 1] [0] 256.06/90.16 = [x] 256.06/90.16 256.06/90.16 [+(x, s(y))] = [1 0] x + [0 0] y + [0] 256.06/90.16 [0 1] [0 2] [1] 256.06/90.16 >= [0 0] x + [0 0] y + [0] 256.06/90.16 [0 1] [0 2] [1] 256.06/90.16 = [s(+(x, y))] 256.06/90.16 256.06/90.16 [+(0(), y)] = [1 0] y + [0] 256.06/90.16 [0 2] [1] 256.06/90.16 >= [1 0] y + [0] 256.06/90.16 [0 1] [0] 256.06/90.16 = [y] 256.06/90.16 256.06/90.16 [+(s(x), y)] = [0 0] x + [1 0] y + [0] 256.06/90.16 [0 1] [0 2] [1] 256.06/90.16 >= [0 0] x + [0 0] y + [0] 256.06/90.16 [0 1] [0 2] [1] 256.06/90.16 = [s(+(x, y))] 256.06/90.16 256.06/90.16 [+^#(x, +(y, z))] = [0 4] y + [0 8] z + [4] 256.06/90.16 [0 0] [0 0] [0] 256.06/90.16 > [0 4] y + [0 8] z + [1] 256.06/90.16 [0 0] [0 0] [0] 256.06/90.16 = [c_1(+^#(+(x, y), z), +^#(x, y))] 256.06/90.16 256.06/90.16 [+^#(x, s(y))] = [0 4] y + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 >= [0 4] y + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 = [c_3(+^#(x, y))] 256.06/90.16 256.06/90.16 [+^#(s(x), y)] = [0 4] y + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 >= [0 4] y + [0] 256.06/90.16 [0 0] [0] 256.06/90.16 = [c_5(+^#(x, y))] 256.06/90.16 256.06/90.16 [f^#(h(x, h(y, z)))] = [0 4] y + [4 4] z + [0] 256.06/90.16 [0 0] [0 0] [4] 256.06/90.16 >= [0 4] y + [4 4] z + [0] 256.06/90.16 [0 0] [0 0] [3] 256.06/90.16 = [c_8(f^#(h(+(x, y), z)), +^#(x, y))] 256.06/90.16 256.06/90.16 256.06/90.16 The strictly oriented rules are moved into the weak component. 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(n^3)). 256.06/90.16 256.06/90.16 Strict DPs: 256.06/90.16 { +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 , f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 Weak DPs: 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(x, s(y)) -> c_3(+^#(x, y)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(n^3)) 256.06/90.16 256.06/90.16 We decompose the input problem according to the dependency graph 256.06/90.16 into the upper component 256.06/90.16 256.06/90.16 { f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 256.06/90.16 and lower component 256.06/90.16 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 , +^#(s(x), y) -> c_5(+^#(x, y)) } 256.06/90.16 256.06/90.16 Further, following extension rules are added to the lower 256.06/90.16 component. 256.06/90.16 256.06/90.16 { f^#(h(x, h(y, z))) -> +^#(x, y) 256.06/90.16 , f^#(h(x, h(y, z))) -> f^#(h(+(x, y), z)) } 256.06/90.16 256.06/90.16 TcT solves the upper component with certificate YES(O(1),O(n^1)). 256.06/90.16 256.06/90.16 Sub-proof: 256.06/90.16 ---------- 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(n^1)). 256.06/90.16 256.06/90.16 Strict DPs: 256.06/90.16 { f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(n^1)) 256.06/90.16 256.06/90.16 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 256.06/90.16 to orient following rules strictly. 256.06/90.16 256.06/90.16 DPs: 256.06/90.16 { 1: f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 256.06/90.16 Sub-proof: 256.06/90.16 ---------- 256.06/90.16 The input was oriented with the instance of 'Small Polynomial Path 256.06/90.16 Order (PS,1-bounded)' as induced by the safe mapping 256.06/90.16 256.06/90.16 safe(+) = {1, 2}, safe(0) = {}, safe(s) = {1}, safe(h) = {1, 2}, 256.06/90.16 safe(+^#) = {}, safe(f^#) = {}, safe(c_8) = {} 256.06/90.16 256.06/90.16 and precedence 256.06/90.16 256.06/90.16 empty . 256.06/90.16 256.06/90.16 Following symbols are considered recursive: 256.06/90.16 256.06/90.16 {f^#} 256.06/90.16 256.06/90.16 The recursion depth is 1. 256.06/90.16 256.06/90.16 Further, following argument filtering is employed: 256.06/90.16 256.06/90.16 pi(+) = [], pi(0) = [], pi(s) = [], pi(h) = [2], pi(+^#) = [], 256.06/90.16 pi(f^#) = [1], pi(c_8) = [1, 2] 256.06/90.16 256.06/90.16 Usable defined function symbols are a subset of: 256.06/90.16 256.06/90.16 {+^#, f^#} 256.06/90.16 256.06/90.16 For your convenience, here are the satisfied ordering constraints: 256.06/90.16 256.06/90.16 pi(f^#(h(x, h(y, z)))) = f^#(h(; h(; z));) 256.06/90.16 > c_8(f^#(h(; z);), +^#();) 256.06/90.16 = pi(c_8(f^#(h(+(x, y), z)), +^#(x, y))) 256.06/90.16 256.06/90.16 256.06/90.16 The strictly oriented rules are moved into the weak component. 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(1)). 256.06/90.16 256.06/90.16 Weak DPs: 256.06/90.16 { f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(1)) 256.06/90.16 256.06/90.16 The following weak DPs constitute a sub-graph of the DG that is 256.06/90.16 closed under successors. The DPs are removed. 256.06/90.16 256.06/90.16 { f^#(h(x, h(y, z))) -> c_8(f^#(h(+(x, y), z)), +^#(x, y)) } 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(1)). 256.06/90.16 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(1)) 256.06/90.16 256.06/90.16 No rule is usable, rules are removed from the input problem. 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(1)). 256.06/90.16 256.06/90.16 Rules: Empty 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(1)) 256.06/90.16 256.06/90.16 Empty rules are trivially bounded 256.06/90.16 256.06/90.16 We return to the main proof. 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(n^2)). 256.06/90.16 256.06/90.16 Strict DPs: { +^#(s(x), y) -> c_5(+^#(x, y)) } 256.06/90.16 Weak DPs: 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 , f^#(h(x, h(y, z))) -> +^#(x, y) 256.06/90.16 , f^#(h(x, h(y, z))) -> f^#(h(+(x, y), z)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(n^2)) 256.06/90.16 256.06/90.16 We use the processor 'polynomial interpretation' to orient 256.06/90.16 following rules strictly. 256.06/90.16 256.06/90.16 DPs: 256.06/90.16 { 1: +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 , 3: +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 , 4: f^#(h(x, h(y, z))) -> +^#(x, y) } 256.06/90.16 Trs: 256.06/90.16 { +(x, 0()) -> x 256.06/90.16 , +(0(), y) -> y } 256.06/90.16 256.06/90.16 Sub-proof: 256.06/90.16 ---------- 256.06/90.16 We consider the following typing: 256.06/90.16 256.06/90.16 + :: (a,a) -> a 256.06/90.16 0 :: a 256.06/90.16 s :: a -> a 256.06/90.16 h :: (a,c) -> c 256.06/90.16 +^# :: (a,a) -> b 256.06/90.16 c_1 :: (b,b) -> b 256.06/90.16 c_3 :: b -> b 256.06/90.16 c_5 :: b -> b 256.06/90.16 f^# :: c -> b 256.06/90.16 256.06/90.16 The following argument positions are considered usable: 256.06/90.16 256.06/90.16 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1} 256.06/90.16 256.06/90.16 TcT has computed the following constructor-restricted 256.06/90.16 typedpolynomial interpretation. 256.06/90.16 256.06/90.16 [+](x1, x2) = 1 + x1 + x2 256.06/90.16 256.06/90.16 [0]() = 1 256.06/90.16 256.06/90.16 [s](x1) = 2 + x1 256.06/90.16 256.06/90.16 [h](x1, x2) = 1 + x1 + x2 256.06/90.16 256.06/90.16 [+^#](x1, x2) = x1 + 2*x1*x2 + x2^2 256.06/90.16 256.06/90.16 [c_1](x1, x2) = x1 + x2 256.06/90.16 256.06/90.16 [c_3](x1) = x1 256.06/90.16 256.06/90.16 [c_5](x1) = x1 256.06/90.16 256.06/90.16 [f^#](x1) = x1^2 256.06/90.16 256.06/90.16 256.06/90.16 This order satisfies the following ordering constraints. 256.06/90.16 256.06/90.16 [+(x, +(y, z))] = 2 + x + y + z 256.06/90.16 >= 2 + x + y + z 256.06/90.16 = [+(+(x, y), z)] 256.06/90.16 256.06/90.16 [+(x, 0())] = 2 + x 256.06/90.16 > x 256.06/90.16 = [x] 256.06/90.16 256.06/90.16 [+(x, s(y))] = 3 + x + y 256.06/90.16 >= 3 + x + y 256.06/90.16 = [s(+(x, y))] 256.06/90.16 256.06/90.16 [+(0(), y)] = 2 + y 256.06/90.16 > y 256.06/90.16 = [y] 256.06/90.16 256.06/90.16 [+(s(x), y)] = 3 + x + y 256.06/90.16 >= 3 + x + y 256.06/90.16 = [s(+(x, y))] 256.06/90.16 256.06/90.16 [+^#(x, +(y, z))] = 3*x + 2*x*y + 2*x*z + 1 + 2*y + 2*z + y^2 + y*z + z*y + z^2 256.06/90.16 >= 1 + 2*x + y + 2*z + 2*x*z + 2*y*z + z^2 + 2*x*y + y^2 256.06/90.16 = [c_1(+^#(+(x, y), z), +^#(x, y))] 256.06/90.16 256.06/90.16 [+^#(x, s(y))] = 5*x + 2*x*y + 4 + 4*y + y^2 256.06/90.16 > x + 2*x*y + y^2 256.06/90.16 = [c_3(+^#(x, y))] 256.06/90.16 256.06/90.16 [+^#(s(x), y)] = 2 + x + 4*y + 2*x*y + y^2 256.06/90.16 > x + 2*x*y + y^2 256.06/90.16 = [c_5(+^#(x, y))] 256.06/90.16 256.06/90.16 [f^#(h(x, h(y, z)))] = 4 + 4*x + 4*y + 4*z + x^2 + x*y + x*z + y*x + y^2 + y*z + z*x + z*y + z^2 256.06/90.16 > x + 2*x*y + y^2 256.06/90.16 = [+^#(x, y)] 256.06/90.16 256.06/90.16 [f^#(h(x, h(y, z)))] = 4 + 4*x + 4*y + 4*z + x^2 + x*y + x*z + y*x + y^2 + y*z + z*x + z*y + z^2 256.06/90.16 >= 4 + 4*x + 4*y + 4*z + x^2 + x*y + x*z + y*x + y^2 + y*z + z*x + z*y + z^2 256.06/90.16 = [f^#(h(+(x, y), z))] 256.06/90.16 256.06/90.16 256.06/90.16 The strictly oriented rules are moved into the weak component. 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(1)). 256.06/90.16 256.06/90.16 Weak DPs: 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 , f^#(h(x, h(y, z))) -> +^#(x, y) 256.06/90.16 , f^#(h(x, h(y, z))) -> f^#(h(+(x, y), z)) } 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(1)) 256.06/90.16 256.06/90.16 The following weak DPs constitute a sub-graph of the DG that is 256.06/90.16 closed under successors. The DPs are removed. 256.06/90.16 256.06/90.16 { +^#(x, +(y, z)) -> c_1(+^#(+(x, y), z), +^#(x, y)) 256.06/90.16 , +^#(x, s(y)) -> c_3(+^#(x, y)) 256.06/90.16 , +^#(s(x), y) -> c_5(+^#(x, y)) 256.06/90.16 , f^#(h(x, h(y, z))) -> +^#(x, y) 256.06/90.16 , f^#(h(x, h(y, z))) -> f^#(h(+(x, y), z)) } 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(1)). 256.06/90.16 256.06/90.16 Weak Trs: 256.06/90.16 { +(x, +(y, z)) -> +(+(x, y), z) 256.06/90.16 , +(x, 0()) -> x 256.06/90.16 , +(x, s(y)) -> s(+(x, y)) 256.06/90.16 , +(0(), y) -> y 256.06/90.16 , +(s(x), y) -> s(+(x, y)) } 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(1)) 256.06/90.16 256.06/90.16 No rule is usable, rules are removed from the input problem. 256.06/90.16 256.06/90.16 We are left with following problem, upon which TcT provides the 256.06/90.16 certificate YES(O(1),O(1)). 256.06/90.16 256.06/90.16 Rules: Empty 256.06/90.16 Obligation: 256.06/90.16 innermost runtime complexity 256.06/90.16 Answer: 256.06/90.16 YES(O(1),O(1)) 256.06/90.16 256.06/90.16 Empty rules are trivially bounded 256.06/90.16 256.06/90.16 Hurray, we answered YES(O(1),O(n^3)) 256.27/90.24 EOF