YES(O(1),O(n^2)) 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict Trs: 44.38/21.10 { and(tt(), X) -> activate(X) 44.38/21.10 , activate(X) -> X 44.38/21.10 , plus(N, 0()) -> N 44.38/21.10 , plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 We add the following weak dependency pairs: 44.38/21.10 44.38/21.10 Strict DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , x^#(N, 0()) -> c_5() 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 44.38/21.10 and mark the set of starting terms. 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , x^#(N, 0()) -> c_5() 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Strict Trs: 44.38/21.10 { and(tt(), X) -> activate(X) 44.38/21.10 , activate(X) -> X 44.38/21.10 , plus(N, 0()) -> N 44.38/21.10 , plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 We replace rewrite rules by usable rules: 44.38/21.10 44.38/21.10 Strict Usable Rules: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , x^#(N, 0()) -> c_5() 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Strict Trs: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 We estimate the number of application of {5} by applications of 44.38/21.10 Pre({5}) = {2,3}. Here rules are labeled as follows: 44.38/21.10 44.38/21.10 DPs: 44.38/21.10 { 1: and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , 2: activate^#(X) -> c_2(X) 44.38/21.10 , 3: plus^#(N, 0()) -> c_3(N) 44.38/21.10 , 4: plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , 5: x^#(N, 0()) -> c_5() 44.38/21.10 , 6: x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Strict Trs: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Weak DPs: { x^#(N, 0()) -> c_5() } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 The weightgap principle applies (using the following nonconstant 44.38/21.10 growth matrix-interpretation) 44.38/21.10 44.38/21.10 The following argument positions are usable: 44.38/21.10 Uargs(plus) = {1}, Uargs(s) = {1}, Uargs(c_1) = {1}, 44.38/21.10 Uargs(plus^#) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 44.38/21.10 Uargs(c_6) = {1} 44.38/21.10 44.38/21.10 TcT has computed the following matrix interpretation satisfying 44.38/21.10 not(EDA) and not(IDA(1)). 44.38/21.10 44.38/21.10 [tt] = [7] 44.38/21.10 44.38/21.10 [plus](x1, x2) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [0] = [7] 44.38/21.10 44.38/21.10 [s](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [x](x1, x2) = [1] x2 + [7] 44.38/21.10 44.38/21.10 [and^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_1](x1) = [1] x1 + [3] 44.38/21.10 44.38/21.10 [activate^#](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [c_2](x1) = [1] x1 + [6] 44.38/21.10 44.38/21.10 [plus^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_3](x1) = [1] x1 + [5] 44.38/21.10 44.38/21.10 [c_4](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [x^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_5] = [5] 44.38/21.10 44.38/21.10 [c_6](x1) = [1] x1 + [1] 44.38/21.10 44.38/21.10 The order satisfies the following ordering constraints: 44.38/21.10 44.38/21.10 [plus(N, 0())] = [1] N + [7] 44.38/21.10 > [1] N + [0] 44.38/21.10 = [N] 44.38/21.10 44.38/21.10 [plus(N, s(M))] = [1] N + [7] 44.38/21.10 ? [1] N + [14] 44.38/21.10 = [s(plus(N, M))] 44.38/21.10 44.38/21.10 [x(N, 0())] = [14] 44.38/21.10 > [7] 44.38/21.10 = [0()] 44.38/21.10 44.38/21.10 [x(N, s(M))] = [1] M + [14] 44.38/21.10 >= [1] M + [14] 44.38/21.10 = [plus(x(N, M), N)] 44.38/21.10 44.38/21.10 [and^#(tt(), X)] = [1] X + [14] 44.38/21.10 > [1] X + [10] 44.38/21.10 = [c_1(activate^#(X))] 44.38/21.10 44.38/21.10 [activate^#(X)] = [1] X + [7] 44.38/21.10 > [1] X + [6] 44.38/21.10 = [c_2(X)] 44.38/21.10 44.38/21.10 [plus^#(N, 0())] = [1] N + [14] 44.38/21.10 > [1] N + [5] 44.38/21.10 = [c_3(N)] 44.38/21.10 44.38/21.10 [plus^#(N, s(M))] = [1] N + [1] M + [14] 44.38/21.10 >= [1] N + [1] M + [14] 44.38/21.10 = [c_4(plus^#(N, M))] 44.38/21.10 44.38/21.10 [x^#(N, 0())] = [1] N + [14] 44.38/21.10 > [5] 44.38/21.10 = [c_5()] 44.38/21.10 44.38/21.10 [x^#(N, s(M))] = [1] N + [1] M + [14] 44.38/21.10 ? [1] N + [1] M + [15] 44.38/21.10 = [c_6(plus^#(x(N, M), N))] 44.38/21.10 44.38/21.10 44.38/21.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict DPs: 44.38/21.10 { plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Strict Trs: 44.38/21.10 { plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Weak DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , x^#(N, 0()) -> c_5() } 44.38/21.10 Weak Trs: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , x(N, 0()) -> 0() } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 The weightgap principle applies (using the following nonconstant 44.38/21.10 growth matrix-interpretation) 44.38/21.10 44.38/21.10 The following argument positions are usable: 44.38/21.10 Uargs(plus) = {1}, Uargs(s) = {1}, Uargs(c_1) = {1}, 44.38/21.10 Uargs(plus^#) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 44.38/21.10 Uargs(c_6) = {1} 44.38/21.10 44.38/21.10 TcT has computed the following matrix interpretation satisfying 44.38/21.10 not(EDA) and not(IDA(1)). 44.38/21.10 44.38/21.10 [tt] = [7] 44.38/21.10 44.38/21.10 [plus](x1, x2) = [1] x1 + [4] 44.38/21.10 44.38/21.10 [0] = [4] 44.38/21.10 44.38/21.10 [s](x1) = [1] x1 + [0] 44.38/21.10 44.38/21.10 [x](x1, x2) = [4] 44.38/21.10 44.38/21.10 [and^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_1](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [activate^#](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [c_2](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [plus^#](x1, x2) = [1] x1 + [1] x2 + [0] 44.38/21.10 44.38/21.10 [c_3](x1) = [1] x1 + [4] 44.38/21.10 44.38/21.10 [c_4](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [x^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_5] = [3] 44.38/21.10 44.38/21.10 [c_6](x1) = [1] x1 + [2] 44.38/21.10 44.38/21.10 The order satisfies the following ordering constraints: 44.38/21.10 44.38/21.10 [plus(N, 0())] = [1] N + [4] 44.38/21.10 > [1] N + [0] 44.38/21.10 = [N] 44.38/21.10 44.38/21.10 [plus(N, s(M))] = [1] N + [4] 44.38/21.10 >= [1] N + [4] 44.38/21.10 = [s(plus(N, M))] 44.38/21.10 44.38/21.10 [x(N, 0())] = [4] 44.38/21.10 >= [4] 44.38/21.10 = [0()] 44.38/21.10 44.38/21.10 [x(N, s(M))] = [4] 44.38/21.10 ? [8] 44.38/21.10 = [plus(x(N, M), N)] 44.38/21.10 44.38/21.10 [and^#(tt(), X)] = [1] X + [14] 44.38/21.10 >= [1] X + [14] 44.38/21.10 = [c_1(activate^#(X))] 44.38/21.10 44.38/21.10 [activate^#(X)] = [1] X + [7] 44.38/21.10 >= [1] X + [7] 44.38/21.10 = [c_2(X)] 44.38/21.10 44.38/21.10 [plus^#(N, 0())] = [1] N + [4] 44.38/21.10 >= [1] N + [4] 44.38/21.10 = [c_3(N)] 44.38/21.10 44.38/21.10 [plus^#(N, s(M))] = [1] N + [1] M + [0] 44.38/21.10 ? [1] N + [1] M + [7] 44.38/21.10 = [c_4(plus^#(N, M))] 44.38/21.10 44.38/21.10 [x^#(N, 0())] = [1] N + [11] 44.38/21.10 > [3] 44.38/21.10 = [c_5()] 44.38/21.10 44.38/21.10 [x^#(N, s(M))] = [1] N + [1] M + [7] 44.38/21.10 > [1] N + [6] 44.38/21.10 = [c_6(plus^#(x(N, M), N))] 44.38/21.10 44.38/21.10 44.38/21.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict DPs: { plus^#(N, s(M)) -> c_4(plus^#(N, M)) } 44.38/21.10 Strict Trs: 44.38/21.10 { plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Weak DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , x^#(N, 0()) -> c_5() 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Weak Trs: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , x(N, 0()) -> 0() } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 The weightgap principle applies (using the following nonconstant 44.38/21.10 growth matrix-interpretation) 44.38/21.10 44.38/21.10 The following argument positions are usable: 44.38/21.10 Uargs(plus) = {1}, Uargs(s) = {1}, Uargs(c_1) = {1}, 44.38/21.10 Uargs(plus^#) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 44.38/21.10 Uargs(c_6) = {1} 44.38/21.10 44.38/21.10 TcT has computed the following matrix interpretation satisfying 44.38/21.10 not(EDA) and not(IDA(1)). 44.38/21.10 44.38/21.10 [tt] = [7] 44.38/21.10 44.38/21.10 [plus](x1, x2) = [1] x1 + [0] 44.38/21.10 44.38/21.10 [0] = [7] 44.38/21.10 44.38/21.10 [s](x1) = [1] x1 + [4] 44.38/21.10 44.38/21.10 [x](x1, x2) = [1] x1 + [1] x2 + [4] 44.38/21.10 44.38/21.10 [and^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_1](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [activate^#](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [c_2](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [plus^#](x1, x2) = [1] x1 + [0] 44.38/21.10 44.38/21.10 [c_3](x1) = [1] x1 + [0] 44.38/21.10 44.38/21.10 [c_4](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [x^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_5] = [5] 44.38/21.10 44.38/21.10 [c_6](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 The order satisfies the following ordering constraints: 44.38/21.10 44.38/21.10 [plus(N, 0())] = [1] N + [0] 44.38/21.10 >= [1] N + [0] 44.38/21.10 = [N] 44.38/21.10 44.38/21.10 [plus(N, s(M))] = [1] N + [0] 44.38/21.10 ? [1] N + [4] 44.38/21.10 = [s(plus(N, M))] 44.38/21.10 44.38/21.10 [x(N, 0())] = [1] N + [11] 44.38/21.10 > [7] 44.38/21.10 = [0()] 44.38/21.10 44.38/21.10 [x(N, s(M))] = [1] N + [1] M + [8] 44.38/21.10 > [1] N + [1] M + [4] 44.38/21.10 = [plus(x(N, M), N)] 44.38/21.10 44.38/21.10 [and^#(tt(), X)] = [1] X + [14] 44.38/21.10 >= [1] X + [14] 44.38/21.10 = [c_1(activate^#(X))] 44.38/21.10 44.38/21.10 [activate^#(X)] = [1] X + [7] 44.38/21.10 >= [1] X + [7] 44.38/21.10 = [c_2(X)] 44.38/21.10 44.38/21.10 [plus^#(N, 0())] = [1] N + [0] 44.38/21.10 >= [1] N + [0] 44.38/21.10 = [c_3(N)] 44.38/21.10 44.38/21.10 [plus^#(N, s(M))] = [1] N + [0] 44.38/21.10 ? [1] N + [7] 44.38/21.10 = [c_4(plus^#(N, M))] 44.38/21.10 44.38/21.10 [x^#(N, 0())] = [1] N + [14] 44.38/21.10 > [5] 44.38/21.10 = [c_5()] 44.38/21.10 44.38/21.10 [x^#(N, s(M))] = [1] N + [1] M + [11] 44.38/21.10 >= [1] N + [1] M + [11] 44.38/21.10 = [c_6(plus^#(x(N, M), N))] 44.38/21.10 44.38/21.10 44.38/21.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict DPs: { plus^#(N, s(M)) -> c_4(plus^#(N, M)) } 44.38/21.10 Strict Trs: { plus(N, s(M)) -> s(plus(N, M)) } 44.38/21.10 Weak DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , x^#(N, 0()) -> c_5() 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Weak Trs: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 The weightgap principle applies (using the following nonconstant 44.38/21.10 growth matrix-interpretation) 44.38/21.10 44.38/21.10 The following argument positions are usable: 44.38/21.10 Uargs(plus) = {1}, Uargs(s) = {1}, Uargs(c_1) = {1}, 44.38/21.10 Uargs(plus^#) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 44.38/21.10 Uargs(c_6) = {1} 44.38/21.10 44.38/21.10 TcT has computed the following matrix interpretation satisfying 44.38/21.10 not(EDA) and not(IDA(1)). 44.38/21.10 44.38/21.10 [tt] = [7] 44.38/21.10 44.38/21.10 [plus](x1, x2) = [1] x1 + [0] 44.38/21.10 44.38/21.10 [0] = [7] 44.38/21.10 44.38/21.10 [s](x1) = [1] x1 + [4] 44.38/21.10 44.38/21.10 [x](x1, x2) = [1] x2 + [0] 44.38/21.10 44.38/21.10 [and^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_1](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [activate^#](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [c_2](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 [plus^#](x1, x2) = [1] x1 + [1] x2 + [4] 44.38/21.10 44.38/21.10 [c_3](x1) = [1] x1 + [3] 44.38/21.10 44.38/21.10 [c_4](x1) = [1] x1 + [3] 44.38/21.10 44.38/21.10 [x^#](x1, x2) = [1] x1 + [1] x2 + [7] 44.38/21.10 44.38/21.10 [c_5] = [5] 44.38/21.10 44.38/21.10 [c_6](x1) = [1] x1 + [7] 44.38/21.10 44.38/21.10 The order satisfies the following ordering constraints: 44.38/21.10 44.38/21.10 [plus(N, 0())] = [1] N + [0] 44.38/21.10 >= [1] N + [0] 44.38/21.10 = [N] 44.38/21.10 44.38/21.10 [plus(N, s(M))] = [1] N + [0] 44.38/21.10 ? [1] N + [4] 44.38/21.10 = [s(plus(N, M))] 44.38/21.10 44.38/21.10 [x(N, 0())] = [7] 44.38/21.10 >= [7] 44.38/21.10 = [0()] 44.38/21.10 44.38/21.10 [x(N, s(M))] = [1] M + [4] 44.38/21.10 > [1] M + [0] 44.38/21.10 = [plus(x(N, M), N)] 44.38/21.10 44.38/21.10 [and^#(tt(), X)] = [1] X + [14] 44.38/21.10 >= [1] X + [14] 44.38/21.10 = [c_1(activate^#(X))] 44.38/21.10 44.38/21.10 [activate^#(X)] = [1] X + [7] 44.38/21.10 >= [1] X + [7] 44.38/21.10 = [c_2(X)] 44.38/21.10 44.38/21.10 [plus^#(N, 0())] = [1] N + [11] 44.38/21.10 > [1] N + [3] 44.38/21.10 = [c_3(N)] 44.38/21.10 44.38/21.10 [plus^#(N, s(M))] = [1] N + [1] M + [8] 44.38/21.10 > [1] N + [1] M + [7] 44.38/21.10 = [c_4(plus^#(N, M))] 44.38/21.10 44.38/21.10 [x^#(N, 0())] = [1] N + [14] 44.38/21.10 > [5] 44.38/21.10 = [c_5()] 44.38/21.10 44.38/21.10 [x^#(N, s(M))] = [1] N + [1] M + [11] 44.38/21.10 >= [1] N + [1] M + [11] 44.38/21.10 = [c_6(plus^#(x(N, M), N))] 44.38/21.10 44.38/21.10 44.38/21.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(n^2)). 44.38/21.10 44.38/21.10 Strict Trs: { plus(N, s(M)) -> s(plus(N, M)) } 44.38/21.10 Weak DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , x^#(N, 0()) -> c_5() 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Weak Trs: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(n^2)) 44.38/21.10 44.38/21.10 We use the processor 'polynomial interpretation' to orient 44.38/21.10 following rules strictly. 44.38/21.10 44.38/21.10 Trs: { plus(N, s(M)) -> s(plus(N, M)) } 44.38/21.10 44.38/21.10 The induced complexity on above rules (modulo remaining rules) is 44.38/21.10 YES(?,O(n^2)) . These rules are moved into the corresponding weak 44.38/21.10 component(s). 44.38/21.10 44.38/21.10 Sub-proof: 44.38/21.10 ---------- 44.38/21.10 We consider the following typing: 44.38/21.10 44.38/21.10 tt :: a 44.38/21.10 plus :: (e,e) -> e 44.38/21.10 0 :: e 44.38/21.10 s :: e -> e 44.38/21.10 x :: (e,e) -> e 44.38/21.10 and^# :: (a,c) -> b 44.38/21.10 c_1 :: d -> b 44.38/21.10 activate^# :: c -> d 44.38/21.10 c_2 :: c -> d 44.38/21.10 plus^# :: (e,e) -> f 44.38/21.10 c_3 :: e -> f 44.38/21.10 c_4 :: f -> f 44.38/21.10 x^# :: (e,e) -> g 44.38/21.10 c_5 :: g 44.38/21.10 c_6 :: f -> g 44.38/21.10 44.38/21.10 The following argument positions are considered usable: 44.38/21.10 44.38/21.10 Uargs(plus) = {1}, Uargs(s) = {1}, Uargs(c_1) = {1}, 44.38/21.10 Uargs(plus^#) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 44.38/21.10 Uargs(c_6) = {1} 44.38/21.10 44.38/21.10 TcT has computed the following constructor-restricted 44.38/21.10 typedpolynomial interpretation. 44.38/21.10 44.38/21.10 [tt]() = 0 44.38/21.10 44.38/21.10 [plus](x1, x2) = x1 + 2*x2 44.38/21.10 44.38/21.10 [0]() = 0 44.38/21.10 44.38/21.10 [s](x1) = 2 + x1 44.38/21.10 44.38/21.10 [x](x1, x2) = x1*x2 44.38/21.10 44.38/21.10 [and^#](x1, x2) = 3 + 3*x1 + 3*x1*x2 + 2*x1^2 + 3*x2 + 3*x2^2 44.38/21.10 44.38/21.10 [c_1](x1) = 1 + 2*x1 44.38/21.10 44.38/21.10 [activate^#](x1) = x1^2 44.38/21.10 44.38/21.10 [c_2](x1) = x1^2 44.38/21.10 44.38/21.10 [plus^#](x1, x2) = x1 44.38/21.10 44.38/21.10 [c_3](x1) = x1 44.38/21.10 44.38/21.10 [c_4](x1) = x1 44.38/21.10 44.38/21.10 [x^#](x1, x2) = x1 + x1*x2 + 3*x1^2 44.38/21.10 44.38/21.10 [c_5]() = 0 44.38/21.10 44.38/21.10 [c_6](x1) = x1 44.38/21.10 44.38/21.10 44.38/21.10 This order satisfies the following ordering constraints. 44.38/21.10 44.38/21.10 [plus(N, 0())] = N 44.38/21.10 >= N 44.38/21.10 = [N] 44.38/21.10 44.38/21.10 [plus(N, s(M))] = N + 4 + 2*M 44.38/21.10 > 2 + N + 2*M 44.38/21.10 = [s(plus(N, M))] 44.38/21.10 44.38/21.10 [x(N, 0())] = 44.38/21.10 >= 44.38/21.10 = [0()] 44.38/21.10 44.38/21.10 [x(N, s(M))] = 2*N + N*M 44.38/21.10 >= N*M + 2*N 44.38/21.10 = [plus(x(N, M), N)] 44.38/21.10 44.38/21.10 44.38/21.10 We return to the main proof. 44.38/21.10 44.38/21.10 We are left with following problem, upon which TcT provides the 44.38/21.10 certificate YES(O(1),O(1)). 44.38/21.10 44.38/21.10 Weak DPs: 44.38/21.10 { and^#(tt(), X) -> c_1(activate^#(X)) 44.38/21.10 , activate^#(X) -> c_2(X) 44.38/21.10 , plus^#(N, 0()) -> c_3(N) 44.38/21.10 , plus^#(N, s(M)) -> c_4(plus^#(N, M)) 44.38/21.10 , x^#(N, 0()) -> c_5() 44.38/21.10 , x^#(N, s(M)) -> c_6(plus^#(x(N, M), N)) } 44.38/21.10 Weak Trs: 44.38/21.10 { plus(N, 0()) -> N 44.38/21.10 , plus(N, s(M)) -> s(plus(N, M)) 44.38/21.10 , x(N, 0()) -> 0() 44.38/21.10 , x(N, s(M)) -> plus(x(N, M), N) } 44.38/21.10 Obligation: 44.38/21.10 runtime complexity 44.38/21.10 Answer: 44.38/21.10 YES(O(1),O(1)) 44.38/21.10 44.38/21.10 Empty rules are trivially bounded 44.38/21.10 44.38/21.10 Hurray, we answered YES(O(1),O(n^2)) 44.38/21.16 EOF