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