YES(O(1),O(n^5)) 215.65/60.02 YES(O(1),O(n^5)) 215.65/60.02 215.65/60.02 We are left with following problem, upon which TcT provides the 215.65/60.02 certificate YES(O(1),O(n^5)). 215.65/60.02 215.65/60.02 Strict Trs: 215.65/60.02 { +(x, +(y, z)) -> +(+(x, y), z) 215.65/60.02 , +(x, 0()) -> x 215.65/60.02 , +(x, s(y)) -> s(+(x, y)) 215.65/60.02 , +(0(), y) -> y 215.65/60.02 , +(s(x), y) -> s(+(x, y)) 215.65/60.02 , f(g(f(x))) -> f(h(s(0()), x)) 215.65/60.02 , f(g(h(x, y))) -> f(h(s(x), y)) 215.65/60.02 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 215.65/60.02 Obligation: 215.65/60.02 derivational complexity 215.65/60.02 Answer: 215.65/60.02 YES(O(1),O(n^5)) 215.65/60.02 215.65/60.02 We use the processor 'matrix interpretation of dimension 1' to 215.65/60.02 orient following rules strictly. 215.65/60.02 215.65/60.02 Trs: 215.65/60.02 { +(x, 0()) -> x 215.65/60.02 , +(0(), y) -> y 215.65/60.02 , f(g(f(x))) -> f(h(s(0()), x)) 215.65/60.02 , f(g(h(x, y))) -> f(h(s(x), y)) 215.65/60.02 , f(h(x, h(y, z))) -> f(h(+(x, y), z)) } 215.65/60.02 215.65/60.02 The induced complexity on above rules (modulo remaining rules) is 215.65/60.02 YES(?,O(n^1)) . These rules are removed from the problem. Note that 215.65/60.02 none of the weakly oriented rules is size-increasing. The overall 215.65/60.02 complexity is obtained by composition . 215.65/60.02 215.65/60.02 Sub-proof: 215.65/60.02 ---------- 215.65/60.02 TcT has computed the following triangular matrix interpretation. 215.65/60.02 215.65/60.02 [+](x1, x2) = [1] x1 + [1] x2 + [1] 215.65/60.02 215.65/60.02 [0] = [0] 215.65/60.02 215.65/60.02 [s](x1) = [1] x1 + [0] 215.65/60.02 215.65/60.02 [f](x1) = [1] x1 + [2] 215.65/60.02 215.65/60.02 [g](x1) = [1] x1 + [1] 215.65/60.02 215.65/60.02 [h](x1, x2) = [1] x1 + [1] x2 + [2] 215.65/60.02 215.65/60.02 The order satisfies the following ordering constraints: 215.65/60.02 215.65/60.02 [+(x, +(y, z))] = [1] x + [1] y + [1] z + [2] 215.65/60.02 >= [1] x + [1] y + [1] z + [2] 215.65/60.02 = [+(+(x, y), z)] 215.65/60.02 215.65/60.02 [+(x, 0())] = [1] x + [1] 215.65/60.02 > [1] x + [0] 215.65/60.02 = [x] 215.65/60.02 215.65/60.02 [+(x, s(y))] = [1] x + [1] y + [1] 215.65/60.02 >= [1] x + [1] y + [1] 215.65/60.02 = [s(+(x, y))] 215.65/60.02 215.65/60.02 [+(0(), y)] = [1] y + [1] 215.65/60.02 > [1] y + [0] 215.65/60.02 = [y] 215.65/60.02 215.65/60.02 [+(s(x), y)] = [1] x + [1] y + [1] 215.65/60.02 >= [1] x + [1] y + [1] 215.65/60.02 = [s(+(x, y))] 215.65/60.02 215.65/60.02 [f(g(f(x)))] = [1] x + [5] 215.65/60.02 > [1] x + [4] 215.65/60.02 = [f(h(s(0()), x))] 215.65/60.02 215.65/60.02 [f(g(h(x, y)))] = [1] x + [1] y + [5] 215.65/60.02 > [1] x + [1] y + [4] 215.65/60.02 = [f(h(s(x), y))] 215.65/60.02 215.65/60.02 [f(h(x, h(y, z)))] = [1] x + [1] y + [1] z + [6] 215.65/60.02 > [1] x + [1] y + [1] z + [5] 215.65/60.02 = [f(h(+(x, y), z))] 215.65/60.02 215.65/60.02 215.65/60.02 We return to the main proof. 215.65/60.02 215.65/60.02 We are left with following problem, upon which TcT provides the 215.65/60.02 certificate YES(O(1),O(n^4)). 215.65/60.02 215.65/60.02 Strict Trs: 215.65/60.02 { +(x, +(y, z)) -> +(+(x, y), z) 215.65/60.02 , +(x, s(y)) -> s(+(x, y)) 215.65/60.02 , +(s(x), y) -> s(+(x, y)) } 215.65/60.02 Obligation: 215.65/60.02 derivational complexity 215.65/60.02 Answer: 215.65/60.02 YES(O(1),O(n^4)) 215.65/60.02 215.65/60.02 We use the processor 'matrix interpretation of dimension 2' to 215.65/60.02 orient following rules strictly. 215.65/60.02 215.65/60.02 Trs: 215.65/60.02 { +(x, +(y, z)) -> +(+(x, y), z) 215.65/60.02 , +(x, s(y)) -> s(+(x, y)) } 215.65/60.02 215.65/60.02 The induced complexity on above rules (modulo remaining rules) is 215.65/60.02 YES(?,O(n^2)) . These rules are removed from the problem. Note that 215.65/60.02 no rule is size-increasing. The overall complexity is obtained by 215.65/60.02 multiplication . 215.65/60.02 215.65/60.02 Sub-proof: 215.65/60.02 ---------- 215.65/60.02 TcT has computed the following triangular matrix interpretation. 215.65/60.02 215.65/60.02 [+](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 215.65/60.02 [0 1] [0 1] [1] 215.65/60.02 215.65/60.02 [s](x1) = [1 0] x1 + [2] 215.65/60.02 [0 1] [2] 215.65/60.02 215.65/60.02 The order satisfies the following ordering constraints: 215.65/60.02 215.65/60.02 [+(x, +(y, z))] = [1 0] x + [1 1] y + [1 2] z + [1] 215.65/60.02 [0 1] [0 1] [0 1] [2] 215.65/60.02 > [1 0] x + [1 1] y + [1 1] z + [0] 215.65/60.02 [0 1] [0 1] [0 1] [2] 215.65/60.02 = [+(+(x, y), z)] 215.65/60.02 215.65/60.02 [+(x, s(y))] = [1 0] x + [1 1] y + [4] 215.65/60.02 [0 1] [0 1] [3] 215.65/60.02 > [1 0] x + [1 1] y + [2] 215.65/60.02 [0 1] [0 1] [3] 215.65/60.02 = [s(+(x, y))] 215.65/60.02 215.65/60.02 [+(s(x), y)] = [1 0] x + [1 1] y + [2] 215.65/60.02 [0 1] [0 1] [3] 215.65/60.02 >= [1 0] x + [1 1] y + [2] 215.65/60.02 [0 1] [0 1] [3] 215.65/60.02 = [s(+(x, y))] 215.65/60.02 215.65/60.02 215.65/60.02 We return to the main proof. 215.65/60.02 215.65/60.02 We are left with following problem, upon which TcT provides the 215.65/60.02 certificate YES(?,O(n^2)). 215.65/60.02 215.65/60.02 Strict Trs: { +(s(x), y) -> s(+(x, y)) } 215.65/60.02 Obligation: 215.65/60.02 derivational complexity 215.65/60.02 Answer: 215.65/60.02 YES(?,O(n^2)) 215.65/60.02 215.65/60.02 TcT has computed the following triangular matrix interpretation. 215.65/60.02 215.65/60.02 [+](x1, x2) = [1 4] x1 + [1 7] x2 + [0] 215.65/60.02 [0 1] [0 0] [0] 215.65/60.02 215.65/60.02 [s](x1) = [1 4] x1 + [0] 215.65/60.02 [0 1] [2] 215.65/60.02 215.65/60.02 The order satisfies the following ordering constraints: 215.65/60.02 215.65/60.02 [+(s(x), y)] = [1 8] x + [1 7] y + [8] 215.65/60.02 [0 1] [0 0] [2] 215.65/60.02 > [1 8] x + [1 7] y + [0] 215.65/60.02 [0 1] [0 0] [2] 215.65/60.02 = [s(+(x, y))] 215.65/60.02 215.65/60.02 215.65/60.02 Hurray, we answered YES(O(1),O(n^5)) 215.65/60.06 EOF