YES(O(1),O(n^1)) 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 We add the following dependency tuples: 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { i^#(x, x) -> c_1(i^#(a(), b())) 580.34/148.66 , g^#(x, x) -> c_2(g^#(a(), b())) 580.34/148.66 , g^#(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 c_3(g^#(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))), 580.34/148.66 g^#(a(), g(a(), g(x, g(b(), g(b(), y))))), 580.34/148.66 g^#(a(), g(x, g(b(), g(b(), y)))), 580.34/148.66 g^#(x, g(b(), g(b(), y))), 580.34/148.66 g^#(b(), g(b(), y)), 580.34/148.66 g^#(b(), y)) 580.34/148.66 , h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 , h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 , f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) 580.34/148.66 , f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 580.34/148.66 and mark the set of starting terms. 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { i^#(x, x) -> c_1(i^#(a(), b())) 580.34/148.66 , g^#(x, x) -> c_2(g^#(a(), b())) 580.34/148.66 , g^#(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 c_3(g^#(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))), 580.34/148.66 g^#(a(), g(a(), g(x, g(b(), g(b(), y))))), 580.34/148.66 g^#(a(), g(x, g(b(), g(b(), y)))), 580.34/148.66 g^#(x, g(b(), g(b(), y))), 580.34/148.66 g^#(b(), g(b(), y)), 580.34/148.66 g^#(b(), y)) 580.34/148.66 , h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 , h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 , f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) 580.34/148.66 , f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 Weak Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 Consider the dependency graph: 580.34/148.66 580.34/148.66 1: i^#(x, x) -> c_1(i^#(a(), b())) 580.34/148.66 580.34/148.66 2: g^#(x, x) -> c_2(g^#(a(), b())) 580.34/148.66 580.34/148.66 3: g^#(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 c_3(g^#(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))), 580.34/148.66 g^#(a(), g(a(), g(x, g(b(), g(b(), y))))), 580.34/148.66 g^#(a(), g(x, g(b(), g(b(), y)))), 580.34/148.66 g^#(x, g(b(), g(b(), y))), 580.34/148.66 g^#(b(), g(b(), y)), 580.34/148.66 g^#(b(), y)) 580.34/148.66 -->_4 g^#(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 c_3(g^#(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))), 580.34/148.66 g^#(a(), g(a(), g(x, g(b(), g(b(), y))))), 580.34/148.66 g^#(a(), g(x, g(b(), g(b(), y)))), 580.34/148.66 g^#(x, g(b(), g(b(), y))), 580.34/148.66 g^#(b(), g(b(), y)), 580.34/148.66 g^#(b(), y)) :3 580.34/148.66 -->_3 g^#(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 c_3(g^#(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))), 580.34/148.66 g^#(a(), g(a(), g(x, g(b(), g(b(), y))))), 580.34/148.66 g^#(a(), g(x, g(b(), g(b(), y)))), 580.34/148.66 g^#(x, g(b(), g(b(), y))), 580.34/148.66 g^#(b(), g(b(), y)), 580.34/148.66 g^#(b(), y)) :3 580.34/148.66 -->_2 g^#(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 c_3(g^#(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))), 580.34/148.66 g^#(a(), g(a(), g(x, g(b(), g(b(), y))))), 580.34/148.66 g^#(a(), g(x, g(b(), g(b(), y)))), 580.34/148.66 g^#(x, g(b(), g(b(), y))), 580.34/148.66 g^#(b(), g(b(), y)), 580.34/148.66 g^#(b(), y)) :3 580.34/148.66 -->_6 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 -->_5 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 -->_4 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 -->_3 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 -->_2 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 -->_1 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 580.34/148.66 4: h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 -->_4 h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) :6 580.34/148.66 -->_3 h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) :6 580.34/148.66 -->_4 h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) :5 580.34/148.66 -->_3 h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) :5 580.34/148.66 -->_4 h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), 580.34/148.66 i^#(c(), h(h(y))), 580.34/148.66 h^#(h(y)), 580.34/148.66 h^#(y)) :4 580.34/148.66 -->_3 h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), 580.34/148.66 i^#(c(), h(h(y))), 580.34/148.66 h^#(h(y)), 580.34/148.66 h^#(y)) :4 580.34/148.66 -->_2 i^#(x, x) -> c_1(i^#(a(), b())) :1 580.34/148.66 -->_1 i^#(x, x) -> c_1(i^#(a(), b())) :1 580.34/148.66 580.34/148.66 5: h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 -->_1 h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) :6 580.34/148.66 -->_1 h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) :5 580.34/148.66 -->_1 h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), 580.34/148.66 i^#(c(), h(h(y))), 580.34/148.66 h^#(h(y)), 580.34/148.66 h^#(y)) :4 580.34/148.66 -->_2 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 580.34/148.66 6: h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 -->_1 h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) :6 580.34/148.66 -->_1 h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) :5 580.34/148.66 -->_1 h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), 580.34/148.66 i^#(c(), h(h(y))), 580.34/148.66 h^#(h(y)), 580.34/148.66 h^#(y)) :4 580.34/148.66 580.34/148.66 7: f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) 580.34/148.66 -->_1 f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) :8 580.34/148.66 -->_1 f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) :7 580.34/148.66 -->_2 g^#(x, x) -> c_2(g^#(a(), b())) :2 580.34/148.66 580.34/148.66 8: f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) 580.34/148.66 -->_1 f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) :8 580.34/148.66 -->_1 f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) :7 580.34/148.66 -->_2 h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) :6 580.34/148.66 580.34/148.66 580.34/148.66 Only the nodes {1,2,8,7,6,5,4} are reachable from nodes {1,2,8} 580.34/148.66 that start derivation from marked basic terms. The nodes not 580.34/148.66 reachable are removed from the problem. 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { i^#(x, x) -> c_1(i^#(a(), b())) 580.34/148.66 , g^#(x, x) -> c_2(g^#(a(), b())) 580.34/148.66 , h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 , h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 , f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) 580.34/148.66 , f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 Weak Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 We estimate the number of application of {1,2} by applications of 580.34/148.66 Pre({1,2}) = {3,4,6}. Here rules are labeled as follows: 580.34/148.66 580.34/148.66 DPs: 580.34/148.66 { 1: i^#(x, x) -> c_1(i^#(a(), b())) 580.34/148.66 , 2: g^#(x, x) -> c_2(g^#(a(), b())) 580.34/148.66 , 3: h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 , 4: h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 , 5: h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 , 6: f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) 580.34/148.66 , 7: f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 , h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 , f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) 580.34/148.66 , f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 Weak DPs: 580.34/148.66 { i^#(x, x) -> c_1(i^#(a(), b())) 580.34/148.66 , g^#(x, x) -> c_2(g^#(a(), b())) } 580.34/148.66 Weak Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 The following weak DPs constitute a sub-graph of the DG that is 580.34/148.66 closed under successors. The DPs are removed. 580.34/148.66 580.34/148.66 { i^#(x, x) -> c_1(i^#(a(), b())) 580.34/148.66 , g^#(x, x) -> c_2(g^#(a(), b())) } 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 , h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 , f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) 580.34/148.66 , f^#(s(x)) -> c_8(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 Weak Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 Due to missing edges in the dependency-graph, the right-hand sides 580.34/148.66 of following rules could be simplified: 580.34/148.66 580.34/148.66 { h^#(i(x, y)) -> 580.34/148.66 c_4(i^#(i(c(), h(h(y))), x), i^#(c(), h(h(y))), h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_5(h^#(g(s(x), y)), g^#(s(x), y)) 580.34/148.66 , h^#(s(f(x))) -> c_6(h^#(f(x)), f^#(x)) 580.34/148.66 , f^#(g(s(x), y)) -> c_7(f^#(g(x, s(y))), g^#(x, s(y))) } 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { h^#(i(x, y)) -> c_1(h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_2(h^#(g(s(x), y))) 580.34/148.66 , h^#(s(f(x))) -> c_3(h^#(f(x))) 580.34/148.66 , f^#(g(s(x), y)) -> c_4(f^#(g(x, s(y)))) 580.34/148.66 , f^#(s(x)) -> c_5(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 Weak Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 We use the processor 'matrix interpretation of dimension 2' to 580.34/148.66 orient following rules strictly. 580.34/148.66 580.34/148.66 DPs: 580.34/148.66 { 3: h^#(s(f(x))) -> c_3(h^#(f(x))) } 580.34/148.66 Trs: { f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 580.34/148.66 Sub-proof: 580.34/148.66 ---------- 580.34/148.66 The following argument positions are usable: 580.34/148.66 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, 580.34/148.66 Uargs(c_5) = {1, 2} 580.34/148.66 580.34/148.66 TcT has computed the following constructor-based matrix 580.34/148.66 interpretation satisfying not(EDA) and not(IDA(1)). 580.34/148.66 580.34/148.66 [i](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 580.34/148.66 [4 1] [0 0] [0] 580.34/148.66 580.34/148.66 [a] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [b] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [g](x1, x2) = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [h](x1) = [0 1] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [s](x1) = [0 3] x1 + [1] 580.34/148.66 [0 1] [0] 580.34/148.66 580.34/148.66 [f](x1) = [4 0] x1 + [0] 580.34/148.66 [3 0] [0] 580.34/148.66 580.34/148.66 [c] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [h^#](x1) = [1 0] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [f^#](x1) = [3 0] x1 + [0] 580.34/148.66 [1 6] [0] 580.34/148.66 580.34/148.66 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 580.34/148.66 [0 0] [0 0] [0] 580.34/148.66 580.34/148.66 [c_2](x1) = [1 0] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [c_3](x1) = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [c_4](x1) = [4 0] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [c_5](x1, x2) = [1 0] x1 + [2 0] x2 + [1] 580.34/148.66 [0 0] [0 0] [1] 580.34/148.66 580.34/148.66 The order satisfies the following ordering constraints: 580.34/148.66 580.34/148.66 [i(x, x)] = [1 1] x + [0] 580.34/148.66 [4 1] [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [i(a(), b())] 580.34/148.66 580.34/148.66 [g(x, x)] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [g(a(), b())] 580.34/148.66 580.34/148.66 [g(a(), g(x, g(b(), g(a(), g(x, y)))))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y))))))] 580.34/148.66 580.34/148.66 [h(i(x, y))] = [4 1] x + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 >= [1 1] x + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 = [i(i(c(), h(h(y))), x)] 580.34/148.66 580.34/148.66 [h(g(x, s(y)))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [h(g(s(x), y))] 580.34/148.66 580.34/148.66 [h(s(f(x)))] = [3 0] x + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 >= [3 0] x + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 = [h(f(x))] 580.34/148.66 580.34/148.66 [f(g(s(x), y))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [f(g(x, s(y)))] 580.34/148.66 580.34/148.66 [f(s(x))] = [0 12] x + [4] 580.34/148.66 [0 9] [3] 580.34/148.66 > [0 9] x + [1] 580.34/148.66 [0 3] [0] 580.34/148.66 = [s(s(f(h(s(x)))))] 580.34/148.66 580.34/148.66 [h^#(i(x, y))] = [1 1] y + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 >= [1 1] y + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 = [c_1(h^#(h(y)), h^#(y))] 580.34/148.66 580.34/148.66 [h^#(g(x, s(y)))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [c_2(h^#(g(s(x), y)))] 580.34/148.66 580.34/148.66 [h^#(s(f(x)))] = [9 0] x + [1] 580.34/148.66 [0 0] [0] 580.34/148.66 > [0] 580.34/148.66 [0] 580.34/148.66 = [c_3(h^#(f(x)))] 580.34/148.66 580.34/148.66 [f^#(g(s(x), y))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [c_4(f^#(g(x, s(y))))] 580.34/148.66 580.34/148.66 [f^#(s(x))] = [0 9] x + [3] 580.34/148.66 [0 9] [1] 580.34/148.66 >= [0 9] x + [3] 580.34/148.66 [0 0] [1] 580.34/148.66 = [c_5(f^#(h(s(x))), h^#(s(x)))] 580.34/148.66 580.34/148.66 580.34/148.66 The strictly oriented rules are moved into the weak component. 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { h^#(i(x, y)) -> c_1(h^#(h(y)), h^#(y)) 580.34/148.66 , h^#(g(x, s(y))) -> c_2(h^#(g(s(x), y))) 580.34/148.66 , f^#(g(s(x), y)) -> c_4(f^#(g(x, s(y)))) 580.34/148.66 , f^#(s(x)) -> c_5(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 Weak DPs: { h^#(s(f(x))) -> c_3(h^#(f(x))) } 580.34/148.66 Weak Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 We use the processor 'matrix interpretation of dimension 2' to 580.34/148.66 orient following rules strictly. 580.34/148.66 580.34/148.66 DPs: 580.34/148.66 { 2: h^#(g(x, s(y))) -> c_2(h^#(g(s(x), y))) } 580.34/148.66 Trs: { h(s(f(x))) -> h(f(x)) } 580.34/148.66 580.34/148.66 Sub-proof: 580.34/148.66 ---------- 580.34/148.66 The following argument positions are usable: 580.34/148.66 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, 580.34/148.66 Uargs(c_5) = {1, 2} 580.34/148.66 580.34/148.66 TcT has computed the following constructor-based matrix 580.34/148.66 interpretation satisfying not(EDA) and not(IDA(1)). 580.34/148.66 580.34/148.66 [i](x1, x2) = [0 4] x1 + [1 2] x2 + [0] 580.34/148.66 [1 2] [0 0] [0] 580.34/148.66 580.34/148.66 [a] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [b] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [g](x1, x2) = [0 2] x2 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [h](x1) = [0 1] x1 + [0] 580.34/148.66 [2 0] [0] 580.34/148.66 580.34/148.66 [s](x1) = [0 0] x1 + [0] 580.34/148.66 [0 1] [1] 580.34/148.66 580.34/148.66 [f](x1) = [0 0] x1 + [0] 580.34/148.66 [0 4] [0] 580.34/148.66 580.34/148.66 [c] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [h^#](x1) = [4 0] x1 + [0] 580.34/148.66 [0 0] [4] 580.34/148.66 580.34/148.66 [f^#](x1) = [0 0] x1 + [0] 580.34/148.66 [4 0] [0] 580.34/148.66 580.34/148.66 [c_1](x1, x2) = [2 0] x1 + [1 0] x2 + [0] 580.34/148.66 [0 0] [0 0] [3] 580.34/148.66 580.34/148.66 [c_2](x1) = [1 0] x1 + [5] 580.34/148.66 [0 0] [3] 580.34/148.66 580.34/148.66 [c_3](x1) = [0] 580.34/148.66 [3] 580.34/148.66 580.34/148.66 [c_4](x1) = [1 0] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [c_5](x1, x2) = [2 0] x1 + [2 0] x2 + [0] 580.34/148.66 [0 0] [0 0] [0] 580.34/148.66 580.34/148.66 The order satisfies the following ordering constraints: 580.34/148.66 580.34/148.66 [i(x, x)] = [1 6] x + [0] 580.34/148.66 [1 2] [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [i(a(), b())] 580.34/148.66 580.34/148.66 [g(x, x)] = [0 2] x + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [g(a(), b())] 580.34/148.66 580.34/148.66 [g(a(), g(x, g(b(), g(a(), g(x, y)))))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y))))))] 580.34/148.66 580.34/148.66 [h(i(x, y))] = [1 2] x + [0 0] y + [0] 580.34/148.66 [0 8] [2 4] [0] 580.34/148.66 >= [1 2] x + [0 0] y + [0] 580.34/148.66 [0 0] [2 4] [0] 580.34/148.66 = [i(i(c(), h(h(y))), x)] 580.34/148.66 580.34/148.66 [h(g(x, s(y)))] = [0 0] y + [0] 580.34/148.66 [0 4] [4] 580.34/148.66 >= [0 0] y + [0] 580.34/148.66 [0 4] [0] 580.34/148.66 = [h(g(s(x), y))] 580.34/148.66 580.34/148.66 [h(s(f(x)))] = [0 4] x + [1] 580.34/148.66 [0 0] [0] 580.34/148.66 > [0 4] x + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 = [h(f(x))] 580.34/148.66 580.34/148.66 [f(g(s(x), y))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [f(g(x, s(y)))] 580.34/148.66 580.34/148.66 [f(s(x))] = [0 0] x + [0] 580.34/148.66 [0 4] [4] 580.34/148.66 >= [0] 580.34/148.66 [2] 580.34/148.66 = [s(s(f(h(s(x)))))] 580.34/148.66 580.34/148.66 [h^#(i(x, y))] = [0 16] x + [4 8] y + [0] 580.34/148.66 [0 0] [0 0] [4] 580.34/148.66 >= [4 8] y + [0] 580.34/148.66 [0 0] [3] 580.34/148.66 = [c_1(h^#(h(y)), h^#(y))] 580.34/148.66 580.34/148.66 [h^#(g(x, s(y)))] = [0 8] y + [8] 580.34/148.66 [0 0] [4] 580.34/148.66 > [0 8] y + [5] 580.34/148.66 [0 0] [3] 580.34/148.66 = [c_2(h^#(g(s(x), y)))] 580.34/148.66 580.34/148.66 [h^#(s(f(x)))] = [0] 580.34/148.66 [4] 580.34/148.66 >= [0] 580.34/148.66 [3] 580.34/148.66 = [c_3(h^#(f(x)))] 580.34/148.66 580.34/148.66 [f^#(g(s(x), y))] = [0 0] y + [0] 580.34/148.66 [0 8] [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [c_4(f^#(g(x, s(y))))] 580.34/148.66 580.34/148.66 [f^#(s(x))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [c_5(f^#(h(s(x))), h^#(s(x)))] 580.34/148.66 580.34/148.66 580.34/148.66 The strictly oriented rules are moved into the weak component. 580.34/148.66 580.34/148.66 We are left with following problem, upon which TcT provides the 580.34/148.66 certificate YES(O(1),O(n^1)). 580.34/148.66 580.34/148.66 Strict DPs: 580.34/148.66 { h^#(i(x, y)) -> c_1(h^#(h(y)), h^#(y)) 580.34/148.66 , f^#(g(s(x), y)) -> c_4(f^#(g(x, s(y)))) 580.34/148.66 , f^#(s(x)) -> c_5(f^#(h(s(x))), h^#(s(x))) } 580.34/148.66 Weak DPs: 580.34/148.66 { h^#(g(x, s(y))) -> c_2(h^#(g(s(x), y))) 580.34/148.66 , h^#(s(f(x))) -> c_3(h^#(f(x))) } 580.34/148.66 Weak Trs: 580.34/148.66 { i(x, x) -> i(a(), b()) 580.34/148.66 , g(x, x) -> g(a(), b()) 580.34/148.66 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.66 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.66 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.66 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.66 , h(s(f(x))) -> h(f(x)) 580.34/148.66 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.66 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.66 Obligation: 580.34/148.66 innermost runtime complexity 580.34/148.66 Answer: 580.34/148.66 YES(O(1),O(n^1)) 580.34/148.66 580.34/148.66 We use the processor 'matrix interpretation of dimension 2' to 580.34/148.66 orient following rules strictly. 580.34/148.66 580.34/148.66 DPs: 580.34/148.66 { 1: h^#(i(x, y)) -> c_1(h^#(h(y)), h^#(y)) } 580.34/148.66 Trs: { h(i(x, y)) -> i(i(c(), h(h(y))), x) } 580.34/148.66 580.34/148.66 Sub-proof: 580.34/148.66 ---------- 580.34/148.66 The following argument positions are usable: 580.34/148.66 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, 580.34/148.66 Uargs(c_5) = {1, 2} 580.34/148.66 580.34/148.66 TcT has computed the following constructor-based matrix 580.34/148.66 interpretation satisfying not(EDA) and not(IDA(1)). 580.34/148.66 580.34/148.66 [i](x1, x2) = [2 1] x1 + [0 0] x2 + [1] 580.34/148.66 [0 0] [2 1] [1] 580.34/148.66 580.34/148.66 [a] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [b] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [g](x1, x2) = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [h](x1) = [0 6] x1 + [0] 580.34/148.66 [1 0] [0] 580.34/148.66 580.34/148.66 [s](x1) = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [f](x1) = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [c] = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [h^#](x1) = [0 4] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [f^#](x1) = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 580.34/148.66 [0 0] [0 0] [0] 580.34/148.66 580.34/148.66 [c_2](x1) = [1 0] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [c_3](x1) = [0] 580.34/148.66 [0] 580.34/148.66 580.34/148.66 [c_4](x1) = [1 0] x1 + [0] 580.34/148.66 [0 0] [0] 580.34/148.66 580.34/148.66 [c_5](x1, x2) = [4 0] x1 + [1 0] x2 + [0] 580.34/148.66 [0 0] [0 0] [0] 580.34/148.66 580.34/148.66 The order satisfies the following ordering constraints: 580.34/148.66 580.34/148.66 [i(x, x)] = [2 1] x + [1] 580.34/148.66 [2 1] [1] 580.34/148.66 >= [1] 580.34/148.66 [1] 580.34/148.66 = [i(a(), b())] 580.34/148.66 580.34/148.66 [g(x, x)] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [g(a(), b())] 580.34/148.66 580.34/148.66 [g(a(), g(x, g(b(), g(a(), g(x, y)))))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y))))))] 580.34/148.66 580.34/148.66 [h(i(x, y))] = [0 0] x + [12 6] y + [6] 580.34/148.66 [2 1] [ 0 0] [1] 580.34/148.66 > [0 0] x + [12 6] y + [4] 580.34/148.66 [2 1] [ 0 0] [1] 580.34/148.66 = [i(i(c(), h(h(y))), x)] 580.34/148.66 580.34/148.66 [h(g(x, s(y)))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [h(g(s(x), y))] 580.34/148.66 580.34/148.66 [h(s(f(x)))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [h(f(x))] 580.34/148.66 580.34/148.66 [f(g(s(x), y))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [f(g(x, s(y)))] 580.34/148.66 580.34/148.66 [f(s(x))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.66 = [s(s(f(h(s(x)))))] 580.34/148.66 580.34/148.66 [h^#(i(x, y))] = [8 4] y + [4] 580.34/148.66 [0 0] [0] 580.34/148.66 > [4 4] y + [1] 580.34/148.66 [0 0] [0] 580.34/148.66 = [c_1(h^#(h(y)), h^#(y))] 580.34/148.66 580.34/148.66 [h^#(g(x, s(y)))] = [0] 580.34/148.66 [0] 580.34/148.66 >= [0] 580.34/148.66 [0] 580.34/148.67 = [c_2(h^#(g(s(x), y)))] 580.34/148.67 580.34/148.67 [h^#(s(f(x)))] = [0] 580.34/148.67 [0] 580.34/148.67 >= [0] 580.34/148.67 [0] 580.34/148.67 = [c_3(h^#(f(x)))] 580.34/148.67 580.34/148.67 [f^#(g(s(x), y))] = [0] 580.34/148.67 [0] 580.34/148.67 >= [0] 580.34/148.67 [0] 580.34/148.67 = [c_4(f^#(g(x, s(y))))] 580.34/148.67 580.34/148.67 [f^#(s(x))] = [0] 580.34/148.67 [0] 580.34/148.67 >= [0] 580.34/148.67 [0] 580.34/148.67 = [c_5(f^#(h(s(x))), h^#(s(x)))] 580.34/148.67 580.34/148.67 580.34/148.67 The strictly oriented rules are moved into the weak component. 580.34/148.67 580.34/148.67 We are left with following problem, upon which TcT provides the 580.34/148.67 certificate YES(O(1),O(n^1)). 580.34/148.67 580.34/148.67 Strict DPs: 580.34/148.67 { f^#(g(s(x), y)) -> c_4(f^#(g(x, s(y)))) 580.34/148.67 , f^#(s(x)) -> c_5(f^#(h(s(x))), h^#(s(x))) } 580.34/148.67 Weak DPs: 580.34/148.67 { h^#(i(x, y)) -> c_1(h^#(h(y)), h^#(y)) 580.34/148.67 , h^#(g(x, s(y))) -> c_2(h^#(g(s(x), y))) 580.34/148.67 , h^#(s(f(x))) -> c_3(h^#(f(x))) } 580.34/148.67 Weak Trs: 580.34/148.67 { i(x, x) -> i(a(), b()) 580.34/148.67 , g(x, x) -> g(a(), b()) 580.34/148.67 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.67 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.67 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.67 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.67 , h(s(f(x))) -> h(f(x)) 580.34/148.67 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.67 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.67 Obligation: 580.34/148.67 innermost runtime complexity 580.34/148.67 Answer: 580.34/148.67 YES(O(1),O(n^1)) 580.34/148.67 580.34/148.67 The following weak DPs constitute a sub-graph of the DG that is 580.34/148.67 closed under successors. The DPs are removed. 580.34/148.67 580.34/148.67 { h^#(i(x, y)) -> c_1(h^#(h(y)), h^#(y)) 580.34/148.67 , h^#(g(x, s(y))) -> c_2(h^#(g(s(x), y))) 580.34/148.67 , h^#(s(f(x))) -> c_3(h^#(f(x))) } 580.34/148.67 580.34/148.67 We are left with following problem, upon which TcT provides the 580.34/148.67 certificate YES(O(1),O(n^1)). 580.34/148.67 580.34/148.67 Strict DPs: 580.34/148.67 { f^#(g(s(x), y)) -> c_4(f^#(g(x, s(y)))) 580.34/148.67 , f^#(s(x)) -> c_5(f^#(h(s(x))), h^#(s(x))) } 580.34/148.67 Weak Trs: 580.34/148.67 { i(x, x) -> i(a(), b()) 580.34/148.67 , g(x, x) -> g(a(), b()) 580.34/148.67 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.67 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.67 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.67 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.67 , h(s(f(x))) -> h(f(x)) 580.34/148.67 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.67 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.67 Obligation: 580.34/148.67 innermost runtime complexity 580.34/148.67 Answer: 580.34/148.67 YES(O(1),O(n^1)) 580.34/148.67 580.34/148.67 Due to missing edges in the dependency-graph, the right-hand sides 580.34/148.67 of following rules could be simplified: 580.34/148.67 580.34/148.67 { f^#(s(x)) -> c_5(f^#(h(s(x))), h^#(s(x))) } 580.34/148.67 580.34/148.67 We are left with following problem, upon which TcT provides the 580.34/148.67 certificate YES(O(1),O(n^1)). 580.34/148.67 580.34/148.67 Strict DPs: 580.34/148.67 { f^#(g(s(x), y)) -> c_1(f^#(g(x, s(y)))) 580.34/148.67 , f^#(s(x)) -> c_2(f^#(h(s(x)))) } 580.34/148.67 Weak Trs: 580.34/148.67 { i(x, x) -> i(a(), b()) 580.34/148.67 , g(x, x) -> g(a(), b()) 580.34/148.67 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.67 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.67 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.67 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.67 , h(s(f(x))) -> h(f(x)) 580.34/148.67 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.67 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.67 Obligation: 580.34/148.67 innermost runtime complexity 580.34/148.67 Answer: 580.34/148.67 YES(O(1),O(n^1)) 580.34/148.67 580.34/148.67 We use the processor 'matrix interpretation of dimension 1' to 580.34/148.67 orient following rules strictly. 580.34/148.67 580.34/148.67 DPs: 580.34/148.67 { 2: f^#(s(x)) -> c_2(f^#(h(s(x)))) } 580.34/148.67 580.34/148.67 Sub-proof: 580.34/148.67 ---------- 580.34/148.67 The following argument positions are usable: 580.34/148.67 Uargs(c_1) = {1}, Uargs(c_2) = {1} 580.34/148.67 580.34/148.67 TcT has computed the following constructor-restricted matrix 580.34/148.67 interpretation. Note that the diagonal of the component-wise maxima 580.34/148.67 of interpretation-entries (of constructors) contains no more than 0 580.34/148.67 non-zero entries. 580.34/148.67 580.34/148.67 [i](x1, x2) = [0] 580.34/148.67 580.34/148.67 [a] = [0] 580.34/148.67 580.34/148.67 [b] = [0] 580.34/148.67 580.34/148.67 [g](x1, x2) = [0] 580.34/148.67 580.34/148.67 [h](x1) = [0] 580.34/148.67 580.34/148.67 [s](x1) = [2] 580.34/148.67 580.34/148.67 [f](x1) = [0] 580.34/148.67 580.34/148.67 [c] = [4] 580.34/148.67 580.34/148.67 [h^#](x1) = [0] 580.34/148.67 580.34/148.67 [f^#](x1) = [1] x1 + [0] 580.34/148.67 580.34/148.67 [c_1](x1, x2) = [0] 580.34/148.67 580.34/148.67 [c_2](x1) = [0] 580.34/148.67 580.34/148.67 [c_3](x1) = [0] 580.34/148.67 580.34/148.67 [c_4](x1) = [0] 580.34/148.67 580.34/148.67 [c_5](x1, x2) = [0] 580.34/148.67 580.34/148.67 [c] = [0] 580.34/148.67 580.34/148.67 [c_1](x1) = [1] x1 + [0] 580.34/148.67 580.34/148.67 [c_2](x1) = [2] x1 + [1] 580.34/148.67 580.34/148.67 The order satisfies the following ordering constraints: 580.34/148.67 580.34/148.67 [i(x, x)] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [i(a(), b())] 580.34/148.67 580.34/148.67 [g(x, x)] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [g(a(), b())] 580.34/148.67 580.34/148.67 [g(a(), g(x, g(b(), g(a(), g(x, y)))))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y))))))] 580.34/148.67 580.34/148.67 [h(i(x, y))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [i(i(c(), h(h(y))), x)] 580.34/148.67 580.34/148.67 [h(g(x, s(y)))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [h(g(s(x), y))] 580.34/148.67 580.34/148.67 [h(s(f(x)))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [h(f(x))] 580.34/148.67 580.34/148.67 [f(g(s(x), y))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [f(g(x, s(y)))] 580.34/148.67 580.34/148.67 [f(s(x))] = [0] 580.34/148.67 ? [2] 580.34/148.67 = [s(s(f(h(s(x)))))] 580.34/148.67 580.34/148.67 [f^#(g(s(x), y))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [c_1(f^#(g(x, s(y))))] 580.34/148.67 580.34/148.67 [f^#(s(x))] = [2] 580.34/148.67 > [1] 580.34/148.67 = [c_2(f^#(h(s(x))))] 580.34/148.67 580.34/148.67 580.34/148.67 The strictly oriented rules are moved into the weak component. 580.34/148.67 580.34/148.67 We are left with following problem, upon which TcT provides the 580.34/148.67 certificate YES(O(1),O(n^1)). 580.34/148.67 580.34/148.67 Strict DPs: { f^#(g(s(x), y)) -> c_1(f^#(g(x, s(y)))) } 580.34/148.67 Weak DPs: { f^#(s(x)) -> c_2(f^#(h(s(x)))) } 580.34/148.67 Weak Trs: 580.34/148.67 { i(x, x) -> i(a(), b()) 580.34/148.67 , g(x, x) -> g(a(), b()) 580.34/148.67 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.67 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.67 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.67 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.67 , h(s(f(x))) -> h(f(x)) 580.34/148.67 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.67 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.67 Obligation: 580.34/148.67 innermost runtime complexity 580.34/148.67 Answer: 580.34/148.67 YES(O(1),O(n^1)) 580.34/148.67 580.34/148.67 We use the processor 'matrix interpretation of dimension 1' to 580.34/148.67 orient following rules strictly. 580.34/148.67 580.34/148.67 DPs: 580.34/148.67 { 1: f^#(g(s(x), y)) -> c_1(f^#(g(x, s(y)))) 580.34/148.67 , 2: f^#(s(x)) -> c_2(f^#(h(s(x)))) } 580.34/148.67 580.34/148.67 Sub-proof: 580.34/148.67 ---------- 580.34/148.67 The following argument positions are usable: 580.34/148.67 Uargs(c_1) = {1}, Uargs(c_2) = {1} 580.34/148.67 580.34/148.67 TcT has computed the following constructor-based matrix 580.34/148.67 interpretation satisfying not(EDA). 580.34/148.67 580.34/148.67 [i](x1, x2) = [0] 580.34/148.67 580.34/148.67 [a] = [0] 580.34/148.67 580.34/148.67 [b] = [0] 580.34/148.67 580.34/148.67 [g](x1, x2) = [2] x1 + [1] x2 + [0] 580.34/148.67 580.34/148.67 [h](x1) = [0] 580.34/148.67 580.34/148.67 [s](x1) = [1] x1 + [1] 580.34/148.67 580.34/148.67 [f](x1) = [1] 580.34/148.67 580.34/148.67 [c] = [4] 580.34/148.67 580.34/148.67 [h^#](x1) = [7] x1 + [0] 580.34/148.67 580.34/148.67 [f^#](x1) = [7] x1 + [0] 580.34/148.67 580.34/148.67 [c_1](x1, x2) = [7] x1 + [7] x2 + [0] 580.34/148.67 580.34/148.67 [c_2](x1) = [7] x1 + [0] 580.34/148.67 580.34/148.67 [c_3](x1) = [7] x1 + [0] 580.34/148.67 580.34/148.67 [c_4](x1) = [7] x1 + [0] 580.34/148.67 580.34/148.67 [c_5](x1, x2) = [7] x1 + [7] x2 + [0] 580.34/148.67 580.34/148.67 [c] = [0] 580.34/148.67 580.34/148.67 [c_1](x1) = [1] x1 + [3] 580.34/148.67 580.34/148.67 [c_2](x1) = [1] x1 + [3] 580.34/148.67 580.34/148.67 The order satisfies the following ordering constraints: 580.34/148.67 580.34/148.67 [i(x, x)] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [i(a(), b())] 580.34/148.67 580.34/148.67 [g(x, x)] = [3] x + [0] 580.34/148.67 >= [0] 580.34/148.67 = [g(a(), b())] 580.34/148.67 580.34/148.67 [g(a(), g(x, g(b(), g(a(), g(x, y)))))] = [4] x + [1] y + [0] 580.34/148.67 >= [2] x + [1] y + [0] 580.34/148.67 = [g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y))))))] 580.34/148.67 580.34/148.67 [h(i(x, y))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [i(i(c(), h(h(y))), x)] 580.34/148.67 580.34/148.67 [h(g(x, s(y)))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [h(g(s(x), y))] 580.34/148.67 580.34/148.67 [h(s(f(x)))] = [0] 580.34/148.67 >= [0] 580.34/148.67 = [h(f(x))] 580.34/148.67 580.34/148.67 [f(g(s(x), y))] = [1] 580.34/148.67 >= [1] 580.34/148.67 = [f(g(x, s(y)))] 580.34/148.67 580.34/148.67 [f(s(x))] = [1] 580.34/148.67 ? [3] 580.34/148.67 = [s(s(f(h(s(x)))))] 580.34/148.67 580.34/148.67 [f^#(g(s(x), y))] = [14] x + [7] y + [14] 580.34/148.67 > [14] x + [7] y + [10] 580.34/148.67 = [c_1(f^#(g(x, s(y))))] 580.34/148.67 580.34/148.67 [f^#(s(x))] = [7] x + [7] 580.34/148.67 > [3] 580.34/148.67 = [c_2(f^#(h(s(x))))] 580.34/148.67 580.34/148.67 580.34/148.67 The strictly oriented rules are moved into the weak component. 580.34/148.67 580.34/148.67 We are left with following problem, upon which TcT provides the 580.34/148.67 certificate YES(O(1),O(1)). 580.34/148.67 580.34/148.67 Weak DPs: 580.34/148.67 { f^#(g(s(x), y)) -> c_1(f^#(g(x, s(y)))) 580.34/148.67 , f^#(s(x)) -> c_2(f^#(h(s(x)))) } 580.34/148.67 Weak Trs: 580.34/148.67 { i(x, x) -> i(a(), b()) 580.34/148.67 , g(x, x) -> g(a(), b()) 580.34/148.67 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.67 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.67 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.67 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.67 , h(s(f(x))) -> h(f(x)) 580.34/148.67 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.67 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.67 Obligation: 580.34/148.67 innermost runtime complexity 580.34/148.67 Answer: 580.34/148.67 YES(O(1),O(1)) 580.34/148.67 580.34/148.67 The following weak DPs constitute a sub-graph of the DG that is 580.34/148.67 closed under successors. The DPs are removed. 580.34/148.67 580.34/148.67 { f^#(g(s(x), y)) -> c_1(f^#(g(x, s(y)))) 580.34/148.67 , f^#(s(x)) -> c_2(f^#(h(s(x)))) } 580.34/148.67 580.34/148.67 We are left with following problem, upon which TcT provides the 580.34/148.67 certificate YES(O(1),O(1)). 580.34/148.67 580.34/148.67 Weak Trs: 580.34/148.67 { i(x, x) -> i(a(), b()) 580.34/148.67 , g(x, x) -> g(a(), b()) 580.34/148.67 , g(a(), g(x, g(b(), g(a(), g(x, y))))) -> 580.34/148.67 g(a(), g(a(), g(a(), g(x, g(b(), g(b(), y)))))) 580.34/148.67 , h(i(x, y)) -> i(i(c(), h(h(y))), x) 580.34/148.67 , h(g(x, s(y))) -> h(g(s(x), y)) 580.34/148.67 , h(s(f(x))) -> h(f(x)) 580.34/148.67 , f(g(s(x), y)) -> f(g(x, s(y))) 580.34/148.67 , f(s(x)) -> s(s(f(h(s(x))))) } 580.34/148.67 Obligation: 580.34/148.67 innermost runtime complexity 580.34/148.67 Answer: 580.34/148.67 YES(O(1),O(1)) 580.34/148.67 580.34/148.67 No rule is usable, rules are removed from the input problem. 580.34/148.67 580.34/148.67 We are left with following problem, upon which TcT provides the 580.34/148.67 certificate YES(O(1),O(1)). 580.34/148.67 580.34/148.67 Rules: Empty 580.34/148.67 Obligation: 580.34/148.67 innermost runtime complexity 580.34/148.67 Answer: 580.34/148.67 YES(O(1),O(1)) 580.34/148.67 580.34/148.67 Empty rules are trivially bounded 580.34/148.67 580.34/148.67 Hurray, we answered YES(O(1),O(n^1)) 581.12/149.23 EOF