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..