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