YES(O(1),O(n^1)) 0.00/0.51 YES(O(1),O(n^1)) 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(n^1)). 0.00/0.51 0.00/0.51 Strict Trs: 0.00/0.51 { ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X) 0.00/0.51 , u21(ackout(X), Y) -> u22(ackin(Y, X)) } 0.00/0.51 Obligation: 0.00/0.51 runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(n^1)) 0.00/0.51 0.00/0.51 The weightgap principle applies (using the following nonconstant 0.00/0.51 growth matrix-interpretation) 0.00/0.51 0.00/0.51 The following argument positions are usable: 0.00/0.51 Uargs(u21) = {1}, Uargs(u22) = {1} 0.00/0.51 0.00/0.51 TcT has computed the following matrix interpretation satisfying 0.00/0.51 not(EDA) and not(IDA(1)). 0.00/0.51 0.00/0.51 [ackin](x1, x2) = [1] x2 + [7] 0.00/0.51 0.00/0.51 [s](x1) = [1] x1 + [7] 0.00/0.51 0.00/0.51 [u21](x1, x2) = [1] x1 + [7] 0.00/0.51 0.00/0.51 [ackout](x1) = [1] x1 + [7] 0.00/0.51 0.00/0.51 [u22](x1) = [1] x1 + [3] 0.00/0.51 0.00/0.51 The order satisfies the following ordering constraints: 0.00/0.51 0.00/0.51 [ackin(s(X), s(Y))] = [1] Y + [14] 0.00/0.51 >= [1] Y + [14] 0.00/0.51 = [u21(ackin(s(X), Y), X)] 0.00/0.51 0.00/0.51 [u21(ackout(X), Y)] = [1] X + [14] 0.00/0.51 > [1] X + [10] 0.00/0.51 = [u22(ackin(Y, X))] 0.00/0.51 0.00/0.51 0.00/0.51 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(n^1)). 0.00/0.51 0.00/0.51 Strict Trs: { ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X) } 0.00/0.51 Weak Trs: { u21(ackout(X), Y) -> u22(ackin(Y, X)) } 0.00/0.51 Obligation: 0.00/0.51 runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(n^1)) 0.00/0.51 0.00/0.51 The weightgap principle applies (using the following nonconstant 0.00/0.51 growth matrix-interpretation) 0.00/0.51 0.00/0.51 The following argument positions are usable: 0.00/0.51 Uargs(u21) = {1}, Uargs(u22) = {1} 0.00/0.51 0.00/0.51 TcT has computed the following matrix interpretation satisfying 0.00/0.51 not(EDA) and not(IDA(1)). 0.00/0.51 0.00/0.51 [ackin](x1, x2) = [1] x2 + [7] 0.00/0.51 0.00/0.51 [s](x1) = [1] x1 + [7] 0.00/0.51 0.00/0.51 [u21](x1, x2) = [1] x1 + [6] 0.00/0.51 0.00/0.51 [ackout](x1) = [1] x1 + [7] 0.00/0.51 0.00/0.51 [u22](x1) = [1] x1 + [3] 0.00/0.51 0.00/0.51 The order satisfies the following ordering constraints: 0.00/0.51 0.00/0.51 [ackin(s(X), s(Y))] = [1] Y + [14] 0.00/0.51 > [1] Y + [13] 0.00/0.51 = [u21(ackin(s(X), Y), X)] 0.00/0.51 0.00/0.51 [u21(ackout(X), Y)] = [1] X + [13] 0.00/0.51 > [1] X + [10] 0.00/0.51 = [u22(ackin(Y, X))] 0.00/0.51 0.00/0.51 0.00/0.51 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Weak Trs: 0.00/0.51 { ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X) 0.00/0.51 , u21(ackout(X), Y) -> u22(ackin(Y, X)) } 0.00/0.51 Obligation: 0.00/0.51 runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 Empty rules are trivially bounded 0.00/0.51 0.00/0.51 Hurray, we answered YES(O(1),O(n^1)) 0.00/0.52 EOF