MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { qsort(xs) -> qs(half(length(xs)), xs) , qs(n, nil()) -> nil() , qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , length(nil()) -> 0() , length(cons(x, xs)) -> s(length(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) , get(n, nil()) -> 0() , get(n, cons(x, nil())) -> x , get(0(), cons(x, cons(y, xs))) -> x , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, 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^#(xs) -> c_1(qs^#(half(length(xs)), xs), half^#(length(xs)), length^#(xs)) , qs^#(n, nil()) -> c_2() , qs^#(n, cons(x, xs)) -> c_3(append^#(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))), qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) , half^#(0()) -> c_4() , half^#(s(0())) -> c_5() , half^#(s(s(x))) -> c_6(half^#(x)) , length^#(nil()) -> c_7() , length^#(cons(x, xs)) -> c_8(length^#(xs)) , append^#(nil(), ys()) -> c_9() , append^#(cons(x, xs), ys()) -> c_10(append^#(xs, ys())) , filterlow^#(n, nil()) -> c_11() , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , get^#(n, nil()) -> c_13() , get^#(n, cons(x, nil())) -> c_14() , get^#(0(), cons(x, cons(y, xs))) -> c_15() , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs))) , filterhigh^#(n, nil()) -> c_17() , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_20(filterlow^#(n, xs)) , ge^#(x, 0()) -> c_21() , ge^#(0(), s(x)) -> c_22() , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_25(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^#(xs) -> c_1(qs^#(half(length(xs)), xs), half^#(length(xs)), length^#(xs)) , qs^#(n, nil()) -> c_2() , qs^#(n, cons(x, xs)) -> c_3(append^#(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))), qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) , half^#(0()) -> c_4() , half^#(s(0())) -> c_5() , half^#(s(s(x))) -> c_6(half^#(x)) , length^#(nil()) -> c_7() , length^#(cons(x, xs)) -> c_8(length^#(xs)) , append^#(nil(), ys()) -> c_9() , append^#(cons(x, xs), ys()) -> c_10(append^#(xs, ys())) , filterlow^#(n, nil()) -> c_11() , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , get^#(n, nil()) -> c_13() , get^#(n, cons(x, nil())) -> c_14() , get^#(0(), cons(x, cons(y, xs))) -> c_15() , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs))) , filterhigh^#(n, nil()) -> c_17() , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_20(filterlow^#(n, xs)) , ge^#(x, 0()) -> c_21() , ge^#(0(), s(x)) -> c_22() , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_25(filterhigh^#(n, xs)) } Weak Trs: { qsort(xs) -> qs(half(length(xs)), xs) , qs(n, nil()) -> nil() , qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , length(nil()) -> 0() , length(cons(x, xs)) -> s(length(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) , get(n, nil()) -> 0() , get(n, cons(x, nil())) -> x , get(0(), cons(x, cons(y, xs))) -> x , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, 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 {2,4,5,7,9,11,13,14,15,17,21,22} by applications of Pre({2,4,5,7,9,11,13,14,15,17,21,22}) = {1,3,6,8,10,12,16,18,19,20,23,24,25}. Here rules are labeled as follows: DPs: { 1: qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs), half^#(length(xs)), length^#(xs)) , 2: qs^#(n, nil()) -> c_2() , 3: qs^#(n, cons(x, xs)) -> c_3(append^#(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))), qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) , 4: half^#(0()) -> c_4() , 5: half^#(s(0())) -> c_5() , 6: half^#(s(s(x))) -> c_6(half^#(x)) , 7: length^#(nil()) -> c_7() , 8: length^#(cons(x, xs)) -> c_8(length^#(xs)) , 9: append^#(nil(), ys()) -> c_9() , 10: append^#(cons(x, xs), ys()) -> c_10(append^#(xs, ys())) , 11: filterlow^#(n, nil()) -> c_11() , 12: filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , 13: get^#(n, nil()) -> c_13() , 14: get^#(n, cons(x, nil())) -> c_14() , 15: get^#(0(), cons(x, cons(y, xs))) -> c_15() , 16: get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs))) , 17: filterhigh^#(n, nil()) -> c_17() , 18: filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , 19: if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs)) , 20: if1^#(false(), n, x, xs) -> c_20(filterlow^#(n, xs)) , 21: ge^#(x, 0()) -> c_21() , 22: ge^#(0(), s(x)) -> c_22() , 23: ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) , 24: if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs)) , 25: if2^#(false(), n, x, xs) -> c_25(filterhigh^#(n, xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs), half^#(length(xs)), length^#(xs)) , qs^#(n, cons(x, xs)) -> c_3(append^#(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))), qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) , half^#(s(s(x))) -> c_6(half^#(x)) , length^#(cons(x, xs)) -> c_8(length^#(xs)) , append^#(cons(x, xs), ys()) -> c_10(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs))) , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_20(filterlow^#(n, xs)) , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_25(filterhigh^#(n, xs)) } Weak DPs: { qs^#(n, nil()) -> c_2() , half^#(0()) -> c_4() , half^#(s(0())) -> c_5() , length^#(nil()) -> c_7() , append^#(nil(), ys()) -> c_9() , filterlow^#(n, nil()) -> c_11() , get^#(n, nil()) -> c_13() , get^#(n, cons(x, nil())) -> c_14() , get^#(0(), cons(x, cons(y, xs))) -> c_15() , filterhigh^#(n, nil()) -> c_17() , ge^#(x, 0()) -> c_21() , ge^#(0(), s(x)) -> c_22() } Weak Trs: { qsort(xs) -> qs(half(length(xs)), xs) , qs(n, nil()) -> nil() , qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , length(nil()) -> 0() , length(cons(x, xs)) -> s(length(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) , get(n, nil()) -> 0() , get(n, cons(x, nil())) -> x , get(0(), cons(x, cons(y, xs))) -> x , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, 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. { qs^#(n, nil()) -> c_2() , half^#(0()) -> c_4() , half^#(s(0())) -> c_5() , length^#(nil()) -> c_7() , append^#(nil(), ys()) -> c_9() , filterlow^#(n, nil()) -> c_11() , get^#(n, nil()) -> c_13() , get^#(n, cons(x, nil())) -> c_14() , get^#(0(), cons(x, cons(y, xs))) -> c_15() , filterhigh^#(n, nil()) -> c_17() , ge^#(x, 0()) -> c_21() , ge^#(0(), s(x)) -> c_22() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs), half^#(length(xs)), length^#(xs)) , qs^#(n, cons(x, xs)) -> c_3(append^#(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))), qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) , half^#(s(s(x))) -> c_6(half^#(x)) , length^#(cons(x, xs)) -> c_8(length^#(xs)) , append^#(cons(x, xs), ys()) -> c_10(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs))) , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs), ge^#(x, n)) , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_20(filterlow^#(n, xs)) , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_25(filterhigh^#(n, xs)) } Weak Trs: { qsort(xs) -> qs(half(length(xs)), xs) , qs(n, nil()) -> nil() , qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , length(nil()) -> 0() , length(cons(x, xs)) -> s(length(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) , get(n, nil()) -> 0() , get(n, cons(x, nil())) -> x , get(0(), cons(x, cons(y, xs))) -> x , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, 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: { qs^#(n, cons(x, xs)) -> c_3(append^#(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))), qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs), half^#(length(xs)), length^#(xs)) , qs^#(n, cons(x, xs)) -> c_2(qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) , half^#(s(s(x))) -> c_3(half^#(x)) , length^#(cons(x, xs)) -> c_4(length^#(xs)) , append^#(cons(x, xs), ys()) -> c_5(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , get^#(s(n), cons(x, cons(y, xs))) -> c_7(get^#(n, cons(y, xs))) , 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_11(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_12(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_13(filterhigh^#(n, xs)) } Weak Trs: { qsort(xs) -> qs(half(length(xs)), xs) , qs(n, nil()) -> nil() , qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , length(nil()) -> 0() , length(cons(x, xs)) -> s(length(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) , get(n, nil()) -> 0() , get(n, cons(x, nil())) -> x , get(0(), cons(x, cons(y, xs))) -> x , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, 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: { half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , length(nil()) -> 0() , length(cons(x, xs)) -> s(length(xs)) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , get(n, nil()) -> 0() , get(n, cons(x, nil())) -> x , get(0(), cons(x, cons(y, xs))) -> x , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, 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^#(xs) -> c_1(qs^#(half(length(xs)), xs), half^#(length(xs)), length^#(xs)) , qs^#(n, cons(x, xs)) -> c_2(qs^#(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterlow^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs)), get^#(n, cons(x, xs)), qs^#(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))), half^#(n), filterhigh^#(get(n, cons(x, xs)), cons(x, xs)), get^#(n, cons(x, xs))) , half^#(s(s(x))) -> c_3(half^#(x)) , length^#(cons(x, xs)) -> c_4(length^#(xs)) , append^#(cons(x, xs), ys()) -> c_5(append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs), ge^#(n, x)) , get^#(s(n), cons(x, cons(y, xs))) -> c_7(get^#(n, cons(y, xs))) , 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_11(ge^#(x, y)) , if2^#(true(), n, x, xs) -> c_12(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_13(filterhigh^#(n, xs)) } Weak Trs: { half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , length(nil()) -> 0() , length(cons(x, xs)) -> s(length(xs)) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , get(n, nil()) -> 0() , get(n, cons(x, nil())) -> x , get(0(), cons(x, cons(y, xs))) -> x , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, 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..