YES(O(1),O(n^2)) 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 We are left with following problem, upon which TcT provides the 73.10/24.05 certificate YES(O(1),O(n^2)). 73.10/24.05 73.10/24.05 Strict Trs: 73.10/24.05 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.05 , minus(n__0(), Y) -> 0() 73.10/24.05 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.05 , 0() -> n__0() 73.10/24.05 , activate(X) -> X 73.10/24.05 , activate(n__0()) -> 0() 73.10/24.05 , activate(n__s(X)) -> s(activate(X)) 73.10/24.05 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.05 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.05 , geq(X, n__0()) -> true() 73.10/24.05 , geq(n__0(), n__s(Y)) -> false() 73.10/24.05 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) 73.10/24.05 , div(X1, X2) -> n__div(X1, X2) 73.10/24.05 , div(0(), n__s(Y)) -> 0() 73.10/24.05 , div(s(X), n__s(Y)) -> 73.10/24.05 if(geq(X, activate(Y)), 73.10/24.05 n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), 73.10/24.05 n__0()) 73.10/24.05 , s(X) -> n__s(X) 73.10/24.05 , if(true(), X, Y) -> activate(X) 73.10/24.05 , if(false(), X, Y) -> activate(Y) } 73.10/24.05 Obligation: 73.10/24.05 innermost runtime complexity 73.10/24.05 Answer: 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 Arguments of following rules are not normal-forms: 73.10/24.05 73.10/24.05 { div(0(), n__s(Y)) -> 0() 73.10/24.05 , div(s(X), n__s(Y)) -> 73.10/24.05 if(geq(X, activate(Y)), 73.10/24.05 n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), 73.10/24.05 n__0()) } 73.10/24.05 73.10/24.05 All above mentioned rules can be savely removed. 73.10/24.05 73.10/24.05 We are left with following problem, upon which TcT provides the 73.10/24.05 certificate YES(O(1),O(n^2)). 73.10/24.05 73.10/24.05 Strict Trs: 73.10/24.05 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.05 , minus(n__0(), Y) -> 0() 73.10/24.05 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.05 , 0() -> n__0() 73.10/24.05 , activate(X) -> X 73.10/24.05 , activate(n__0()) -> 0() 73.10/24.05 , activate(n__s(X)) -> s(activate(X)) 73.10/24.05 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.05 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.05 , geq(X, n__0()) -> true() 73.10/24.05 , geq(n__0(), n__s(Y)) -> false() 73.10/24.05 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) 73.10/24.05 , div(X1, X2) -> n__div(X1, X2) 73.10/24.05 , s(X) -> n__s(X) 73.10/24.05 , if(true(), X, Y) -> activate(X) 73.10/24.05 , if(false(), X, Y) -> activate(Y) } 73.10/24.05 Obligation: 73.10/24.05 innermost runtime complexity 73.10/24.05 Answer: 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 The weightgap principle applies (using the following nonconstant 73.10/24.05 growth matrix-interpretation) 73.10/24.05 73.10/24.05 The following argument positions are usable: 73.10/24.05 Uargs(minus) = {1, 2}, Uargs(geq) = {1, 2}, Uargs(div) = {1}, 73.10/24.05 Uargs(s) = {1} 73.10/24.05 73.10/24.05 TcT has computed the following matrix interpretation satisfying 73.10/24.05 not(EDA) and not(IDA(1)). 73.10/24.05 73.10/24.05 [minus](x1, x2) = [1] x1 + [1] x2 + [1] 73.10/24.05 73.10/24.05 [n__0] = [7] 73.10/24.05 73.10/24.05 [0] = [7] 73.10/24.05 73.10/24.05 [n__s](x1) = [1] x1 + [7] 73.10/24.05 73.10/24.05 [activate](x1) = [1] x1 + [7] 73.10/24.05 73.10/24.05 [geq](x1, x2) = [1] x1 + [1] x2 + [1] 73.10/24.05 73.10/24.05 [true] = [7] 73.10/24.05 73.10/24.05 [false] = [7] 73.10/24.05 73.10/24.05 [div](x1, x2) = [1] x1 + [1] x2 + [7] 73.10/24.05 73.10/24.05 [s](x1) = [1] x1 + [7] 73.10/24.05 73.10/24.05 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 73.10/24.05 73.10/24.05 [n__div](x1, x2) = [1] x1 + [1] x2 + [7] 73.10/24.05 73.10/24.05 [n__minus](x1, x2) = [1] x1 + [1] x2 + [7] 73.10/24.05 73.10/24.05 The order satisfies the following ordering constraints: 73.10/24.05 73.10/24.05 [minus(X1, X2)] = [1] X1 + [1] X2 + [1] 73.10/24.05 ? [1] X1 + [1] X2 + [7] 73.10/24.05 = [n__minus(X1, X2)] 73.10/24.05 73.10/24.05 [minus(n__0(), Y)] = [1] Y + [8] 73.10/24.05 > [7] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [minus(n__s(X), n__s(Y))] = [1] Y + [1] X + [15] 73.10/24.05 >= [1] Y + [1] X + [15] 73.10/24.05 = [minus(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [0()] = [7] 73.10/24.05 >= [7] 73.10/24.05 = [n__0()] 73.10/24.05 73.10/24.05 [activate(X)] = [1] X + [7] 73.10/24.05 > [1] X + [0] 73.10/24.05 = [X] 73.10/24.05 73.10/24.05 [activate(n__0())] = [14] 73.10/24.05 > [7] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [activate(n__s(X))] = [1] X + [14] 73.10/24.05 >= [1] X + [14] 73.10/24.05 = [s(activate(X))] 73.10/24.05 73.10/24.05 [activate(n__div(X1, X2))] = [1] X1 + [1] X2 + [14] 73.10/24.05 >= [1] X1 + [1] X2 + [14] 73.10/24.05 = [div(activate(X1), X2)] 73.10/24.05 73.10/24.05 [activate(n__minus(X1, X2))] = [1] X1 + [1] X2 + [14] 73.10/24.05 > [1] X1 + [1] X2 + [1] 73.10/24.05 = [minus(X1, X2)] 73.10/24.05 73.10/24.05 [geq(X, n__0())] = [1] X + [8] 73.10/24.05 > [7] 73.10/24.05 = [true()] 73.10/24.05 73.10/24.05 [geq(n__0(), n__s(Y))] = [1] Y + [15] 73.10/24.05 > [7] 73.10/24.05 = [false()] 73.10/24.05 73.10/24.05 [geq(n__s(X), n__s(Y))] = [1] Y + [1] X + [15] 73.10/24.05 >= [1] Y + [1] X + [15] 73.10/24.05 = [geq(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [div(X1, X2)] = [1] X1 + [1] X2 + [7] 73.10/24.05 >= [1] X1 + [1] X2 + [7] 73.10/24.05 = [n__div(X1, X2)] 73.10/24.05 73.10/24.05 [s(X)] = [1] X + [7] 73.10/24.05 >= [1] X + [7] 73.10/24.05 = [n__s(X)] 73.10/24.05 73.10/24.05 [if(true(), X, Y)] = [1] Y + [1] X + [14] 73.10/24.05 > [1] X + [7] 73.10/24.05 = [activate(X)] 73.10/24.05 73.10/24.05 [if(false(), X, Y)] = [1] Y + [1] X + [14] 73.10/24.05 > [1] Y + [7] 73.10/24.05 = [activate(Y)] 73.10/24.05 73.10/24.05 73.10/24.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 73.10/24.05 73.10/24.05 We are left with following problem, upon which TcT provides the 73.10/24.05 certificate YES(O(1),O(n^2)). 73.10/24.05 73.10/24.05 Strict Trs: 73.10/24.05 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.05 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.05 , 0() -> n__0() 73.10/24.05 , activate(n__s(X)) -> s(activate(X)) 73.10/24.05 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.05 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) 73.10/24.05 , div(X1, X2) -> n__div(X1, X2) 73.10/24.05 , s(X) -> n__s(X) } 73.10/24.05 Weak Trs: 73.10/24.05 { minus(n__0(), Y) -> 0() 73.10/24.05 , activate(X) -> X 73.10/24.05 , activate(n__0()) -> 0() 73.10/24.05 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.05 , geq(X, n__0()) -> true() 73.10/24.05 , geq(n__0(), n__s(Y)) -> false() 73.10/24.05 , if(true(), X, Y) -> activate(X) 73.10/24.05 , if(false(), X, Y) -> activate(Y) } 73.10/24.05 Obligation: 73.10/24.05 innermost runtime complexity 73.10/24.05 Answer: 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 The weightgap principle applies (using the following nonconstant 73.10/24.05 growth matrix-interpretation) 73.10/24.05 73.10/24.05 The following argument positions are usable: 73.10/24.05 Uargs(minus) = {1, 2}, Uargs(geq) = {1, 2}, Uargs(div) = {1}, 73.10/24.05 Uargs(s) = {1} 73.10/24.05 73.10/24.05 TcT has computed the following matrix interpretation satisfying 73.10/24.05 not(EDA) and not(IDA(1)). 73.10/24.05 73.10/24.05 [minus](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [n__0] = [4] 73.10/24.05 73.10/24.05 [0] = [0] 73.10/24.05 73.10/24.05 [n__s](x1) = [1] x1 + [0] 73.10/24.05 73.10/24.05 [activate](x1) = [1] x1 + [0] 73.10/24.05 73.10/24.05 [geq](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [true] = [0] 73.10/24.05 73.10/24.05 [false] = [0] 73.10/24.05 73.10/24.05 [div](x1, x2) = [1] x1 + [1] x2 + [1] 73.10/24.05 73.10/24.05 [s](x1) = [1] x1 + [0] 73.10/24.05 73.10/24.05 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 73.10/24.05 73.10/24.05 [n__div](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [n__minus](x1, x2) = [1] x1 + [1] x2 + [5] 73.10/24.05 73.10/24.05 The order satisfies the following ordering constraints: 73.10/24.05 73.10/24.05 [minus(X1, X2)] = [1] X1 + [1] X2 + [0] 73.10/24.05 ? [1] X1 + [1] X2 + [5] 73.10/24.05 = [n__minus(X1, X2)] 73.10/24.05 73.10/24.05 [minus(n__0(), Y)] = [1] Y + [4] 73.10/24.05 > [0] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [minus(n__s(X), n__s(Y))] = [1] Y + [1] X + [0] 73.10/24.05 >= [1] Y + [1] X + [0] 73.10/24.05 = [minus(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [0()] = [0] 73.10/24.05 ? [4] 73.10/24.05 = [n__0()] 73.10/24.05 73.10/24.05 [activate(X)] = [1] X + [0] 73.10/24.05 >= [1] X + [0] 73.10/24.05 = [X] 73.10/24.05 73.10/24.05 [activate(n__0())] = [4] 73.10/24.05 > [0] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [activate(n__s(X))] = [1] X + [0] 73.10/24.05 >= [1] X + [0] 73.10/24.05 = [s(activate(X))] 73.10/24.05 73.10/24.05 [activate(n__div(X1, X2))] = [1] X1 + [1] X2 + [0] 73.10/24.05 ? [1] X1 + [1] X2 + [1] 73.10/24.05 = [div(activate(X1), X2)] 73.10/24.05 73.10/24.05 [activate(n__minus(X1, X2))] = [1] X1 + [1] X2 + [5] 73.10/24.05 > [1] X1 + [1] X2 + [0] 73.10/24.05 = [minus(X1, X2)] 73.10/24.05 73.10/24.05 [geq(X, n__0())] = [1] X + [4] 73.10/24.05 > [0] 73.10/24.05 = [true()] 73.10/24.05 73.10/24.05 [geq(n__0(), n__s(Y))] = [1] Y + [4] 73.10/24.05 > [0] 73.10/24.05 = [false()] 73.10/24.05 73.10/24.05 [geq(n__s(X), n__s(Y))] = [1] Y + [1] X + [0] 73.10/24.05 >= [1] Y + [1] X + [0] 73.10/24.05 = [geq(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [div(X1, X2)] = [1] X1 + [1] X2 + [1] 73.10/24.05 > [1] X1 + [1] X2 + [0] 73.10/24.05 = [n__div(X1, X2)] 73.10/24.05 73.10/24.05 [s(X)] = [1] X + [0] 73.10/24.05 >= [1] X + [0] 73.10/24.05 = [n__s(X)] 73.10/24.05 73.10/24.05 [if(true(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.05 > [1] X + [0] 73.10/24.05 = [activate(X)] 73.10/24.05 73.10/24.05 [if(false(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.05 > [1] Y + [0] 73.10/24.05 = [activate(Y)] 73.10/24.05 73.10/24.05 73.10/24.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 73.10/24.05 73.10/24.05 We are left with following problem, upon which TcT provides the 73.10/24.05 certificate YES(O(1),O(n^2)). 73.10/24.05 73.10/24.05 Strict Trs: 73.10/24.05 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.05 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.05 , 0() -> n__0() 73.10/24.05 , activate(n__s(X)) -> s(activate(X)) 73.10/24.05 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.05 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) 73.10/24.05 , s(X) -> n__s(X) } 73.10/24.05 Weak Trs: 73.10/24.05 { minus(n__0(), Y) -> 0() 73.10/24.05 , activate(X) -> X 73.10/24.05 , activate(n__0()) -> 0() 73.10/24.05 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.05 , geq(X, n__0()) -> true() 73.10/24.05 , geq(n__0(), n__s(Y)) -> false() 73.10/24.05 , div(X1, X2) -> n__div(X1, X2) 73.10/24.05 , if(true(), X, Y) -> activate(X) 73.10/24.05 , if(false(), X, Y) -> activate(Y) } 73.10/24.05 Obligation: 73.10/24.05 innermost runtime complexity 73.10/24.05 Answer: 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 The weightgap principle applies (using the following nonconstant 73.10/24.05 growth matrix-interpretation) 73.10/24.05 73.10/24.05 The following argument positions are usable: 73.10/24.05 Uargs(minus) = {1, 2}, Uargs(geq) = {1, 2}, Uargs(div) = {1}, 73.10/24.05 Uargs(s) = {1} 73.10/24.05 73.10/24.05 TcT has computed the following matrix interpretation satisfying 73.10/24.05 not(EDA) and not(IDA(1)). 73.10/24.05 73.10/24.05 [minus](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [n__0] = [4] 73.10/24.05 73.10/24.05 [0] = [3] 73.10/24.05 73.10/24.05 [n__s](x1) = [1] x1 + [0] 73.10/24.05 73.10/24.05 [activate](x1) = [1] x1 + [0] 73.10/24.05 73.10/24.05 [geq](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [true] = [0] 73.10/24.05 73.10/24.05 [false] = [0] 73.10/24.05 73.10/24.05 [div](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [s](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 73.10/24.05 73.10/24.05 [n__div](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [n__minus](x1, x2) = [1] x1 + [1] x2 + [5] 73.10/24.05 73.10/24.05 The order satisfies the following ordering constraints: 73.10/24.05 73.10/24.05 [minus(X1, X2)] = [1] X1 + [1] X2 + [0] 73.10/24.05 ? [1] X1 + [1] X2 + [5] 73.10/24.05 = [n__minus(X1, X2)] 73.10/24.05 73.10/24.05 [minus(n__0(), Y)] = [1] Y + [4] 73.10/24.05 > [3] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [minus(n__s(X), n__s(Y))] = [1] Y + [1] X + [0] 73.10/24.05 >= [1] Y + [1] X + [0] 73.10/24.05 = [minus(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [0()] = [3] 73.10/24.05 ? [4] 73.10/24.05 = [n__0()] 73.10/24.05 73.10/24.05 [activate(X)] = [1] X + [0] 73.10/24.05 >= [1] X + [0] 73.10/24.05 = [X] 73.10/24.05 73.10/24.05 [activate(n__0())] = [4] 73.10/24.05 > [3] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [activate(n__s(X))] = [1] X + [0] 73.10/24.05 ? [1] X + [4] 73.10/24.05 = [s(activate(X))] 73.10/24.05 73.10/24.05 [activate(n__div(X1, X2))] = [1] X1 + [1] X2 + [0] 73.10/24.05 >= [1] X1 + [1] X2 + [0] 73.10/24.05 = [div(activate(X1), X2)] 73.10/24.05 73.10/24.05 [activate(n__minus(X1, X2))] = [1] X1 + [1] X2 + [5] 73.10/24.05 > [1] X1 + [1] X2 + [0] 73.10/24.05 = [minus(X1, X2)] 73.10/24.05 73.10/24.05 [geq(X, n__0())] = [1] X + [4] 73.10/24.05 > [0] 73.10/24.05 = [true()] 73.10/24.05 73.10/24.05 [geq(n__0(), n__s(Y))] = [1] Y + [4] 73.10/24.05 > [0] 73.10/24.05 = [false()] 73.10/24.05 73.10/24.05 [geq(n__s(X), n__s(Y))] = [1] Y + [1] X + [0] 73.10/24.05 >= [1] Y + [1] X + [0] 73.10/24.05 = [geq(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [div(X1, X2)] = [1] X1 + [1] X2 + [0] 73.10/24.05 >= [1] X1 + [1] X2 + [0] 73.10/24.05 = [n__div(X1, X2)] 73.10/24.05 73.10/24.05 [s(X)] = [1] X + [4] 73.10/24.05 > [1] X + [0] 73.10/24.05 = [n__s(X)] 73.10/24.05 73.10/24.05 [if(true(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.05 > [1] X + [0] 73.10/24.05 = [activate(X)] 73.10/24.05 73.10/24.05 [if(false(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.05 > [1] Y + [0] 73.10/24.05 = [activate(Y)] 73.10/24.05 73.10/24.05 73.10/24.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 73.10/24.05 73.10/24.05 We are left with following problem, upon which TcT provides the 73.10/24.05 certificate YES(O(1),O(n^2)). 73.10/24.05 73.10/24.05 Strict Trs: 73.10/24.05 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.05 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.05 , 0() -> n__0() 73.10/24.05 , activate(n__s(X)) -> s(activate(X)) 73.10/24.05 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.05 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) } 73.10/24.05 Weak Trs: 73.10/24.05 { minus(n__0(), Y) -> 0() 73.10/24.05 , activate(X) -> X 73.10/24.05 , activate(n__0()) -> 0() 73.10/24.05 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.05 , geq(X, n__0()) -> true() 73.10/24.05 , geq(n__0(), n__s(Y)) -> false() 73.10/24.05 , div(X1, X2) -> n__div(X1, X2) 73.10/24.05 , s(X) -> n__s(X) 73.10/24.05 , if(true(), X, Y) -> activate(X) 73.10/24.05 , if(false(), X, Y) -> activate(Y) } 73.10/24.05 Obligation: 73.10/24.05 innermost runtime complexity 73.10/24.05 Answer: 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 The weightgap principle applies (using the following nonconstant 73.10/24.05 growth matrix-interpretation) 73.10/24.05 73.10/24.05 The following argument positions are usable: 73.10/24.05 Uargs(minus) = {1, 2}, Uargs(geq) = {1, 2}, Uargs(div) = {1}, 73.10/24.05 Uargs(s) = {1} 73.10/24.05 73.10/24.05 TcT has computed the following matrix interpretation satisfying 73.10/24.05 not(EDA) and not(IDA(1)). 73.10/24.05 73.10/24.05 [minus](x1, x2) = [1] x1 + [1] x2 + [4] 73.10/24.05 73.10/24.05 [n__0] = [4] 73.10/24.05 73.10/24.05 [0] = [6] 73.10/24.05 73.10/24.05 [n__s](x1) = [1] x1 + [0] 73.10/24.05 73.10/24.05 [activate](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [geq](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [true] = [0] 73.10/24.05 73.10/24.05 [false] = [4] 73.10/24.05 73.10/24.05 [div](x1, x2) = [1] x1 + [1] x2 + [4] 73.10/24.05 73.10/24.05 [s](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 73.10/24.05 73.10/24.05 [n__div](x1, x2) = [1] x1 + [1] x2 + [4] 73.10/24.05 73.10/24.05 [n__minus](x1, x2) = [1] x1 + [1] x2 + [5] 73.10/24.05 73.10/24.05 The order satisfies the following ordering constraints: 73.10/24.05 73.10/24.05 [minus(X1, X2)] = [1] X1 + [1] X2 + [4] 73.10/24.05 ? [1] X1 + [1] X2 + [5] 73.10/24.05 = [n__minus(X1, X2)] 73.10/24.05 73.10/24.05 [minus(n__0(), Y)] = [1] Y + [8] 73.10/24.05 > [6] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [minus(n__s(X), n__s(Y))] = [1] Y + [1] X + [4] 73.10/24.05 ? [1] Y + [1] X + [12] 73.10/24.05 = [minus(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [0()] = [6] 73.10/24.05 > [4] 73.10/24.05 = [n__0()] 73.10/24.05 73.10/24.05 [activate(X)] = [1] X + [4] 73.10/24.05 > [1] X + [0] 73.10/24.05 = [X] 73.10/24.05 73.10/24.05 [activate(n__0())] = [8] 73.10/24.05 > [6] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [activate(n__s(X))] = [1] X + [4] 73.10/24.05 ? [1] X + [8] 73.10/24.05 = [s(activate(X))] 73.10/24.05 73.10/24.05 [activate(n__div(X1, X2))] = [1] X1 + [1] X2 + [8] 73.10/24.05 >= [1] X1 + [1] X2 + [8] 73.10/24.05 = [div(activate(X1), X2)] 73.10/24.05 73.10/24.05 [activate(n__minus(X1, X2))] = [1] X1 + [1] X2 + [9] 73.10/24.05 > [1] X1 + [1] X2 + [4] 73.10/24.05 = [minus(X1, X2)] 73.10/24.05 73.10/24.05 [geq(X, n__0())] = [1] X + [4] 73.10/24.05 > [0] 73.10/24.05 = [true()] 73.10/24.05 73.10/24.05 [geq(n__0(), n__s(Y))] = [1] Y + [4] 73.10/24.05 >= [4] 73.10/24.05 = [false()] 73.10/24.05 73.10/24.05 [geq(n__s(X), n__s(Y))] = [1] Y + [1] X + [0] 73.10/24.05 ? [1] Y + [1] X + [8] 73.10/24.05 = [geq(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [div(X1, X2)] = [1] X1 + [1] X2 + [4] 73.10/24.05 >= [1] X1 + [1] X2 + [4] 73.10/24.05 = [n__div(X1, X2)] 73.10/24.05 73.10/24.05 [s(X)] = [1] X + [4] 73.10/24.05 > [1] X + [0] 73.10/24.05 = [n__s(X)] 73.10/24.05 73.10/24.05 [if(true(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.05 >= [1] X + [4] 73.10/24.05 = [activate(X)] 73.10/24.05 73.10/24.05 [if(false(), X, Y)] = [1] Y + [1] X + [8] 73.10/24.05 > [1] Y + [4] 73.10/24.05 = [activate(Y)] 73.10/24.05 73.10/24.05 73.10/24.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 73.10/24.05 73.10/24.05 We are left with following problem, upon which TcT provides the 73.10/24.05 certificate YES(O(1),O(n^2)). 73.10/24.05 73.10/24.05 Strict Trs: 73.10/24.05 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.05 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.05 , activate(n__s(X)) -> s(activate(X)) 73.10/24.05 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.05 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) } 73.10/24.05 Weak Trs: 73.10/24.05 { minus(n__0(), Y) -> 0() 73.10/24.05 , 0() -> n__0() 73.10/24.05 , activate(X) -> X 73.10/24.05 , activate(n__0()) -> 0() 73.10/24.05 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.05 , geq(X, n__0()) -> true() 73.10/24.05 , geq(n__0(), n__s(Y)) -> false() 73.10/24.05 , div(X1, X2) -> n__div(X1, X2) 73.10/24.05 , s(X) -> n__s(X) 73.10/24.05 , if(true(), X, Y) -> activate(X) 73.10/24.05 , if(false(), X, Y) -> activate(Y) } 73.10/24.05 Obligation: 73.10/24.05 innermost runtime complexity 73.10/24.05 Answer: 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 The weightgap principle applies (using the following nonconstant 73.10/24.05 growth matrix-interpretation) 73.10/24.05 73.10/24.05 The following argument positions are usable: 73.10/24.05 Uargs(minus) = {1, 2}, Uargs(geq) = {1, 2}, Uargs(div) = {1}, 73.10/24.05 Uargs(s) = {1} 73.10/24.05 73.10/24.05 TcT has computed the following matrix interpretation satisfying 73.10/24.05 not(EDA) and not(IDA(1)). 73.10/24.05 73.10/24.05 [minus](x1, x2) = [1] x1 + [1] x2 + [4] 73.10/24.05 73.10/24.05 [n__0] = [0] 73.10/24.05 73.10/24.05 [0] = [3] 73.10/24.05 73.10/24.05 [n__s](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [activate](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [geq](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [true] = [0] 73.10/24.05 73.10/24.05 [false] = [0] 73.10/24.05 73.10/24.05 [div](x1, x2) = [1] x1 + [1] x2 + [4] 73.10/24.05 73.10/24.05 [s](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 73.10/24.05 73.10/24.05 [n__div](x1, x2) = [1] x1 + [1] x2 + [1] 73.10/24.05 73.10/24.05 [n__minus](x1, x2) = [1] x1 + [1] x2 + [1] 73.10/24.05 73.10/24.05 The order satisfies the following ordering constraints: 73.10/24.05 73.10/24.05 [minus(X1, X2)] = [1] X1 + [1] X2 + [4] 73.10/24.05 > [1] X1 + [1] X2 + [1] 73.10/24.05 = [n__minus(X1, X2)] 73.10/24.05 73.10/24.05 [minus(n__0(), Y)] = [1] Y + [4] 73.10/24.05 > [3] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [minus(n__s(X), n__s(Y))] = [1] Y + [1] X + [12] 73.10/24.05 >= [1] Y + [1] X + [12] 73.10/24.05 = [minus(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [0()] = [3] 73.10/24.05 > [0] 73.10/24.05 = [n__0()] 73.10/24.05 73.10/24.05 [activate(X)] = [1] X + [4] 73.10/24.05 > [1] X + [0] 73.10/24.05 = [X] 73.10/24.05 73.10/24.05 [activate(n__0())] = [4] 73.10/24.05 > [3] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [activate(n__s(X))] = [1] X + [8] 73.10/24.05 >= [1] X + [8] 73.10/24.05 = [s(activate(X))] 73.10/24.05 73.10/24.05 [activate(n__div(X1, X2))] = [1] X1 + [1] X2 + [5] 73.10/24.05 ? [1] X1 + [1] X2 + [8] 73.10/24.05 = [div(activate(X1), X2)] 73.10/24.05 73.10/24.05 [activate(n__minus(X1, X2))] = [1] X1 + [1] X2 + [5] 73.10/24.05 > [1] X1 + [1] X2 + [4] 73.10/24.05 = [minus(X1, X2)] 73.10/24.05 73.10/24.05 [geq(X, n__0())] = [1] X + [0] 73.10/24.05 >= [0] 73.10/24.05 = [true()] 73.10/24.05 73.10/24.05 [geq(n__0(), n__s(Y))] = [1] Y + [4] 73.10/24.05 > [0] 73.10/24.05 = [false()] 73.10/24.05 73.10/24.05 [geq(n__s(X), n__s(Y))] = [1] Y + [1] X + [8] 73.10/24.05 >= [1] Y + [1] X + [8] 73.10/24.05 = [geq(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [div(X1, X2)] = [1] X1 + [1] X2 + [4] 73.10/24.05 > [1] X1 + [1] X2 + [1] 73.10/24.05 = [n__div(X1, X2)] 73.10/24.05 73.10/24.05 [s(X)] = [1] X + [4] 73.10/24.05 >= [1] X + [4] 73.10/24.05 = [n__s(X)] 73.10/24.05 73.10/24.05 [if(true(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.05 >= [1] X + [4] 73.10/24.05 = [activate(X)] 73.10/24.05 73.10/24.05 [if(false(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.05 >= [1] Y + [4] 73.10/24.05 = [activate(Y)] 73.10/24.05 73.10/24.05 73.10/24.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 73.10/24.05 73.10/24.05 We are left with following problem, upon which TcT provides the 73.10/24.05 certificate YES(O(1),O(n^2)). 73.10/24.05 73.10/24.05 Strict Trs: 73.10/24.05 { minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.05 , activate(n__s(X)) -> s(activate(X)) 73.10/24.05 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.05 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) } 73.10/24.05 Weak Trs: 73.10/24.05 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.05 , minus(n__0(), Y) -> 0() 73.10/24.05 , 0() -> n__0() 73.10/24.05 , activate(X) -> X 73.10/24.05 , activate(n__0()) -> 0() 73.10/24.05 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.05 , geq(X, n__0()) -> true() 73.10/24.05 , geq(n__0(), n__s(Y)) -> false() 73.10/24.05 , div(X1, X2) -> n__div(X1, X2) 73.10/24.05 , s(X) -> n__s(X) 73.10/24.05 , if(true(), X, Y) -> activate(X) 73.10/24.05 , if(false(), X, Y) -> activate(Y) } 73.10/24.05 Obligation: 73.10/24.05 innermost runtime complexity 73.10/24.05 Answer: 73.10/24.05 YES(O(1),O(n^2)) 73.10/24.05 73.10/24.05 The weightgap principle applies (using the following nonconstant 73.10/24.05 growth matrix-interpretation) 73.10/24.05 73.10/24.05 The following argument positions are usable: 73.10/24.05 Uargs(minus) = {1, 2}, Uargs(geq) = {1, 2}, Uargs(div) = {1}, 73.10/24.05 Uargs(s) = {1} 73.10/24.05 73.10/24.05 TcT has computed the following matrix interpretation satisfying 73.10/24.05 not(EDA) and not(IDA(1)). 73.10/24.05 73.10/24.05 [minus](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [n__0] = [4] 73.10/24.05 73.10/24.05 [0] = [4] 73.10/24.05 73.10/24.05 [n__s](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [activate](x1) = [1] x1 + [0] 73.10/24.05 73.10/24.05 [geq](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 [true] = [0] 73.10/24.05 73.10/24.05 [false] = [4] 73.10/24.05 73.10/24.05 [div](x1, x2) = [1] x1 + [1] x2 + [4] 73.10/24.05 73.10/24.05 [s](x1) = [1] x1 + [4] 73.10/24.05 73.10/24.05 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 73.10/24.05 73.10/24.05 [n__div](x1, x2) = [1] x1 + [1] x2 + [1] 73.10/24.05 73.10/24.05 [n__minus](x1, x2) = [1] x1 + [1] x2 + [0] 73.10/24.05 73.10/24.05 The order satisfies the following ordering constraints: 73.10/24.05 73.10/24.05 [minus(X1, X2)] = [1] X1 + [1] X2 + [0] 73.10/24.05 >= [1] X1 + [1] X2 + [0] 73.10/24.05 = [n__minus(X1, X2)] 73.10/24.05 73.10/24.05 [minus(n__0(), Y)] = [1] Y + [4] 73.10/24.05 >= [4] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [minus(n__s(X), n__s(Y))] = [1] Y + [1] X + [8] 73.10/24.05 > [1] Y + [1] X + [0] 73.10/24.05 = [minus(activate(X), activate(Y))] 73.10/24.05 73.10/24.05 [0()] = [4] 73.10/24.05 >= [4] 73.10/24.05 = [n__0()] 73.10/24.05 73.10/24.05 [activate(X)] = [1] X + [0] 73.10/24.05 >= [1] X + [0] 73.10/24.05 = [X] 73.10/24.05 73.10/24.05 [activate(n__0())] = [4] 73.10/24.05 >= [4] 73.10/24.05 = [0()] 73.10/24.05 73.10/24.05 [activate(n__s(X))] = [1] X + [4] 73.10/24.05 >= [1] X + [4] 73.10/24.05 = [s(activate(X))] 73.10/24.05 73.10/24.05 [activate(n__div(X1, X2))] = [1] X1 + [1] X2 + [1] 73.10/24.05 ? [1] X1 + [1] X2 + [4] 73.10/24.06 = [div(activate(X1), X2)] 73.10/24.06 73.10/24.06 [activate(n__minus(X1, X2))] = [1] X1 + [1] X2 + [0] 73.10/24.06 >= [1] X1 + [1] X2 + [0] 73.10/24.06 = [minus(X1, X2)] 73.10/24.06 73.10/24.06 [geq(X, n__0())] = [1] X + [4] 73.10/24.06 > [0] 73.10/24.06 = [true()] 73.10/24.06 73.10/24.06 [geq(n__0(), n__s(Y))] = [1] Y + [8] 73.10/24.06 > [4] 73.10/24.06 = [false()] 73.10/24.06 73.10/24.06 [geq(n__s(X), n__s(Y))] = [1] Y + [1] X + [8] 73.10/24.06 > [1] Y + [1] X + [0] 73.10/24.06 = [geq(activate(X), activate(Y))] 73.10/24.06 73.10/24.06 [div(X1, X2)] = [1] X1 + [1] X2 + [4] 73.10/24.06 > [1] X1 + [1] X2 + [1] 73.10/24.06 = [n__div(X1, X2)] 73.10/24.06 73.10/24.06 [s(X)] = [1] X + [4] 73.10/24.06 >= [1] X + [4] 73.10/24.06 = [n__s(X)] 73.10/24.06 73.10/24.06 [if(true(), X, Y)] = [1] Y + [1] X + [4] 73.10/24.06 > [1] X + [0] 73.10/24.06 = [activate(X)] 73.10/24.06 73.10/24.06 [if(false(), X, Y)] = [1] Y + [1] X + [8] 73.10/24.06 > [1] Y + [0] 73.10/24.06 = [activate(Y)] 73.10/24.06 73.10/24.06 73.10/24.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 73.10/24.06 73.10/24.06 We are left with following problem, upon which TcT provides the 73.10/24.06 certificate YES(O(1),O(n^2)). 73.10/24.06 73.10/24.06 Strict Trs: 73.10/24.06 { activate(n__s(X)) -> s(activate(X)) 73.10/24.06 , activate(n__div(X1, X2)) -> div(activate(X1), X2) } 73.10/24.06 Weak Trs: 73.10/24.06 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.06 , minus(n__0(), Y) -> 0() 73.10/24.06 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.06 , 0() -> n__0() 73.10/24.06 , activate(X) -> X 73.10/24.06 , activate(n__0()) -> 0() 73.10/24.06 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.06 , geq(X, n__0()) -> true() 73.10/24.06 , geq(n__0(), n__s(Y)) -> false() 73.10/24.06 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) 73.10/24.06 , div(X1, X2) -> n__div(X1, X2) 73.10/24.06 , s(X) -> n__s(X) 73.10/24.06 , if(true(), X, Y) -> activate(X) 73.10/24.06 , if(false(), X, Y) -> activate(Y) } 73.10/24.06 Obligation: 73.10/24.06 innermost runtime complexity 73.10/24.06 Answer: 73.10/24.06 YES(O(1),O(n^2)) 73.10/24.06 73.10/24.06 We use the processor 'matrix interpretation of dimension 2' to 73.10/24.06 orient following rules strictly. 73.10/24.06 73.10/24.06 Trs: 73.10/24.06 { activate(n__s(X)) -> s(activate(X)) 73.10/24.06 , activate(n__div(X1, X2)) -> div(activate(X1), X2) } 73.10/24.06 73.10/24.06 The induced complexity on above rules (modulo remaining rules) is 73.10/24.06 YES(?,O(n^2)) . These rules are moved into the corresponding weak 73.10/24.06 component(s). 73.10/24.06 73.10/24.06 Sub-proof: 73.10/24.06 ---------- 73.10/24.06 The following argument positions are usable: 73.10/24.06 Uargs(minus) = {1, 2}, Uargs(geq) = {1, 2}, Uargs(div) = {1}, 73.10/24.06 Uargs(s) = {1} 73.10/24.06 73.10/24.06 TcT has computed the following constructor-based matrix 73.10/24.06 interpretation satisfying not(EDA). 73.10/24.06 73.10/24.06 [minus](x1, x2) = [1 0] x1 + [1 4] x2 + [3] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 73.10/24.06 [n__0] = [5] 73.10/24.06 [4] 73.10/24.06 73.10/24.06 [0] = [6] 73.10/24.06 [4] 73.10/24.06 73.10/24.06 [n__s](x1) = [1 4] x1 + [3] 73.10/24.06 [0 1] [1] 73.10/24.06 73.10/24.06 [activate](x1) = [1 1] x1 + [0] 73.10/24.06 [0 1] [0] 73.10/24.06 73.10/24.06 [geq](x1, x2) = [2 0] x1 + [1 1] x2 + [0] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 73.10/24.06 [true] = [4] 73.10/24.06 [0] 73.10/24.06 73.10/24.06 [false] = [0] 73.10/24.06 [0] 73.10/24.06 73.10/24.06 [div](x1, x2) = [1 0] x1 + [0 3] x2 + [0] 73.10/24.06 [0 1] [0 1] [4] 73.10/24.06 73.10/24.06 [s](x1) = [1 4] x1 + [3] 73.10/24.06 [0 1] [1] 73.10/24.06 73.10/24.06 [if](x1, x2, x3) = [2 0] x1 + [7 7] x2 + [7 7] x3 + [0] 73.10/24.06 [0 0] [7 7] [7 7] [4] 73.10/24.06 73.10/24.06 [n__div](x1, x2) = [1 0] x1 + [0 2] x2 + [0] 73.10/24.06 [0 1] [0 1] [4] 73.10/24.06 73.10/24.06 [n__minus](x1, x2) = [1 0] x1 + [1 4] x2 + [0] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 73.10/24.06 The order satisfies the following ordering constraints: 73.10/24.06 73.10/24.06 [minus(X1, X2)] = [1 0] X1 + [1 4] X2 + [3] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 > [1 0] X1 + [1 4] X2 + [0] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 = [n__minus(X1, X2)] 73.10/24.06 73.10/24.06 [minus(n__0(), Y)] = [1 4] Y + [8] 73.10/24.06 [0 0] [4] 73.10/24.06 > [6] 73.10/24.06 [4] 73.10/24.06 = [0()] 73.10/24.06 73.10/24.06 [minus(n__s(X), n__s(Y))] = [1 8] Y + [1 4] X + [13] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 > [1 5] Y + [1 1] X + [3] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 = [minus(activate(X), activate(Y))] 73.10/24.06 73.10/24.06 [0()] = [6] 73.10/24.06 [4] 73.10/24.06 > [5] 73.10/24.06 [4] 73.10/24.06 = [n__0()] 73.10/24.06 73.10/24.06 [activate(X)] = [1 1] X + [0] 73.10/24.06 [0 1] [0] 73.10/24.06 >= [1 0] X + [0] 73.10/24.06 [0 1] [0] 73.10/24.06 = [X] 73.10/24.06 73.10/24.06 [activate(n__0())] = [9] 73.10/24.06 [4] 73.10/24.06 > [6] 73.10/24.06 [4] 73.10/24.06 = [0()] 73.10/24.06 73.10/24.06 [activate(n__s(X))] = [1 5] X + [4] 73.10/24.06 [0 1] [1] 73.10/24.06 > [1 5] X + [3] 73.10/24.06 [0 1] [1] 73.10/24.06 = [s(activate(X))] 73.10/24.06 73.10/24.06 [activate(n__div(X1, X2))] = [1 1] X1 + [0 3] X2 + [4] 73.10/24.06 [0 1] [0 1] [4] 73.10/24.06 > [1 1] X1 + [0 3] X2 + [0] 73.10/24.06 [0 1] [0 1] [4] 73.10/24.06 = [div(activate(X1), X2)] 73.10/24.06 73.10/24.06 [activate(n__minus(X1, X2))] = [1 0] X1 + [1 4] X2 + [4] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 > [1 0] X1 + [1 4] X2 + [3] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 = [minus(X1, X2)] 73.10/24.06 73.10/24.06 [geq(X, n__0())] = [2 0] X + [9] 73.10/24.06 [0 0] [4] 73.10/24.06 > [4] 73.10/24.06 [0] 73.10/24.06 = [true()] 73.10/24.06 73.10/24.06 [geq(n__0(), n__s(Y))] = [1 5] Y + [14] 73.10/24.06 [0 0] [4] 73.10/24.06 > [0] 73.10/24.06 [0] 73.10/24.06 = [false()] 73.10/24.06 73.10/24.06 [geq(n__s(X), n__s(Y))] = [1 5] Y + [2 8] X + [10] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 > [1 2] Y + [2 2] X + [0] 73.10/24.06 [0 0] [0 0] [4] 73.10/24.06 = [geq(activate(X), activate(Y))] 73.10/24.06 73.10/24.06 [div(X1, X2)] = [1 0] X1 + [0 3] X2 + [0] 73.10/24.06 [0 1] [0 1] [4] 73.10/24.06 >= [1 0] X1 + [0 2] X2 + [0] 73.10/24.06 [0 1] [0 1] [4] 73.10/24.06 = [n__div(X1, X2)] 73.10/24.06 73.10/24.06 [s(X)] = [1 4] X + [3] 73.10/24.06 [0 1] [1] 73.10/24.06 >= [1 4] X + [3] 73.10/24.06 [0 1] [1] 73.10/24.06 = [n__s(X)] 73.10/24.06 73.10/24.06 [if(true(), X, Y)] = [7 7] Y + [7 7] X + [8] 73.10/24.06 [7 7] [7 7] [4] 73.10/24.06 > [1 1] X + [0] 73.10/24.06 [0 1] [0] 73.10/24.06 = [activate(X)] 73.10/24.06 73.10/24.06 [if(false(), X, Y)] = [7 7] Y + [7 7] X + [0] 73.10/24.06 [7 7] [7 7] [4] 73.10/24.06 >= [1 1] Y + [0] 73.10/24.06 [0 1] [0] 73.10/24.06 = [activate(Y)] 73.10/24.06 73.10/24.06 73.10/24.06 We return to the main proof. 73.10/24.06 73.10/24.06 We are left with following problem, upon which TcT provides the 73.10/24.06 certificate YES(O(1),O(1)). 73.10/24.06 73.10/24.06 Weak Trs: 73.10/24.06 { minus(X1, X2) -> n__minus(X1, X2) 73.10/24.06 , minus(n__0(), Y) -> 0() 73.10/24.06 , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)) 73.10/24.06 , 0() -> n__0() 73.10/24.06 , activate(X) -> X 73.10/24.06 , activate(n__0()) -> 0() 73.10/24.06 , activate(n__s(X)) -> s(activate(X)) 73.10/24.06 , activate(n__div(X1, X2)) -> div(activate(X1), X2) 73.10/24.06 , activate(n__minus(X1, X2)) -> minus(X1, X2) 73.10/24.06 , geq(X, n__0()) -> true() 73.10/24.06 , geq(n__0(), n__s(Y)) -> false() 73.10/24.06 , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)) 73.10/24.06 , div(X1, X2) -> n__div(X1, X2) 73.10/24.06 , s(X) -> n__s(X) 73.10/24.06 , if(true(), X, Y) -> activate(X) 73.10/24.06 , if(false(), X, Y) -> activate(Y) } 73.10/24.06 Obligation: 73.10/24.06 innermost runtime complexity 73.10/24.06 Answer: 73.10/24.06 YES(O(1),O(1)) 73.10/24.06 73.10/24.06 Empty rules are trivially bounded 73.10/24.06 73.10/24.06 Hurray, we answered YES(O(1),O(n^2)) 73.10/24.07 EOF