YES(O(1),O(n^2)) 559.50/148.06 YES(O(1),O(n^2)) 559.50/148.06 559.50/148.06 We are left with following problem, upon which TcT provides the 559.50/148.06 certificate YES(O(1),O(n^2)). 559.50/148.06 559.50/148.06 Strict Trs: 559.50/148.06 { part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.06 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.06 , app(Nil(), ys) -> ys 559.50/148.06 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.06 , quicksort(Nil()) -> Nil() 559.50/148.06 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.06 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.06 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.06 , qs(x', Cons(x, xs)) -> 559.50/148.06 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.06 , notEmpty(Nil()) -> False() 559.50/148.06 , notEmpty(Cons(x, xs)) -> True() } 559.50/148.06 Weak Trs: 559.50/148.06 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part(x', xs, Cons(x, xs1), xs2) 559.50/148.06 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.06 x', 559.50/148.06 Cons(x, xs), 559.50/148.06 xs1, 559.50/148.06 xs2) 559.50/148.06 , >(S(x), S(y)) -> >(x, y) 559.50/148.06 , >(S(x), 0()) -> True() 559.50/148.06 , >(0(), y) -> False() 559.50/148.06 , <(x, 0()) -> False() 559.50/148.06 , <(S(x), S(y)) -> <(x, y) 559.50/148.06 , <(0(), S(y)) -> True() } 559.50/148.06 Obligation: 559.50/148.06 innermost runtime complexity 559.50/148.06 Answer: 559.50/148.06 YES(O(1),O(n^2)) 559.50/148.06 559.50/148.06 We add the following dependency tuples: 559.50/148.06 559.50/148.06 Strict DPs: 559.50/148.06 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.06 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2), 559.50/148.06 >^#(x', x)) 559.50/148.06 , app^#(Nil(), ys) -> c_3() 559.50/148.06 , app^#(Cons(x, xs), ys) -> c_4(app^#(xs, ys)) 559.50/148.06 , quicksort^#(Nil()) -> c_5() 559.50/148.06 , quicksort^#(Cons(x, Nil())) -> c_6() 559.50/148.06 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.06 c_7(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.06 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.06 , qs^#(x', Cons(x, xs)) -> 559.50/148.06 c_8(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.06 quicksort^#(xs)) 559.50/148.06 , notEmpty^#(Nil()) -> c_9() 559.50/148.06 , notEmpty^#(Cons(x, xs)) -> c_10() } 559.50/148.06 Weak DPs: 559.50/148.06 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_11(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.06 , part[Ite][True][Ite]^#(False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_12(<^#(x', x)) 559.50/148.06 , >^#(S(x), S(y)) -> c_13(>^#(x, y)) 559.50/148.06 , >^#(S(x), 0()) -> c_14() 559.50/148.06 , >^#(0(), y) -> c_15() 559.50/148.06 , <^#(x, 0()) -> c_16() 559.50/148.06 , <^#(S(x), S(y)) -> c_17(<^#(x, y)) 559.50/148.06 , <^#(0(), S(y)) -> c_18() } 559.50/148.06 559.50/148.06 and mark the set of starting terms. 559.50/148.06 559.50/148.06 We are left with following problem, upon which TcT provides the 559.50/148.06 certificate YES(O(1),O(n^2)). 559.50/148.06 559.50/148.06 Strict DPs: 559.50/148.06 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.06 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2), 559.50/148.06 >^#(x', x)) 559.50/148.06 , app^#(Nil(), ys) -> c_3() 559.50/148.06 , app^#(Cons(x, xs), ys) -> c_4(app^#(xs, ys)) 559.50/148.06 , quicksort^#(Nil()) -> c_5() 559.50/148.06 , quicksort^#(Cons(x, Nil())) -> c_6() 559.50/148.06 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.06 c_7(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.06 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.06 , qs^#(x', Cons(x, xs)) -> 559.50/148.06 c_8(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.06 quicksort^#(xs)) 559.50/148.06 , notEmpty^#(Nil()) -> c_9() 559.50/148.06 , notEmpty^#(Cons(x, xs)) -> c_10() } 559.50/148.06 Weak DPs: 559.50/148.06 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_11(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.06 , part[Ite][True][Ite]^#(False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_12(<^#(x', x)) 559.50/148.06 , >^#(S(x), S(y)) -> c_13(>^#(x, y)) 559.50/148.06 , >^#(S(x), 0()) -> c_14() 559.50/148.06 , >^#(0(), y) -> c_15() 559.50/148.06 , <^#(x, 0()) -> c_16() 559.50/148.06 , <^#(S(x), S(y)) -> c_17(<^#(x, y)) 559.50/148.06 , <^#(0(), S(y)) -> c_18() } 559.50/148.06 Weak Trs: 559.50/148.06 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part(x', xs, Cons(x, xs1), xs2) 559.50/148.06 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.06 x', 559.50/148.06 Cons(x, xs), 559.50/148.06 xs1, 559.50/148.06 xs2) 559.50/148.06 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.06 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.06 , app(Nil(), ys) -> ys 559.50/148.06 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.06 , quicksort(Nil()) -> Nil() 559.50/148.06 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.06 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.06 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.06 , qs(x', Cons(x, xs)) -> 559.50/148.06 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.06 , >(S(x), S(y)) -> >(x, y) 559.50/148.06 , >(S(x), 0()) -> True() 559.50/148.06 , >(0(), y) -> False() 559.50/148.06 , <(x, 0()) -> False() 559.50/148.06 , <(S(x), S(y)) -> <(x, y) 559.50/148.06 , <(0(), S(y)) -> True() 559.50/148.06 , notEmpty(Nil()) -> False() 559.50/148.06 , notEmpty(Cons(x, xs)) -> True() } 559.50/148.06 Obligation: 559.50/148.06 innermost runtime complexity 559.50/148.06 Answer: 559.50/148.06 YES(O(1),O(n^2)) 559.50/148.06 559.50/148.06 We estimate the number of application of {3,5,6,9,10} by 559.50/148.06 applications of Pre({3,5,6,9,10}) = {1,4,8}. Here rules are labeled 559.50/148.06 as follows: 559.50/148.06 559.50/148.06 DPs: 559.50/148.06 { 1: part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.06 , 2: part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2), 559.50/148.06 >^#(x', x)) 559.50/148.06 , 3: app^#(Nil(), ys) -> c_3() 559.50/148.06 , 4: app^#(Cons(x, xs), ys) -> c_4(app^#(xs, ys)) 559.50/148.06 , 5: quicksort^#(Nil()) -> c_5() 559.50/148.06 , 6: quicksort^#(Cons(x, Nil())) -> c_6() 559.50/148.06 , 7: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.06 c_7(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.06 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.06 , 8: qs^#(x', Cons(x, xs)) -> 559.50/148.06 c_8(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.06 quicksort^#(xs)) 559.50/148.06 , 9: notEmpty^#(Nil()) -> c_9() 559.50/148.06 , 10: notEmpty^#(Cons(x, xs)) -> c_10() 559.50/148.06 , 11: part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_11(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.06 , 12: part[Ite][True][Ite]^#(False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_12(<^#(x', x)) 559.50/148.06 , 13: >^#(S(x), S(y)) -> c_13(>^#(x, y)) 559.50/148.06 , 14: >^#(S(x), 0()) -> c_14() 559.50/148.06 , 15: >^#(0(), y) -> c_15() 559.50/148.06 , 16: <^#(x, 0()) -> c_16() 559.50/148.06 , 17: <^#(S(x), S(y)) -> c_17(<^#(x, y)) 559.50/148.06 , 18: <^#(0(), S(y)) -> c_18() } 559.50/148.06 559.50/148.06 We are left with following problem, upon which TcT provides the 559.50/148.06 certificate YES(O(1),O(n^2)). 559.50/148.06 559.50/148.06 Strict DPs: 559.50/148.06 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.06 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2), 559.50/148.06 >^#(x', x)) 559.50/148.06 , app^#(Cons(x, xs), ys) -> c_4(app^#(xs, ys)) 559.50/148.06 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.06 c_7(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.06 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.06 , qs^#(x', Cons(x, xs)) -> 559.50/148.06 c_8(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.06 quicksort^#(xs)) } 559.50/148.06 Weak DPs: 559.50/148.06 { app^#(Nil(), ys) -> c_3() 559.50/148.06 , part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_11(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.06 , part[Ite][True][Ite]^#(False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 c_12(<^#(x', x)) 559.50/148.06 , >^#(S(x), S(y)) -> c_13(>^#(x, y)) 559.50/148.06 , >^#(S(x), 0()) -> c_14() 559.50/148.06 , >^#(0(), y) -> c_15() 559.50/148.06 , quicksort^#(Nil()) -> c_5() 559.50/148.06 , quicksort^#(Cons(x, Nil())) -> c_6() 559.50/148.06 , notEmpty^#(Nil()) -> c_9() 559.50/148.06 , notEmpty^#(Cons(x, xs)) -> c_10() 559.50/148.06 , <^#(x, 0()) -> c_16() 559.50/148.06 , <^#(S(x), S(y)) -> c_17(<^#(x, y)) 559.50/148.06 , <^#(0(), S(y)) -> c_18() } 559.50/148.06 Weak Trs: 559.50/148.06 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part(x', xs, Cons(x, xs1), xs2) 559.50/148.06 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.06 x', 559.50/148.06 Cons(x, xs), 559.50/148.06 xs1, 559.50/148.06 xs2) 559.50/148.06 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.06 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.06 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.06 , app(Nil(), ys) -> ys 559.50/148.06 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.06 , quicksort(Nil()) -> Nil() 559.50/148.07 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.07 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs(x', Cons(x, xs)) -> 559.50/148.07 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.07 , >(S(x), S(y)) -> >(x, y) 559.50/148.07 , >(S(x), 0()) -> True() 559.50/148.07 , >(0(), y) -> False() 559.50/148.07 , <(x, 0()) -> False() 559.50/148.07 , <(S(x), S(y)) -> <(x, y) 559.50/148.07 , <(0(), S(y)) -> True() 559.50/148.07 , notEmpty(Nil()) -> False() 559.50/148.07 , notEmpty(Cons(x, xs)) -> True() } 559.50/148.07 Obligation: 559.50/148.07 innermost runtime complexity 559.50/148.07 Answer: 559.50/148.07 YES(O(1),O(n^2)) 559.50/148.07 559.50/148.07 The following weak DPs constitute a sub-graph of the DG that is 559.50/148.07 closed under successors. The DPs are removed. 559.50/148.07 559.50/148.07 { app^#(Nil(), ys) -> c_3() 559.50/148.07 , part[Ite][True][Ite]^#(False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_12(<^#(x', x)) 559.50/148.07 , >^#(S(x), S(y)) -> c_13(>^#(x, y)) 559.50/148.07 , >^#(S(x), 0()) -> c_14() 559.50/148.07 , >^#(0(), y) -> c_15() 559.50/148.07 , quicksort^#(Nil()) -> c_5() 559.50/148.07 , quicksort^#(Cons(x, Nil())) -> c_6() 559.50/148.07 , notEmpty^#(Nil()) -> c_9() 559.50/148.07 , notEmpty^#(Cons(x, xs)) -> c_10() 559.50/148.07 , <^#(x, 0()) -> c_16() 559.50/148.07 , <^#(S(x), S(y)) -> c_17(<^#(x, y)) 559.50/148.07 , <^#(0(), S(y)) -> c_18() } 559.50/148.07 559.50/148.07 We are left with following problem, upon which TcT provides the 559.50/148.07 certificate YES(O(1),O(n^2)). 559.50/148.07 559.50/148.07 Strict DPs: 559.50/148.07 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.07 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2), 559.50/148.07 >^#(x', x)) 559.50/148.07 , app^#(Cons(x, xs), ys) -> c_4(app^#(xs, ys)) 559.50/148.07 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 c_7(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs^#(x', Cons(x, xs)) -> 559.50/148.07 c_8(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.07 quicksort^#(xs)) } 559.50/148.07 Weak DPs: 559.50/148.07 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_11(part^#(x', xs, Cons(x, xs1), xs2)) } 559.50/148.07 Weak Trs: 559.50/148.07 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part(x', xs, Cons(x, xs1), xs2) 559.50/148.07 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.07 x', 559.50/148.07 Cons(x, xs), 559.50/148.07 xs1, 559.50/148.07 xs2) 559.50/148.07 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.07 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.07 , app(Nil(), ys) -> ys 559.50/148.07 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.07 , quicksort(Nil()) -> Nil() 559.50/148.07 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.07 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs(x', Cons(x, xs)) -> 559.50/148.07 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.07 , >(S(x), S(y)) -> >(x, y) 559.50/148.07 , >(S(x), 0()) -> True() 559.50/148.07 , >(0(), y) -> False() 559.50/148.07 , <(x, 0()) -> False() 559.50/148.07 , <(S(x), S(y)) -> <(x, y) 559.50/148.07 , <(0(), S(y)) -> True() 559.50/148.07 , notEmpty(Nil()) -> False() 559.50/148.07 , notEmpty(Cons(x, xs)) -> True() } 559.50/148.07 Obligation: 559.50/148.07 innermost runtime complexity 559.50/148.07 Answer: 559.50/148.07 YES(O(1),O(n^2)) 559.50/148.07 559.50/148.07 Due to missing edges in the dependency-graph, the right-hand sides 559.50/148.07 of following rules could be simplified: 559.50/148.07 559.50/148.07 { part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2), 559.50/148.07 >^#(x', x)) } 559.50/148.07 559.50/148.07 We are left with following problem, upon which TcT provides the 559.50/148.07 certificate YES(O(1),O(n^2)). 559.50/148.07 559.50/148.07 Strict DPs: 559.50/148.07 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.07 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.50/148.07 , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) 559.50/148.07 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs^#(x', Cons(x, xs)) -> 559.50/148.07 c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.07 quicksort^#(xs)) } 559.50/148.07 Weak DPs: 559.50/148.07 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_6(part^#(x', xs, Cons(x, xs1), xs2)) } 559.50/148.07 Weak Trs: 559.50/148.07 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part(x', xs, Cons(x, xs1), xs2) 559.50/148.07 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.07 x', 559.50/148.07 Cons(x, xs), 559.50/148.07 xs1, 559.50/148.07 xs2) 559.50/148.07 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.07 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.07 , app(Nil(), ys) -> ys 559.50/148.07 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.07 , quicksort(Nil()) -> Nil() 559.50/148.07 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.07 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs(x', Cons(x, xs)) -> 559.50/148.07 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.07 , >(S(x), S(y)) -> >(x, y) 559.50/148.07 , >(S(x), 0()) -> True() 559.50/148.07 , >(0(), y) -> False() 559.50/148.07 , <(x, 0()) -> False() 559.50/148.07 , <(S(x), S(y)) -> <(x, y) 559.50/148.07 , <(0(), S(y)) -> True() 559.50/148.07 , notEmpty(Nil()) -> False() 559.50/148.07 , notEmpty(Cons(x, xs)) -> True() } 559.50/148.07 Obligation: 559.50/148.07 innermost runtime complexity 559.50/148.07 Answer: 559.50/148.07 YES(O(1),O(n^2)) 559.50/148.07 559.50/148.07 We replace rewrite rules by usable rules: 559.50/148.07 559.50/148.07 Weak Usable Rules: 559.50/148.07 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part(x', xs, Cons(x, xs1), xs2) 559.50/148.07 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.07 x', 559.50/148.07 Cons(x, xs), 559.50/148.07 xs1, 559.50/148.07 xs2) 559.50/148.07 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.07 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.07 , app(Nil(), ys) -> ys 559.50/148.07 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.07 , quicksort(Nil()) -> Nil() 559.50/148.07 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.07 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs(x', Cons(x, xs)) -> 559.50/148.07 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.07 , >(S(x), S(y)) -> >(x, y) 559.50/148.07 , >(S(x), 0()) -> True() 559.50/148.07 , >(0(), y) -> False() 559.50/148.07 , <(x, 0()) -> False() 559.50/148.07 , <(S(x), S(y)) -> <(x, y) 559.50/148.07 , <(0(), S(y)) -> True() } 559.50/148.07 559.50/148.07 We are left with following problem, upon which TcT provides the 559.50/148.07 certificate YES(O(1),O(n^2)). 559.50/148.07 559.50/148.07 Strict DPs: 559.50/148.07 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.07 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.50/148.07 , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) 559.50/148.07 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs^#(x', Cons(x, xs)) -> 559.50/148.07 c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.07 quicksort^#(xs)) } 559.50/148.07 Weak DPs: 559.50/148.07 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_6(part^#(x', xs, Cons(x, xs1), xs2)) } 559.50/148.07 Weak Trs: 559.50/148.07 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part(x', xs, Cons(x, xs1), xs2) 559.50/148.07 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.07 x', 559.50/148.07 Cons(x, xs), 559.50/148.07 xs1, 559.50/148.07 xs2) 559.50/148.07 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.07 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.07 , app(Nil(), ys) -> ys 559.50/148.07 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.07 , quicksort(Nil()) -> Nil() 559.50/148.07 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.07 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs(x', Cons(x, xs)) -> 559.50/148.07 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.07 , >(S(x), S(y)) -> >(x, y) 559.50/148.07 , >(S(x), 0()) -> True() 559.50/148.07 , >(0(), y) -> False() 559.50/148.07 , <(x, 0()) -> False() 559.50/148.07 , <(S(x), S(y)) -> <(x, y) 559.50/148.07 , <(0(), S(y)) -> True() } 559.50/148.07 Obligation: 559.50/148.07 innermost runtime complexity 559.50/148.07 Answer: 559.50/148.07 YES(O(1),O(n^2)) 559.50/148.07 559.50/148.07 We decompose the input problem according to the dependency graph 559.50/148.07 into the upper component 559.50/148.07 559.50/148.07 { quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs^#(x', Cons(x, xs)) -> 559.50/148.07 c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.07 quicksort^#(xs)) } 559.50/148.07 559.50/148.07 and lower component 559.50/148.07 559.50/148.07 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.07 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.50/148.07 , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) 559.50/148.07 , part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 c_6(part^#(x', xs, Cons(x, xs1), xs2)) } 559.50/148.07 559.50/148.07 Further, following extension rules are added to the lower 559.50/148.07 component. 559.50/148.07 559.50/148.07 { quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil()) 559.50/148.07 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs^#(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs^#(x', Cons(x, xs)) -> 559.50/148.07 app^#(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.07 , qs^#(x', Cons(x, xs)) -> quicksort^#(xs) } 559.50/148.07 559.50/148.07 TcT solves the upper component with certificate YES(O(1),O(n^1)). 559.50/148.07 559.50/148.07 Sub-proof: 559.50/148.07 ---------- 559.50/148.07 We are left with following problem, upon which TcT provides the 559.50/148.07 certificate YES(O(1),O(n^1)). 559.50/148.07 559.50/148.07 Strict DPs: 559.50/148.07 { quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs^#(x', Cons(x, xs)) -> 559.50/148.07 c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.07 quicksort^#(xs)) } 559.50/148.07 Weak Trs: 559.50/148.07 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part(x', xs, Cons(x, xs1), xs2) 559.50/148.07 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.07 x', 559.50/148.07 Cons(x, xs), 559.50/148.07 xs1, 559.50/148.07 xs2) 559.50/148.07 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.07 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.07 , app(Nil(), ys) -> ys 559.50/148.07 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.07 , quicksort(Nil()) -> Nil() 559.50/148.07 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.07 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , qs(x', Cons(x, xs)) -> 559.50/148.07 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.07 , >(S(x), S(y)) -> >(x, y) 559.50/148.07 , >(S(x), 0()) -> True() 559.50/148.07 , >(0(), y) -> False() 559.50/148.07 , <(x, 0()) -> False() 559.50/148.07 , <(S(x), S(y)) -> <(x, y) 559.50/148.07 , <(0(), S(y)) -> True() } 559.50/148.07 Obligation: 559.50/148.07 innermost runtime complexity 559.50/148.07 Answer: 559.50/148.07 YES(O(1),O(n^1)) 559.50/148.07 559.50/148.07 We use the processor 'matrix interpretation of dimension 1' to 559.50/148.07 orient following rules strictly. 559.50/148.07 559.50/148.07 DPs: 559.50/148.07 { 1: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.07 c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.07 , 2: qs^#(x', Cons(x, xs)) -> 559.50/148.07 c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.07 quicksort^#(xs)) } 559.50/148.07 Trs: 559.50/148.07 { part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.07 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.07 x', 559.50/148.07 Cons(x, xs), 559.50/148.07 xs1, 559.50/148.07 xs2) 559.50/148.07 , quicksort(Nil()) -> Nil() 559.50/148.07 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.07 qs(x, part(x, Cons(x', xs), Nil(), Nil())) } 559.50/148.07 559.50/148.07 Sub-proof: 559.50/148.07 ---------- 559.50/148.07 The following argument positions are usable: 559.50/148.07 Uargs(c_4) = {1}, Uargs(c_5) = {1, 2} 559.50/148.07 559.50/148.07 TcT has computed the following constructor-based matrix 559.50/148.07 interpretation satisfying not(EDA). 559.50/148.07 559.50/148.07 [part[Ite][True][Ite]](x1, x2, x3, x4, x5) = [1] x3 + [1] x4 + [2] x5 + [0] 559.50/148.07 559.50/148.07 [part](x1, x2, x3, x4) = [1] x2 + [1] x3 + [2] x4 + [0] 559.50/148.07 559.50/148.07 [True] = [0] 559.50/148.07 559.50/148.07 [app](x1, x2) = [1] x1 + [2] x2 + [0] 559.50/148.07 559.50/148.07 [Nil] = [0] 559.50/148.07 559.50/148.07 [quicksort](x1) = [1] 559.50/148.07 559.50/148.07 [part[Ite][True][Ite][False][Ite]](x1, x2, x3, x4, x5) = [1] x4 + [1] x5 + [1] 559.50/148.07 559.50/148.07 [qs](x1, x2) = [0] 559.50/148.07 559.50/148.07 [>](x1, x2) = [0] 559.50/148.07 559.50/148.07 [<](x1, x2) = [0] 559.50/148.07 559.50/148.07 [S](x1) = [1] x1 + [0] 559.50/148.07 559.50/148.07 [Cons](x1, x2) = [1] x2 + [2] 559.50/148.07 559.50/148.07 [0] = [0] 559.50/148.07 559.50/148.07 [False] = [0] 559.50/148.07 559.50/148.07 [part^#](x1, x2, x3, x4) = [7] x1 + [7] x3 + [7] x4 + [7] 559.50/148.07 559.50/148.07 [app^#](x1, x2) = [0] 559.50/148.07 559.50/148.07 [quicksort^#](x1) = [1] x1 + [3] 559.50/148.07 559.50/148.07 [qs^#](x1, x2) = [1] x2 + [4] 559.50/148.07 559.50/148.07 [c_4](x1, x2) = [1] x1 + [0] 559.50/148.07 559.50/148.07 [c_5](x1, x2) = [4] x1 + [1] x2 + [0] 559.50/148.07 559.50/148.07 The order satisfies the following ordering constraints: 559.50/148.07 559.50/148.07 [part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [2] xs2 + [2] 559.50/148.07 >= [1] xs + [1] xs1 + [2] xs2 + [2] 559.50/148.07 = [part(x', xs, Cons(x, xs1), xs2)] 559.50/148.07 559.50/148.07 [part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [2] xs2 + [2] 559.50/148.07 > [1] xs1 + [1] xs2 + [1] 559.50/148.07 = [part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.07 x', 559.50/148.07 Cons(x, xs), 559.50/148.07 xs1, 559.50/148.07 xs2)] 559.50/148.07 559.50/148.07 [part(x, Nil(), xs1, xs2)] = [1] xs1 + [2] xs2 + [0] 559.50/148.07 >= [1] xs1 + [2] xs2 + [0] 559.50/148.07 = [app(xs1, xs2)] 559.50/148.07 559.50/148.07 [part(x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [2] xs2 + [2] 559.50/148.07 >= [1] xs + [1] xs1 + [2] xs2 + [2] 559.50/148.07 = [part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2)] 559.50/148.07 559.50/148.07 [app(Nil(), ys)] = [2] ys + [0] 559.50/148.07 >= [1] ys + [0] 559.50/148.07 = [ys] 559.50/148.07 559.50/148.07 [app(Cons(x, xs), ys)] = [1] xs + [2] ys + [2] 559.50/148.07 >= [1] xs + [2] ys + [2] 559.50/148.07 = [Cons(x, app(xs, ys))] 559.50/148.07 559.50/148.07 [quicksort(Nil())] = [1] 559.50/148.07 > [0] 559.50/148.07 = [Nil()] 559.50/148.07 559.50/148.07 [quicksort(Cons(x, Nil()))] = [1] 559.50/148.07 ? [2] 559.50/148.07 = [Cons(x, Nil())] 559.50/148.07 559.50/148.07 [quicksort(Cons(x, Cons(x', xs)))] = [1] 559.50/148.07 > [0] 559.50/148.07 = [qs(x, part(x, Cons(x', xs), Nil(), Nil()))] 559.50/148.07 559.50/148.07 [qs(x', Cons(x, xs))] = [0] 559.50/148.07 ? [8] 559.50/148.07 = [app(Cons(x, Nil()), Cons(x', quicksort(xs)))] 559.50/148.07 559.50/148.07 [>(S(x), S(y))] = [0] 559.50/148.07 >= [0] 559.50/148.07 = [>(x, y)] 559.50/148.07 559.50/148.07 [>(S(x), 0())] = [0] 559.50/148.07 >= [0] 559.50/148.07 = [True()] 559.50/148.07 559.50/148.07 [>(0(), y)] = [0] 559.50/148.07 >= [0] 559.50/148.07 = [False()] 559.50/148.07 559.50/148.07 [<(x, 0())] = [0] 559.50/148.07 >= [0] 559.50/148.07 = [False()] 559.50/148.07 559.50/148.07 [<(S(x), S(y))] = [0] 559.50/148.07 >= [0] 559.50/148.07 = [<(x, y)] 559.50/148.07 559.50/148.07 [<(0(), S(y))] = [0] 559.50/148.07 >= [0] 559.50/148.07 = [True()] 559.50/148.07 559.50/148.07 [quicksort^#(Cons(x, Cons(x', xs)))] = [1] xs + [7] 559.50/148.07 > [1] xs + [6] 559.50/148.07 = [c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.07 part^#(x, Cons(x', xs), Nil(), Nil()))] 559.50/148.07 559.50/148.07 [qs^#(x', Cons(x, xs))] = [1] xs + [6] 559.50/148.08 > [1] xs + [3] 559.50/148.08 = [c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.08 quicksort^#(xs))] 559.50/148.08 559.50/148.08 559.50/148.08 The strictly oriented rules are moved into the weak component. 559.50/148.08 559.50/148.08 We are left with following problem, upon which TcT provides the 559.50/148.08 certificate YES(O(1),O(1)). 559.50/148.08 559.50/148.08 Weak DPs: 559.50/148.08 { quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.08 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> 559.50/148.08 c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.08 quicksort^#(xs)) } 559.50/148.08 Weak Trs: 559.50/148.08 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part(x', xs, Cons(x, xs1), xs2) 559.50/148.08 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2) 559.50/148.08 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.08 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.08 , app(Nil(), ys) -> ys 559.50/148.08 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.08 , quicksort(Nil()) -> Nil() 559.50/148.08 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.08 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs(x', Cons(x, xs)) -> 559.50/148.08 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , >(S(x), S(y)) -> >(x, y) 559.50/148.08 , >(S(x), 0()) -> True() 559.50/148.08 , >(0(), y) -> False() 559.50/148.08 , <(x, 0()) -> False() 559.50/148.08 , <(S(x), S(y)) -> <(x, y) 559.50/148.08 , <(0(), S(y)) -> True() } 559.50/148.08 Obligation: 559.50/148.08 innermost runtime complexity 559.50/148.08 Answer: 559.50/148.08 YES(O(1),O(1)) 559.50/148.08 559.50/148.08 The following weak DPs constitute a sub-graph of the DG that is 559.50/148.08 closed under successors. The DPs are removed. 559.50/148.08 559.50/148.08 { quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 c_4(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())), 559.50/148.08 part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> 559.50/148.08 c_5(app^#(Cons(x, Nil()), Cons(x', quicksort(xs))), 559.50/148.08 quicksort^#(xs)) } 559.50/148.08 559.50/148.08 We are left with following problem, upon which TcT provides the 559.50/148.08 certificate YES(O(1),O(1)). 559.50/148.08 559.50/148.08 Weak Trs: 559.50/148.08 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part(x', xs, Cons(x, xs1), xs2) 559.50/148.08 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2) 559.50/148.08 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.08 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.08 , app(Nil(), ys) -> ys 559.50/148.08 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.08 , quicksort(Nil()) -> Nil() 559.50/148.08 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.08 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs(x', Cons(x, xs)) -> 559.50/148.08 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , >(S(x), S(y)) -> >(x, y) 559.50/148.08 , >(S(x), 0()) -> True() 559.50/148.08 , >(0(), y) -> False() 559.50/148.08 , <(x, 0()) -> False() 559.50/148.08 , <(S(x), S(y)) -> <(x, y) 559.50/148.08 , <(0(), S(y)) -> True() } 559.50/148.08 Obligation: 559.50/148.08 innermost runtime complexity 559.50/148.08 Answer: 559.50/148.08 YES(O(1),O(1)) 559.50/148.08 559.50/148.08 No rule is usable, rules are removed from the input problem. 559.50/148.08 559.50/148.08 We are left with following problem, upon which TcT provides the 559.50/148.08 certificate YES(O(1),O(1)). 559.50/148.08 559.50/148.08 Rules: Empty 559.50/148.08 Obligation: 559.50/148.08 innermost runtime complexity 559.50/148.08 Answer: 559.50/148.08 YES(O(1),O(1)) 559.50/148.08 559.50/148.08 Empty rules are trivially bounded 559.50/148.08 559.50/148.08 We return to the main proof. 559.50/148.08 559.50/148.08 We are left with following problem, upon which TcT provides the 559.50/148.08 certificate YES(O(1),O(n^1)). 559.50/148.08 559.50/148.08 Strict DPs: 559.50/148.08 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.08 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.50/148.08 , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) } 559.50/148.08 Weak DPs: 559.50/148.08 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_6(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 part^#(x, Cons(x', xs), Nil(), Nil()) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs^#(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> 559.50/148.08 app^#(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> quicksort^#(xs) } 559.50/148.08 Weak Trs: 559.50/148.08 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part(x', xs, Cons(x, xs1), xs2) 559.50/148.08 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2) 559.50/148.08 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.08 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.08 , app(Nil(), ys) -> ys 559.50/148.08 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.08 , quicksort(Nil()) -> Nil() 559.50/148.08 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.08 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs(x', Cons(x, xs)) -> 559.50/148.08 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , >(S(x), S(y)) -> >(x, y) 559.50/148.08 , >(S(x), 0()) -> True() 559.50/148.08 , >(0(), y) -> False() 559.50/148.08 , <(x, 0()) -> False() 559.50/148.08 , <(S(x), S(y)) -> <(x, y) 559.50/148.08 , <(0(), S(y)) -> True() } 559.50/148.08 Obligation: 559.50/148.08 innermost runtime complexity 559.50/148.08 Answer: 559.50/148.08 YES(O(1),O(n^1)) 559.50/148.08 559.50/148.08 We use the processor 'matrix interpretation of dimension 1' to 559.50/148.08 orient following rules strictly. 559.50/148.08 559.50/148.08 DPs: 559.50/148.08 { 3: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) 559.50/148.08 , 5: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 part^#(x, Cons(x', xs), Nil(), Nil()) 559.50/148.08 , 6: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs^#(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , 8: qs^#(x', Cons(x, xs)) -> quicksort^#(xs) } 559.50/148.08 Trs: 559.50/148.08 { quicksort(Nil()) -> Nil() 559.50/148.08 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs(x, part(x, Cons(x', xs), Nil(), Nil())) } 559.50/148.08 559.50/148.08 Sub-proof: 559.50/148.08 ---------- 559.50/148.08 The following argument positions are usable: 559.50/148.08 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 559.50/148.08 Uargs(c_6) = {1} 559.50/148.08 559.50/148.08 TcT has computed the following constructor-based matrix 559.50/148.08 interpretation satisfying not(EDA). 559.50/148.08 559.50/148.08 [part[Ite][True][Ite]](x1, x2, x3, x4, x5) = [1] x3 + [1] x4 + [4] x5 + [0] 559.50/148.08 559.50/148.08 [part](x1, x2, x3, x4) = [1] x2 + [1] x3 + [4] x4 + [0] 559.50/148.08 559.50/148.08 [True] = [0] 559.50/148.08 559.50/148.08 [app](x1, x2) = [1] x1 + [4] x2 + [0] 559.50/148.08 559.50/148.08 [Nil] = [0] 559.50/148.08 559.50/148.08 [quicksort](x1) = [1] 559.50/148.08 559.50/148.08 [part[Ite][True][Ite][False][Ite]](x1, x2, x3, x4, x5) = [1] x4 + [1] x5 + [1] 559.50/148.08 559.50/148.08 [qs](x1, x2) = [0] 559.50/148.08 559.50/148.08 [>](x1, x2) = [0] 559.50/148.08 559.50/148.08 [<](x1, x2) = [0] 559.50/148.08 559.50/148.08 [S](x1) = [1] x1 + [0] 559.50/148.08 559.50/148.08 [Cons](x1, x2) = [1] x2 + [1] 559.50/148.08 559.50/148.08 [0] = [0] 559.50/148.08 559.50/148.08 [False] = [0] 559.50/148.08 559.50/148.08 [part^#](x1, x2, x3, x4) = [1] x2 + [1] x3 + [0] 559.50/148.08 559.50/148.08 [app^#](x1, x2) = [1] x1 + [0] 559.50/148.08 559.50/148.08 [part[Ite][True][Ite]^#](x1, x2, x3, x4, x5) = [1] x3 + [1] x4 + [0] 559.50/148.08 559.50/148.08 [quicksort^#](x1) = [1] x1 + [0] 559.50/148.08 559.50/148.08 [qs^#](x1, x2) = [1] x2 + [0] 559.50/148.08 559.50/148.08 [c_1](x1) = [1] x1 + [0] 559.50/148.08 559.50/148.08 [c_2](x1) = [1] x1 + [0] 559.50/148.08 559.50/148.08 [c_3](x1) = [1] x1 + [0] 559.50/148.08 559.50/148.08 [c_6](x1) = [1] x1 + [0] 559.50/148.08 559.50/148.08 The order satisfies the following ordering constraints: 559.50/148.08 559.50/148.08 [part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [4] xs2 + [1] 559.50/148.08 >= [1] xs + [1] xs1 + [4] xs2 + [1] 559.50/148.08 = [part(x', xs, Cons(x, xs1), xs2)] 559.50/148.08 559.50/148.08 [part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [4] xs2 + [1] 559.50/148.08 >= [1] xs1 + [1] xs2 + [1] 559.50/148.08 = [part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2)] 559.50/148.08 559.50/148.08 [part(x, Nil(), xs1, xs2)] = [1] xs1 + [4] xs2 + [0] 559.50/148.08 >= [1] xs1 + [4] xs2 + [0] 559.50/148.08 = [app(xs1, xs2)] 559.50/148.08 559.50/148.08 [part(x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [4] xs2 + [1] 559.50/148.08 >= [1] xs + [1] xs1 + [4] xs2 + [1] 559.50/148.08 = [part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2)] 559.50/148.08 559.50/148.08 [app(Nil(), ys)] = [4] ys + [0] 559.50/148.08 >= [1] ys + [0] 559.50/148.08 = [ys] 559.50/148.08 559.50/148.08 [app(Cons(x, xs), ys)] = [1] xs + [4] ys + [1] 559.50/148.08 >= [1] xs + [4] ys + [1] 559.50/148.08 = [Cons(x, app(xs, ys))] 559.50/148.08 559.50/148.08 [quicksort(Nil())] = [1] 559.50/148.08 > [0] 559.50/148.08 = [Nil()] 559.50/148.08 559.50/148.08 [quicksort(Cons(x, Nil()))] = [1] 559.50/148.08 >= [1] 559.50/148.08 = [Cons(x, Nil())] 559.50/148.08 559.50/148.08 [quicksort(Cons(x, Cons(x', xs)))] = [1] 559.50/148.08 > [0] 559.50/148.08 = [qs(x, part(x, Cons(x', xs), Nil(), Nil()))] 559.50/148.08 559.50/148.08 [qs(x', Cons(x, xs))] = [0] 559.50/148.08 ? [9] 559.50/148.08 = [app(Cons(x, Nil()), Cons(x', quicksort(xs)))] 559.50/148.08 559.50/148.08 [>(S(x), S(y))] = [0] 559.50/148.08 >= [0] 559.50/148.08 = [>(x, y)] 559.50/148.08 559.50/148.08 [>(S(x), 0())] = [0] 559.50/148.08 >= [0] 559.50/148.08 = [True()] 559.50/148.08 559.50/148.08 [>(0(), y)] = [0] 559.50/148.08 >= [0] 559.50/148.08 = [False()] 559.50/148.08 559.50/148.08 [<(x, 0())] = [0] 559.50/148.08 >= [0] 559.50/148.08 = [False()] 559.50/148.08 559.50/148.08 [<(S(x), S(y))] = [0] 559.50/148.08 >= [0] 559.50/148.08 = [<(x, y)] 559.50/148.08 559.50/148.08 [<(0(), S(y))] = [0] 559.50/148.08 >= [0] 559.50/148.08 = [True()] 559.50/148.08 559.50/148.08 [part^#(x, Nil(), xs1, xs2)] = [1] xs1 + [0] 559.50/148.08 >= [1] xs1 + [0] 559.50/148.08 = [c_1(app^#(xs1, xs2))] 559.50/148.08 559.50/148.08 [part^#(x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [1] 559.50/148.08 >= [1] xs + [1] xs1 + [1] 559.50/148.08 = [c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2))] 559.50/148.08 559.50/148.08 [app^#(Cons(x, xs), ys)] = [1] xs + [1] 559.50/148.08 > [1] xs + [0] 559.50/148.08 = [c_3(app^#(xs, ys))] 559.50/148.08 559.50/148.08 [part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [1] 559.50/148.08 >= [1] xs + [1] xs1 + [1] 559.50/148.08 = [c_6(part^#(x', xs, Cons(x, xs1), xs2))] 559.50/148.08 559.50/148.08 [quicksort^#(Cons(x, Cons(x', xs)))] = [1] xs + [2] 559.50/148.08 > [1] xs + [1] 559.50/148.08 = [part^#(x, Cons(x', xs), Nil(), Nil())] 559.50/148.08 559.50/148.08 [quicksort^#(Cons(x, Cons(x', xs)))] = [1] xs + [2] 559.50/148.08 > [1] xs + [1] 559.50/148.08 = [qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))] 559.50/148.08 559.50/148.08 [qs^#(x', Cons(x, xs))] = [1] xs + [1] 559.50/148.08 >= [1] 559.50/148.08 = [app^#(Cons(x, Nil()), Cons(x', quicksort(xs)))] 559.50/148.08 559.50/148.08 [qs^#(x', Cons(x, xs))] = [1] xs + [1] 559.50/148.08 > [1] xs + [0] 559.50/148.08 = [quicksort^#(xs)] 559.50/148.08 559.50/148.08 559.50/148.08 We return to the main proof. Consider the set of all dependency 559.50/148.08 pairs 559.50/148.08 559.50/148.08 : 559.50/148.08 { 1: part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.08 , 2: part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.50/148.08 , 3: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) 559.50/148.08 , 4: part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_6(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.08 , 5: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 part^#(x, Cons(x', xs), Nil(), Nil()) 559.50/148.08 , 6: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs^#(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , 7: qs^#(x', Cons(x, xs)) -> 559.50/148.08 app^#(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , 8: qs^#(x', Cons(x, xs)) -> quicksort^#(xs) } 559.50/148.08 559.50/148.08 Processor 'matrix interpretation of dimension 1' induces the 559.50/148.08 complexity certificate YES(?,O(n^1)) on application of dependency 559.50/148.08 pairs {3,5,6,8}. These cover all (indirect) predecessors of 559.50/148.08 dependency pairs {3,5,6,7,8}, their number of application is 559.50/148.08 equally bounded. The dependency pairs are shifted into the weak 559.50/148.08 component. 559.50/148.08 559.50/148.08 We are left with following problem, upon which TcT provides the 559.50/148.08 certificate YES(O(1),O(n^1)). 559.50/148.08 559.50/148.08 Strict DPs: 559.50/148.08 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.08 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2)) } 559.50/148.08 Weak DPs: 559.50/148.08 { app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) 559.50/148.08 , part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_6(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 part^#(x, Cons(x', xs), Nil(), Nil()) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs^#(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> 559.50/148.08 app^#(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> quicksort^#(xs) } 559.50/148.08 Weak Trs: 559.50/148.08 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part(x', xs, Cons(x, xs1), xs2) 559.50/148.08 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2) 559.50/148.08 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.08 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.08 , app(Nil(), ys) -> ys 559.50/148.08 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.08 , quicksort(Nil()) -> Nil() 559.50/148.08 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.08 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs(x', Cons(x, xs)) -> 559.50/148.08 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , >(S(x), S(y)) -> >(x, y) 559.50/148.08 , >(S(x), 0()) -> True() 559.50/148.08 , >(0(), y) -> False() 559.50/148.08 , <(x, 0()) -> False() 559.50/148.08 , <(S(x), S(y)) -> <(x, y) 559.50/148.08 , <(0(), S(y)) -> True() } 559.50/148.08 Obligation: 559.50/148.08 innermost runtime complexity 559.50/148.08 Answer: 559.50/148.08 YES(O(1),O(n^1)) 559.50/148.08 559.50/148.08 The following weak DPs constitute a sub-graph of the DG that is 559.50/148.08 closed under successors. The DPs are removed. 559.50/148.08 559.50/148.08 { app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> 559.50/148.08 app^#(Cons(x, Nil()), Cons(x', quicksort(xs))) } 559.50/148.08 559.50/148.08 We are left with following problem, upon which TcT provides the 559.50/148.08 certificate YES(O(1),O(n^1)). 559.50/148.08 559.50/148.08 Strict DPs: 559.50/148.08 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) 559.50/148.08 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2)) } 559.50/148.08 Weak DPs: 559.50/148.08 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_6(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 part^#(x, Cons(x', xs), Nil(), Nil()) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs^#(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> quicksort^#(xs) } 559.50/148.08 Weak Trs: 559.50/148.08 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part(x', xs, Cons(x, xs1), xs2) 559.50/148.08 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2) 559.50/148.08 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.08 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.08 , app(Nil(), ys) -> ys 559.50/148.08 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.08 , quicksort(Nil()) -> Nil() 559.50/148.08 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.08 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs(x', Cons(x, xs)) -> 559.50/148.08 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.08 , >(S(x), S(y)) -> >(x, y) 559.50/148.08 , >(S(x), 0()) -> True() 559.50/148.08 , >(0(), y) -> False() 559.50/148.08 , <(x, 0()) -> False() 559.50/148.08 , <(S(x), S(y)) -> <(x, y) 559.50/148.08 , <(0(), S(y)) -> True() } 559.50/148.08 Obligation: 559.50/148.08 innermost runtime complexity 559.50/148.08 Answer: 559.50/148.08 YES(O(1),O(n^1)) 559.50/148.08 559.50/148.08 Due to missing edges in the dependency-graph, the right-hand sides 559.50/148.08 of following rules could be simplified: 559.50/148.08 559.50/148.08 { part^#(x, Nil(), xs1, xs2) -> c_1(app^#(xs1, xs2)) } 559.50/148.08 559.50/148.08 We are left with following problem, upon which TcT provides the 559.50/148.08 certificate YES(O(1),O(n^1)). 559.50/148.08 559.50/148.08 Strict DPs: 559.50/148.08 { part^#(x, Nil(), xs1, xs2) -> c_1() 559.50/148.08 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2)) } 559.50/148.08 Weak DPs: 559.50/148.08 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.08 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.50/148.08 , qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.50/148.08 Weak Trs: 559.50/148.08 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part(x', xs, Cons(x, xs1), xs2) 559.50/148.08 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.08 x', 559.50/148.08 Cons(x, xs), 559.50/148.08 xs1, 559.50/148.08 xs2) 559.50/148.08 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.08 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.08 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.08 , app(Nil(), ys) -> ys 559.50/148.08 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.08 , quicksort(Nil()) -> Nil() 559.50/148.08 , quicksort(Cons(x, Nil())) -> Cons(x, Nil()) 559.50/148.08 , quicksort(Cons(x, Cons(x', xs))) -> 559.50/148.08 qs(x, part(x, Cons(x', xs), Nil(), Nil())) 559.50/148.08 , qs(x', Cons(x, xs)) -> 559.50/148.09 app(Cons(x, Nil()), Cons(x', quicksort(xs))) 559.50/148.09 , >(S(x), S(y)) -> >(x, y) 559.50/148.09 , >(S(x), 0()) -> True() 559.50/148.09 , >(0(), y) -> False() 559.50/148.09 , <(x, 0()) -> False() 559.50/148.09 , <(S(x), S(y)) -> <(x, y) 559.50/148.09 , <(0(), S(y)) -> True() } 559.50/148.09 Obligation: 559.50/148.09 innermost runtime complexity 559.50/148.09 Answer: 559.50/148.09 YES(O(1),O(n^1)) 559.50/148.09 559.50/148.09 We replace rewrite rules by usable rules: 559.50/148.09 559.50/148.09 Weak Usable Rules: 559.50/148.09 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part(x', xs, Cons(x, xs1), xs2) 559.50/148.09 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2) 559.50/148.09 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.09 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.09 , app(Nil(), ys) -> ys 559.50/148.09 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.09 , >(S(x), S(y)) -> >(x, y) 559.50/148.09 , >(S(x), 0()) -> True() 559.50/148.09 , >(0(), y) -> False() 559.50/148.09 , <(x, 0()) -> False() 559.50/148.09 , <(S(x), S(y)) -> <(x, y) 559.50/148.09 , <(0(), S(y)) -> True() } 559.50/148.09 559.50/148.09 We are left with following problem, upon which TcT provides the 559.50/148.09 certificate YES(O(1),O(n^1)). 559.50/148.09 559.50/148.09 Strict DPs: 559.50/148.09 { part^#(x, Nil(), xs1, xs2) -> c_1() 559.50/148.09 , part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2)) } 559.50/148.09 Weak DPs: 559.50/148.09 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.09 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.09 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.50/148.09 , qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.50/148.09 Weak Trs: 559.50/148.09 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part(x', xs, Cons(x, xs1), xs2) 559.50/148.09 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2) 559.50/148.09 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.09 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.09 , app(Nil(), ys) -> ys 559.50/148.09 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.09 , >(S(x), S(y)) -> >(x, y) 559.50/148.09 , >(S(x), 0()) -> True() 559.50/148.09 , >(0(), y) -> False() 559.50/148.09 , <(x, 0()) -> False() 559.50/148.09 , <(S(x), S(y)) -> <(x, y) 559.50/148.09 , <(0(), S(y)) -> True() } 559.50/148.09 Obligation: 559.50/148.09 innermost runtime complexity 559.50/148.09 Answer: 559.50/148.09 YES(O(1),O(n^1)) 559.50/148.09 559.50/148.09 We use the processor 'matrix interpretation of dimension 1' to 559.50/148.09 orient following rules strictly. 559.50/148.09 559.50/148.09 DPs: 559.50/148.09 { 1: part^#(x, Nil(), xs1, xs2) -> c_1() } 559.50/148.09 559.50/148.09 Sub-proof: 559.50/148.09 ---------- 559.50/148.09 The following argument positions are usable: 559.50/148.09 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 559.50/148.09 Uargs(c_5) = {1}, Uargs(c_6) = {1} 559.50/148.09 559.50/148.09 TcT has computed the following constructor-restricted matrix 559.50/148.09 interpretation. Note that the diagonal of the component-wise maxima 559.50/148.09 of interpretation-entries (of constructors) contains no more than 0 559.50/148.09 non-zero entries. 559.50/148.09 559.50/148.09 [part[Ite][True][Ite]](x1, x2, x3, x4, x5) = [3] x2 + [7] x3 + [4] x5 + [0] 559.50/148.09 559.50/148.09 [part](x1, x2, x3, x4) = [0] 559.50/148.09 559.50/148.09 [True] = [0] 559.50/148.09 559.50/148.09 [app](x1, x2) = [4] x2 + [0] 559.50/148.09 559.50/148.09 [Nil] = [0] 559.50/148.09 559.50/148.09 [quicksort](x1) = [0] 559.50/148.09 559.50/148.09 [part[Ite][True][Ite][False][Ite]](x1, x2, x3, x4, x5) = [6] 559.50/148.09 559.50/148.09 [qs](x1, x2) = [0] 559.50/148.09 559.50/148.09 [>](x1, x2) = [0] 559.50/148.09 559.50/148.09 [<](x1, x2) = [0] 559.50/148.09 559.50/148.09 [S](x1) = [0] 559.50/148.09 559.50/148.09 [Cons](x1, x2) = [0] 559.50/148.09 559.50/148.09 [0] = [0] 559.50/148.09 559.50/148.09 [False] = [4] 559.50/148.09 559.50/148.09 [part^#](x1, x2, x3, x4) = [2] 559.50/148.09 559.50/148.09 [app^#](x1, x2) = [0] 559.50/148.09 559.50/148.09 [part[Ite][True][Ite]^#](x1, x2, x3, x4, x5) = [2] 559.50/148.09 559.50/148.09 [quicksort^#](x1) = [2] 559.50/148.09 559.50/148.09 [qs^#](x1, x2) = [2] 559.50/148.09 559.50/148.09 [c_1](x1) = [0] 559.50/148.09 559.50/148.09 [c_2](x1) = [0] 559.50/148.09 559.50/148.09 [c_3](x1) = [0] 559.50/148.09 559.50/148.09 [c_6](x1) = [0] 559.50/148.09 559.50/148.09 [c] = [0] 559.50/148.09 559.50/148.09 [c_1] = [0] 559.50/148.09 559.50/148.09 [c_2](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 [c_3](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 [c_4](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 [c_5](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 [c_6](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 The order satisfies the following ordering constraints: 559.50/148.09 559.50/148.09 [part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2)] = [3] x' + [4] xs2 + [0] 559.50/148.09 >= [0] 559.50/148.09 = [part(x', xs, Cons(x, xs1), xs2)] 559.50/148.09 559.50/148.09 [part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2)] = [3] x' + [4] xs2 + [0] 559.50/148.09 ? [6] 559.50/148.09 = [part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2)] 559.50/148.09 559.50/148.09 [part(x, Nil(), xs1, xs2)] = [0] 559.50/148.09 ? [4] xs2 + [0] 559.50/148.09 = [app(xs1, xs2)] 559.50/148.09 559.50/148.09 [part(x', Cons(x, xs), xs1, xs2)] = [0] 559.50/148.09 ? [3] x' + [4] xs2 + [0] 559.50/148.09 = [part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2)] 559.50/148.09 559.50/148.09 [app(Nil(), ys)] = [4] ys + [0] 559.50/148.09 >= [1] ys + [0] 559.50/148.09 = [ys] 559.50/148.09 559.50/148.09 [app(Cons(x, xs), ys)] = [4] ys + [0] 559.50/148.09 >= [0] 559.50/148.09 = [Cons(x, app(xs, ys))] 559.50/148.09 559.50/148.09 [>(S(x), S(y))] = [0] 559.50/148.09 >= [0] 559.50/148.09 = [>(x, y)] 559.50/148.09 559.50/148.09 [>(S(x), 0())] = [0] 559.50/148.09 >= [0] 559.50/148.09 = [True()] 559.50/148.09 559.50/148.09 [>(0(), y)] = [0] 559.50/148.09 ? [4] 559.50/148.09 = [False()] 559.50/148.09 559.50/148.09 [<(x, 0())] = [0] 559.50/148.09 ? [4] 559.50/148.09 = [False()] 559.50/148.09 559.50/148.09 [<(S(x), S(y))] = [0] 559.50/148.09 >= [0] 559.50/148.09 = [<(x, y)] 559.50/148.09 559.50/148.09 [<(0(), S(y))] = [0] 559.50/148.09 >= [0] 559.50/148.09 = [True()] 559.50/148.09 559.50/148.09 [part^#(x, Nil(), xs1, xs2)] = [2] 559.50/148.09 > [0] 559.50/148.09 = [c_1()] 559.50/148.09 559.50/148.09 [part^#(x', Cons(x, xs), xs1, xs2)] = [2] 559.50/148.09 >= [2] 559.50/148.09 = [c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2))] 559.50/148.09 559.50/148.09 [part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2)] = [2] 559.50/148.09 >= [2] 559.50/148.09 = [c_3(part^#(x', xs, Cons(x, xs1), xs2))] 559.50/148.09 559.50/148.09 [quicksort^#(Cons(x, Cons(x', xs)))] = [2] 559.50/148.09 >= [2] 559.50/148.09 = [c_4(part^#(x, Cons(x', xs), Nil(), Nil()))] 559.50/148.09 559.50/148.09 [quicksort^#(Cons(x, Cons(x', xs)))] = [2] 559.50/148.09 >= [2] 559.50/148.09 = [c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())))] 559.50/148.09 559.50/148.09 [qs^#(x', Cons(x, xs))] = [2] 559.50/148.09 >= [2] 559.50/148.09 = [c_6(quicksort^#(xs))] 559.50/148.09 559.50/148.09 559.50/148.09 The strictly oriented rules are moved into the weak component. 559.50/148.09 559.50/148.09 We are left with following problem, upon which TcT provides the 559.50/148.09 certificate YES(O(1),O(n^1)). 559.50/148.09 559.50/148.09 Strict DPs: 559.50/148.09 { part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2)) } 559.50/148.09 Weak DPs: 559.50/148.09 { part^#(x, Nil(), xs1, xs2) -> c_1() 559.50/148.09 , part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.09 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.09 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.50/148.09 , qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.50/148.09 Weak Trs: 559.50/148.09 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part(x', xs, Cons(x, xs1), xs2) 559.50/148.09 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2) 559.50/148.09 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.09 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.09 , app(Nil(), ys) -> ys 559.50/148.09 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.09 , >(S(x), S(y)) -> >(x, y) 559.50/148.09 , >(S(x), 0()) -> True() 559.50/148.09 , >(0(), y) -> False() 559.50/148.09 , <(x, 0()) -> False() 559.50/148.09 , <(S(x), S(y)) -> <(x, y) 559.50/148.09 , <(0(), S(y)) -> True() } 559.50/148.09 Obligation: 559.50/148.09 innermost runtime complexity 559.50/148.09 Answer: 559.50/148.09 YES(O(1),O(n^1)) 559.50/148.09 559.50/148.09 The following weak DPs constitute a sub-graph of the DG that is 559.50/148.09 closed under successors. The DPs are removed. 559.50/148.09 559.50/148.09 { part^#(x, Nil(), xs1, xs2) -> c_1() } 559.50/148.09 559.50/148.09 We are left with following problem, upon which TcT provides the 559.50/148.09 certificate YES(O(1),O(n^1)). 559.50/148.09 559.50/148.09 Strict DPs: 559.50/148.09 { part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2)) } 559.50/148.09 Weak DPs: 559.50/148.09 { part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.09 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.09 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.50/148.09 , qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.50/148.09 Weak Trs: 559.50/148.09 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part(x', xs, Cons(x, xs1), xs2) 559.50/148.09 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2) 559.50/148.09 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.50/148.09 , part(x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.50/148.09 , app(Nil(), ys) -> ys 559.50/148.09 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.50/148.09 , >(S(x), S(y)) -> >(x, y) 559.50/148.09 , >(S(x), 0()) -> True() 559.50/148.09 , >(0(), y) -> False() 559.50/148.09 , <(x, 0()) -> False() 559.50/148.09 , <(S(x), S(y)) -> <(x, y) 559.50/148.09 , <(0(), S(y)) -> True() } 559.50/148.09 Obligation: 559.50/148.09 innermost runtime complexity 559.50/148.09 Answer: 559.50/148.09 YES(O(1),O(n^1)) 559.50/148.09 559.50/148.09 We use the processor 'matrix interpretation of dimension 1' to 559.50/148.09 orient following rules strictly. 559.50/148.09 559.50/148.09 DPs: 559.50/148.09 { 2: part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.09 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.09 , 3: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.09 , 4: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.09 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.50/148.09 , 5: qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.50/148.09 559.50/148.09 Sub-proof: 559.50/148.09 ---------- 559.50/148.09 The following argument positions are usable: 559.50/148.09 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 559.50/148.09 Uargs(c_5) = {1}, Uargs(c_6) = {1} 559.50/148.09 559.50/148.09 TcT has computed the following constructor-based matrix 559.50/148.09 interpretation satisfying not(EDA). 559.50/148.09 559.50/148.09 [part[Ite][True][Ite]](x1, x2, x3, x4, x5) = [1] x3 + [1] x4 + [2] x5 + [0] 559.50/148.09 559.50/148.09 [part](x1, x2, x3, x4) = [1] x2 + [1] x3 + [2] x4 + [0] 559.50/148.09 559.50/148.09 [True] = [0] 559.50/148.09 559.50/148.09 [app](x1, x2) = [1] x1 + [2] x2 + [0] 559.50/148.09 559.50/148.09 [Nil] = [0] 559.50/148.09 559.50/148.09 [quicksort](x1) = [7] x1 + [0] 559.50/148.09 559.50/148.09 [part[Ite][True][Ite][False][Ite]](x1, x2, x3, x4, x5) = [1] x4 + [1] x5 + [1] 559.50/148.09 559.50/148.09 [qs](x1, x2) = [7] x1 + [7] x2 + [0] 559.50/148.09 559.50/148.09 [>](x1, x2) = [0] 559.50/148.09 559.50/148.09 [<](x1, x2) = [0] 559.50/148.09 559.50/148.09 [S](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 [Cons](x1, x2) = [1] x2 + [1] 559.50/148.09 559.50/148.09 [0] = [0] 559.50/148.09 559.50/148.09 [False] = [0] 559.50/148.09 559.50/148.09 [part^#](x1, x2, x3, x4) = [1] x2 + [0] 559.50/148.09 559.50/148.09 [app^#](x1, x2) = [7] x1 + [7] x2 + [0] 559.50/148.09 559.50/148.09 [part[Ite][True][Ite]^#](x1, x2, x3, x4, x5) = [1] x3 + [0] 559.50/148.09 559.50/148.09 [quicksort^#](x1) = [4] x1 + [0] 559.50/148.09 559.50/148.09 [qs^#](x1, x2) = [4] x2 + [0] 559.50/148.09 559.50/148.09 [c_1](x1) = [7] x1 + [0] 559.50/148.09 559.50/148.09 [c_2](x1) = [7] x1 + [0] 559.50/148.09 559.50/148.09 [c_3](x1) = [7] x1 + [0] 559.50/148.09 559.50/148.09 [c_6](x1) = [7] x1 + [0] 559.50/148.09 559.50/148.09 [c] = [0] 559.50/148.09 559.50/148.09 [c_1] = [0] 559.50/148.09 559.50/148.09 [c_2](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 [c_3](x1) = [1] x1 + [0] 559.50/148.09 559.50/148.09 [c_4](x1) = [4] x1 + [3] 559.50/148.09 559.50/148.09 [c_5](x1) = [1] x1 + [3] 559.50/148.09 559.50/148.09 [c_6](x1) = [1] x1 + [1] 559.50/148.09 559.50/148.09 The order satisfies the following ordering constraints: 559.50/148.09 559.50/148.09 [part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [2] xs2 + [1] 559.50/148.09 >= [1] xs + [1] xs1 + [2] xs2 + [1] 559.50/148.09 = [part(x', xs, Cons(x, xs1), xs2)] 559.50/148.09 559.50/148.09 [part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [2] xs2 + [1] 559.50/148.09 >= [1] xs1 + [1] xs2 + [1] 559.50/148.09 = [part[Ite][True][Ite][False][Ite](<(x', x), 559.50/148.09 x', 559.50/148.09 Cons(x, xs), 559.50/148.09 xs1, 559.50/148.09 xs2)] 559.50/148.09 559.50/148.09 [part(x, Nil(), xs1, xs2)] = [1] xs1 + [2] xs2 + [0] 559.50/148.09 >= [1] xs1 + [2] xs2 + [0] 559.50/148.09 = [app(xs1, xs2)] 559.50/148.09 559.50/148.09 [part(x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] xs1 + [2] xs2 + [1] 559.50/148.09 >= [1] xs + [1] xs1 + [2] xs2 + [1] 559.50/148.09 = [part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2)] 559.50/148.09 559.50/148.09 [app(Nil(), ys)] = [2] ys + [0] 559.50/148.09 >= [1] ys + [0] 559.50/148.09 = [ys] 559.50/148.09 559.50/148.09 [app(Cons(x, xs), ys)] = [1] xs + [2] ys + [1] 559.50/148.09 >= [1] xs + [2] ys + [1] 559.50/148.09 = [Cons(x, app(xs, ys))] 559.50/148.10 559.50/148.10 [>(S(x), S(y))] = [0] 559.50/148.10 >= [0] 559.50/148.10 = [>(x, y)] 559.50/148.10 559.50/148.10 [>(S(x), 0())] = [0] 559.50/148.10 >= [0] 559.50/148.10 = [True()] 559.50/148.10 559.50/148.10 [>(0(), y)] = [0] 559.50/148.10 >= [0] 559.50/148.10 = [False()] 559.50/148.10 559.50/148.10 [<(x, 0())] = [0] 559.50/148.10 >= [0] 559.50/148.10 = [False()] 559.50/148.10 559.50/148.10 [<(S(x), S(y))] = [0] 559.50/148.10 >= [0] 559.50/148.10 = [<(x, y)] 559.50/148.10 559.50/148.10 [<(0(), S(y))] = [0] 559.50/148.10 >= [0] 559.50/148.10 = [True()] 559.50/148.10 559.50/148.10 [part^#(x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] 559.50/148.10 >= [1] xs + [1] 559.50/148.10 = [c_2(part[Ite][True][Ite]^#(>(x', x), 559.50/148.10 x', 559.50/148.10 Cons(x, xs), 559.50/148.10 xs1, 559.50/148.10 xs2))] 559.50/148.10 559.50/148.10 [part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2)] = [1] xs + [1] 559.50/148.10 > [1] xs + [0] 559.50/148.10 = [c_3(part^#(x', xs, Cons(x, xs1), xs2))] 559.50/148.10 559.50/148.10 [quicksort^#(Cons(x, Cons(x', xs)))] = [4] xs + [8] 559.50/148.10 > [4] xs + [7] 559.50/148.10 = [c_4(part^#(x, Cons(x', xs), Nil(), Nil()))] 559.50/148.10 559.50/148.10 [quicksort^#(Cons(x, Cons(x', xs)))] = [4] xs + [8] 559.50/148.10 > [4] xs + [7] 559.50/148.10 = [c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil())))] 559.50/148.10 559.50/148.10 [qs^#(x', Cons(x, xs))] = [4] xs + [4] 559.50/148.10 > [4] xs + [1] 559.50/148.10 = [c_6(quicksort^#(xs))] 559.50/148.10 559.50/148.10 559.50/148.10 We return to the main proof. Consider the set of all dependency 559.50/148.10 pairs 559.50/148.10 559.50/148.10 : 559.50/148.10 { 1: part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.10 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.50/148.10 , 2: part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.10 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.10 , 3: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.10 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.10 , 4: quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.10 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.50/148.10 , 5: qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.50/148.10 559.50/148.10 Processor 'matrix interpretation of dimension 1' induces the 559.50/148.10 complexity certificate YES(?,O(n^1)) on application of dependency 559.50/148.10 pairs {2,3,4,5}. These cover all (indirect) predecessors of 559.50/148.10 dependency pairs {1,2,3,4,5}, their number of application is 559.50/148.10 equally bounded. The dependency pairs are shifted into the weak 559.50/148.10 component. 559.50/148.10 559.50/148.10 We are left with following problem, upon which TcT provides the 559.50/148.10 certificate YES(O(1),O(1)). 559.50/148.10 559.50/148.10 Weak DPs: 559.50/148.10 { part^#(x', Cons(x, xs), xs1, xs2) -> 559.50/148.10 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.50/148.10 , part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.10 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.50/148.10 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.10 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.50/148.10 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.50/148.10 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.50/148.10 , qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.50/148.10 Weak Trs: 559.50/148.10 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.10 part(x', xs, Cons(x, xs1), xs2) 559.50/148.10 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.50/148.10 part[Ite][True][Ite][False][Ite](<(x', x), 559.85/148.10 x', 559.85/148.10 Cons(x, xs), 559.85/148.10 xs1, 559.85/148.10 xs2) 559.85/148.10 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.85/148.10 , part(x', Cons(x, xs), xs1, xs2) -> 559.85/148.10 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.85/148.10 , app(Nil(), ys) -> ys 559.85/148.10 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.85/148.10 , >(S(x), S(y)) -> >(x, y) 559.85/148.10 , >(S(x), 0()) -> True() 559.85/148.10 , >(0(), y) -> False() 559.85/148.10 , <(x, 0()) -> False() 559.85/148.10 , <(S(x), S(y)) -> <(x, y) 559.85/148.10 , <(0(), S(y)) -> True() } 559.85/148.10 Obligation: 559.85/148.10 innermost runtime complexity 559.85/148.10 Answer: 559.85/148.10 YES(O(1),O(1)) 559.85/148.10 559.85/148.10 The following weak DPs constitute a sub-graph of the DG that is 559.85/148.10 closed under successors. The DPs are removed. 559.85/148.10 559.85/148.10 { part^#(x', Cons(x, xs), xs1, xs2) -> 559.85/148.10 c_2(part[Ite][True][Ite]^#(>(x', x), x', Cons(x, xs), xs1, xs2)) 559.85/148.10 , part[Ite][True][Ite]^#(True(), x', Cons(x, xs), xs1, xs2) -> 559.85/148.10 c_3(part^#(x', xs, Cons(x, xs1), xs2)) 559.85/148.10 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.85/148.10 c_4(part^#(x, Cons(x', xs), Nil(), Nil())) 559.85/148.10 , quicksort^#(Cons(x, Cons(x', xs))) -> 559.85/148.10 c_5(qs^#(x, part(x, Cons(x', xs), Nil(), Nil()))) 559.85/148.10 , qs^#(x', Cons(x, xs)) -> c_6(quicksort^#(xs)) } 559.85/148.10 559.85/148.10 We are left with following problem, upon which TcT provides the 559.85/148.10 certificate YES(O(1),O(1)). 559.85/148.10 559.85/148.10 Weak Trs: 559.85/148.10 { part[Ite][True][Ite](True(), x', Cons(x, xs), xs1, xs2) -> 559.85/148.10 part(x', xs, Cons(x, xs1), xs2) 559.85/148.10 , part[Ite][True][Ite](False(), x', Cons(x, xs), xs1, xs2) -> 559.85/148.10 part[Ite][True][Ite][False][Ite](<(x', x), 559.85/148.10 x', 559.85/148.10 Cons(x, xs), 559.85/148.10 xs1, 559.85/148.10 xs2) 559.85/148.10 , part(x, Nil(), xs1, xs2) -> app(xs1, xs2) 559.85/148.10 , part(x', Cons(x, xs), xs1, xs2) -> 559.85/148.10 part[Ite][True][Ite](>(x', x), x', Cons(x, xs), xs1, xs2) 559.85/148.10 , app(Nil(), ys) -> ys 559.85/148.10 , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) 559.85/148.10 , >(S(x), S(y)) -> >(x, y) 559.85/148.10 , >(S(x), 0()) -> True() 559.85/148.10 , >(0(), y) -> False() 559.85/148.10 , <(x, 0()) -> False() 559.85/148.10 , <(S(x), S(y)) -> <(x, y) 559.85/148.10 , <(0(), S(y)) -> True() } 559.85/148.10 Obligation: 559.85/148.10 innermost runtime complexity 559.85/148.10 Answer: 559.85/148.10 YES(O(1),O(1)) 559.85/148.10 559.85/148.10 No rule is usable, rules are removed from the input problem. 559.85/148.10 559.85/148.10 We are left with following problem, upon which TcT provides the 559.85/148.10 certificate YES(O(1),O(1)). 559.85/148.10 559.85/148.10 Rules: Empty 559.85/148.10 Obligation: 559.85/148.10 innermost runtime complexity 559.85/148.10 Answer: 559.85/148.10 YES(O(1),O(1)) 559.85/148.10 559.85/148.10 Empty rules are trivially bounded 559.85/148.10 559.85/148.10 Hurray, we answered YES(O(1),O(n^2)) 560.04/148.39 EOF