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