YES(O(1),O(n^3)) 441.38/149.44 YES(O(1),O(n^3)) 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^3)). 441.38/149.44 441.38/149.44 Strict Trs: 441.38/149.44 { shuffle(Cons(x, xs)) -> Cons(x, shuffle(reverse(xs))) 441.38/149.44 , shuffle(Nil()) -> Nil() 441.38/149.44 , reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys 441.38/149.44 , goal(xs) -> shuffle(xs) } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^3)) 441.38/149.44 441.38/149.44 We add the following dependency tuples: 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 , shuffle^#(Nil()) -> c_2() 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , reverse^#(Nil()) -> c_4() 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) 441.38/149.44 , append^#(Nil(), ys) -> c_6() 441.38/149.44 , goal^#(xs) -> c_7(shuffle^#(xs)) } 441.38/149.44 441.38/149.44 and mark the set of starting terms. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^3)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 , shuffle^#(Nil()) -> c_2() 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , reverse^#(Nil()) -> c_4() 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) 441.38/149.44 , append^#(Nil(), ys) -> c_6() 441.38/149.44 , goal^#(xs) -> c_7(shuffle^#(xs)) } 441.38/149.44 Weak Trs: 441.38/149.44 { shuffle(Cons(x, xs)) -> Cons(x, shuffle(reverse(xs))) 441.38/149.44 , shuffle(Nil()) -> Nil() 441.38/149.44 , reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys 441.38/149.44 , goal(xs) -> shuffle(xs) } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^3)) 441.38/149.44 441.38/149.44 We estimate the number of application of {2,4,6} by applications of 441.38/149.44 Pre({2,4,6}) = {1,3,5,7}. Here rules are labeled as follows: 441.38/149.44 441.38/149.44 DPs: 441.38/149.44 { 1: shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 , 2: shuffle^#(Nil()) -> c_2() 441.38/149.44 , 3: reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , 4: reverse^#(Nil()) -> c_4() 441.38/149.44 , 5: append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) 441.38/149.44 , 6: append^#(Nil(), ys) -> c_6() 441.38/149.44 , 7: goal^#(xs) -> c_7(shuffle^#(xs)) } 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^3)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) 441.38/149.44 , goal^#(xs) -> c_7(shuffle^#(xs)) } 441.38/149.44 Weak DPs: 441.38/149.44 { shuffle^#(Nil()) -> c_2() 441.38/149.44 , reverse^#(Nil()) -> c_4() 441.38/149.44 , append^#(Nil(), ys) -> c_6() } 441.38/149.44 Weak Trs: 441.38/149.44 { shuffle(Cons(x, xs)) -> Cons(x, shuffle(reverse(xs))) 441.38/149.44 , shuffle(Nil()) -> Nil() 441.38/149.44 , reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys 441.38/149.44 , goal(xs) -> shuffle(xs) } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^3)) 441.38/149.44 441.38/149.44 The following weak DPs constitute a sub-graph of the DG that is 441.38/149.44 closed under successors. The DPs are removed. 441.38/149.44 441.38/149.44 { shuffle^#(Nil()) -> c_2() 441.38/149.44 , reverse^#(Nil()) -> c_4() 441.38/149.44 , append^#(Nil(), ys) -> c_6() } 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^3)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) 441.38/149.44 , goal^#(xs) -> c_7(shuffle^#(xs)) } 441.38/149.44 Weak Trs: 441.38/149.44 { shuffle(Cons(x, xs)) -> Cons(x, shuffle(reverse(xs))) 441.38/149.44 , shuffle(Nil()) -> Nil() 441.38/149.44 , reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys 441.38/149.44 , goal(xs) -> shuffle(xs) } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^3)) 441.38/149.44 441.38/149.44 Consider the dependency graph 441.38/149.44 441.38/149.44 1: shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 -->_2 reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) :2 441.38/149.44 -->_1 shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) :1 441.38/149.44 441.38/149.44 2: reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 -->_1 append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) :3 441.38/149.44 -->_2 reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) :2 441.38/149.44 441.38/149.44 3: append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) 441.38/149.44 -->_1 append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) :3 441.38/149.44 441.38/149.44 4: goal^#(xs) -> c_7(shuffle^#(xs)) 441.38/149.44 -->_1 shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) :1 441.38/149.44 441.38/149.44 441.38/149.44 Following roots of the dependency graph are removed, as the 441.38/149.44 considered set of starting terms is closed under reduction with 441.38/149.44 respect to these rules (modulo compound contexts). 441.38/149.44 441.38/149.44 { goal^#(xs) -> c_7(shuffle^#(xs)) } 441.38/149.44 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^3)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 Weak Trs: 441.38/149.44 { shuffle(Cons(x, xs)) -> Cons(x, shuffle(reverse(xs))) 441.38/149.44 , shuffle(Nil()) -> Nil() 441.38/149.44 , reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys 441.38/149.44 , goal(xs) -> shuffle(xs) } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^3)) 441.38/149.44 441.38/149.44 We replace rewrite rules by usable rules: 441.38/149.44 441.38/149.44 Weak Usable Rules: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^3)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^3)) 441.38/149.44 441.38/149.44 We decompose the input problem according to the dependency graph 441.38/149.44 into the upper component 441.38/149.44 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) } 441.38/149.44 441.38/149.44 and lower component 441.38/149.44 441.38/149.44 { reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 441.38/149.44 Further, following extension rules are added to the lower 441.38/149.44 component. 441.38/149.44 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) } 441.38/149.44 441.38/149.44 TcT solves the upper component with certificate YES(O(1),O(n^1)). 441.38/149.44 441.38/149.44 Sub-proof: 441.38/149.44 ---------- 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^1)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^1)) 441.38/149.44 441.38/149.44 We use the processor 'matrix interpretation of dimension 1' to 441.38/149.44 orient following rules strictly. 441.38/149.44 441.38/149.44 DPs: 441.38/149.44 { 1: shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) } 441.38/149.44 441.38/149.44 Sub-proof: 441.38/149.44 ---------- 441.38/149.44 The following argument positions are usable: 441.38/149.44 Uargs(c_1) = {1} 441.38/149.44 441.38/149.44 TcT has computed the following constructor-based matrix 441.38/149.44 interpretation satisfying not(EDA). 441.38/149.44 441.38/149.44 [Cons](x1, x2) = [1] x1 + [1] x2 + [2] 441.38/149.44 441.38/149.44 [reverse](x1) = [1] x1 + [0] 441.38/149.44 441.38/149.44 [append](x1, x2) = [1] x1 + [1] x2 + [0] 441.38/149.44 441.38/149.44 [Nil] = [0] 441.38/149.44 441.38/149.44 [shuffle^#](x1) = [1] x1 + [2] 441.38/149.44 441.38/149.44 [c_1](x1, x2) = [1] x1 + [0] 441.38/149.44 441.38/149.44 [reverse^#](x1) = [7] x1 + [7] 441.38/149.44 441.38/149.44 The order satisfies the following ordering constraints: 441.38/149.44 441.38/149.44 [reverse(Cons(x, xs))] = [1] x + [1] xs + [2] 441.38/149.44 >= [1] x + [1] xs + [2] 441.38/149.44 = [append(reverse(xs), Cons(x, Nil()))] 441.38/149.44 441.38/149.44 [reverse(Nil())] = [0] 441.38/149.44 >= [0] 441.38/149.44 = [Nil()] 441.38/149.44 441.38/149.44 [append(Cons(x, xs), ys)] = [1] x + [1] xs + [1] ys + [2] 441.38/149.44 >= [1] x + [1] xs + [1] ys + [2] 441.38/149.44 = [Cons(x, append(xs, ys))] 441.38/149.44 441.38/149.44 [append(Nil(), ys)] = [1] ys + [0] 441.38/149.44 >= [1] ys + [0] 441.38/149.44 = [ys] 441.38/149.44 441.38/149.44 [shuffle^#(Cons(x, xs))] = [1] x + [1] xs + [4] 441.38/149.44 > [1] xs + [2] 441.38/149.44 = [c_1(shuffle^#(reverse(xs)), reverse^#(xs))] 441.38/149.44 441.38/149.44 441.38/149.44 The strictly oriented rules are moved into the weak component. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Weak DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 The following weak DPs constitute a sub-graph of the DG that is 441.38/149.44 closed under successors. The DPs are removed. 441.38/149.44 441.38/149.44 { shuffle^#(Cons(x, xs)) -> 441.38/149.44 c_1(shuffle^#(reverse(xs)), reverse^#(xs)) } 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 No rule is usable, rules are removed from the input problem. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Rules: Empty 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 Empty rules are trivially bounded 441.38/149.44 441.38/149.44 We return to the main proof. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^2)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 Weak DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^2)) 441.38/149.44 441.38/149.44 We decompose the input problem according to the dependency graph 441.38/149.44 into the upper component 441.38/149.44 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) } 441.38/149.44 441.38/149.44 and lower component 441.38/149.44 441.38/149.44 { append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 441.38/149.44 Further, following extension rules are added to the lower 441.38/149.44 component. 441.38/149.44 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> append^#(reverse(xs), Cons(x, Nil())) } 441.38/149.44 441.38/149.44 TcT solves the upper component with certificate YES(O(1),O(n^1)). 441.38/149.44 441.38/149.44 Sub-proof: 441.38/149.44 ---------- 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^1)). 441.38/149.44 441.38/149.44 Strict DPs: 441.38/149.44 { reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) } 441.38/149.44 Weak DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^1)) 441.38/149.44 441.38/149.44 We use the processor 'matrix interpretation of dimension 1' to 441.38/149.44 orient following rules strictly. 441.38/149.44 441.38/149.44 DPs: 441.38/149.44 { 1: reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) 441.38/149.44 , 2: shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , 3: shuffle^#(Cons(x, xs)) -> reverse^#(xs) } 441.38/149.44 441.38/149.44 Sub-proof: 441.38/149.44 ---------- 441.38/149.44 The following argument positions are usable: 441.38/149.44 Uargs(c_3) = {1, 2} 441.38/149.44 441.38/149.44 TcT has computed the following constructor-based matrix 441.38/149.44 interpretation satisfying not(EDA). 441.38/149.44 441.38/149.44 [Cons](x1, x2) = [1] x1 + [1] x2 + [1] 441.38/149.44 441.38/149.44 [reverse](x1) = [1] x1 + [0] 441.38/149.44 441.38/149.44 [append](x1, x2) = [1] x1 + [1] x2 + [0] 441.38/149.44 441.38/149.44 [Nil] = [0] 441.38/149.44 441.38/149.44 [shuffle^#](x1) = [2] x1 + [2] 441.38/149.44 441.38/149.44 [reverse^#](x1) = [2] x1 + [0] 441.38/149.44 441.38/149.44 [c_3](x1, x2) = [2] x1 + [1] x2 + [1] 441.38/149.44 441.38/149.44 [append^#](x1, x2) = [0] 441.38/149.44 441.38/149.44 The order satisfies the following ordering constraints: 441.38/149.44 441.38/149.44 [reverse(Cons(x, xs))] = [1] x + [1] xs + [1] 441.38/149.44 >= [1] x + [1] xs + [1] 441.38/149.44 = [append(reverse(xs), Cons(x, Nil()))] 441.38/149.44 441.38/149.44 [reverse(Nil())] = [0] 441.38/149.44 >= [0] 441.38/149.44 = [Nil()] 441.38/149.44 441.38/149.44 [append(Cons(x, xs), ys)] = [1] x + [1] xs + [1] ys + [1] 441.38/149.44 >= [1] x + [1] xs + [1] ys + [1] 441.38/149.44 = [Cons(x, append(xs, ys))] 441.38/149.44 441.38/149.44 [append(Nil(), ys)] = [1] ys + [0] 441.38/149.44 >= [1] ys + [0] 441.38/149.44 = [ys] 441.38/149.44 441.38/149.44 [shuffle^#(Cons(x, xs))] = [2] x + [2] xs + [4] 441.38/149.44 > [2] xs + [2] 441.38/149.44 = [shuffle^#(reverse(xs))] 441.38/149.44 441.38/149.44 [shuffle^#(Cons(x, xs))] = [2] x + [2] xs + [4] 441.38/149.44 > [2] xs + [0] 441.38/149.44 = [reverse^#(xs)] 441.38/149.44 441.38/149.44 [reverse^#(Cons(x, xs))] = [2] x + [2] xs + [2] 441.38/149.44 > [2] xs + [1] 441.38/149.44 = [c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs))] 441.38/149.44 441.38/149.44 441.38/149.44 The strictly oriented rules are moved into the weak component. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Weak DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 The following weak DPs constitute a sub-graph of the DG that is 441.38/149.44 closed under successors. The DPs are removed. 441.38/149.44 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> 441.38/149.44 c_3(append^#(reverse(xs), Cons(x, Nil())), reverse^#(xs)) } 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 No rule is usable, rules are removed from the input problem. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Rules: Empty 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 Empty rules are trivially bounded 441.38/149.44 441.38/149.44 We return to the main proof. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(n^1)). 441.38/149.44 441.38/149.44 Strict DPs: { append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 Weak DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> append^#(reverse(xs), Cons(x, Nil())) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(n^1)) 441.38/149.44 441.38/149.44 We use the processor 'matrix interpretation of dimension 1' to 441.38/149.44 orient following rules strictly. 441.38/149.44 441.38/149.44 DPs: 441.38/149.44 { 1: append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) 441.38/149.44 , 2: shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , 3: shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , 4: reverse^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , 5: reverse^#(Cons(x, xs)) -> 441.38/149.44 append^#(reverse(xs), Cons(x, Nil())) } 441.38/149.44 441.38/149.44 Sub-proof: 441.38/149.44 ---------- 441.38/149.44 The following argument positions are usable: 441.38/149.44 Uargs(c_5) = {1} 441.38/149.44 441.38/149.44 TcT has computed the following constructor-based matrix 441.38/149.44 interpretation satisfying not(EDA). 441.38/149.44 441.38/149.44 [Cons](x1, x2) = [1] x1 + [1] x2 + [2] 441.38/149.44 441.38/149.44 [reverse](x1) = [1] x1 + [0] 441.38/149.44 441.38/149.44 [append](x1, x2) = [1] x1 + [1] x2 + [0] 441.38/149.44 441.38/149.44 [Nil] = [0] 441.38/149.44 441.38/149.44 [shuffle^#](x1) = [4] x1 + [0] 441.38/149.44 441.38/149.44 [reverse^#](x1) = [4] x1 + [0] 441.38/149.44 441.38/149.44 [append^#](x1, x2) = [4] x1 + [0] 441.38/149.44 441.38/149.44 [c_5](x1) = [1] x1 + [1] 441.38/149.44 441.38/149.44 The order satisfies the following ordering constraints: 441.38/149.44 441.38/149.44 [reverse(Cons(x, xs))] = [1] x + [1] xs + [2] 441.38/149.44 >= [1] x + [1] xs + [2] 441.38/149.44 = [append(reverse(xs), Cons(x, Nil()))] 441.38/149.44 441.38/149.44 [reverse(Nil())] = [0] 441.38/149.44 >= [0] 441.38/149.44 = [Nil()] 441.38/149.44 441.38/149.44 [append(Cons(x, xs), ys)] = [1] x + [1] xs + [1] ys + [2] 441.38/149.44 >= [1] x + [1] xs + [1] ys + [2] 441.38/149.44 = [Cons(x, append(xs, ys))] 441.38/149.44 441.38/149.44 [append(Nil(), ys)] = [1] ys + [0] 441.38/149.44 >= [1] ys + [0] 441.38/149.44 = [ys] 441.38/149.44 441.38/149.44 [shuffle^#(Cons(x, xs))] = [4] x + [4] xs + [8] 441.38/149.44 > [4] xs + [0] 441.38/149.44 = [shuffle^#(reverse(xs))] 441.38/149.44 441.38/149.44 [shuffle^#(Cons(x, xs))] = [4] x + [4] xs + [8] 441.38/149.44 > [4] xs + [0] 441.38/149.44 = [reverse^#(xs)] 441.38/149.44 441.38/149.44 [reverse^#(Cons(x, xs))] = [4] x + [4] xs + [8] 441.38/149.44 > [4] xs + [0] 441.38/149.44 = [reverse^#(xs)] 441.38/149.44 441.38/149.44 [reverse^#(Cons(x, xs))] = [4] x + [4] xs + [8] 441.38/149.44 > [4] xs + [0] 441.38/149.44 = [append^#(reverse(xs), Cons(x, Nil()))] 441.38/149.44 441.38/149.44 [append^#(Cons(x, xs), ys)] = [4] x + [4] xs + [8] 441.38/149.44 > [4] xs + [1] 441.38/149.44 = [c_5(append^#(xs, ys))] 441.38/149.44 441.38/149.44 441.38/149.44 The strictly oriented rules are moved into the weak component. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Weak DPs: 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> append^#(reverse(xs), Cons(x, Nil())) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 The following weak DPs constitute a sub-graph of the DG that is 441.38/149.44 closed under successors. The DPs are removed. 441.38/149.44 441.38/149.44 { shuffle^#(Cons(x, xs)) -> shuffle^#(reverse(xs)) 441.38/149.44 , shuffle^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> reverse^#(xs) 441.38/149.44 , reverse^#(Cons(x, xs)) -> append^#(reverse(xs), Cons(x, Nil())) 441.38/149.44 , append^#(Cons(x, xs), ys) -> c_5(append^#(xs, ys)) } 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Weak Trs: 441.38/149.44 { reverse(Cons(x, xs)) -> append(reverse(xs), Cons(x, Nil())) 441.38/149.44 , reverse(Nil()) -> Nil() 441.38/149.44 , append(Cons(x, xs), ys) -> Cons(x, append(xs, ys)) 441.38/149.44 , append(Nil(), ys) -> ys } 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 No rule is usable, rules are removed from the input problem. 441.38/149.44 441.38/149.44 We are left with following problem, upon which TcT provides the 441.38/149.44 certificate YES(O(1),O(1)). 441.38/149.44 441.38/149.44 Rules: Empty 441.38/149.44 Obligation: 441.38/149.44 innermost runtime complexity 441.38/149.44 Answer: 441.38/149.44 YES(O(1),O(1)) 441.38/149.44 441.38/149.44 Empty rules are trivially bounded 441.38/149.44 441.38/149.44 Hurray, we answered YES(O(1),O(n^3)) 441.58/149.50 EOF