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: { minus(0(), Y) -> 0() , minus(s(X), s(Y)) -> minus(X, Y) , geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() , geq(s(X), s(Y)) -> geq(X, Y) , div(0(), s(Y)) -> 0() , div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(false(), X, Y) -> Y } 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(minus) = {1}, Uargs(s) = {1}, Uargs(geq) = {1}, Uargs(div) = {1}, Uargs(if) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [minus](x1, x2) = [2 0] x1 + [0] [0 0] [0] [0] = [0] [0] [s](x1) = [1 0] x1 + [0] [1 0] [2] [geq](x1, x2) = [1 0] x1 + [0] [0 0] [1] [true] = [0] [0] [false] = [0] [1] [div](x1, x2) = [1 2] x1 + [0] [4 4] [4] [if](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 4] x3 + [0] [0 0] [0 4] [7 2] [0] The following symbols are considered usable {minus, geq, div, if} The order satisfies the following ordering constraints: [minus(0(), Y)] = [0] [0] >= [0] [0] = [0()] [minus(s(X), s(Y))] = [2 0] X + [0] [0 0] [0] >= [2 0] X + [0] [0 0] [0] = [minus(X, Y)] [geq(X, 0())] = [1 0] X + [0] [0 0] [1] >= [0] [0] = [true()] [geq(0(), s(Y))] = [0] [1] >= [0] [1] = [false()] [geq(s(X), s(Y))] = [1 0] X + [0] [0 0] [1] >= [1 0] X + [0] [0 0] [1] = [geq(X, Y)] [div(0(), s(Y))] = [0] [4] >= [0] [0] = [0()] [div(s(X), s(Y))] = [3 0] X + [4] [8 0] [12] > [3 0] X + [2] [8 0] [8] = [if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())] [if(true(), X, Y)] = [1 4] Y + [1 0] X + [0] [7 2] [0 4] [0] >= [1 0] X + [0] [0 1] [0] = [X] [if(false(), X, Y)] = [1 4] Y + [1 0] X + [2] [7 2] [0 4] [0] > [1 0] Y + [0] [0 1] [0] = [Y] 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: { minus(0(), Y) -> 0() , minus(s(X), s(Y)) -> minus(X, Y) , geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() , geq(s(X), s(Y)) -> geq(X, Y) , div(0(), s(Y)) -> 0() , if(true(), X, Y) -> X } Weak Trs: { div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(false(), X, Y) -> Y } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { if(true(), X, Y) -> 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(minus) = {1}, Uargs(s) = {1}, Uargs(geq) = {1}, Uargs(div) = {1}, Uargs(if) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [minus](x1, x2) = [2 0] x1 + [0] [0 0] [0] [0] = [0] [0] [s](x1) = [1 0] x1 + [0] [1 0] [2] [geq](x1, x2) = [1 0] x1 + [0] [0 0] [1] [true] = [0] [1] [false] = [0] [0] [div](x1, x2) = [1 4] x1 + [0] [4 0] [4] [if](x1, x2, x3) = [1 2] x1 + [2 0] x2 + [1 4] x3 + [0] [0 0] [0 2] [7 4] [0] The following symbols are considered usable {minus, geq, div, if} The order satisfies the following ordering constraints: [minus(0(), Y)] = [0] [0] >= [0] [0] = [0()] [minus(s(X), s(Y))] = [2 0] X + [0] [0 0] [0] >= [2 0] X + [0] [0 0] [0] = [minus(X, Y)] [geq(X, 0())] = [1 0] X + [0] [0 0] [1] >= [0] [1] = [true()] [geq(0(), s(Y))] = [0] [1] >= [0] [0] = [false()] [geq(s(X), s(Y))] = [1 0] X + [0] [0 0] [1] >= [1 0] X + [0] [0 0] [1] = [geq(X, Y)] [div(0(), s(Y))] = [0] [4] >= [0] [0] = [0()] [div(s(X), s(Y))] = [5 0] X + [8] [4 0] [4] > [5 0] X + [2] [4 0] [4] = [if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())] [if(true(), X, Y)] = [1 4] Y + [2 0] X + [2] [7 4] [0 2] [0] > [1 0] X + [0] [0 1] [0] = [X] [if(false(), X, Y)] = [1 4] Y + [2 0] X + [0] [7 4] [0 2] [0] >= [1 0] Y + [0] [0 1] [0] = [Y] 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: { minus(0(), Y) -> 0() , minus(s(X), s(Y)) -> minus(X, Y) , geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() , geq(s(X), s(Y)) -> geq(X, Y) , div(0(), s(Y)) -> 0() } Weak Trs: { div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { div(0(), s(Y)) -> 0() } 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(minus) = {1}, Uargs(s) = {1}, Uargs(geq) = {1}, Uargs(div) = {1}, Uargs(if) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [minus](x1, x2) = [1 0] x1 + [0] [0 0] [4] [0] = [0] [0] [s](x1) = [1 0] x1 + [0] [1 0] [4] [geq](x1, x2) = [1 0] x1 + [0] [0 0] [0] [true] = [0] [0] [false] = [0] [0] [div](x1, x2) = [4 1] x1 + [1] [7 1] [5] [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 4] x3 + [0] [0 0] [0 1] [7 2] [0] The following symbols are considered usable {minus, geq, div, if} The order satisfies the following ordering constraints: [minus(0(), Y)] = [0] [4] >= [0] [0] = [0()] [minus(s(X), s(Y))] = [1 0] X + [0] [0 0] [4] >= [1 0] X + [0] [0 0] [4] = [minus(X, Y)] [geq(X, 0())] = [1 0] X + [0] [0 0] [0] >= [0] [0] = [true()] [geq(0(), s(Y))] = [0] [0] >= [0] [0] = [false()] [geq(s(X), s(Y))] = [1 0] X + [0] [0 0] [0] >= [1 0] X + [0] [0 0] [0] = [geq(X, Y)] [div(0(), s(Y))] = [1] [5] > [0] [0] = [0()] [div(s(X), s(Y))] = [5 0] X + [5] [8 0] [9] >= [5 0] X + [5] [4 0] [9] = [if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())] [if(true(), X, Y)] = [1 4] Y + [1 0] X + [0] [7 2] [0 1] [0] >= [1 0] X + [0] [0 1] [0] = [X] [if(false(), X, Y)] = [1 4] Y + [1 0] X + [0] [7 2] [0 1] [0] >= [1 0] Y + [0] [0 1] [0] = [Y] 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: { minus(0(), Y) -> 0() , minus(s(X), s(Y)) -> minus(X, Y) , geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() , geq(s(X), s(Y)) -> geq(X, Y) } Weak Trs: { div(0(), s(Y)) -> 0() , div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { minus(s(X), s(Y)) -> minus(X, Y) , geq(s(X), s(Y)) -> geq(X, Y) } 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(minus) = {1}, Uargs(s) = {1}, Uargs(geq) = {1}, Uargs(div) = {1}, Uargs(if) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [minus](x1, x2) = [1 0] x1 + [0] [0 0] [0] [0] = [0] [0] [s](x1) = [1 0] x1 + [1] [1 0] [0] [geq](x1, x2) = [1 0] x1 + [0] [0 0] [1] [true] = [0] [0] [false] = [0] [0] [div](x1, x2) = [4 5] x1 + [0] [1 7] [0] [if](x1, x2, x3) = [1 2] x1 + [2 0] x2 + [1 4] x3 + [0] [0 0] [0 2] [7 1] [0] The following symbols are considered usable {minus, geq, div, if} The order satisfies the following ordering constraints: [minus(0(), Y)] = [0] [0] >= [0] [0] = [0()] [minus(s(X), s(Y))] = [1 0] X + [1] [0 0] [0] > [1 0] X + [0] [0 0] [0] = [minus(X, Y)] [geq(X, 0())] = [1 0] X + [0] [0 0] [1] >= [0] [0] = [true()] [geq(0(), s(Y))] = [0] [1] >= [0] [0] = [false()] [geq(s(X), s(Y))] = [1 0] X + [1] [0 0] [1] > [1 0] X + [0] [0 0] [1] = [geq(X, Y)] [div(0(), s(Y))] = [0] [0] >= [0] [0] = [0()] [div(s(X), s(Y))] = [9 0] X + [4] [8 0] [1] >= [9 0] X + [4] [8 0] [0] = [if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())] [if(true(), X, Y)] = [1 4] Y + [2 0] X + [0] [7 1] [0 2] [0] >= [1 0] X + [0] [0 1] [0] = [X] [if(false(), X, Y)] = [1 4] Y + [2 0] X + [0] [7 1] [0 2] [0] >= [1 0] Y + [0] [0 1] [0] = [Y] 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: { minus(0(), Y) -> 0() , geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() } Weak Trs: { minus(s(X), s(Y)) -> minus(X, Y) , geq(s(X), s(Y)) -> geq(X, Y) , div(0(), s(Y)) -> 0() , div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() } 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(minus) = {1}, Uargs(s) = {1}, Uargs(geq) = {1}, Uargs(div) = {1}, Uargs(if) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [minus](x1, x2) = [1 0] x1 + [0] [0 0] [0] [0] = [0] [0] [s](x1) = [1 0] x1 + [1] [1 0] [0] [geq](x1, x2) = [2 0] x1 + [1] [0 0] [1] [true] = [0] [0] [false] = [0] [0] [div](x1, x2) = [4 6] x1 + [0 0] x2 + [0] [2 6] [4 4] [0] [if](x1, x2, x3) = [1 1] x1 + [2 0] x2 + [4 4] x3 + [0] [0 0] [0 2] [7 2] [0] The following symbols are considered usable {minus, geq, div, if} The order satisfies the following ordering constraints: [minus(0(), Y)] = [0] [0] >= [0] [0] = [0()] [minus(s(X), s(Y))] = [1 0] X + [1] [0 0] [0] > [1 0] X + [0] [0 0] [0] = [minus(X, Y)] [geq(X, 0())] = [2 0] X + [1] [0 0] [1] > [0] [0] = [true()] [geq(0(), s(Y))] = [1] [1] > [0] [0] = [false()] [geq(s(X), s(Y))] = [2 0] X + [3] [0 0] [1] > [2 0] X + [1] [0 0] [1] = [geq(X, Y)] [div(0(), s(Y))] = [0 0] Y + [0] [8 0] [4] >= [0] [0] = [0()] [div(s(X), s(Y))] = [0 0] Y + [10 0] X + [4] [8 0] [ 8 0] [6] >= [10 0] X + [4] [ 8 0] [0] = [if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())] [if(true(), X, Y)] = [4 4] Y + [2 0] X + [0] [7 2] [0 2] [0] >= [1 0] X + [0] [0 1] [0] = [X] [if(false(), X, Y)] = [4 4] Y + [2 0] X + [0] [7 2] [0 2] [0] >= [1 0] Y + [0] [0 1] [0] = [Y] 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: { minus(0(), Y) -> 0() } Weak Trs: { minus(s(X), s(Y)) -> minus(X, Y) , geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() , geq(s(X), s(Y)) -> geq(X, Y) , div(0(), s(Y)) -> 0() , div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { minus(0(), Y) -> 0() } 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(minus) = {1}, Uargs(s) = {1}, Uargs(geq) = {1}, Uargs(div) = {1}, Uargs(if) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [minus](x1, x2) = [2 0] x1 + [0] [0 0] [0] [0] = [1] [0] [s](x1) = [1 0] x1 + [4] [1 0] [0] [geq](x1, x2) = [2 0] x1 + [0] [0 0] [4] [true] = [0] [0] [false] = [0] [0] [div](x1, x2) = [2 4] x1 + [0] [1 7] [4] [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 4] x3 + [0] [0 0] [0 2] [0 4] [0] The following symbols are considered usable {minus, geq, div, if} The order satisfies the following ordering constraints: [minus(0(), Y)] = [2] [0] > [1] [0] = [0()] [minus(s(X), s(Y))] = [2 0] X + [8] [0 0] [0] > [2 0] X + [0] [0 0] [0] = [minus(X, Y)] [geq(X, 0())] = [2 0] X + [0] [0 0] [4] >= [0] [0] = [true()] [geq(0(), s(Y))] = [2] [4] > [0] [0] = [false()] [geq(s(X), s(Y))] = [2 0] X + [8] [0 0] [4] > [2 0] X + [0] [0 0] [4] = [geq(X, Y)] [div(0(), s(Y))] = [2] [5] > [1] [0] = [0()] [div(s(X), s(Y))] = [6 0] X + [8] [8 0] [8] > [6 0] X + [5] [8 0] [0] = [if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())] [if(true(), X, Y)] = [1 4] Y + [1 0] X + [0] [0 4] [0 2] [0] >= [1 0] X + [0] [0 1] [0] = [X] [if(false(), X, Y)] = [1 4] Y + [1 0] X + [0] [0 4] [0 2] [0] >= [1 0] Y + [0] [0 1] [0] = [Y] 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: { minus(0(), Y) -> 0() , minus(s(X), s(Y)) -> minus(X, Y) , geq(X, 0()) -> true() , geq(0(), s(Y)) -> false() , geq(s(X), s(Y)) -> geq(X, Y) , div(0(), s(Y)) -> 0() , div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y } Obligation: runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))