YES(O(1),O(n^1)) 327.68/148.03 YES(O(1),O(n^1)) 327.68/148.03 327.68/148.03 We are left with following problem, upon which TcT provides the 327.68/148.03 certificate YES(O(1),O(n^1)). 327.68/148.03 327.68/148.03 Strict Trs: 327.68/148.03 { dx(X) -> one() 327.68/148.03 , dx(a()) -> zero() 327.68/148.03 , dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)) 327.68/148.03 , dx(times(ALPHA, BETA)) -> 327.68/148.03 plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))) 327.68/148.03 , dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)) 327.68/148.03 , dx(neg(ALPHA)) -> neg(dx(ALPHA)) 327.68/148.03 , dx(div(ALPHA, BETA)) -> 327.68/148.03 minus(div(dx(ALPHA), BETA), 327.68/148.03 times(ALPHA, div(dx(BETA), exp(BETA, two())))) 327.68/148.03 , dx(exp(ALPHA, BETA)) -> 327.68/148.03 plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), 327.68/148.03 times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))) 327.68/148.03 , dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA) } 327.68/148.03 Obligation: 327.68/148.03 innermost runtime complexity 327.68/148.03 Answer: 327.68/148.03 YES(O(1),O(n^1)) 327.68/148.03 327.68/148.03 We add the following weak dependency pairs: 327.68/148.03 327.68/148.03 Strict DPs: 327.68/148.03 { dx^#(X) -> c_1() 327.68/148.03 , dx^#(a()) -> c_2() 327.68/148.03 , dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 327.68/148.03 and mark the set of starting terms. 327.68/148.03 327.68/148.03 We are left with following problem, upon which TcT provides the 327.68/148.03 certificate YES(O(1),O(n^1)). 327.68/148.03 327.68/148.03 Strict DPs: 327.68/148.03 { dx^#(X) -> c_1() 327.68/148.03 , dx^#(a()) -> c_2() 327.68/148.03 , dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 Strict Trs: 327.68/148.03 { dx(X) -> one() 327.68/148.03 , dx(a()) -> zero() 327.68/148.03 , dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)) 327.68/148.03 , dx(times(ALPHA, BETA)) -> 327.68/148.03 plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))) 327.68/148.03 , dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)) 327.68/148.03 , dx(neg(ALPHA)) -> neg(dx(ALPHA)) 327.68/148.03 , dx(div(ALPHA, BETA)) -> 327.68/148.03 minus(div(dx(ALPHA), BETA), 327.68/148.03 times(ALPHA, div(dx(BETA), exp(BETA, two())))) 327.68/148.03 , dx(exp(ALPHA, BETA)) -> 327.68/148.03 plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), 327.68/148.03 times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))) 327.68/148.03 , dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA) } 327.68/148.03 Obligation: 327.68/148.03 innermost runtime complexity 327.68/148.03 Answer: 327.68/148.03 YES(O(1),O(n^1)) 327.68/148.03 327.68/148.03 No rule is usable, rules are removed from the input problem. 327.68/148.03 327.68/148.03 We are left with following problem, upon which TcT provides the 327.68/148.03 certificate YES(O(1),O(n^1)). 327.68/148.03 327.68/148.03 Strict DPs: 327.68/148.03 { dx^#(X) -> c_1() 327.68/148.03 , dx^#(a()) -> c_2() 327.68/148.03 , dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 Obligation: 327.68/148.03 innermost runtime complexity 327.68/148.03 Answer: 327.68/148.03 YES(O(1),O(n^1)) 327.68/148.03 327.68/148.03 The weightgap principle applies (using the following constant 327.68/148.03 growth matrix-interpretation) 327.68/148.03 327.68/148.03 The following argument positions are usable: 327.68/148.03 Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}, 327.68/148.03 Uargs(c_6) = {1}, Uargs(c_7) = {1, 2}, Uargs(c_8) = {1, 2}, 327.68/148.03 Uargs(c_9) = {1} 327.68/148.03 327.68/148.03 TcT has computed the following constructor-restricted matrix 327.68/148.03 interpretation. 327.68/148.03 327.68/148.03 [a] = [0] 327.68/148.03 [0] 327.68/148.03 327.68/148.03 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 327.68/148.03 [0 0] [0 0] [0] 327.68/148.03 327.68/148.03 [times](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 327.68/148.03 [0 0] [0 0] [0] 327.68/148.03 327.68/148.03 [minus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 327.68/148.03 [0 0] [0 0] [0] 327.68/148.03 327.68/148.03 [neg](x1) = [1 0] x1 + [0] 327.68/148.03 [0 0] [0] 327.68/148.03 327.68/148.03 [div](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 327.68/148.03 [0 0] [0 0] [0] 327.68/148.03 327.68/148.03 [exp](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 327.68/148.03 [0 0] [0 0] [0] 327.68/148.03 327.68/148.03 [ln](x1) = [1 0] x1 + [0] 327.68/148.03 [0 0] [0] 327.68/148.03 327.68/148.03 [dx^#](x1) = [1] 327.68/148.03 [0] 327.68/148.03 327.68/148.03 [c_1] = [0] 327.68/148.03 [0] 327.68/148.03 327.68/148.03 [c_2] = [0] 327.68/148.03 [0] 327.68/148.03 327.68/148.03 [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 327.68/148.03 [0 1] [0 1] [1] 327.68/148.03 327.68/148.03 [c_4](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 327.68/148.03 [0 1] [0 1] [0] 327.68/148.03 327.68/148.03 [c_5](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 327.68/148.03 [0 1] [0 1] [2] 327.68/148.03 327.68/148.03 [c_6](x1) = [1 0] x1 + [1] 327.68/148.03 [0 1] [0] 327.68/148.03 327.68/148.03 [c_7](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 327.68/148.03 [0 1] [0 1] [1] 327.68/148.03 327.68/148.03 [c_8](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 327.68/148.03 [0 1] [0 1] [0] 327.68/148.03 327.68/148.03 [c_9](x1) = [1 0] x1 + [1] 327.68/148.03 [0 1] [0] 327.68/148.03 327.68/148.03 The order satisfies the following ordering constraints: 327.68/148.03 327.68/148.03 [dx^#(X)] = [1] 327.68/148.03 [0] 327.68/148.03 > [0] 327.68/148.03 [0] 327.68/148.03 = [c_1()] 327.68/148.03 327.68/148.03 [dx^#(a())] = [1] 327.68/148.03 [0] 327.68/148.03 > [0] 327.68/148.03 [0] 327.68/148.03 = [c_2()] 327.68/148.03 327.68/148.03 [dx^#(plus(ALPHA, BETA))] = [1] 327.68/148.03 [0] 327.68/148.03 ? [4] 327.68/148.03 [1] 327.68/148.03 = [c_3(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(times(ALPHA, BETA))] = [1] 327.68/148.03 [0] 327.68/148.03 ? [4] 327.68/148.03 [0] 327.68/148.03 = [c_4(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(minus(ALPHA, BETA))] = [1] 327.68/148.03 [0] 327.68/148.03 ? [4] 327.68/148.03 [2] 327.68/148.03 = [c_5(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(neg(ALPHA))] = [1] 327.68/148.03 [0] 327.68/148.03 ? [2] 327.68/148.03 [0] 327.68/148.03 = [c_6(dx^#(ALPHA))] 327.68/148.03 327.68/148.03 [dx^#(div(ALPHA, BETA))] = [1] 327.68/148.03 [0] 327.68/148.03 ? [4] 327.68/148.03 [1] 327.68/148.03 = [c_7(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(exp(ALPHA, BETA))] = [1] 327.68/148.03 [0] 327.68/148.03 ? [4] 327.68/148.03 [0] 327.68/148.03 = [c_8(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(ln(ALPHA))] = [1] 327.68/148.03 [0] 327.68/148.03 ? [2] 327.68/148.03 [0] 327.68/148.03 = [c_9(dx^#(ALPHA))] 327.68/148.03 327.68/148.03 327.68/148.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 327.68/148.03 327.68/148.03 We are left with following problem, upon which TcT provides the 327.68/148.03 certificate YES(O(1),O(n^1)). 327.68/148.03 327.68/148.03 Strict DPs: 327.68/148.03 { dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 Weak DPs: 327.68/148.03 { dx^#(X) -> c_1() 327.68/148.03 , dx^#(a()) -> c_2() } 327.68/148.03 Obligation: 327.68/148.03 innermost runtime complexity 327.68/148.03 Answer: 327.68/148.03 YES(O(1),O(n^1)) 327.68/148.03 327.68/148.03 The following weak DPs constitute a sub-graph of the DG that is 327.68/148.03 closed under successors. The DPs are removed. 327.68/148.03 327.68/148.03 { dx^#(X) -> c_1() 327.68/148.03 , dx^#(a()) -> c_2() } 327.68/148.03 327.68/148.03 We are left with following problem, upon which TcT provides the 327.68/148.03 certificate YES(O(1),O(n^1)). 327.68/148.03 327.68/148.03 Strict DPs: 327.68/148.03 { dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 Obligation: 327.68/148.03 innermost runtime complexity 327.68/148.03 Answer: 327.68/148.03 YES(O(1),O(n^1)) 327.68/148.03 327.68/148.03 We use the processor 'matrix interpretation of dimension 1' to 327.68/148.03 orient following rules strictly. 327.68/148.03 327.68/148.03 DPs: 327.68/148.03 { 1: dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , 2: dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , 3: dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , 4: dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , 5: dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , 6: dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , 7: dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 327.68/148.03 Sub-proof: 327.68/148.03 ---------- 327.68/148.03 The following argument positions are usable: 327.68/148.03 Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}, 327.68/148.03 Uargs(c_6) = {1}, Uargs(c_7) = {1, 2}, Uargs(c_8) = {1, 2}, 327.68/148.03 Uargs(c_9) = {1} 327.68/148.03 327.68/148.03 TcT has computed the following constructor-based matrix 327.68/148.03 interpretation satisfying not(EDA). 327.68/148.03 327.68/148.03 [plus](x1, x2) = [1] x1 + [1] x2 + [4] 327.68/148.03 327.68/148.03 [times](x1, x2) = [1] x1 + [1] x2 + [4] 327.68/148.03 327.68/148.03 [minus](x1, x2) = [1] x1 + [1] x2 + [4] 327.68/148.03 327.68/148.03 [neg](x1) = [1] x1 + [4] 327.68/148.03 327.68/148.03 [div](x1, x2) = [1] x1 + [1] x2 + [4] 327.68/148.03 327.68/148.03 [exp](x1, x2) = [1] x1 + [1] x2 + [4] 327.68/148.03 327.68/148.03 [ln](x1) = [1] x1 + [4] 327.68/148.03 327.68/148.03 [dx^#](x1) = [2] x1 + [0] 327.68/148.03 327.68/148.03 [c_3](x1, x2) = [1] x1 + [1] x2 + [3] 327.68/148.03 327.68/148.03 [c_4](x1, x2) = [1] x1 + [1] x2 + [3] 327.68/148.03 327.68/148.03 [c_5](x1, x2) = [1] x1 + [1] x2 + [5] 327.68/148.03 327.68/148.03 [c_6](x1) = [1] x1 + [7] 327.68/148.03 327.68/148.03 [c_7](x1, x2) = [1] x1 + [1] x2 + [3] 327.68/148.03 327.68/148.03 [c_8](x1, x2) = [1] x1 + [1] x2 + [3] 327.68/148.03 327.68/148.03 [c_9](x1) = [1] x1 + [3] 327.68/148.03 327.68/148.03 The order satisfies the following ordering constraints: 327.68/148.03 327.68/148.03 [dx^#(plus(ALPHA, BETA))] = [2] ALPHA + [2] BETA + [8] 327.68/148.03 > [2] ALPHA + [2] BETA + [3] 327.68/148.03 = [c_3(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(times(ALPHA, BETA))] = [2] ALPHA + [2] BETA + [8] 327.68/148.03 > [2] ALPHA + [2] BETA + [3] 327.68/148.03 = [c_4(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(minus(ALPHA, BETA))] = [2] ALPHA + [2] BETA + [8] 327.68/148.03 > [2] ALPHA + [2] BETA + [5] 327.68/148.03 = [c_5(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(neg(ALPHA))] = [2] ALPHA + [8] 327.68/148.03 > [2] ALPHA + [7] 327.68/148.03 = [c_6(dx^#(ALPHA))] 327.68/148.03 327.68/148.03 [dx^#(div(ALPHA, BETA))] = [2] ALPHA + [2] BETA + [8] 327.68/148.03 > [2] ALPHA + [2] BETA + [3] 327.68/148.03 = [c_7(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(exp(ALPHA, BETA))] = [2] ALPHA + [2] BETA + [8] 327.68/148.03 > [2] ALPHA + [2] BETA + [3] 327.68/148.03 = [c_8(dx^#(ALPHA), dx^#(BETA))] 327.68/148.03 327.68/148.03 [dx^#(ln(ALPHA))] = [2] ALPHA + [8] 327.68/148.03 > [2] ALPHA + [3] 327.68/148.03 = [c_9(dx^#(ALPHA))] 327.68/148.03 327.68/148.03 327.68/148.03 The strictly oriented rules are moved into the weak component. 327.68/148.03 327.68/148.03 We are left with following problem, upon which TcT provides the 327.68/148.03 certificate YES(O(1),O(1)). 327.68/148.03 327.68/148.03 Weak DPs: 327.68/148.03 { dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 Obligation: 327.68/148.03 innermost runtime complexity 327.68/148.03 Answer: 327.68/148.03 YES(O(1),O(1)) 327.68/148.03 327.68/148.03 The following weak DPs constitute a sub-graph of the DG that is 327.68/148.03 closed under successors. The DPs are removed. 327.68/148.03 327.68/148.03 { dx^#(plus(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(times(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(minus(ALPHA, BETA)) -> c_5(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(neg(ALPHA)) -> c_6(dx^#(ALPHA)) 327.68/148.03 , dx^#(div(ALPHA, BETA)) -> c_7(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA)) 327.68/148.03 , dx^#(ln(ALPHA)) -> c_9(dx^#(ALPHA)) } 327.68/148.03 327.68/148.03 We are left with following problem, upon which TcT provides the 327.68/148.03 certificate YES(O(1),O(1)). 327.68/148.03 327.68/148.03 Rules: Empty 327.68/148.03 Obligation: 327.68/148.03 innermost runtime complexity 327.68/148.03 Answer: 327.68/148.03 YES(O(1),O(1)) 327.68/148.03 327.68/148.03 Empty rules are trivially bounded 327.68/148.03 327.68/148.03 Hurray, we answered YES(O(1),O(n^1)) 327.91/148.16 EOF