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: { f(x, nil()) -> g(nil(), x) , f(x, g(y, z)) -> g(f(x, y), z) , ++(x, nil()) -> x , ++(x, g(y, z)) -> g(++(x, y), z) , null(nil()) -> true() , null(g(x, y)) -> false() , mem(x, max(x)) -> not(null(x)) , mem(nil(), y) -> false() , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) , max(g(g(nil(), x), y)) -> max'(x, y) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Obligation: 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(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, Uargs(max') = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [f](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [g](x1, x2) = [1] x1 + [1] x2 + [0] [++](x1, x2) = [1] x1 + [1] x2 + [0] [null](x1) = [1] [true] = [0] [false] = [0] [mem](x1, x2) = [0] [or](x1, x2) = [1] x1 + [1] x2 + [0] [=](x1, x2) = [3] [max](x1) = [1] x1 + [0] [not](x1) = [1] x1 + [5] [max'](x1, x2) = [1] x1 + [1] x2 + [0] [u] = [0] The following symbols are considered usable {f, ++, null, mem, max} The order satisfies the following ordering constraints: [f(x, nil())] = [1] x + [0] >= [1] x + [0] = [g(nil(), x)] [f(x, g(y, z))] = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = [g(f(x, y), z)] [++(x, nil())] = [1] x + [0] >= [1] x + [0] = [x] [++(x, g(y, z))] = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = [g(++(x, y), z)] [null(nil())] = [1] > [0] = [true()] [null(g(x, y))] = [1] > [0] = [false()] [mem(x, max(x))] = [0] ? [6] = [not(null(x))] [mem(nil(), y)] = [0] >= [0] = [false()] [mem(g(x, y), z)] = [0] ? [3] = [or(=(y, z), mem(x, z))] [max(g(g(nil(), x), y))] = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = [max'(x, y)] [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = [max'(max(g(g(x, y), z)), u())] 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: { f(x, nil()) -> g(nil(), x) , f(x, g(y, z)) -> g(f(x, y), z) , ++(x, nil()) -> x , ++(x, g(y, z)) -> g(++(x, y), z) , mem(x, max(x)) -> not(null(x)) , mem(nil(), y) -> false() , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) , max(g(g(nil(), x), y)) -> max'(x, y) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Weak Trs: { null(nil()) -> true() , null(g(x, y)) -> false() } Obligation: 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(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, Uargs(max') = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [f](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [1] [g](x1, x2) = [1] x1 + [1] x2 + [0] [++](x1, x2) = [1] x1 + [1] x2 + [0] [null](x1) = [1] x1 + [7] [true] = [0] [false] = [0] [mem](x1, x2) = [1] x1 + [1] x2 + [0] [or](x1, x2) = [1] x1 + [1] x2 + [1] [=](x1, x2) = [1] x1 + [1] [max](x1) = [1] x1 + [0] [not](x1) = [1] x1 + [7] [max'](x1, x2) = [1] x1 + [1] x2 + [0] [u] = [0] The following symbols are considered usable {f, ++, null, mem, max} The order satisfies the following ordering constraints: [f(x, nil())] = [1] x + [1] >= [1] x + [1] = [g(nil(), x)] [f(x, g(y, z))] = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = [g(f(x, y), z)] [++(x, nil())] = [1] x + [1] > [1] x + [0] = [x] [++(x, g(y, z))] = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = [g(++(x, y), z)] [null(nil())] = [8] > [0] = [true()] [null(g(x, y))] = [1] x + [1] y + [7] > [0] = [false()] [mem(x, max(x))] = [2] x + [0] ? [1] x + [14] = [not(null(x))] [mem(nil(), y)] = [1] y + [1] > [0] = [false()] [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [0] ? [1] x + [1] y + [1] z + [2] = [or(=(y, z), mem(x, z))] [max(g(g(nil(), x), y))] = [1] x + [1] y + [1] > [1] x + [1] y + [0] = [max'(x, y)] [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = [max'(max(g(g(x, y), z)), u())] 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: { f(x, nil()) -> g(nil(), x) , f(x, g(y, z)) -> g(f(x, y), z) , ++(x, g(y, z)) -> g(++(x, y), z) , mem(x, max(x)) -> not(null(x)) , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Weak Trs: { ++(x, nil()) -> x , null(nil()) -> true() , null(g(x, y)) -> false() , mem(nil(), y) -> false() , max(g(g(nil(), x), y)) -> max'(x, y) } Obligation: 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(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, Uargs(max') = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [f](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [g](x1, x2) = [1] x1 + [1] x2 + [0] [++](x1, x2) = [1] x1 + [1] x2 + [7] [null](x1) = [1] x1 + [5] [true] = [4] [false] = [5] [mem](x1, x2) = [1] x1 + [1] x2 + [7] [or](x1, x2) = [1] x1 + [1] x2 + [3] [=](x1, x2) = [1] x1 + [3] [max](x1) = [1] x1 + [7] [not](x1) = [1] x1 + [7] [max'](x1, x2) = [1] x1 + [1] x2 + [7] [u] = [0] The following symbols are considered usable {f, ++, null, mem, max} The order satisfies the following ordering constraints: [f(x, nil())] = [1] x + [14] > [1] x + [7] = [g(nil(), x)] [f(x, g(y, z))] = [1] x + [1] y + [1] z + [7] >= [1] x + [1] y + [1] z + [7] = [g(f(x, y), z)] [++(x, nil())] = [1] x + [14] > [1] x + [0] = [x] [++(x, g(y, z))] = [1] x + [1] y + [1] z + [7] >= [1] x + [1] y + [1] z + [7] = [g(++(x, y), z)] [null(nil())] = [12] > [4] = [true()] [null(g(x, y))] = [1] x + [1] y + [5] >= [5] = [false()] [mem(x, max(x))] = [2] x + [14] > [1] x + [12] = [not(null(x))] [mem(nil(), y)] = [1] y + [14] > [5] = [false()] [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [7] ? [1] x + [1] y + [1] z + [13] = [or(=(y, z), mem(x, z))] [max(g(g(nil(), x), y))] = [1] x + [1] y + [14] > [1] x + [1] y + [7] = [max'(x, y)] [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [7] ? [1] x + [1] y + [1] z + [14] = [max'(max(g(g(x, y), z)), u())] 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: { f(x, g(y, z)) -> g(f(x, y), z) , ++(x, g(y, z)) -> g(++(x, y), z) , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Weak Trs: { f(x, nil()) -> g(nil(), x) , ++(x, nil()) -> x , null(nil()) -> true() , null(g(x, y)) -> false() , mem(x, max(x)) -> not(null(x)) , mem(nil(), y) -> false() , max(g(g(nil(), x), y)) -> max'(x, y) } Obligation: 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(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, Uargs(max') = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [f](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [g](x1, x2) = [1] x1 + [1] x2 + [0] [++](x1, x2) = [1] x1 + [1] x2 + [1] [null](x1) = [1] x1 + [1] [true] = [1] [false] = [1] [mem](x1, x2) = [1] x1 + [1] x2 + [7] [or](x1, x2) = [1] x1 + [1] x2 + [3] [=](x1, x2) = [1] x1 + [2] [max](x1) = [1] x1 + [0] [not](x1) = [1] x1 + [6] [max'](x1, x2) = [1] x1 + [0] [u] = [1] The following symbols are considered usable {f, ++, null, mem, max} The order satisfies the following ordering constraints: [f(x, nil())] = [1] x + [0] >= [1] x + [0] = [g(nil(), x)] [f(x, g(y, z))] = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = [g(f(x, y), z)] [++(x, nil())] = [1] x + [1] > [1] x + [0] = [x] [++(x, g(y, z))] = [1] x + [1] y + [1] z + [1] >= [1] x + [1] y + [1] z + [1] = [g(++(x, y), z)] [null(nil())] = [1] >= [1] = [true()] [null(g(x, y))] = [1] x + [1] y + [1] >= [1] = [false()] [mem(x, max(x))] = [2] x + [7] >= [1] x + [7] = [not(null(x))] [mem(nil(), y)] = [1] y + [7] > [1] = [false()] [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [7] ? [1] x + [1] y + [1] z + [12] = [or(=(y, z), mem(x, z))] [max(g(g(nil(), x), y))] = [1] x + [1] y + [0] >= [1] x + [0] = [max'(x, y)] [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [1] > [1] x + [1] y + [1] z + [0] = [max'(max(g(g(x, y), z)), u())] 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: { f(x, g(y, z)) -> g(f(x, y), z) , ++(x, g(y, z)) -> g(++(x, y), z) , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) } Weak Trs: { f(x, nil()) -> g(nil(), x) , ++(x, nil()) -> x , null(nil()) -> true() , null(g(x, y)) -> false() , mem(x, max(x)) -> not(null(x)) , mem(nil(), y) -> false() , max(g(g(nil(), x), y)) -> max'(x, y) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Obligation: 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(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, Uargs(max') = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [f](x1, x2) = [1] x1 + [1] x2 + [4] [nil] = [4] [g](x1, x2) = [1] x1 + [1] x2 + [1] [++](x1, x2) = [1] x1 + [1] x2 + [0] [null](x1) = [1] x1 + [1] [true] = [5] [false] = [1] [mem](x1, x2) = [1] x1 + [1] x2 + [3] [or](x1, x2) = [1] x1 + [1] x2 + [0] [=](x1, x2) = [1] x1 + [0] [max](x1) = [1] x1 + [0] [not](x1) = [1] x1 + [2] [max'](x1, x2) = [1] x1 + [0] [u] = [6] The following symbols are considered usable {f, ++, null, mem, max} The order satisfies the following ordering constraints: [f(x, nil())] = [1] x + [8] > [1] x + [5] = [g(nil(), x)] [f(x, g(y, z))] = [1] x + [1] y + [1] z + [5] >= [1] x + [1] y + [1] z + [5] = [g(f(x, y), z)] [++(x, nil())] = [1] x + [4] > [1] x + [0] = [x] [++(x, g(y, z))] = [1] x + [1] y + [1] z + [1] >= [1] x + [1] y + [1] z + [1] = [g(++(x, y), z)] [null(nil())] = [5] >= [5] = [true()] [null(g(x, y))] = [1] x + [1] y + [2] > [1] = [false()] [mem(x, max(x))] = [2] x + [3] >= [1] x + [3] = [not(null(x))] [mem(nil(), y)] = [1] y + [7] > [1] = [false()] [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [4] > [1] x + [1] y + [1] z + [3] = [or(=(y, z), mem(x, z))] [max(g(g(nil(), x), y))] = [1] x + [1] y + [6] > [1] x + [0] = [max'(x, y)] [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [9] > [1] x + [1] y + [1] z + [2] = [max'(max(g(g(x, y), z)), u())] 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: { f(x, g(y, z)) -> g(f(x, y), z) , ++(x, g(y, z)) -> g(++(x, y), z) } Weak Trs: { f(x, nil()) -> g(nil(), x) , ++(x, nil()) -> x , null(nil()) -> true() , null(g(x, y)) -> false() , mem(x, max(x)) -> not(null(x)) , mem(nil(), y) -> false() , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) , max(g(g(nil(), x), y)) -> max'(x, y) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { f(x, g(y, z)) -> g(f(x, y), z) } 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(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, Uargs(max') = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [f](x1, x2) = [7] x1 + [2] x2 + [0] [nil] = [4] [g](x1, x2) = [1] x1 + [1] x2 + [4] [++](x1, x2) = [7] x1 + [1] x2 + [0] [null](x1) = [0] [true] = [0] [false] = [0] [mem](x1, x2) = [1] x1 + [0] [or](x1, x2) = [1] x1 + [1] x2 + [1] [=](x1, x2) = [1] x1 + [1] [max](x1) = [1] x1 + [0] [not](x1) = [1] x1 + [0] [max'](x1, x2) = [1] x1 + [0] [u] = [0] The following symbols are considered usable {f, ++, null, mem, max} The order satisfies the following ordering constraints: [f(x, nil())] = [7] x + [8] >= [1] x + [8] = [g(nil(), x)] [f(x, g(y, z))] = [7] x + [2] y + [2] z + [8] > [7] x + [2] y + [1] z + [4] = [g(f(x, y), z)] [++(x, nil())] = [7] x + [4] > [1] x + [0] = [x] [++(x, g(y, z))] = [7] x + [1] y + [1] z + [4] >= [7] x + [1] y + [1] z + [4] = [g(++(x, y), z)] [null(nil())] = [0] >= [0] = [true()] [null(g(x, y))] = [0] >= [0] = [false()] [mem(x, max(x))] = [1] x + [0] >= [0] = [not(null(x))] [mem(nil(), y)] = [4] > [0] = [false()] [mem(g(x, y), z)] = [1] x + [1] y + [4] > [1] x + [1] y + [2] = [or(=(y, z), mem(x, z))] [max(g(g(nil(), x), y))] = [1] x + [1] y + [12] > [1] x + [0] = [max'(x, y)] [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [12] > [1] x + [1] y + [1] z + [8] = [max'(max(g(g(x, y), z)), u())] 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: { ++(x, g(y, z)) -> g(++(x, y), z) } Weak Trs: { f(x, nil()) -> g(nil(), x) , f(x, g(y, z)) -> g(f(x, y), z) , ++(x, nil()) -> x , null(nil()) -> true() , null(g(x, y)) -> false() , mem(x, max(x)) -> not(null(x)) , mem(nil(), y) -> false() , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) , max(g(g(nil(), x), y)) -> max'(x, y) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Obligation: runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { ++(x, g(y, z)) -> g(++(x, y), z) } 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(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, Uargs(max') = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [f](x1, x2) = [7] x1 + [3] x2 + [0] [nil] = [4] [g](x1, x2) = [1] x1 + [1] x2 + [3] [++](x1, x2) = [7] x1 + [3] x2 + [0] [null](x1) = [0] [true] = [0] [false] = [0] [mem](x1, x2) = [0] [or](x1, x2) = [1] x1 + [1] x2 + [0] [=](x1, x2) = [0] [max](x1) = [1] x1 + [0] [not](x1) = [1] x1 + [0] [max'](x1, x2) = [1] x1 + [1] x2 + [0] [u] = [2] The following symbols are considered usable {f, ++, null, mem, max} The order satisfies the following ordering constraints: [f(x, nil())] = [7] x + [12] > [1] x + [7] = [g(nil(), x)] [f(x, g(y, z))] = [7] x + [3] y + [3] z + [9] > [7] x + [3] y + [1] z + [3] = [g(f(x, y), z)] [++(x, nil())] = [7] x + [12] > [1] x + [0] = [x] [++(x, g(y, z))] = [7] x + [3] y + [3] z + [9] > [7] x + [3] y + [1] z + [3] = [g(++(x, y), z)] [null(nil())] = [0] >= [0] = [true()] [null(g(x, y))] = [0] >= [0] = [false()] [mem(x, max(x))] = [0] >= [0] = [not(null(x))] [mem(nil(), y)] = [0] >= [0] = [false()] [mem(g(x, y), z)] = [0] >= [0] = [or(=(y, z), mem(x, z))] [max(g(g(nil(), x), y))] = [1] x + [1] y + [10] > [1] x + [1] y + [0] = [max'(x, y)] [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [11] > [1] x + [1] y + [1] z + [8] = [max'(max(g(g(x, y), z)), u())] 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: { f(x, nil()) -> g(nil(), x) , f(x, g(y, z)) -> g(f(x, y), z) , ++(x, nil()) -> x , ++(x, g(y, z)) -> g(++(x, y), z) , null(nil()) -> true() , null(g(x, y)) -> false() , mem(x, max(x)) -> not(null(x)) , mem(nil(), y) -> false() , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) , max(g(g(nil(), x), y)) -> max'(x, y) , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } Obligation: runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))