YES(O(1),O(1)) 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Strict Trs: 0.00/0.51 { f(x, x, y) -> x 0.00/0.51 , f(x, y, y) -> y 0.00/0.51 , f(x, y, g(y)) -> x 0.00/0.51 , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) 0.00/0.51 , f(g(x), x, y) -> y } 0.00/0.51 Obligation: 0.00/0.51 innermost runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 We add the following weak dependency pairs: 0.00/0.51 0.00/0.51 Strict DPs: 0.00/0.51 { f^#(x, x, y) -> c_1() 0.00/0.51 , f^#(x, y, y) -> c_2() 0.00/0.51 , f^#(x, y, g(y)) -> c_3() 0.00/0.51 , f^#(f(x, y, z), u, f(x, y, v)) -> c_4(f^#(x, y, f(z, u, v))) 0.00/0.51 , f^#(g(x), x, y) -> c_5() } 0.00/0.51 0.00/0.51 and mark the set of starting terms. 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Strict DPs: 0.00/0.51 { f^#(x, x, y) -> c_1() 0.00/0.51 , f^#(x, y, y) -> c_2() 0.00/0.51 , f^#(x, y, g(y)) -> c_3() 0.00/0.51 , f^#(f(x, y, z), u, f(x, y, v)) -> c_4(f^#(x, y, f(z, u, v))) 0.00/0.51 , f^#(g(x), x, y) -> c_5() } 0.00/0.51 Strict Trs: 0.00/0.51 { f(x, x, y) -> x 0.00/0.51 , f(x, y, y) -> y 0.00/0.51 , f(x, y, g(y)) -> x 0.00/0.51 , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) 0.00/0.51 , f(g(x), x, y) -> y } 0.00/0.51 Obligation: 0.00/0.51 innermost runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 The weightgap principle applies (using the following constant 0.00/0.51 growth matrix-interpretation) 0.00/0.51 0.00/0.51 The following argument positions are usable: 0.00/0.51 Uargs(f) = {3}, Uargs(f^#) = {3}, Uargs(c_4) = {1} 0.00/0.51 0.00/0.51 TcT has computed the following constructor-restricted matrix 0.00/0.51 interpretation. 0.00/0.51 0.00/0.51 [f](x1, x2, x3) = [1 0] x1 + [1 0] x3 + [1] 0.00/0.51 [0 1] [0 1] [0] 0.00/0.51 0.00/0.51 [g](x1) = [0] 0.00/0.51 [0] 0.00/0.51 0.00/0.51 [f^#](x1, x2, x3) = [2 0] x1 + [0 0] x2 + [2 0] x3 + [0] 0.00/0.51 [0 0] [1 1] [0 0] [0] 0.00/0.51 0.00/0.51 [c_1] = [1] 0.00/0.51 [1] 0.00/0.51 0.00/0.51 [c_2] = [1] 0.00/0.51 [1] 0.00/0.51 0.00/0.51 [c_3] = [1] 0.00/0.51 [0] 0.00/0.51 0.00/0.51 [c_4](x1) = [1 0] x1 + [2] 0.00/0.51 [0 1] [2] 0.00/0.51 0.00/0.51 [c_5] = [1] 0.00/0.51 [0] 0.00/0.51 0.00/0.51 The order satisfies the following ordering constraints: 0.00/0.51 0.00/0.51 [f(x, x, y)] = [1 0] x + [1 0] y + [1] 0.00/0.51 [0 1] [0 1] [0] 0.00/0.51 > [1 0] x + [0] 0.00/0.51 [0 1] [0] 0.00/0.51 = [x] 0.00/0.51 0.00/0.51 [f(x, y, y)] = [1 0] x + [1 0] y + [1] 0.00/0.51 [0 1] [0 1] [0] 0.00/0.51 > [1 0] y + [0] 0.00/0.51 [0 1] [0] 0.00/0.51 = [y] 0.00/0.51 0.00/0.51 [f(x, y, g(y))] = [1 0] x + [1] 0.00/0.51 [0 1] [0] 0.00/0.51 > [1 0] x + [0] 0.00/0.51 [0 1] [0] 0.00/0.51 = [x] 0.00/0.51 0.00/0.51 [f(f(x, y, z), u, f(x, y, v))] = [2 0] x + [1 0] z + [1 0] v + [3] 0.00/0.51 [0 2] [0 1] [0 1] [0] 0.00/0.51 > [1 0] x + [1 0] z + [1 0] v + [2] 0.00/0.51 [0 1] [0 1] [0 1] [0] 0.00/0.51 = [f(x, y, f(z, u, v))] 0.00/0.51 0.00/0.51 [f(g(x), x, y)] = [1 0] y + [1] 0.00/0.51 [0 1] [0] 0.00/0.51 > [1 0] y + [0] 0.00/0.51 [0 1] [0] 0.00/0.51 = [y] 0.00/0.51 0.00/0.51 [f^#(x, x, y)] = [2 0] x + [2 0] y + [0] 0.00/0.51 [1 1] [0 0] [0] 0.00/0.51 ? [1] 0.00/0.51 [1] 0.00/0.51 = [c_1()] 0.00/0.51 0.00/0.51 [f^#(x, y, y)] = [2 0] x + [2 0] y + [0] 0.00/0.51 [0 0] [1 1] [0] 0.00/0.51 ? [1] 0.00/0.51 [1] 0.00/0.51 = [c_2()] 0.00/0.51 0.00/0.51 [f^#(x, y, g(y))] = [2 0] x + [0 0] y + [0] 0.00/0.51 [0 0] [1 1] [0] 0.00/0.51 ? [1] 0.00/0.51 [0] 0.00/0.51 = [c_3()] 0.00/0.51 0.00/0.51 [f^#(f(x, y, z), u, f(x, y, v))] = [4 0] x + [2 0] z + [0 0] u + [2 0] v + [4] 0.00/0.51 [0 0] [0 0] [1 1] [0 0] [0] 0.00/0.51 ? [2 0] x + [0 0] y + [2 0] z + [2 0] v + [4] 0.00/0.51 [0 0] [1 1] [0 0] [0 0] [2] 0.00/0.51 = [c_4(f^#(x, y, f(z, u, v)))] 0.00/0.51 0.00/0.51 [f^#(g(x), x, y)] = [0 0] x + [2 0] y + [0] 0.00/0.51 [1 1] [0 0] [0] 0.00/0.51 ? [1] 0.00/0.51 [0] 0.00/0.51 = [c_5()] 0.00/0.51 0.00/0.51 0.00/0.51 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Strict DPs: 0.00/0.51 { f^#(x, x, y) -> c_1() 0.00/0.51 , f^#(x, y, y) -> c_2() 0.00/0.51 , f^#(x, y, g(y)) -> c_3() 0.00/0.51 , f^#(f(x, y, z), u, f(x, y, v)) -> c_4(f^#(x, y, f(z, u, v))) 0.00/0.51 , f^#(g(x), x, y) -> c_5() } 0.00/0.51 Weak Trs: 0.00/0.51 { f(x, x, y) -> x 0.00/0.51 , f(x, y, y) -> y 0.00/0.51 , f(x, y, g(y)) -> x 0.00/0.51 , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) 0.00/0.51 , f(g(x), x, y) -> y } 0.00/0.51 Obligation: 0.00/0.51 innermost runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 Consider the dependency graph: 0.00/0.51 0.00/0.51 1: f^#(x, x, y) -> c_1() 0.00/0.51 0.00/0.51 2: f^#(x, y, y) -> c_2() 0.00/0.51 0.00/0.51 3: f^#(x, y, g(y)) -> c_3() 0.00/0.51 0.00/0.51 4: f^#(f(x, y, z), u, f(x, y, v)) -> c_4(f^#(x, y, f(z, u, v))) 0.00/0.51 -->_1 f^#(f(x, y, z), u, f(x, y, v)) -> 0.00/0.51 c_4(f^#(x, y, f(z, u, v))) :4 0.00/0.51 -->_1 f^#(x, y, g(y)) -> c_3() :3 0.00/0.51 -->_1 f^#(x, y, y) -> c_2() :2 0.00/0.51 0.00/0.51 5: f^#(g(x), x, y) -> c_5() 0.00/0.51 0.00/0.51 0.00/0.51 Only the nodes {1,2,3,5} are reachable from nodes {1,2,3,5} that 0.00/0.51 start derivation from marked basic terms. The nodes not reachable 0.00/0.51 are removed from the problem. 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Strict DPs: 0.00/0.51 { f^#(x, x, y) -> c_1() 0.00/0.51 , f^#(x, y, y) -> c_2() 0.00/0.51 , f^#(x, y, g(y)) -> c_3() 0.00/0.51 , f^#(g(x), x, y) -> c_5() } 0.00/0.51 Weak Trs: 0.00/0.51 { f(x, x, y) -> x 0.00/0.51 , f(x, y, y) -> y 0.00/0.51 , f(x, y, g(y)) -> x 0.00/0.51 , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) 0.00/0.51 , f(g(x), x, y) -> y } 0.00/0.51 Obligation: 0.00/0.51 innermost runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 We estimate the number of application of {1,2,3,4} by applications 0.00/0.51 of Pre({1,2,3,4}) = {}. Here rules are labeled as follows: 0.00/0.51 0.00/0.51 DPs: 0.00/0.51 { 1: f^#(x, x, y) -> c_1() 0.00/0.51 , 2: f^#(x, y, y) -> c_2() 0.00/0.51 , 3: f^#(x, y, g(y)) -> c_3() 0.00/0.51 , 4: f^#(g(x), x, y) -> c_5() } 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Weak DPs: 0.00/0.51 { f^#(x, x, y) -> c_1() 0.00/0.51 , f^#(x, y, y) -> c_2() 0.00/0.51 , f^#(x, y, g(y)) -> c_3() 0.00/0.51 , f^#(g(x), x, y) -> c_5() } 0.00/0.51 Weak Trs: 0.00/0.51 { f(x, x, y) -> x 0.00/0.51 , f(x, y, y) -> y 0.00/0.51 , f(x, y, g(y)) -> x 0.00/0.51 , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) 0.00/0.51 , f(g(x), x, y) -> y } 0.00/0.51 Obligation: 0.00/0.51 innermost runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.51 closed under successors. The DPs are removed. 0.00/0.51 0.00/0.51 { f^#(x, x, y) -> c_1() 0.00/0.51 , f^#(x, y, y) -> c_2() 0.00/0.51 , f^#(x, y, g(y)) -> c_3() 0.00/0.51 , f^#(g(x), x, y) -> c_5() } 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Weak Trs: 0.00/0.51 { f(x, x, y) -> x 0.00/0.51 , f(x, y, y) -> y 0.00/0.51 , f(x, y, g(y)) -> x 0.00/0.51 , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) 0.00/0.51 , f(g(x), x, y) -> y } 0.00/0.51 Obligation: 0.00/0.51 innermost runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 No rule is usable, rules are removed from the input problem. 0.00/0.51 0.00/0.51 We are left with following problem, upon which TcT provides the 0.00/0.51 certificate YES(O(1),O(1)). 0.00/0.51 0.00/0.51 Rules: Empty 0.00/0.51 Obligation: 0.00/0.51 innermost runtime complexity 0.00/0.51 Answer: 0.00/0.51 YES(O(1),O(1)) 0.00/0.51 0.00/0.51 Empty rules are trivially bounded 0.00/0.51 0.00/0.51 Hurray, we answered YES(O(1),O(1)) 0.00/0.51 EOF