YES(O(1),O(n^3)) 389.15/137.30 YES(O(1),O(n^3)) 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^3)). 389.15/137.30 389.15/137.30 Strict Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 389.15/137.30 , shuffle(nil()) -> nil() 389.15/137.30 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^3)) 389.15/137.30 389.15/137.30 We add the following dependency tuples: 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { app^#(nil(), y) -> c_1() 389.15/137.30 , app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , reverse^#(nil()) -> c_3() 389.15/137.30 , reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 389.15/137.30 , shuffle^#(nil()) -> c_5() 389.15/137.30 , shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 389.15/137.30 and mark the set of starting terms. 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^3)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { app^#(nil(), y) -> c_1() 389.15/137.30 , app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , reverse^#(nil()) -> c_3() 389.15/137.30 , reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 389.15/137.30 , shuffle^#(nil()) -> c_5() 389.15/137.30 , shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 389.15/137.30 , shuffle(nil()) -> nil() 389.15/137.30 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^3)) 389.15/137.30 389.15/137.30 We estimate the number of application of {1,3,5} by applications of 389.15/137.30 Pre({1,3,5}) = {2,4,6}. Here rules are labeled as follows: 389.15/137.30 389.15/137.30 DPs: 389.15/137.30 { 1: app^#(nil(), y) -> c_1() 389.15/137.30 , 2: app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , 3: reverse^#(nil()) -> c_3() 389.15/137.30 , 4: reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 389.15/137.30 , 5: shuffle^#(nil()) -> c_5() 389.15/137.30 , 6: shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^3)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 Weak DPs: 389.15/137.30 { app^#(nil(), y) -> c_1() 389.15/137.30 , reverse^#(nil()) -> c_3() 389.15/137.30 , shuffle^#(nil()) -> c_5() } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 389.15/137.30 , shuffle(nil()) -> nil() 389.15/137.30 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^3)) 389.15/137.30 389.15/137.30 The following weak DPs constitute a sub-graph of the DG that is 389.15/137.30 closed under successors. The DPs are removed. 389.15/137.30 389.15/137.30 { app^#(nil(), y) -> c_1() 389.15/137.30 , reverse^#(nil()) -> c_3() 389.15/137.30 , shuffle^#(nil()) -> c_5() } 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^3)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 389.15/137.30 , shuffle(nil()) -> nil() 389.15/137.30 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^3)) 389.15/137.30 389.15/137.30 We replace rewrite rules by usable rules: 389.15/137.30 389.15/137.30 Weak Usable Rules: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^3)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^3)) 389.15/137.30 389.15/137.30 We decompose the input problem according to the dependency graph 389.15/137.30 into the upper component 389.15/137.30 389.15/137.30 { shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 389.15/137.30 and lower component 389.15/137.30 389.15/137.30 { app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 389.15/137.30 389.15/137.30 Further, following extension rules are added to the lower 389.15/137.30 component. 389.15/137.30 389.15/137.30 { shuffle^#(add(n, x)) -> reverse^#(x) 389.15/137.30 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 389.15/137.30 389.15/137.30 TcT solves the upper component with certificate YES(O(1),O(n^1)). 389.15/137.30 389.15/137.30 Sub-proof: 389.15/137.30 ---------- 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^1)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^1)) 389.15/137.30 389.15/137.30 We use the processor 'matrix interpretation of dimension 1' to 389.15/137.30 orient following rules strictly. 389.15/137.30 389.15/137.30 DPs: 389.15/137.30 { 1: shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 389.15/137.30 Sub-proof: 389.15/137.30 ---------- 389.15/137.30 The following argument positions are usable: 389.15/137.30 Uargs(c_6) = {1} 389.15/137.30 389.15/137.30 TcT has computed the following constructor-based matrix 389.15/137.30 interpretation satisfying not(EDA). 389.15/137.30 389.15/137.30 [app](x1, x2) = [1] x1 + [1] x2 + [0] 389.15/137.30 389.15/137.30 [nil] = [0] 389.15/137.30 389.15/137.30 [add](x1, x2) = [1] x1 + [1] x2 + [2] 389.15/137.30 389.15/137.30 [reverse](x1) = [1] x1 + [0] 389.15/137.30 389.15/137.30 [reverse^#](x1) = [7] x1 + [7] 389.15/137.30 389.15/137.30 [shuffle^#](x1) = [4] x1 + [0] 389.15/137.30 389.15/137.30 [c_6](x1, x2) = [1] x1 + [1] 389.15/137.30 389.15/137.30 The order satisfies the following ordering constraints: 389.15/137.30 389.15/137.30 [app(nil(), y)] = [1] y + [0] 389.15/137.30 >= [1] y + [0] 389.15/137.30 = [y] 389.15/137.30 389.15/137.30 [app(add(n, x), y)] = [1] y + [1] n + [1] x + [2] 389.15/137.30 >= [1] y + [1] n + [1] x + [2] 389.15/137.30 = [add(n, app(x, y))] 389.15/137.30 389.15/137.30 [reverse(nil())] = [0] 389.15/137.30 >= [0] 389.15/137.30 = [nil()] 389.15/137.30 389.15/137.30 [reverse(add(n, x))] = [1] n + [1] x + [2] 389.15/137.30 >= [1] n + [1] x + [2] 389.15/137.30 = [app(reverse(x), add(n, nil()))] 389.15/137.30 389.15/137.30 [shuffle^#(add(n, x))] = [4] n + [4] x + [8] 389.15/137.30 > [4] x + [1] 389.15/137.30 = [c_6(shuffle^#(reverse(x)), reverse^#(x))] 389.15/137.30 389.15/137.30 389.15/137.30 The strictly oriented rules are moved into the weak component. 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(1)). 389.15/137.30 389.15/137.30 Weak DPs: 389.15/137.30 { shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(1)) 389.15/137.30 389.15/137.30 The following weak DPs constitute a sub-graph of the DG that is 389.15/137.30 closed under successors. The DPs are removed. 389.15/137.30 389.15/137.30 { shuffle^#(add(n, x)) -> 389.15/137.30 c_6(shuffle^#(reverse(x)), reverse^#(x)) } 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(1)). 389.15/137.30 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(1)) 389.15/137.30 389.15/137.30 No rule is usable, rules are removed from the input problem. 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(1)). 389.15/137.30 389.15/137.30 Rules: Empty 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(1)) 389.15/137.30 389.15/137.30 Empty rules are trivially bounded 389.15/137.30 389.15/137.30 We return to the main proof. 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^2)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 389.15/137.30 Weak DPs: 389.15/137.30 { shuffle^#(add(n, x)) -> reverse^#(x) 389.15/137.30 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^2)) 389.15/137.30 389.15/137.30 We use the processor 'polynomial interpretation' to orient 389.15/137.30 following rules strictly. 389.15/137.30 389.15/137.30 DPs: 389.15/137.30 { 1: app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , 3: shuffle^#(add(n, x)) -> reverse^#(x) } 389.15/137.30 Trs: { reverse(nil()) -> nil() } 389.15/137.30 389.15/137.30 Sub-proof: 389.15/137.30 ---------- 389.15/137.30 We consider the following typing: 389.15/137.30 389.15/137.30 app :: (d,d) -> d 389.15/137.30 nil :: d 389.15/137.30 add :: (a,d) -> d 389.15/137.30 reverse :: d -> d 389.15/137.30 app^# :: (d,d) -> b 389.15/137.30 c_2 :: b -> b 389.15/137.30 reverse^# :: d -> c 389.15/137.30 c_4 :: (b,c) -> c 389.15/137.30 shuffle^# :: d -> c 389.15/137.30 389.15/137.30 The following argument positions are considered usable: 389.15/137.30 389.15/137.30 Uargs(c_2) = {1}, Uargs(c_4) = {1, 2} 389.15/137.30 389.15/137.30 TcT has computed the following constructor-restricted 389.15/137.30 typedpolynomial interpretation. 389.15/137.30 389.15/137.30 [app](x1, x2) = x1 + x2 389.15/137.30 389.15/137.30 [nil]() = 0 389.15/137.30 389.15/137.30 [add](x1, x2) = 1 + x2 389.15/137.30 389.15/137.30 [reverse](x1) = 1 + x1 389.15/137.30 389.15/137.30 [app^#](x1, x2) = x1 + x1*x2 389.15/137.30 389.15/137.30 [c_2](x1) = x1 389.15/137.30 389.15/137.30 [reverse^#](x1) = 1 + 2*x1 + x1^2 389.15/137.30 389.15/137.30 [c_4](x1, x2) = 1 + x1 + x2 389.15/137.30 389.15/137.30 [shuffle^#](x1) = 2 + 2*x1 + x1^2 389.15/137.30 389.15/137.30 389.15/137.30 This order satisfies the following ordering constraints. 389.15/137.30 389.15/137.30 [app(nil(), y)] = y 389.15/137.30 >= y 389.15/137.30 = [y] 389.15/137.30 389.15/137.30 [app(add(n, x), y)] = 1 + x + y 389.15/137.30 >= 1 + x + y 389.15/137.30 = [add(n, app(x, y))] 389.15/137.30 389.15/137.30 [reverse(nil())] = 1 389.15/137.30 > 389.15/137.30 = [nil()] 389.15/137.30 389.15/137.30 [reverse(add(n, x))] = 2 + x 389.15/137.30 >= 2 + x 389.15/137.30 = [app(reverse(x), add(n, nil()))] 389.15/137.30 389.15/137.30 [app^#(add(n, x), y)] = 1 + x + y + x*y 389.15/137.30 > x + x*y 389.15/137.30 = [c_2(app^#(x, y))] 389.15/137.30 389.15/137.30 [reverse^#(add(n, x))] = 4 + 4*x + x^2 389.15/137.30 >= 4 + 4*x + x^2 389.15/137.30 = [c_4(app^#(reverse(x), add(n, nil())), reverse^#(x))] 389.15/137.30 389.15/137.30 [shuffle^#(add(n, x))] = 5 + 4*x + x^2 389.15/137.30 > 1 + 2*x + x^2 389.15/137.30 = [reverse^#(x)] 389.15/137.30 389.15/137.30 [shuffle^#(add(n, x))] = 5 + 4*x + x^2 389.15/137.30 >= 5 + 4*x + x^2 389.15/137.30 = [shuffle^#(reverse(x))] 389.15/137.30 389.15/137.30 389.15/137.30 The strictly oriented rules are moved into the weak component. 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^1)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 389.15/137.30 Weak DPs: 389.15/137.30 { app^#(add(n, x), y) -> c_2(app^#(x, y)) 389.15/137.30 , shuffle^#(add(n, x)) -> reverse^#(x) 389.15/137.30 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^1)) 389.15/137.30 389.15/137.30 The following weak DPs constitute a sub-graph of the DG that is 389.15/137.30 closed under successors. The DPs are removed. 389.15/137.30 389.15/137.30 { app^#(add(n, x), y) -> c_2(app^#(x, y)) } 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^1)). 389.15/137.30 389.15/137.30 Strict DPs: 389.15/137.30 { reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 389.15/137.30 Weak DPs: 389.15/137.30 { shuffle^#(add(n, x)) -> reverse^#(x) 389.15/137.30 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^1)) 389.15/137.30 389.15/137.30 Due to missing edges in the dependency-graph, the right-hand sides 389.15/137.30 of following rules could be simplified: 389.15/137.30 389.15/137.30 { reverse^#(add(n, x)) -> 389.15/137.30 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(n^1)). 389.15/137.30 389.15/137.30 Strict DPs: { reverse^#(add(n, x)) -> c_1(reverse^#(x)) } 389.15/137.30 Weak DPs: 389.15/137.30 { shuffle^#(add(n, x)) -> c_2(reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> c_3(shuffle^#(reverse(x))) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(n^1)) 389.15/137.30 389.15/137.30 We use the processor 'matrix interpretation of dimension 1' to 389.15/137.30 orient following rules strictly. 389.15/137.30 389.15/137.30 DPs: 389.15/137.30 { 1: reverse^#(add(n, x)) -> c_1(reverse^#(x)) 389.15/137.30 , 2: shuffle^#(add(n, x)) -> c_2(reverse^#(x)) 389.15/137.30 , 3: shuffle^#(add(n, x)) -> c_3(shuffle^#(reverse(x))) } 389.15/137.30 389.15/137.30 Sub-proof: 389.15/137.30 ---------- 389.15/137.30 The following argument positions are usable: 389.15/137.30 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1} 389.15/137.30 389.15/137.30 TcT has computed the following constructor-based matrix 389.15/137.30 interpretation satisfying not(EDA). 389.15/137.30 389.15/137.30 [app](x1, x2) = [1] x1 + [1] x2 + [0] 389.15/137.30 389.15/137.30 [nil] = [0] 389.15/137.30 389.15/137.30 [add](x1, x2) = [1] x1 + [1] x2 + [2] 389.15/137.30 389.15/137.30 [reverse](x1) = [1] x1 + [0] 389.15/137.30 389.15/137.30 [app^#](x1, x2) = [7] x1 + [7] x2 + [0] 389.15/137.30 389.15/137.30 [c_2](x1) = [7] x1 + [0] 389.15/137.30 389.15/137.30 [reverse^#](x1) = [4] x1 + [0] 389.15/137.30 389.15/137.30 [c_4](x1, x2) = [7] x1 + [7] x2 + [0] 389.15/137.30 389.15/137.30 [shuffle^#](x1) = [4] x1 + [0] 389.15/137.30 389.15/137.30 [c] = [0] 389.15/137.30 389.15/137.30 [c_1](x1) = [1] x1 + [1] 389.15/137.30 389.15/137.30 [c_2](x1) = [1] x1 + [5] 389.15/137.30 389.15/137.30 [c_3](x1) = [1] x1 + [7] 389.15/137.30 389.15/137.30 The order satisfies the following ordering constraints: 389.15/137.30 389.15/137.30 [app(nil(), y)] = [1] y + [0] 389.15/137.30 >= [1] y + [0] 389.15/137.30 = [y] 389.15/137.30 389.15/137.30 [app(add(n, x), y)] = [1] y + [1] n + [1] x + [2] 389.15/137.30 >= [1] y + [1] n + [1] x + [2] 389.15/137.30 = [add(n, app(x, y))] 389.15/137.30 389.15/137.30 [reverse(nil())] = [0] 389.15/137.30 >= [0] 389.15/137.30 = [nil()] 389.15/137.30 389.15/137.30 [reverse(add(n, x))] = [1] n + [1] x + [2] 389.15/137.30 >= [1] n + [1] x + [2] 389.15/137.30 = [app(reverse(x), add(n, nil()))] 389.15/137.30 389.15/137.30 [reverse^#(add(n, x))] = [4] n + [4] x + [8] 389.15/137.30 > [4] x + [1] 389.15/137.30 = [c_1(reverse^#(x))] 389.15/137.30 389.15/137.30 [shuffle^#(add(n, x))] = [4] n + [4] x + [8] 389.15/137.30 > [4] x + [5] 389.15/137.30 = [c_2(reverse^#(x))] 389.15/137.30 389.15/137.30 [shuffle^#(add(n, x))] = [4] n + [4] x + [8] 389.15/137.30 > [4] x + [7] 389.15/137.30 = [c_3(shuffle^#(reverse(x)))] 389.15/137.30 389.15/137.30 389.15/137.30 The strictly oriented rules are moved into the weak component. 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(1)). 389.15/137.30 389.15/137.30 Weak DPs: 389.15/137.30 { reverse^#(add(n, x)) -> c_1(reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> c_2(reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> c_3(shuffle^#(reverse(x))) } 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(1)) 389.15/137.30 389.15/137.30 The following weak DPs constitute a sub-graph of the DG that is 389.15/137.30 closed under successors. The DPs are removed. 389.15/137.30 389.15/137.30 { reverse^#(add(n, x)) -> c_1(reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> c_2(reverse^#(x)) 389.15/137.30 , shuffle^#(add(n, x)) -> c_3(shuffle^#(reverse(x))) } 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(1)). 389.15/137.30 389.15/137.30 Weak Trs: 389.15/137.30 { app(nil(), y) -> y 389.15/137.30 , app(add(n, x), y) -> add(n, app(x, y)) 389.15/137.30 , reverse(nil()) -> nil() 389.15/137.30 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(1)) 389.15/137.30 389.15/137.30 No rule is usable, rules are removed from the input problem. 389.15/137.30 389.15/137.30 We are left with following problem, upon which TcT provides the 389.15/137.30 certificate YES(O(1),O(1)). 389.15/137.30 389.15/137.30 Rules: Empty 389.15/137.30 Obligation: 389.15/137.30 innermost runtime complexity 389.15/137.30 Answer: 389.15/137.30 YES(O(1),O(1)) 389.15/137.30 389.15/137.30 Empty rules are trivially bounded 389.15/137.30 389.15/137.30 Hurray, we answered YES(O(1),O(n^3)) 389.15/137.35 EOF