MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { qsort^#(nil()) -> c_1() , qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))), qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) , append^#(nil(), ys()) -> c_3() , append^#(cons(x, xs), ys()) -> c_4(append^#(xs, ys())) , filterlow^#(n, nil()) -> c_5() , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , filterhigh^#(n, nil()) -> c_7() , filterhigh^#(n, cons(x, xs)) -> c_8(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_9(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_10(filterlow^#(n, xs)) , ge^#(x, 0()) -> c_11() , ge^#(0(), s(x)) -> c_12() , ge^#(s(x), s(y)) -> c_13(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_14(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_15(filterhigh^#(n, xs)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(nil()) -> c_1() , qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))), qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) , append^#(nil(), ys()) -> c_3() , append^#(cons(x, xs), ys()) -> c_4(append^#(xs, ys())) , filterlow^#(n, nil()) -> c_5() , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , filterhigh^#(n, nil()) -> c_7() , filterhigh^#(n, cons(x, xs)) -> c_8(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_9(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_10(filterlow^#(n, xs)) , ge^#(x, 0()) -> c_11() , ge^#(0(), s(x)) -> c_12() , ge^#(s(x), s(y)) -> c_13(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_14(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_15(filterhigh^#(n, xs)) } Weak Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,5,7,11,12} by applications of Pre({1,3,5,7,11,12}) = {2,4,6,8,9,10,13,14,15}. Here rules are labeled as follows: DPs: { 1: qsort^#(nil()) -> c_1() , 2: qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))), qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) , 3: append^#(nil(), ys()) -> c_3() , 4: append^#(cons(x, xs), ys()) -> c_4(append^#(xs, ys())) , 5: filterlow^#(n, nil()) -> c_5() , 6: filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , 7: filterhigh^#(n, nil()) -> c_7() , 8: filterhigh^#(n, cons(x, xs)) -> c_8(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , 9: if1^#(true(), n, x, xs) -> c_9(filterlow^#(n, xs)) , 10: if1^#(false(), n, x, xs) -> c_10(filterlow^#(n, xs)) , 11: ge^#(x, 0()) -> c_11() , 12: ge^#(0(), s(x)) -> c_12() , 13: ge^#(s(x), s(y)) -> c_13(ge^#(x, y)) , 14: if2^#(true(), n, x, xs) -> c_14(filterhigh^#(n, xs)) , 15: if2^#(false(), n, x, xs) -> c_15(filterhigh^#(n, xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))), qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) , append^#(cons(x, xs), ys()) -> c_4(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , filterhigh^#(n, cons(x, xs)) -> c_8(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_9(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_10(filterlow^#(n, xs)) , ge^#(s(x), s(y)) -> c_13(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_14(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_15(filterhigh^#(n, xs)) } Weak DPs: { qsort^#(nil()) -> c_1() , append^#(nil(), ys()) -> c_3() , filterlow^#(n, nil()) -> c_5() , filterhigh^#(n, nil()) -> c_7() , ge^#(x, 0()) -> c_11() , ge^#(0(), s(x)) -> c_12() } Weak Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { qsort^#(nil()) -> c_1() , append^#(nil(), ys()) -> c_3() , filterlow^#(n, nil()) -> c_5() , filterhigh^#(n, nil()) -> c_7() , ge^#(x, 0()) -> c_11() , ge^#(0(), s(x)) -> c_12() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))), qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) , append^#(cons(x, xs), ys()) -> c_4(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , filterhigh^#(n, cons(x, xs)) -> c_8(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_9(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_10(filterlow^#(n, xs)) , ge^#(s(x), s(y)) -> c_13(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_14(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_15(filterhigh^#(n, xs)) } Weak Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))), qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(cons(x, xs)) -> c_1(qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) , append^#(cons(x, xs), ys()) -> c_2(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_3(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , filterhigh^#(n, cons(x, xs)) -> c_4(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_5(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_6(filterlow^#(n, xs)) , ge^#(s(x), s(y)) -> c_7(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_8(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_9(filterhigh^#(n, xs)) } Weak Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(cons(x, xs)) -> c_1(qsort^#(filterlow(x, cons(x, xs))), filterlow^#(x, cons(x, xs)), qsort^#(filterhigh(x, cons(x, xs))), filterhigh^#(x, cons(x, xs))) , append^#(cons(x, xs), ys()) -> c_2(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_3(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , filterhigh^#(n, cons(x, xs)) -> c_4(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_5(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_6(filterlow^#(n, xs)) , ge^#(s(x), s(y)) -> c_7(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_8(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_9(filterhigh^#(n, xs)) } Weak Trs: { filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..