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: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following innermost weak dependency pairs: Strict DPs: { f^#(x, nil()) -> c_1() , f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, nil()) -> c_3() , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , null^#(nil()) -> c_5() , null^#(g(x, y)) -> c_6() , mem^#(x, max(x)) -> c_7(null^#(x)) , mem^#(nil(), y) -> c_8() , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(nil(), x), y)) -> c_10() , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { f^#(x, nil()) -> c_1() , f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, nil()) -> c_3() , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , null^#(nil()) -> c_5() , null^#(g(x, y)) -> c_6() , mem^#(x, max(x)) -> c_7(null^#(x)) , mem^#(nil(), y) -> c_8() , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(nil(), x), y)) -> c_10() , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } 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: innermost runtime complexity Answer: YES(O(1),O(n^1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { f^#(x, nil()) -> c_1() , f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, nil()) -> c_3() , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , null^#(nil()) -> c_5() , null^#(g(x, y)) -> c_6() , mem^#(x, max(x)) -> c_7(null^#(x)) , mem^#(nil(), y) -> c_8() , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(nil(), x), y)) -> c_10() , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1}, Uargs(c_9) = {1}, Uargs(c_11) = {1} TcT has computed the following constructor-restricted matrix interpretation. [nil] = [0] [0] [g](x1, x2) = [0] [2] [max](x1) = [0] [0] [u] = [0] [0] [f^#](x1, x2) = [1 2] x1 + [0 0] x2 + [0] [1 2] [2 2] [2] [c_1] = [1] [1] [c_2](x1) = [1 0] x1 + [2] [0 1] [0] [++^#](x1, x2) = [2 2] x1 + [0 0] x2 + [0] [2 1] [2 2] [1] [c_3] = [1] [1] [c_4](x1) = [1 0] x1 + [2] [0 1] [0] [null^#](x1) = [0] [0] [c_5] = [1] [0] [c_6] = [2] [0] [mem^#](x1, x2) = [0] [0] [c_7](x1) = [1 0] x1 + [2] [0 1] [0] [c_8] = [1] [0] [c_9](x1) = [1 0] x1 + [2] [0 1] [0] [max^#](x1) = [0 2] x1 + [0] [0 0] [0] [c_10] = [1] [0] [c_11](x1) = [1 0] x1 + [1] [0 1] [0] The following symbols are considered usable {f^#, ++^#, null^#, mem^#, max^#} The order satisfies the following ordering constraints: [f^#(x, nil())] = [1 2] x + [0] [1 2] [2] ? [1] [1] = [c_1()] [f^#(x, g(y, z))] = [1 2] x + [0] [1 2] [6] ? [1 2] x + [0 0] y + [2] [1 2] [2 2] [2] = [c_2(f^#(x, y))] [++^#(x, nil())] = [2 2] x + [0] [2 1] [1] ? [1] [1] = [c_3()] [++^#(x, g(y, z))] = [2 2] x + [0] [2 1] [5] ? [2 2] x + [0 0] y + [2] [2 1] [2 2] [1] = [c_4(++^#(x, y))] [null^#(nil())] = [0] [0] ? [1] [0] = [c_5()] [null^#(g(x, y))] = [0] [0] ? [2] [0] = [c_6()] [mem^#(x, max(x))] = [0] [0] ? [2] [0] = [c_7(null^#(x))] [mem^#(nil(), y)] = [0] [0] ? [1] [0] = [c_8()] [mem^#(g(x, y), z)] = [0] [0] ? [2] [0] = [c_9(mem^#(x, z))] [max^#(g(g(nil(), x), y))] = [4] [0] > [1] [0] = [c_10()] [max^#(g(g(g(x, y), z), u()))] = [4] [0] ? [5] [0] = [c_11(max^#(g(g(x, y), z)))] 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 DPs: { f^#(x, nil()) -> c_1() , f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, nil()) -> c_3() , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , null^#(nil()) -> c_5() , null^#(g(x, y)) -> c_6() , mem^#(x, max(x)) -> c_7(null^#(x)) , mem^#(nil(), y) -> c_8() , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } Weak DPs: { max^#(g(g(nil(), x), y)) -> c_10() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {1,3,5,6,8} by applications of Pre({1,3,5,6,8}) = {2,4,7,9}. Here rules are labeled as follows: DPs: { 1: f^#(x, nil()) -> c_1() , 2: f^#(x, g(y, z)) -> c_2(f^#(x, y)) , 3: ++^#(x, nil()) -> c_3() , 4: ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , 5: null^#(nil()) -> c_5() , 6: null^#(g(x, y)) -> c_6() , 7: mem^#(x, max(x)) -> c_7(null^#(x)) , 8: mem^#(nil(), y) -> c_8() , 9: mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , 10: max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) , 11: max^#(g(g(nil(), x), y)) -> c_10() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , mem^#(x, max(x)) -> c_7(null^#(x)) , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } Weak DPs: { f^#(x, nil()) -> c_1() , ++^#(x, nil()) -> c_3() , null^#(nil()) -> c_5() , null^#(g(x, y)) -> c_6() , mem^#(nil(), y) -> c_8() , max^#(g(g(nil(), x), y)) -> c_10() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3} by applications of Pre({3}) = {4}. Here rules are labeled as follows: DPs: { 1: f^#(x, g(y, z)) -> c_2(f^#(x, y)) , 2: ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , 3: mem^#(x, max(x)) -> c_7(null^#(x)) , 4: mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , 5: max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) , 6: f^#(x, nil()) -> c_1() , 7: ++^#(x, nil()) -> c_3() , 8: null^#(nil()) -> c_5() , 9: null^#(g(x, y)) -> c_6() , 10: mem^#(nil(), y) -> c_8() , 11: max^#(g(g(nil(), x), y)) -> c_10() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } Weak DPs: { f^#(x, nil()) -> c_1() , ++^#(x, nil()) -> c_3() , null^#(nil()) -> c_5() , null^#(g(x, y)) -> c_6() , mem^#(x, max(x)) -> c_7(null^#(x)) , mem^#(nil(), y) -> c_8() , max^#(g(g(nil(), x), y)) -> c_10() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f^#(x, nil()) -> c_1() , ++^#(x, nil()) -> c_3() , null^#(nil()) -> c_5() , null^#(g(x, y)) -> c_6() , mem^#(x, max(x)) -> c_7(null^#(x)) , mem^#(nil(), y) -> c_8() , max^#(g(g(nil(), x), y)) -> c_10() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: f^#(x, g(y, z)) -> c_2(f^#(x, y)) , 2: ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , 3: mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , 4: max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(f) = {}, safe(nil) = {}, safe(g) = {1, 2}, safe(++) = {}, safe(null) = {}, safe(true) = {}, safe(false) = {}, safe(mem) = {}, safe(or) = {1, 2}, safe(=) = {1, 2}, safe(max) = {}, safe(not) = {1}, safe(max') = {1, 2}, safe(u) = {}, safe(f^#) = {1}, safe(c_1) = {}, safe(c_2) = {}, safe(++^#) = {1}, safe(c_3) = {}, safe(c_4) = {}, safe(null^#) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(mem^#) = {2}, safe(c_7) = {}, safe(c_8) = {}, safe(c_9) = {}, safe(max^#) = {}, safe(c_10) = {}, safe(c_11) = {} and precedence ++^# ~ mem^#, ++^# ~ max^#, mem^# ~ max^# . Following symbols are considered recursive: {f^#, ++^#, mem^#, max^#} The recursion depth is 1. Further, following argument filtering is employed: pi(f) = [], pi(nil) = [], pi(g) = [1], pi(++) = [], pi(null) = [], pi(true) = [], pi(false) = [], pi(mem) = [], pi(or) = [], pi(=) = [], pi(max) = [], pi(not) = [], pi(max') = [], pi(u) = [], pi(f^#) = [2], pi(c_1) = [], pi(c_2) = [1], pi(++^#) = [2], pi(c_3) = [], pi(c_4) = [1], pi(null^#) = [], pi(c_5) = [], pi(c_6) = [], pi(mem^#) = [1], pi(c_7) = [], pi(c_8) = [], pi(c_9) = [1], pi(max^#) = [1], pi(c_10) = [], pi(c_11) = [1] Usable defined function symbols are a subset of: {f^#, ++^#, null^#, mem^#, max^#} For your convenience, here are the satisfied ordering constraints: pi(f^#(x, g(y, z))) = f^#(g(; y);) > c_2(f^#(y;);) = pi(c_2(f^#(x, y))) pi(++^#(x, g(y, z))) = ++^#(g(; y);) > c_4(++^#(y;);) = pi(c_4(++^#(x, y))) pi(mem^#(g(x, y), z)) = mem^#(g(; x);) > c_9(mem^#(x;);) = pi(c_9(mem^#(x, z))) pi(max^#(g(g(g(x, y), z), u()))) = max^#(g(; g(; g(; x)));) > c_11(max^#(g(; g(; x)););) = pi(c_11(max^#(g(g(x, y), z)))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f^#(x, g(y, z)) -> c_2(f^#(x, y)) , ++^#(x, g(y, z)) -> c_4(++^#(x, y)) , mem^#(g(x, y), z) -> c_9(mem^#(x, z)) , max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))