YES(O(1),O(n^1)) 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(n^1)). 592.21/297.04 592.21/297.04 Strict Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, nil()) -> x 592.21/297.04 , ++(x, g(y, z)) -> g(++(x, y), z) 592.21/297.04 , null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 The weightgap principle applies (using the following nonconstant 592.21/297.04 growth matrix-interpretation) 592.21/297.04 592.21/297.04 The following argument positions are usable: 592.21/297.04 Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, 592.21/297.04 Uargs(max') = {1} 592.21/297.04 592.21/297.04 TcT has computed the following matrix interpretation satisfying 592.21/297.04 not(EDA) and not(IDA(1)). 592.21/297.04 592.21/297.04 [f](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [nil] = [0] 592.21/297.04 592.21/297.04 [g](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [++](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [null](x1) = [1] 592.21/297.04 592.21/297.04 [true] = [0] 592.21/297.04 592.21/297.04 [false] = [0] 592.21/297.04 592.21/297.04 [mem](x1, x2) = [0] 592.21/297.04 592.21/297.04 [or](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [=](x1, x2) = [3] 592.21/297.04 592.21/297.04 [max](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [not](x1) = [1] x1 + [5] 592.21/297.04 592.21/297.04 [max'](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [u] = [0] 592.21/297.04 592.21/297.04 The order satisfies the following ordering constraints: 592.21/297.04 592.21/297.04 [f(x, nil())] = [1] x + [0] 592.21/297.04 >= [1] x + [0] 592.21/297.04 = [g(nil(), x)] 592.21/297.04 592.21/297.04 [f(x, g(y, z))] = [1] x + [1] y + [1] z + [0] 592.21/297.04 >= [1] x + [1] y + [1] z + [0] 592.21/297.04 = [g(f(x, y), z)] 592.21/297.04 592.21/297.04 [++(x, nil())] = [1] x + [0] 592.21/297.04 >= [1] x + [0] 592.21/297.04 = [x] 592.21/297.04 592.21/297.04 [++(x, g(y, z))] = [1] x + [1] y + [1] z + [0] 592.21/297.04 >= [1] x + [1] y + [1] z + [0] 592.21/297.04 = [g(++(x, y), z)] 592.21/297.04 592.21/297.04 [null(nil())] = [1] 592.21/297.04 > [0] 592.21/297.04 = [true()] 592.21/297.04 592.21/297.04 [null(g(x, y))] = [1] 592.21/297.04 > [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(x, max(x))] = [0] 592.21/297.04 ? [6] 592.21/297.04 = [not(null(x))] 592.21/297.04 592.21/297.04 [mem(nil(), y)] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(g(x, y), z)] = [0] 592.21/297.04 ? [3] 592.21/297.04 = [or(=(y, z), mem(x, z))] 592.21/297.04 592.21/297.04 [max(g(g(nil(), x), y))] = [1] x + [1] y + [0] 592.21/297.04 >= [1] x + [1] y + [0] 592.21/297.04 = [max'(x, y)] 592.21/297.04 592.21/297.04 [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [0] 592.21/297.04 >= [1] x + [1] y + [1] z + [0] 592.21/297.04 = [max'(max(g(g(x, y), z)), u())] 592.21/297.04 592.21/297.04 592.21/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(n^1)). 592.21/297.04 592.21/297.04 Strict Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, nil()) -> x 592.21/297.04 , ++(x, g(y, z)) -> g(++(x, y), z) 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Weak Trs: 592.21/297.04 { null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 The weightgap principle applies (using the following nonconstant 592.21/297.04 growth matrix-interpretation) 592.21/297.04 592.21/297.04 The following argument positions are usable: 592.21/297.04 Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, 592.21/297.04 Uargs(max') = {1} 592.21/297.04 592.21/297.04 TcT has computed the following matrix interpretation satisfying 592.21/297.04 not(EDA) and not(IDA(1)). 592.21/297.04 592.21/297.04 [f](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [nil] = [1] 592.21/297.04 592.21/297.04 [g](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [++](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [null](x1) = [1] x1 + [7] 592.21/297.04 592.21/297.04 [true] = [0] 592.21/297.04 592.21/297.04 [false] = [0] 592.21/297.04 592.21/297.04 [mem](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [or](x1, x2) = [1] x1 + [1] x2 + [1] 592.21/297.04 592.21/297.04 [=](x1, x2) = [1] x1 + [1] 592.21/297.04 592.21/297.04 [max](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [not](x1) = [1] x1 + [7] 592.21/297.04 592.21/297.04 [max'](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [u] = [0] 592.21/297.04 592.21/297.04 The order satisfies the following ordering constraints: 592.21/297.04 592.21/297.04 [f(x, nil())] = [1] x + [1] 592.21/297.04 >= [1] x + [1] 592.21/297.04 = [g(nil(), x)] 592.21/297.04 592.21/297.04 [f(x, g(y, z))] = [1] x + [1] y + [1] z + [0] 592.21/297.04 >= [1] x + [1] y + [1] z + [0] 592.21/297.04 = [g(f(x, y), z)] 592.21/297.04 592.21/297.04 [++(x, nil())] = [1] x + [1] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [x] 592.21/297.04 592.21/297.04 [++(x, g(y, z))] = [1] x + [1] y + [1] z + [0] 592.21/297.04 >= [1] x + [1] y + [1] z + [0] 592.21/297.04 = [g(++(x, y), z)] 592.21/297.04 592.21/297.04 [null(nil())] = [8] 592.21/297.04 > [0] 592.21/297.04 = [true()] 592.21/297.04 592.21/297.04 [null(g(x, y))] = [1] x + [1] y + [7] 592.21/297.04 > [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(x, max(x))] = [2] x + [0] 592.21/297.04 ? [1] x + [14] 592.21/297.04 = [not(null(x))] 592.21/297.04 592.21/297.04 [mem(nil(), y)] = [1] y + [1] 592.21/297.04 > [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [0] 592.21/297.04 ? [1] x + [1] y + [1] z + [2] 592.21/297.04 = [or(=(y, z), mem(x, z))] 592.21/297.04 592.21/297.04 [max(g(g(nil(), x), y))] = [1] x + [1] y + [1] 592.21/297.04 > [1] x + [1] y + [0] 592.21/297.04 = [max'(x, y)] 592.21/297.04 592.21/297.04 [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [0] 592.21/297.04 >= [1] x + [1] y + [1] z + [0] 592.21/297.04 = [max'(max(g(g(x, y), z)), u())] 592.21/297.04 592.21/297.04 592.21/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(n^1)). 592.21/297.04 592.21/297.04 Strict Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, g(y, z)) -> g(++(x, y), z) 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Weak Trs: 592.21/297.04 { ++(x, nil()) -> x 592.21/297.04 , null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 The weightgap principle applies (using the following nonconstant 592.21/297.04 growth matrix-interpretation) 592.21/297.04 592.21/297.04 The following argument positions are usable: 592.21/297.04 Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, 592.21/297.04 Uargs(max') = {1} 592.21/297.04 592.21/297.04 TcT has computed the following matrix interpretation satisfying 592.21/297.04 not(EDA) and not(IDA(1)). 592.21/297.04 592.21/297.04 [f](x1, x2) = [1] x1 + [1] x2 + [7] 592.21/297.04 592.21/297.04 [nil] = [7] 592.21/297.04 592.21/297.04 [g](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [++](x1, x2) = [1] x1 + [1] x2 + [7] 592.21/297.04 592.21/297.04 [null](x1) = [1] x1 + [5] 592.21/297.04 592.21/297.04 [true] = [4] 592.21/297.04 592.21/297.04 [false] = [5] 592.21/297.04 592.21/297.04 [mem](x1, x2) = [1] x1 + [1] x2 + [7] 592.21/297.04 592.21/297.04 [or](x1, x2) = [1] x1 + [1] x2 + [3] 592.21/297.04 592.21/297.04 [=](x1, x2) = [1] x1 + [3] 592.21/297.04 592.21/297.04 [max](x1) = [1] x1 + [7] 592.21/297.04 592.21/297.04 [not](x1) = [1] x1 + [7] 592.21/297.04 592.21/297.04 [max'](x1, x2) = [1] x1 + [1] x2 + [7] 592.21/297.04 592.21/297.04 [u] = [0] 592.21/297.04 592.21/297.04 The order satisfies the following ordering constraints: 592.21/297.04 592.21/297.04 [f(x, nil())] = [1] x + [14] 592.21/297.04 > [1] x + [7] 592.21/297.04 = [g(nil(), x)] 592.21/297.04 592.21/297.04 [f(x, g(y, z))] = [1] x + [1] y + [1] z + [7] 592.21/297.04 >= [1] x + [1] y + [1] z + [7] 592.21/297.04 = [g(f(x, y), z)] 592.21/297.04 592.21/297.04 [++(x, nil())] = [1] x + [14] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [x] 592.21/297.04 592.21/297.04 [++(x, g(y, z))] = [1] x + [1] y + [1] z + [7] 592.21/297.04 >= [1] x + [1] y + [1] z + [7] 592.21/297.04 = [g(++(x, y), z)] 592.21/297.04 592.21/297.04 [null(nil())] = [12] 592.21/297.04 > [4] 592.21/297.04 = [true()] 592.21/297.04 592.21/297.04 [null(g(x, y))] = [1] x + [1] y + [5] 592.21/297.04 >= [5] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(x, max(x))] = [2] x + [14] 592.21/297.04 > [1] x + [12] 592.21/297.04 = [not(null(x))] 592.21/297.04 592.21/297.04 [mem(nil(), y)] = [1] y + [14] 592.21/297.04 > [5] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [7] 592.21/297.04 ? [1] x + [1] y + [1] z + [13] 592.21/297.04 = [or(=(y, z), mem(x, z))] 592.21/297.04 592.21/297.04 [max(g(g(nil(), x), y))] = [1] x + [1] y + [14] 592.21/297.04 > [1] x + [1] y + [7] 592.21/297.04 = [max'(x, y)] 592.21/297.04 592.21/297.04 [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [7] 592.21/297.04 ? [1] x + [1] y + [1] z + [14] 592.21/297.04 = [max'(max(g(g(x, y), z)), u())] 592.21/297.04 592.21/297.04 592.21/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(n^1)). 592.21/297.04 592.21/297.04 Strict Trs: 592.21/297.04 { f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, g(y, z)) -> g(++(x, y), z) 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Weak Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , ++(x, nil()) -> x 592.21/297.04 , null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 The weightgap principle applies (using the following nonconstant 592.21/297.04 growth matrix-interpretation) 592.21/297.04 592.21/297.04 The following argument positions are usable: 592.21/297.04 Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, 592.21/297.04 Uargs(max') = {1} 592.21/297.04 592.21/297.04 TcT has computed the following matrix interpretation satisfying 592.21/297.04 not(EDA) and not(IDA(1)). 592.21/297.04 592.21/297.04 [f](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [nil] = [0] 592.21/297.04 592.21/297.04 [g](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [++](x1, x2) = [1] x1 + [1] x2 + [1] 592.21/297.04 592.21/297.04 [null](x1) = [1] x1 + [1] 592.21/297.04 592.21/297.04 [true] = [1] 592.21/297.04 592.21/297.04 [false] = [1] 592.21/297.04 592.21/297.04 [mem](x1, x2) = [1] x1 + [1] x2 + [7] 592.21/297.04 592.21/297.04 [or](x1, x2) = [1] x1 + [1] x2 + [3] 592.21/297.04 592.21/297.04 [=](x1, x2) = [1] x1 + [2] 592.21/297.04 592.21/297.04 [max](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [not](x1) = [1] x1 + [6] 592.21/297.04 592.21/297.04 [max'](x1, x2) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [u] = [1] 592.21/297.04 592.21/297.04 The order satisfies the following ordering constraints: 592.21/297.04 592.21/297.04 [f(x, nil())] = [1] x + [0] 592.21/297.04 >= [1] x + [0] 592.21/297.04 = [g(nil(), x)] 592.21/297.04 592.21/297.04 [f(x, g(y, z))] = [1] x + [1] y + [1] z + [0] 592.21/297.04 >= [1] x + [1] y + [1] z + [0] 592.21/297.04 = [g(f(x, y), z)] 592.21/297.04 592.21/297.04 [++(x, nil())] = [1] x + [1] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [x] 592.21/297.04 592.21/297.04 [++(x, g(y, z))] = [1] x + [1] y + [1] z + [1] 592.21/297.04 >= [1] x + [1] y + [1] z + [1] 592.21/297.04 = [g(++(x, y), z)] 592.21/297.04 592.21/297.04 [null(nil())] = [1] 592.21/297.04 >= [1] 592.21/297.04 = [true()] 592.21/297.04 592.21/297.04 [null(g(x, y))] = [1] x + [1] y + [1] 592.21/297.04 >= [1] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(x, max(x))] = [2] x + [7] 592.21/297.04 >= [1] x + [7] 592.21/297.04 = [not(null(x))] 592.21/297.04 592.21/297.04 [mem(nil(), y)] = [1] y + [7] 592.21/297.04 > [1] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [7] 592.21/297.04 ? [1] x + [1] y + [1] z + [12] 592.21/297.04 = [or(=(y, z), mem(x, z))] 592.21/297.04 592.21/297.04 [max(g(g(nil(), x), y))] = [1] x + [1] y + [0] 592.21/297.04 >= [1] x + [0] 592.21/297.04 = [max'(x, y)] 592.21/297.04 592.21/297.04 [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [1] 592.21/297.04 > [1] x + [1] y + [1] z + [0] 592.21/297.04 = [max'(max(g(g(x, y), z)), u())] 592.21/297.04 592.21/297.04 592.21/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(n^1)). 592.21/297.04 592.21/297.04 Strict Trs: 592.21/297.04 { f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, g(y, z)) -> g(++(x, y), z) 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) } 592.21/297.04 Weak Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , ++(x, nil()) -> x 592.21/297.04 , null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 The weightgap principle applies (using the following nonconstant 592.21/297.04 growth matrix-interpretation) 592.21/297.04 592.21/297.04 The following argument positions are usable: 592.21/297.04 Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, 592.21/297.04 Uargs(max') = {1} 592.21/297.04 592.21/297.04 TcT has computed the following matrix interpretation satisfying 592.21/297.04 not(EDA) and not(IDA(1)). 592.21/297.04 592.21/297.04 [f](x1, x2) = [1] x1 + [1] x2 + [4] 592.21/297.04 592.21/297.04 [nil] = [4] 592.21/297.04 592.21/297.04 [g](x1, x2) = [1] x1 + [1] x2 + [1] 592.21/297.04 592.21/297.04 [++](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [null](x1) = [1] x1 + [1] 592.21/297.04 592.21/297.04 [true] = [5] 592.21/297.04 592.21/297.04 [false] = [1] 592.21/297.04 592.21/297.04 [mem](x1, x2) = [1] x1 + [1] x2 + [3] 592.21/297.04 592.21/297.04 [or](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [=](x1, x2) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [max](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [not](x1) = [1] x1 + [2] 592.21/297.04 592.21/297.04 [max'](x1, x2) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [u] = [6] 592.21/297.04 592.21/297.04 The order satisfies the following ordering constraints: 592.21/297.04 592.21/297.04 [f(x, nil())] = [1] x + [8] 592.21/297.04 > [1] x + [5] 592.21/297.04 = [g(nil(), x)] 592.21/297.04 592.21/297.04 [f(x, g(y, z))] = [1] x + [1] y + [1] z + [5] 592.21/297.04 >= [1] x + [1] y + [1] z + [5] 592.21/297.04 = [g(f(x, y), z)] 592.21/297.04 592.21/297.04 [++(x, nil())] = [1] x + [4] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [x] 592.21/297.04 592.21/297.04 [++(x, g(y, z))] = [1] x + [1] y + [1] z + [1] 592.21/297.04 >= [1] x + [1] y + [1] z + [1] 592.21/297.04 = [g(++(x, y), z)] 592.21/297.04 592.21/297.04 [null(nil())] = [5] 592.21/297.04 >= [5] 592.21/297.04 = [true()] 592.21/297.04 592.21/297.04 [null(g(x, y))] = [1] x + [1] y + [2] 592.21/297.04 > [1] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(x, max(x))] = [2] x + [3] 592.21/297.04 >= [1] x + [3] 592.21/297.04 = [not(null(x))] 592.21/297.04 592.21/297.04 [mem(nil(), y)] = [1] y + [7] 592.21/297.04 > [1] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(g(x, y), z)] = [1] x + [1] y + [1] z + [4] 592.21/297.04 > [1] x + [1] y + [1] z + [3] 592.21/297.04 = [or(=(y, z), mem(x, z))] 592.21/297.04 592.21/297.04 [max(g(g(nil(), x), y))] = [1] x + [1] y + [6] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [max'(x, y)] 592.21/297.04 592.21/297.04 [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [9] 592.21/297.04 > [1] x + [1] y + [1] z + [2] 592.21/297.04 = [max'(max(g(g(x, y), z)), u())] 592.21/297.04 592.21/297.04 592.21/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(n^1)). 592.21/297.04 592.21/297.04 Strict Trs: 592.21/297.04 { f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, g(y, z)) -> g(++(x, y), z) } 592.21/297.04 Weak Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , ++(x, nil()) -> x 592.21/297.04 , null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 We use the processor 'matrix interpretation of dimension 1' to 592.21/297.04 orient following rules strictly. 592.21/297.04 592.21/297.04 Trs: { f(x, g(y, z)) -> g(f(x, y), z) } 592.21/297.04 592.21/297.04 The induced complexity on above rules (modulo remaining rules) is 592.21/297.04 YES(?,O(n^1)) . These rules are moved into the corresponding weak 592.21/297.04 component(s). 592.21/297.04 592.21/297.04 Sub-proof: 592.21/297.04 ---------- 592.21/297.04 The following argument positions are usable: 592.21/297.04 Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, 592.21/297.04 Uargs(max') = {1} 592.21/297.04 592.21/297.04 TcT has computed the following constructor-based matrix 592.21/297.04 interpretation satisfying not(EDA). 592.21/297.04 592.21/297.04 [f](x1, x2) = [7] x1 + [2] x2 + [0] 592.21/297.04 592.21/297.04 [nil] = [4] 592.21/297.04 592.21/297.04 [g](x1, x2) = [1] x1 + [1] x2 + [4] 592.21/297.04 592.21/297.04 [++](x1, x2) = [7] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [null](x1) = [0] 592.21/297.04 592.21/297.04 [true] = [0] 592.21/297.04 592.21/297.04 [false] = [0] 592.21/297.04 592.21/297.04 [mem](x1, x2) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [or](x1, x2) = [1] x1 + [1] x2 + [1] 592.21/297.04 592.21/297.04 [=](x1, x2) = [1] x1 + [1] 592.21/297.04 592.21/297.04 [max](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [not](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [max'](x1, x2) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [u] = [0] 592.21/297.04 592.21/297.04 The order satisfies the following ordering constraints: 592.21/297.04 592.21/297.04 [f(x, nil())] = [7] x + [8] 592.21/297.04 >= [1] x + [8] 592.21/297.04 = [g(nil(), x)] 592.21/297.04 592.21/297.04 [f(x, g(y, z))] = [7] x + [2] y + [2] z + [8] 592.21/297.04 > [7] x + [2] y + [1] z + [4] 592.21/297.04 = [g(f(x, y), z)] 592.21/297.04 592.21/297.04 [++(x, nil())] = [7] x + [4] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [x] 592.21/297.04 592.21/297.04 [++(x, g(y, z))] = [7] x + [1] y + [1] z + [4] 592.21/297.04 >= [7] x + [1] y + [1] z + [4] 592.21/297.04 = [g(++(x, y), z)] 592.21/297.04 592.21/297.04 [null(nil())] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [true()] 592.21/297.04 592.21/297.04 [null(g(x, y))] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(x, max(x))] = [1] x + [0] 592.21/297.04 >= [0] 592.21/297.04 = [not(null(x))] 592.21/297.04 592.21/297.04 [mem(nil(), y)] = [4] 592.21/297.04 > [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(g(x, y), z)] = [1] x + [1] y + [4] 592.21/297.04 > [1] x + [1] y + [2] 592.21/297.04 = [or(=(y, z), mem(x, z))] 592.21/297.04 592.21/297.04 [max(g(g(nil(), x), y))] = [1] x + [1] y + [12] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [max'(x, y)] 592.21/297.04 592.21/297.04 [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [12] 592.21/297.04 > [1] x + [1] y + [1] z + [8] 592.21/297.04 = [max'(max(g(g(x, y), z)), u())] 592.21/297.04 592.21/297.04 592.21/297.04 We return to the main proof. 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(n^1)). 592.21/297.04 592.21/297.04 Strict Trs: { ++(x, g(y, z)) -> g(++(x, y), z) } 592.21/297.04 Weak Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, nil()) -> x 592.21/297.04 , null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(n^1)) 592.21/297.04 592.21/297.04 We use the processor 'matrix interpretation of dimension 1' to 592.21/297.04 orient following rules strictly. 592.21/297.04 592.21/297.04 Trs: { ++(x, g(y, z)) -> g(++(x, y), z) } 592.21/297.04 592.21/297.04 The induced complexity on above rules (modulo remaining rules) is 592.21/297.04 YES(?,O(n^1)) . These rules are moved into the corresponding weak 592.21/297.04 component(s). 592.21/297.04 592.21/297.04 Sub-proof: 592.21/297.04 ---------- 592.21/297.04 The following argument positions are usable: 592.21/297.04 Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1}, 592.21/297.04 Uargs(max') = {1} 592.21/297.04 592.21/297.04 TcT has computed the following constructor-based matrix 592.21/297.04 interpretation satisfying not(EDA). 592.21/297.04 592.21/297.04 [f](x1, x2) = [7] x1 + [3] x2 + [0] 592.21/297.04 592.21/297.04 [nil] = [4] 592.21/297.04 592.21/297.04 [g](x1, x2) = [1] x1 + [1] x2 + [3] 592.21/297.04 592.21/297.04 [++](x1, x2) = [7] x1 + [3] x2 + [0] 592.21/297.04 592.21/297.04 [null](x1) = [0] 592.21/297.04 592.21/297.04 [true] = [0] 592.21/297.04 592.21/297.04 [false] = [0] 592.21/297.04 592.21/297.04 [mem](x1, x2) = [0] 592.21/297.04 592.21/297.04 [or](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [=](x1, x2) = [0] 592.21/297.04 592.21/297.04 [max](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [not](x1) = [1] x1 + [0] 592.21/297.04 592.21/297.04 [max'](x1, x2) = [1] x1 + [1] x2 + [0] 592.21/297.04 592.21/297.04 [u] = [2] 592.21/297.04 592.21/297.04 The order satisfies the following ordering constraints: 592.21/297.04 592.21/297.04 [f(x, nil())] = [7] x + [12] 592.21/297.04 > [1] x + [7] 592.21/297.04 = [g(nil(), x)] 592.21/297.04 592.21/297.04 [f(x, g(y, z))] = [7] x + [3] y + [3] z + [9] 592.21/297.04 > [7] x + [3] y + [1] z + [3] 592.21/297.04 = [g(f(x, y), z)] 592.21/297.04 592.21/297.04 [++(x, nil())] = [7] x + [12] 592.21/297.04 > [1] x + [0] 592.21/297.04 = [x] 592.21/297.04 592.21/297.04 [++(x, g(y, z))] = [7] x + [3] y + [3] z + [9] 592.21/297.04 > [7] x + [3] y + [1] z + [3] 592.21/297.04 = [g(++(x, y), z)] 592.21/297.04 592.21/297.04 [null(nil())] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [true()] 592.21/297.04 592.21/297.04 [null(g(x, y))] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(x, max(x))] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [not(null(x))] 592.21/297.04 592.21/297.04 [mem(nil(), y)] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [false()] 592.21/297.04 592.21/297.04 [mem(g(x, y), z)] = [0] 592.21/297.04 >= [0] 592.21/297.04 = [or(=(y, z), mem(x, z))] 592.21/297.04 592.21/297.04 [max(g(g(nil(), x), y))] = [1] x + [1] y + [10] 592.21/297.04 > [1] x + [1] y + [0] 592.21/297.04 = [max'(x, y)] 592.21/297.04 592.21/297.04 [max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [11] 592.21/297.04 > [1] x + [1] y + [1] z + [8] 592.21/297.04 = [max'(max(g(g(x, y), z)), u())] 592.21/297.04 592.21/297.04 592.21/297.04 We return to the main proof. 592.21/297.04 592.21/297.04 We are left with following problem, upon which TcT provides the 592.21/297.04 certificate YES(O(1),O(1)). 592.21/297.04 592.21/297.04 Weak Trs: 592.21/297.04 { f(x, nil()) -> g(nil(), x) 592.21/297.04 , f(x, g(y, z)) -> g(f(x, y), z) 592.21/297.04 , ++(x, nil()) -> x 592.21/297.04 , ++(x, g(y, z)) -> g(++(x, y), z) 592.21/297.04 , null(nil()) -> true() 592.21/297.04 , null(g(x, y)) -> false() 592.21/297.04 , mem(x, max(x)) -> not(null(x)) 592.21/297.04 , mem(nil(), y) -> false() 592.21/297.04 , mem(g(x, y), z) -> or(=(y, z), mem(x, z)) 592.21/297.04 , max(g(g(nil(), x), y)) -> max'(x, y) 592.21/297.04 , max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) } 592.21/297.04 Obligation: 592.21/297.04 runtime complexity 592.21/297.04 Answer: 592.21/297.04 YES(O(1),O(1)) 592.21/297.04 592.21/297.04 Empty rules are trivially bounded 592.21/297.04 592.21/297.04 Hurray, we answered YES(O(1),O(n^1)) 592.54/297.32 EOF