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