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