YES(O(1),O(n^2)) 456.97/148.06 YES(O(1),O(n^2)) 456.97/148.06 456.97/148.06 We are left with following problem, upon which TcT provides the 456.97/148.06 certificate YES(O(1),O(n^2)). 456.97/148.06 456.97/148.06 Strict Trs: 456.97/148.06 { max(L(x)) -> x 456.97/148.06 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.06 , max(N(L(0()), L(y))) -> y 456.97/148.06 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.06 Obligation: 456.97/148.06 runtime complexity 456.97/148.06 Answer: 456.97/148.06 YES(O(1),O(n^2)) 456.97/148.06 456.97/148.06 The input is overlay and right-linear. Switching to innermost 456.97/148.06 rewriting. 456.97/148.06 456.97/148.06 We are left with following problem, upon which TcT provides the 456.97/148.06 certificate YES(O(1),O(n^2)). 456.97/148.06 456.97/148.06 Strict Trs: 456.97/148.06 { max(L(x)) -> x 456.97/148.06 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.06 , max(N(L(0()), L(y))) -> y 456.97/148.06 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.06 Obligation: 456.97/148.06 innermost runtime complexity 456.97/148.06 Answer: 456.97/148.06 YES(O(1),O(n^2)) 456.97/148.06 456.97/148.06 We add the following dependency tuples: 456.97/148.06 456.97/148.06 Strict DPs: 456.97/148.06 { max^#(L(x)) -> c_1() 456.97/148.06 , max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) 456.97/148.06 , max^#(N(L(0()), L(y))) -> c_3() 456.97/148.06 , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.06 456.97/148.06 and mark the set of starting terms. 456.97/148.06 456.97/148.06 We are left with following problem, upon which TcT provides the 456.97/148.06 certificate YES(O(1),O(n^2)). 456.97/148.06 456.97/148.06 Strict DPs: 456.97/148.06 { max^#(L(x)) -> c_1() 456.97/148.06 , max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) 456.97/148.06 , max^#(N(L(0()), L(y))) -> c_3() 456.97/148.06 , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.06 Weak Trs: 456.97/148.06 { max(L(x)) -> x 456.97/148.06 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.06 , max(N(L(0()), L(y))) -> y 456.97/148.06 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.06 Obligation: 456.97/148.06 innermost runtime complexity 456.97/148.06 Answer: 456.97/148.06 YES(O(1),O(n^2)) 456.97/148.06 456.97/148.06 We estimate the number of application of {1,3} by applications of 456.97/148.06 Pre({1,3}) = {2,4}. Here rules are labeled as follows: 456.97/148.06 456.97/148.06 DPs: 456.97/148.06 { 1: max^#(L(x)) -> c_1() 456.97/148.06 , 2: max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) 456.97/148.06 , 3: max^#(N(L(0()), L(y))) -> c_3() 456.97/148.06 , 4: max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.06 456.97/148.06 We are left with following problem, upon which TcT provides the 456.97/148.06 certificate YES(O(1),O(n^2)). 456.97/148.06 456.97/148.06 Strict DPs: 456.97/148.06 { max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) 456.97/148.06 , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.06 Weak DPs: 456.97/148.06 { max^#(L(x)) -> c_1() 456.97/148.06 , max^#(N(L(0()), L(y))) -> c_3() } 456.97/148.06 Weak Trs: 456.97/148.06 { max(L(x)) -> x 456.97/148.06 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.06 , max(N(L(0()), L(y))) -> y 456.97/148.06 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.06 Obligation: 456.97/148.06 innermost runtime complexity 456.97/148.06 Answer: 456.97/148.06 YES(O(1),O(n^2)) 456.97/148.06 456.97/148.06 The following weak DPs constitute a sub-graph of the DG that is 456.97/148.06 closed under successors. The DPs are removed. 456.97/148.06 456.97/148.06 { max^#(L(x)) -> c_1() 456.97/148.06 , max^#(N(L(0()), L(y))) -> c_3() } 456.97/148.06 456.97/148.06 We are left with following problem, upon which TcT provides the 456.97/148.06 certificate YES(O(1),O(n^2)). 456.97/148.06 456.97/148.06 Strict DPs: 456.97/148.06 { max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) 456.97/148.06 , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.06 Weak Trs: 456.97/148.06 { max(L(x)) -> x 456.97/148.06 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.06 , max(N(L(0()), L(y))) -> y 456.97/148.06 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.06 Obligation: 456.97/148.06 innermost runtime complexity 456.97/148.06 Answer: 456.97/148.06 YES(O(1),O(n^2)) 456.97/148.06 456.97/148.06 We decompose the input problem according to the dependency graph 456.97/148.06 into the upper component 456.97/148.06 456.97/148.06 { max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) } 456.97/148.06 456.97/148.06 and lower component 456.97/148.06 456.97/148.06 { max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.06 456.97/148.06 Further, following extension rules are added to the lower 456.97/148.06 component. 456.97/148.06 456.97/148.06 { max^#(N(L(x), N(y, z))) -> max^#(N(y, z)) 456.97/148.06 , max^#(N(L(x), N(y, z))) -> max^#(N(L(x), L(max(N(y, z))))) } 456.97/148.06 456.97/148.06 TcT solves the upper component with certificate YES(O(1),O(n^1)). 456.97/148.06 456.97/148.06 Sub-proof: 456.97/148.06 ---------- 456.97/148.06 We are left with following problem, upon which TcT provides the 456.97/148.06 certificate YES(O(1),O(n^1)). 456.97/148.06 456.97/148.06 Strict DPs: 456.97/148.06 { max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) } 456.97/148.06 Weak Trs: 456.97/148.06 { max(L(x)) -> x 456.97/148.06 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.06 , max(N(L(0()), L(y))) -> y 456.97/148.06 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.06 Obligation: 456.97/148.06 innermost runtime complexity 456.97/148.06 Answer: 456.97/148.06 YES(O(1),O(n^1)) 456.97/148.06 456.97/148.06 We use the processor 'matrix interpretation of dimension 2' to 456.97/148.06 orient following rules strictly. 456.97/148.06 456.97/148.06 DPs: 456.97/148.06 { 1: max^#(N(L(x), N(y, z))) -> 456.97/148.06 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) } 456.97/148.06 456.97/148.06 Sub-proof: 456.97/148.06 ---------- 456.97/148.06 The following argument positions are usable: 456.97/148.06 Uargs(c_2) = {1, 2} 456.97/148.06 456.97/148.06 TcT has computed the following constructor-based matrix 456.97/148.06 interpretation satisfying not(EDA) and not(IDA(1)). 456.97/148.06 456.97/148.06 [max](x1) = [0] 456.97/148.06 [0] 456.97/148.06 456.97/148.06 [L](x1) = [0] 456.97/148.06 [0] 456.97/148.06 456.97/148.06 [N](x1, x2) = [1 0] x2 + [4] 456.97/148.06 [1 0] [0] 456.97/148.06 456.97/148.06 [0] = [0] 456.97/148.06 [0] 456.97/148.06 456.97/148.06 [s](x1) = [0] 456.97/148.06 [0] 456.97/148.06 456.97/148.06 [max^#](x1) = [0 2] x1 + [0] 456.97/148.06 [0 0] [0] 456.97/148.06 456.97/148.06 [c_2](x1, x2) = [4 0] x1 + [1 0] x2 + [5] 456.97/148.06 [0 0] [0 0] [0] 456.97/148.06 456.97/148.06 The order satisfies the following ordering constraints: 456.97/148.06 456.97/148.06 [max(L(x))] = [0] 456.97/148.06 [0] 456.97/148.06 ? [1 0] x + [0] 456.97/148.06 [0 1] [0] 456.97/148.06 = [x] 456.97/148.06 456.97/148.06 [max(N(L(x), N(y, z)))] = [0] 456.97/148.06 [0] 456.97/148.06 >= [0] 456.97/148.06 [0] 456.97/148.06 = [max(N(L(x), L(max(N(y, z)))))] 456.97/148.06 456.97/148.06 [max(N(L(0()), L(y)))] = [0] 456.97/148.06 [0] 456.97/148.06 ? [1 0] y + [0] 456.97/148.06 [0 1] [0] 456.97/148.06 = [y] 456.97/148.06 456.97/148.06 [max(N(L(s(x)), L(s(y))))] = [0] 456.97/148.06 [0] 456.97/148.06 >= [0] 456.97/148.06 [0] 456.97/148.06 = [s(max(N(L(x), L(y))))] 456.97/148.06 456.97/148.06 [max^#(N(L(x), N(y, z)))] = [2 0] z + [8] 456.97/148.06 [0 0] [0] 456.97/148.06 > [2 0] z + [5] 456.97/148.07 [0 0] [0] 456.97/148.07 = [c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z)))] 456.97/148.07 456.97/148.07 456.97/148.07 The strictly oriented rules are moved into the weak component. 456.97/148.07 456.97/148.07 We are left with following problem, upon which TcT provides the 456.97/148.07 certificate YES(O(1),O(1)). 456.97/148.07 456.97/148.07 Weak DPs: 456.97/148.07 { max^#(N(L(x), N(y, z))) -> 456.97/148.07 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) } 456.97/148.07 Weak Trs: 456.97/148.07 { max(L(x)) -> x 456.97/148.07 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.07 , max(N(L(0()), L(y))) -> y 456.97/148.07 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.07 Obligation: 456.97/148.07 innermost runtime complexity 456.97/148.07 Answer: 456.97/148.07 YES(O(1),O(1)) 456.97/148.07 456.97/148.07 The following weak DPs constitute a sub-graph of the DG that is 456.97/148.07 closed under successors. The DPs are removed. 456.97/148.07 456.97/148.07 { max^#(N(L(x), N(y, z))) -> 456.97/148.07 c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) } 456.97/148.07 456.97/148.07 We are left with following problem, upon which TcT provides the 456.97/148.07 certificate YES(O(1),O(1)). 456.97/148.07 456.97/148.07 Weak Trs: 456.97/148.07 { max(L(x)) -> x 456.97/148.07 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.07 , max(N(L(0()), L(y))) -> y 456.97/148.07 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.07 Obligation: 456.97/148.07 innermost runtime complexity 456.97/148.07 Answer: 456.97/148.07 YES(O(1),O(1)) 456.97/148.07 456.97/148.07 No rule is usable, rules are removed from the input problem. 456.97/148.07 456.97/148.07 We are left with following problem, upon which TcT provides the 456.97/148.07 certificate YES(O(1),O(1)). 456.97/148.07 456.97/148.07 Rules: Empty 456.97/148.07 Obligation: 456.97/148.07 innermost runtime complexity 456.97/148.07 Answer: 456.97/148.07 YES(O(1),O(1)) 456.97/148.07 456.97/148.07 Empty rules are trivially bounded 456.97/148.07 456.97/148.07 We return to the main proof. 456.97/148.07 456.97/148.07 We are left with following problem, upon which TcT provides the 456.97/148.07 certificate YES(O(1),O(n^1)). 456.97/148.07 456.97/148.07 Strict DPs: 456.97/148.07 { max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.07 Weak DPs: 456.97/148.07 { max^#(N(L(x), N(y, z))) -> max^#(N(y, z)) 456.97/148.07 , max^#(N(L(x), N(y, z))) -> max^#(N(L(x), L(max(N(y, z))))) } 456.97/148.07 Weak Trs: 456.97/148.07 { max(L(x)) -> x 456.97/148.07 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.07 , max(N(L(0()), L(y))) -> y 456.97/148.07 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.07 Obligation: 456.97/148.07 innermost runtime complexity 456.97/148.07 Answer: 456.97/148.07 YES(O(1),O(n^1)) 456.97/148.07 456.97/148.07 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 456.97/148.07 to orient following rules strictly. 456.97/148.07 456.97/148.07 DPs: 456.97/148.07 { 1: max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) 456.97/148.07 , 2: max^#(N(L(x), N(y, z))) -> max^#(N(y, z)) } 456.97/148.07 Trs: { max(N(L(0()), L(y))) -> y } 456.97/148.07 456.97/148.07 Sub-proof: 456.97/148.07 ---------- 456.97/148.07 The input was oriented with the instance of 'Small Polynomial Path 456.97/148.07 Order (PS,1-bounded)' as induced by the safe mapping 456.97/148.07 456.97/148.07 safe(max) = {}, safe(L) = {1}, safe(N) = {1, 2}, safe(0) = {}, 456.97/148.07 safe(s) = {1}, safe(max^#) = {}, safe(c_4) = {} 456.97/148.07 456.97/148.07 and precedence 456.97/148.07 456.97/148.07 max ~ max^# . 456.97/148.07 456.97/148.07 Following symbols are considered recursive: 456.97/148.07 456.97/148.07 {max, max^#} 456.97/148.07 456.97/148.07 The recursion depth is 1. 456.97/148.07 456.97/148.07 Further, following argument filtering is employed: 456.97/148.07 456.97/148.07 pi(max) = 1, pi(L) = 1, pi(N) = [2], pi(0) = [], pi(s) = [1], 456.97/148.07 pi(max^#) = [1], pi(c_4) = [1] 456.97/148.07 456.97/148.07 Usable defined function symbols are a subset of: 456.97/148.07 456.97/148.07 {max, max^#} 456.97/148.07 456.97/148.07 For your convenience, here are the satisfied ordering constraints: 456.97/148.07 456.97/148.07 pi(max^#(N(L(x), N(y, z)))) = max^#(N(; N(; z));) 456.97/148.07 > max^#(N(; z);) 456.97/148.07 = pi(max^#(N(y, z))) 456.97/148.07 456.97/148.07 pi(max^#(N(L(x), N(y, z)))) = max^#(N(; N(; z));) 456.97/148.07 >= max^#(N(; N(; z));) 456.97/148.07 = pi(max^#(N(L(x), L(max(N(y, z)))))) 456.97/148.07 456.97/148.07 pi(max^#(N(L(s(x)), L(s(y))))) = max^#(N(; s(; y));) 456.97/148.07 > c_4(max^#(N(; y););) 456.97/148.07 = pi(c_4(max^#(N(L(x), L(y))))) 456.97/148.07 456.97/148.07 pi(max(L(x))) = x 456.97/148.07 >= x 456.97/148.07 = pi(x) 456.97/148.07 456.97/148.07 pi(max(N(L(x), N(y, z)))) = N(; N(; z)) 456.97/148.07 >= N(; N(; z)) 456.97/148.07 = pi(max(N(L(x), L(max(N(y, z)))))) 456.97/148.07 456.97/148.07 pi(max(N(L(0()), L(y)))) = N(; y) 456.97/148.07 > y 456.97/148.07 = pi(y) 456.97/148.07 456.97/148.07 pi(max(N(L(s(x)), L(s(y))))) = N(; s(; y)) 456.97/148.07 >= s(; N(; y)) 456.97/148.07 = pi(s(max(N(L(x), L(y))))) 456.97/148.07 456.97/148.07 456.97/148.07 We return to the main proof. Consider the set of all dependency 456.97/148.07 pairs 456.97/148.07 456.97/148.07 : 456.97/148.07 { 1: max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) 456.97/148.07 , 2: max^#(N(L(x), N(y, z))) -> max^#(N(y, z)) 456.97/148.07 , 3: max^#(N(L(x), N(y, z))) -> max^#(N(L(x), L(max(N(y, z))))) } 456.97/148.07 456.97/148.07 Processor 'Small Polynomial Path Order (PS,1-bounded)' induces the 456.97/148.07 complexity certificate YES(?,O(n^1)) on application of dependency 456.97/148.07 pairs {1,2}. These cover all (indirect) predecessors of dependency 456.97/148.07 pairs {1,2,3}, their number of application is equally bounded. The 456.97/148.07 dependency pairs are shifted into the weak component. 456.97/148.07 456.97/148.07 We are left with following problem, upon which TcT provides the 456.97/148.07 certificate YES(O(1),O(1)). 456.97/148.07 456.97/148.07 Weak DPs: 456.97/148.07 { max^#(N(L(x), N(y, z))) -> max^#(N(y, z)) 456.97/148.07 , max^#(N(L(x), N(y, z))) -> max^#(N(L(x), L(max(N(y, z))))) 456.97/148.07 , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.07 Weak Trs: 456.97/148.07 { max(L(x)) -> x 456.97/148.07 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.07 , max(N(L(0()), L(y))) -> y 456.97/148.07 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.07 Obligation: 456.97/148.07 innermost runtime complexity 456.97/148.07 Answer: 456.97/148.07 YES(O(1),O(1)) 456.97/148.07 456.97/148.07 The following weak DPs constitute a sub-graph of the DG that is 456.97/148.07 closed under successors. The DPs are removed. 456.97/148.07 456.97/148.07 { max^#(N(L(x), N(y, z))) -> max^#(N(y, z)) 456.97/148.07 , max^#(N(L(x), N(y, z))) -> max^#(N(L(x), L(max(N(y, z))))) 456.97/148.07 , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } 456.97/148.07 456.97/148.07 We are left with following problem, upon which TcT provides the 456.97/148.07 certificate YES(O(1),O(1)). 456.97/148.07 456.97/148.07 Weak Trs: 456.97/148.07 { max(L(x)) -> x 456.97/148.07 , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) 456.97/148.07 , max(N(L(0()), L(y))) -> y 456.97/148.07 , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } 456.97/148.07 Obligation: 456.97/148.07 innermost runtime complexity 456.97/148.07 Answer: 456.97/148.07 YES(O(1),O(1)) 456.97/148.07 456.97/148.07 No rule is usable, rules are removed from the input problem. 456.97/148.07 456.97/148.07 We are left with following problem, upon which TcT provides the 456.97/148.07 certificate YES(O(1),O(1)). 456.97/148.07 456.97/148.07 Rules: Empty 456.97/148.07 Obligation: 456.97/148.07 innermost runtime complexity 456.97/148.07 Answer: 456.97/148.07 YES(O(1),O(1)) 456.97/148.07 456.97/148.07 Empty rules are trivially bounded 456.97/148.07 456.97/148.07 Hurray, we answered YES(O(1),O(n^2)) 457.07/148.21 EOF