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