YES(O(1),O(n^2)) 210.50/60.11 YES(O(1),O(n^2)) 210.50/60.11 210.50/60.11 We are left with following problem, upon which TcT provides the 210.50/60.11 certificate YES(O(1),O(n^2)). 210.50/60.11 210.50/60.11 Strict Trs: 210.50/60.11 { g(f(x), y) -> f(h(x, y)) 210.50/60.11 , h(x, y) -> g(x, f(y)) } 210.50/60.11 Obligation: 210.50/60.11 derivational complexity 210.50/60.11 Answer: 210.50/60.11 YES(O(1),O(n^2)) 210.50/60.11 210.50/60.11 The weightgap principle applies (using the following nonconstant 210.50/60.11 growth matrix-interpretation) 210.50/60.11 210.50/60.11 TcT has computed the following triangular matrix interpretation. 210.50/60.11 Note that the diagonal of the component-wise maxima of 210.50/60.11 interpretation-entries contains no more than 1 non-zero entries. 210.50/60.11 210.50/60.11 [g](x1, x2) = [1] x1 + [1] x2 + [0] 210.50/60.11 210.50/60.11 [f](x1) = [1] x1 + [0] 210.50/60.11 210.50/60.11 [h](x1, x2) = [1] x1 + [1] x2 + [1] 210.50/60.11 210.50/60.11 The order satisfies the following ordering constraints: 210.50/60.11 210.50/60.11 [g(f(x), y)] = [1] x + [1] y + [0] 210.50/60.11 ? [1] x + [1] y + [1] 210.50/60.11 = [f(h(x, y))] 210.50/60.11 210.50/60.11 [h(x, y)] = [1] x + [1] y + [1] 210.50/60.11 > [1] x + [1] y + [0] 210.50/60.11 = [g(x, f(y))] 210.50/60.11 210.50/60.11 210.50/60.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 210.50/60.11 210.50/60.11 We are left with following problem, upon which TcT provides the 210.50/60.11 certificate YES(O(1),O(n^2)). 210.50/60.11 210.50/60.11 Strict Trs: { g(f(x), y) -> f(h(x, y)) } 210.50/60.11 Weak Trs: { h(x, y) -> g(x, f(y)) } 210.50/60.11 Obligation: 210.50/60.11 derivational complexity 210.50/60.11 Answer: 210.50/60.11 YES(O(1),O(n^2)) 210.50/60.11 210.50/60.11 We use the processor 'matrix interpretation of dimension 2' to 210.50/60.11 orient following rules strictly. 210.50/60.11 210.50/60.11 Trs: { g(f(x), y) -> f(h(x, y)) } 210.50/60.11 210.50/60.11 The induced complexity on above rules (modulo remaining rules) is 210.50/60.11 YES(?,O(n^2)) . These rules are moved into the corresponding weak 210.50/60.11 component(s). 210.50/60.11 210.50/60.11 Sub-proof: 210.50/60.11 ---------- 210.50/60.11 TcT has computed the following triangular matrix interpretation. 210.50/60.11 210.50/60.11 [g](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 210.50/60.11 [0 1] [0 0] [0] 210.50/60.11 210.50/60.11 [f](x1) = [1 0] x1 + [0] 210.50/60.11 [0 1] [1] 210.50/60.11 210.50/60.11 [h](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 210.50/60.11 [0 1] [0 0] [0] 210.50/60.11 210.50/60.11 The order satisfies the following ordering constraints: 210.50/60.11 210.50/60.11 [g(f(x), y)] = [1 1] x + [1 0] y + [1] 210.50/60.11 [0 1] [0 0] [1] 210.50/60.11 > [1 1] x + [1 0] y + [0] 210.50/60.11 [0 1] [0 0] [1] 210.50/60.11 = [f(h(x, y))] 210.50/60.11 210.50/60.11 [h(x, y)] = [1 1] x + [1 0] y + [0] 210.50/60.11 [0 1] [0 0] [0] 210.50/60.11 >= [1 1] x + [1 0] y + [0] 210.50/60.11 [0 1] [0 0] [0] 210.50/60.11 = [g(x, f(y))] 210.50/60.11 210.50/60.11 210.50/60.11 We return to the main proof. 210.50/60.11 210.50/60.11 We are left with following problem, upon which TcT provides the 210.50/60.11 certificate YES(O(1),O(1)). 210.50/60.11 210.50/60.11 Weak Trs: 210.50/60.11 { g(f(x), y) -> f(h(x, y)) 210.50/60.11 , h(x, y) -> g(x, f(y)) } 210.50/60.11 Obligation: 210.50/60.11 derivational complexity 210.50/60.11 Answer: 210.50/60.11 YES(O(1),O(1)) 210.50/60.11 210.50/60.11 Empty rules are trivially bounded 210.50/60.11 210.50/60.11 Hurray, we answered YES(O(1),O(n^2)) 210.50/60.14 EOF