YES(O(1),O(n^1)) 271.48/98.05 YES(O(1),O(n^1)) 271.48/98.05 271.48/98.05 We are left with following problem, upon which TcT provides the 271.48/98.05 certificate YES(O(1),O(n^1)). 271.48/98.05 271.48/98.05 Strict Trs: 271.48/98.05 { max(L(x)) -> x 271.48/98.05 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 271.48/98.05 , max(N(L(0()), L(y))) -> y 271.48/98.05 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 271.48/98.05 Obligation: 271.48/98.05 derivational complexity 271.48/98.05 Answer: 271.48/98.05 YES(O(1),O(n^1)) 271.48/98.05 271.48/98.05 We use the processor 'matrix interpretation of dimension 1' to 271.48/98.05 orient following rules strictly. 271.48/98.05 271.48/98.05 Trs: { max(N(L(0()), L(y))) -> y } 271.48/98.05 271.48/98.05 The induced complexity on above rules (modulo remaining rules) is 271.48/98.05 YES(?,O(n^1)) . These rules are moved into the corresponding weak 271.48/98.05 component(s). 271.48/98.05 271.48/98.05 Sub-proof: 271.48/98.05 ---------- 271.48/98.05 TcT has computed the following triangular matrix interpretation. 271.48/98.05 271.48/98.05 [max](x1) = [1] x1 + [0] 271.48/98.05 271.48/98.05 [L](x1) = [1] x1 + [0] 271.48/98.05 271.48/98.05 [N](x1, x2) = [1] x1 + [1] x2 + [0] 271.48/98.05 271.48/98.05 [0] = [1] 271.48/98.05 271.48/98.05 [s](x1) = [1] x1 + [0] 271.48/98.05 271.48/98.05 The order satisfies the following ordering constraints: 271.48/98.05 271.48/98.05 [max(L(x))] = [1] x + [0] 271.48/98.05 >= [1] x + [0] 271.48/98.05 = [x] 271.48/98.05 271.48/98.05 [max(N(L(x), N(y, z)))] = [1] x + [1] y + [1] z + [0] 271.48/98.05 >= [1] x + [1] y + [1] z + [0] 271.48/98.05 = [max(N(L(x), L(max(N(y, z)))))] 271.48/98.05 271.48/98.05 [max(N(L(0()), L(y)))] = [1] y + [1] 271.48/98.05 > [1] y + [0] 271.48/98.05 = [y] 271.48/98.05 271.48/98.05 [max(N(L(s(x)), L(s(y))))] = [1] x + [1] y + [0] 271.48/98.05 >= [1] x + [1] y + [0] 271.48/98.05 = [s(max(N(L(x), L(y))))] 271.48/98.05 271.48/98.05 271.48/98.05 We return to the main proof. 271.48/98.05 271.48/98.05 We are left with following problem, upon which TcT provides the 271.48/98.05 certificate YES(O(1),O(n^1)). 271.48/98.05 271.48/98.05 Strict Trs: 271.48/98.05 { max(L(x)) -> x 271.48/98.05 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 271.48/98.05 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 271.48/98.05 Weak Trs: { max(N(L(0()), L(y))) -> y } 271.48/98.05 Obligation: 271.48/98.05 derivational complexity 271.48/98.05 Answer: 271.48/98.05 YES(O(1),O(n^1)) 271.48/98.05 271.48/98.05 We use the processor 'matrix interpretation of dimension 1' to 271.48/98.05 orient following rules strictly. 271.48/98.05 271.48/98.05 Trs: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 271.48/98.05 271.48/98.05 The induced complexity on above rules (modulo remaining rules) is 271.48/98.05 YES(?,O(n^1)) . These rules are moved into the corresponding weak 271.48/98.05 component(s). 271.48/98.05 271.48/98.05 Sub-proof: 271.48/98.05 ---------- 271.48/98.05 TcT has computed the following triangular matrix interpretation. 271.48/98.05 271.48/98.05 [max](x1) = [1] x1 + [0] 271.48/98.05 271.48/98.05 [L](x1) = [1] x1 + [0] 271.48/98.05 271.48/98.05 [N](x1, x2) = [1] x1 + [1] x2 + [0] 271.48/98.05 271.48/98.05 [0] = [0] 271.48/98.05 271.48/98.05 [s](x1) = [1] x1 + [2] 271.48/98.05 271.48/98.05 The order satisfies the following ordering constraints: 271.48/98.05 271.48/98.05 [max(L(x))] = [1] x + [0] 271.48/98.05 >= [1] x + [0] 271.48/98.05 = [x] 271.48/98.05 271.48/98.05 [max(N(L(x), N(y, z)))] = [1] x + [1] y + [1] z + [0] 271.48/98.05 >= [1] x + [1] y + [1] z + [0] 271.48/98.05 = [max(N(L(x), L(max(N(y, z)))))] 271.48/98.05 271.48/98.05 [max(N(L(0()), L(y)))] = [1] y + [0] 271.48/98.05 >= [1] y + [0] 271.48/98.05 = [y] 271.48/98.05 271.48/98.05 [max(N(L(s(x)), L(s(y))))] = [1] x + [1] y + [4] 271.48/98.05 > [1] x + [1] y + [2] 271.48/98.05 = [s(max(N(L(x), L(y))))] 271.48/98.05 271.48/98.05 271.48/98.05 We return to the main proof. 271.48/98.05 271.48/98.05 We are left with following problem, upon which TcT provides the 271.48/98.05 certificate YES(O(1),O(n^1)). 271.48/98.05 271.48/98.05 Strict Trs: 271.48/98.05 { max(L(x)) -> x 271.48/98.05 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) } 271.48/98.05 Weak Trs: 271.48/98.05 { max(N(L(0()), L(y))) -> y 271.48/98.05 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 271.48/98.05 Obligation: 271.48/98.05 derivational complexity 271.48/98.05 Answer: 271.48/98.05 YES(O(1),O(n^1)) 271.48/98.05 271.48/98.05 The weightgap principle applies (using the following nonconstant 271.48/98.05 growth matrix-interpretation) 271.48/98.05 271.48/98.05 TcT has computed the following triangular matrix interpretation. 271.48/98.05 Note that the diagonal of the component-wise maxima of 271.48/98.05 interpretation-entries contains no more than 1 non-zero entries. 271.48/98.05 271.48/98.05 [max](x1) = [1] x1 + [1] 271.48/98.05 271.48/98.05 [L](x1) = [1] x1 + [0] 271.48/98.05 271.48/98.05 [N](x1, x2) = [1] x1 + [1] x2 + [0] 271.48/98.05 271.48/98.05 [0] = [0] 271.48/98.05 271.48/98.05 [s](x1) = [1] x1 + [0] 271.48/98.05 271.48/98.05 The order satisfies the following ordering constraints: 271.48/98.05 271.48/98.05 [max(L(x))] = [1] x + [1] 271.48/98.05 > [1] x + [0] 271.48/98.05 = [x] 271.48/98.05 271.48/98.05 [max(N(L(x), N(y, z)))] = [1] x + [1] y + [1] z + [1] 271.48/98.05 ? [1] x + [1] y + [1] z + [2] 271.48/98.05 = [max(N(L(x), L(max(N(y, z)))))] 271.48/98.05 271.48/98.05 [max(N(L(0()), L(y)))] = [1] y + [1] 271.48/98.05 > [1] y + [0] 271.48/98.05 = [y] 271.48/98.05 271.48/98.05 [max(N(L(s(x)), L(s(y))))] = [1] x + [1] y + [1] 271.48/98.05 >= [1] x + [1] y + [1] 271.48/98.05 = [s(max(N(L(x), L(y))))] 271.48/98.05 271.48/98.05 271.48/98.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 271.48/98.05 271.48/98.05 We are left with following problem, upon which TcT provides the 271.48/98.05 certificate YES(?,O(n^1)). 271.48/98.05 271.48/98.05 Strict Trs: 271.48/98.05 { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) } 271.48/98.05 Weak Trs: 271.48/98.05 { max(L(x)) -> x 271.48/98.05 , max(N(L(0()), L(y))) -> y 271.48/98.05 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 271.48/98.05 Obligation: 271.48/98.05 derivational complexity 271.48/98.05 Answer: 271.48/98.05 YES(?,O(n^1)) 271.48/98.05 271.48/98.05 The problem is match-bounded by 1. The enriched problem is 271.48/98.05 compatible with the following automaton. 271.48/98.05 { max_0(1) -> 1 271.48/98.05 , max_0(1) -> 5 271.48/98.05 , max_0(1) -> 7 271.48/98.05 , max_1(2) -> 1 271.48/98.05 , max_1(2) -> 5 271.48/98.05 , max_1(2) -> 7 271.48/98.05 , max_1(6) -> 1 271.48/98.05 , max_1(6) -> 5 271.48/98.05 , max_1(6) -> 7 271.48/98.05 , max_1(8) -> 7 271.48/98.05 , L_0(1) -> 1 271.48/98.05 , L_0(1) -> 5 271.48/98.05 , L_0(1) -> 7 271.48/98.05 , L_1(1) -> 3 271.48/98.05 , L_1(5) -> 4 271.48/98.05 , L_1(7) -> 3 271.48/98.05 , N_0(1, 1) -> 1 271.48/98.05 , N_0(1, 1) -> 5 271.48/98.05 , N_0(1, 1) -> 7 271.48/98.05 , N_1(1, 1) -> 6 271.48/98.05 , N_1(3, 3) -> 8 271.48/98.05 , N_1(3, 4) -> 2 271.48/98.05 , 0_0() -> 1 271.48/98.05 , 0_0() -> 5 271.48/98.05 , 0_0() -> 7 271.48/98.05 , s_0(1) -> 1 271.48/98.05 , s_0(1) -> 5 271.48/98.05 , s_0(1) -> 7 271.48/98.05 , s_1(7) -> 1 271.48/98.05 , s_1(7) -> 5 271.48/98.05 , s_1(7) -> 7 } 271.48/98.05 271.48/98.05 Hurray, we answered YES(O(1),O(n^1)) 271.59/98.15 EOF