YES(O(1),O(n^2)) 404.63/148.03 YES(O(1),O(n^2)) 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^2)). 404.63/148.03 404.63/148.03 Strict Trs: 404.63/148.03 { f(0()) -> true() 404.63/148.03 , f(1()) -> false() 404.63/148.03 , f(s(x)) -> f(x) 404.63/148.03 , if(true(), s(x), s(y)) -> s(x) 404.63/148.03 , if(false(), s(x), s(y)) -> s(y) 404.63/148.03 , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) 404.63/148.03 , g(x, c(y)) -> c(g(x, y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^2)) 404.63/148.03 404.63/148.03 We add the following dependency tuples: 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { f^#(0()) -> c_1() 404.63/148.03 , f^#(1()) -> c_2() 404.63/148.03 , f^#(s(x)) -> c_3(f^#(x)) 404.63/148.03 , if^#(true(), s(x), s(y)) -> c_4() 404.63/148.03 , if^#(false(), s(x), s(y)) -> c_5() 404.63/148.03 , g^#(x, c(y)) -> 404.63/148.03 c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), 404.63/148.03 if^#(f(x), c(g(s(x), y)), c(y)), 404.63/148.03 f^#(x), 404.63/148.03 g^#(s(x), y)) 404.63/148.03 , g^#(x, c(y)) -> c_7(g^#(x, y)) } 404.63/148.03 404.63/148.03 and mark the set of starting terms. 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^2)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { f^#(0()) -> c_1() 404.63/148.03 , f^#(1()) -> c_2() 404.63/148.03 , f^#(s(x)) -> c_3(f^#(x)) 404.63/148.03 , if^#(true(), s(x), s(y)) -> c_4() 404.63/148.03 , if^#(false(), s(x), s(y)) -> c_5() 404.63/148.03 , g^#(x, c(y)) -> 404.63/148.03 c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), 404.63/148.03 if^#(f(x), c(g(s(x), y)), c(y)), 404.63/148.03 f^#(x), 404.63/148.03 g^#(s(x), y)) 404.63/148.03 , g^#(x, c(y)) -> c_7(g^#(x, y)) } 404.63/148.03 Weak Trs: 404.63/148.03 { f(0()) -> true() 404.63/148.03 , f(1()) -> false() 404.63/148.03 , f(s(x)) -> f(x) 404.63/148.03 , if(true(), s(x), s(y)) -> s(x) 404.63/148.03 , if(false(), s(x), s(y)) -> s(y) 404.63/148.03 , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) 404.63/148.03 , g(x, c(y)) -> c(g(x, y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^2)) 404.63/148.03 404.63/148.03 We estimate the number of application of {1,2,4,5} by applications 404.63/148.03 of Pre({1,2,4,5}) = {3,6}. Here rules are labeled as follows: 404.63/148.03 404.63/148.03 DPs: 404.63/148.03 { 1: f^#(0()) -> c_1() 404.63/148.03 , 2: f^#(1()) -> c_2() 404.63/148.03 , 3: f^#(s(x)) -> c_3(f^#(x)) 404.63/148.03 , 4: if^#(true(), s(x), s(y)) -> c_4() 404.63/148.03 , 5: if^#(false(), s(x), s(y)) -> c_5() 404.63/148.03 , 6: g^#(x, c(y)) -> 404.63/148.03 c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), 404.63/148.03 if^#(f(x), c(g(s(x), y)), c(y)), 404.63/148.03 f^#(x), 404.63/148.03 g^#(s(x), y)) 404.63/148.03 , 7: g^#(x, c(y)) -> c_7(g^#(x, y)) } 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^2)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { f^#(s(x)) -> c_3(f^#(x)) 404.63/148.03 , g^#(x, c(y)) -> 404.63/148.03 c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), 404.63/148.03 if^#(f(x), c(g(s(x), y)), c(y)), 404.63/148.03 f^#(x), 404.63/148.03 g^#(s(x), y)) 404.63/148.03 , g^#(x, c(y)) -> c_7(g^#(x, y)) } 404.63/148.03 Weak DPs: 404.63/148.03 { f^#(0()) -> c_1() 404.63/148.03 , f^#(1()) -> c_2() 404.63/148.03 , if^#(true(), s(x), s(y)) -> c_4() 404.63/148.03 , if^#(false(), s(x), s(y)) -> c_5() } 404.63/148.03 Weak Trs: 404.63/148.03 { f(0()) -> true() 404.63/148.03 , f(1()) -> false() 404.63/148.03 , f(s(x)) -> f(x) 404.63/148.03 , if(true(), s(x), s(y)) -> s(x) 404.63/148.03 , if(false(), s(x), s(y)) -> s(y) 404.63/148.03 , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) 404.63/148.03 , g(x, c(y)) -> c(g(x, y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^2)) 404.63/148.03 404.63/148.03 The following weak DPs constitute a sub-graph of the DG that is 404.63/148.03 closed under successors. The DPs are removed. 404.63/148.03 404.63/148.03 { f^#(0()) -> c_1() 404.63/148.03 , f^#(1()) -> c_2() 404.63/148.03 , if^#(true(), s(x), s(y)) -> c_4() 404.63/148.03 , if^#(false(), s(x), s(y)) -> c_5() } 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^2)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { f^#(s(x)) -> c_3(f^#(x)) 404.63/148.03 , g^#(x, c(y)) -> 404.63/148.03 c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), 404.63/148.03 if^#(f(x), c(g(s(x), y)), c(y)), 404.63/148.03 f^#(x), 404.63/148.03 g^#(s(x), y)) 404.63/148.03 , g^#(x, c(y)) -> c_7(g^#(x, y)) } 404.63/148.03 Weak Trs: 404.63/148.03 { f(0()) -> true() 404.63/148.03 , f(1()) -> false() 404.63/148.03 , f(s(x)) -> f(x) 404.63/148.03 , if(true(), s(x), s(y)) -> s(x) 404.63/148.03 , if(false(), s(x), s(y)) -> s(y) 404.63/148.03 , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) 404.63/148.03 , g(x, c(y)) -> c(g(x, y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^2)) 404.63/148.03 404.63/148.03 Due to missing edges in the dependency-graph, the right-hand sides 404.63/148.03 of following rules could be simplified: 404.63/148.03 404.63/148.03 { g^#(x, c(y)) -> 404.63/148.03 c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), 404.63/148.03 if^#(f(x), c(g(s(x), y)), c(y)), 404.63/148.03 f^#(x), 404.63/148.03 g^#(s(x), y)) } 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^2)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { f^#(s(x)) -> c_1(f^#(x)) 404.63/148.03 , g^#(x, c(y)) -> c_2(g^#(x, y)) 404.63/148.03 , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } 404.63/148.03 Weak Trs: 404.63/148.03 { f(0()) -> true() 404.63/148.03 , f(1()) -> false() 404.63/148.03 , f(s(x)) -> f(x) 404.63/148.03 , if(true(), s(x), s(y)) -> s(x) 404.63/148.03 , if(false(), s(x), s(y)) -> s(y) 404.63/148.03 , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) 404.63/148.03 , g(x, c(y)) -> c(g(x, y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^2)) 404.63/148.03 404.63/148.03 No rule is usable, rules are removed from the input problem. 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^2)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { f^#(s(x)) -> c_1(f^#(x)) 404.63/148.03 , g^#(x, c(y)) -> c_2(g^#(x, y)) 404.63/148.03 , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^2)) 404.63/148.03 404.63/148.03 We use the processor 'polynomial interpretation' to orient 404.63/148.03 following rules strictly. 404.63/148.03 404.63/148.03 DPs: 404.63/148.03 { 1: f^#(s(x)) -> c_1(f^#(x)) } 404.63/148.03 404.63/148.03 Sub-proof: 404.63/148.03 ---------- 404.63/148.03 We consider the following typing: 404.63/148.03 404.63/148.03 s :: a -> a 404.63/148.03 c :: b -> b 404.63/148.03 f^# :: a -> c 404.63/148.03 g^# :: (a,b) -> d 404.63/148.03 c_1 :: c -> c 404.63/148.03 c_2 :: d -> d 404.63/148.03 c_3 :: (c,d) -> d 404.63/148.03 404.63/148.03 The following argument positions are considered usable: 404.63/148.03 404.63/148.03 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2} 404.63/148.03 404.63/148.03 TcT has computed the following constructor-restricted 404.63/148.03 typedpolynomial interpretation. 404.63/148.03 404.63/148.03 [s](x1) = 1 + x1 404.63/148.03 404.63/148.03 [c](x1) = 1 + x1 404.63/148.03 404.63/148.03 [f^#](x1) = x1 404.63/148.03 404.63/148.03 [g^#](x1, x2) = x1*x2 + x2^2 404.63/148.03 404.63/148.03 [c_1](x1) = x1 404.63/148.03 404.63/148.03 [c_2](x1) = 1 + x1 404.63/148.03 404.63/148.03 [c_3](x1, x2) = 1 + x1 + x2 404.63/148.03 404.63/148.03 404.63/148.03 This order satisfies the following ordering constraints. 404.63/148.03 404.63/148.03 [f^#(s(x))] = 1 + x 404.63/148.03 > x 404.63/148.03 = [c_1(f^#(x))] 404.63/148.03 404.63/148.03 [g^#(x, c(y))] = x + x*y + 1 + 2*y + y^2 404.63/148.03 >= 1 + x*y + y^2 404.63/148.03 = [c_2(g^#(x, y))] 404.63/148.03 404.63/148.03 [g^#(x, c(y))] = x + x*y + 1 + 2*y + y^2 404.63/148.03 >= 1 + x + y + x*y + y^2 404.63/148.03 = [c_3(f^#(x), g^#(s(x), y))] 404.63/148.03 404.63/148.03 404.63/148.03 The strictly oriented rules are moved into the weak component. 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^1)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { g^#(x, c(y)) -> c_2(g^#(x, y)) 404.63/148.03 , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } 404.63/148.03 Weak DPs: { f^#(s(x)) -> c_1(f^#(x)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^1)) 404.63/148.03 404.63/148.03 The following weak DPs constitute a sub-graph of the DG that is 404.63/148.03 closed under successors. The DPs are removed. 404.63/148.03 404.63/148.03 { f^#(s(x)) -> c_1(f^#(x)) } 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^1)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { g^#(x, c(y)) -> c_2(g^#(x, y)) 404.63/148.03 , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^1)) 404.63/148.03 404.63/148.03 Due to missing edges in the dependency-graph, the right-hand sides 404.63/148.03 of following rules could be simplified: 404.63/148.03 404.63/148.03 { g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(n^1)). 404.63/148.03 404.63/148.03 Strict DPs: 404.63/148.03 { g^#(x, c(y)) -> c_1(g^#(x, y)) 404.63/148.03 , g^#(x, c(y)) -> c_2(g^#(s(x), y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(n^1)) 404.63/148.03 404.63/148.03 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 404.63/148.03 to orient following rules strictly. 404.63/148.03 404.63/148.03 DPs: 404.63/148.03 { 1: g^#(x, c(y)) -> c_1(g^#(x, y)) 404.63/148.03 , 2: g^#(x, c(y)) -> c_2(g^#(s(x), y)) } 404.63/148.03 404.63/148.03 Sub-proof: 404.63/148.03 ---------- 404.63/148.03 The input was oriented with the instance of 'Small Polynomial Path 404.63/148.03 Order (PS,1-bounded)' as induced by the safe mapping 404.63/148.03 404.63/148.03 safe(s) = {1}, safe(c) = {1}, safe(f^#) = {}, safe(g^#) = {1}, 404.63/148.03 safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c) = {}, 404.63/148.03 safe(c_1) = {}, safe(c_2) = {} 404.63/148.03 404.63/148.03 and precedence 404.63/148.03 404.63/148.03 empty . 404.63/148.03 404.63/148.03 Following symbols are considered recursive: 404.63/148.03 404.63/148.03 {g^#} 404.63/148.03 404.63/148.03 The recursion depth is 1. 404.63/148.03 404.63/148.03 Further, following argument filtering is employed: 404.63/148.03 404.63/148.03 pi(s) = 1, pi(c) = [1], pi(f^#) = [], pi(g^#) = [1, 2], 404.63/148.03 pi(c_1) = [], pi(c_2) = [], pi(c_3) = [], pi(c) = [], 404.63/148.03 pi(c_1) = [1], pi(c_2) = [1] 404.63/148.03 404.63/148.03 Usable defined function symbols are a subset of: 404.63/148.03 404.63/148.03 {f^#, g^#} 404.63/148.03 404.63/148.03 For your convenience, here are the satisfied ordering constraints: 404.63/148.03 404.63/148.03 pi(g^#(x, c(y))) = g^#(c(; y); x) 404.63/148.03 > c_1(g^#(y; x);) 404.63/148.03 = pi(c_1(g^#(x, y))) 404.63/148.03 404.63/148.03 pi(g^#(x, c(y))) = g^#(c(; y); x) 404.63/148.03 > c_2(g^#(y; x);) 404.63/148.03 = pi(c_2(g^#(s(x), y))) 404.63/148.03 404.63/148.03 404.63/148.03 The strictly oriented rules are moved into the weak component. 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(1)). 404.63/148.03 404.63/148.03 Weak DPs: 404.63/148.03 { g^#(x, c(y)) -> c_1(g^#(x, y)) 404.63/148.03 , g^#(x, c(y)) -> c_2(g^#(s(x), y)) } 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(1)) 404.63/148.03 404.63/148.03 The following weak DPs constitute a sub-graph of the DG that is 404.63/148.03 closed under successors. The DPs are removed. 404.63/148.03 404.63/148.03 { g^#(x, c(y)) -> c_1(g^#(x, y)) 404.63/148.03 , g^#(x, c(y)) -> c_2(g^#(s(x), y)) } 404.63/148.03 404.63/148.03 We are left with following problem, upon which TcT provides the 404.63/148.03 certificate YES(O(1),O(1)). 404.63/148.03 404.63/148.03 Rules: Empty 404.63/148.03 Obligation: 404.63/148.03 innermost runtime complexity 404.63/148.03 Answer: 404.63/148.03 YES(O(1),O(1)) 404.63/148.03 404.63/148.03 Empty rules are trivially bounded 404.63/148.03 404.63/148.03 Hurray, we answered YES(O(1),O(n^2)) 404.88/148.24 EOF