MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { lt(0(), s(X)) -> true()
  , lt(s(X), 0()) -> false()
  , lt(s(X), s(Y)) -> lt(X, Y)
  , append(nil(), Y) -> Y
  , append(add(N, X), Y) -> add(N, append(X, Y))
  , split(N, nil()) -> pair(nil(), nil())
  , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
  , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
  , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
  , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
  , qsort(nil()) -> nil()
  , qsort(add(N, X)) -> f_3(split(N, X), N, X)
  , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { lt^#(0(), s(X)) -> c_1()
  , lt^#(s(X), 0()) -> c_2()
  , lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
  , append^#(nil(), Y) -> c_4()
  , append^#(add(N, X), Y) -> c_5(append^#(X, Y))
  , split^#(N, nil()) -> c_6()
  , split^#(N, add(M, Y)) ->
    c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))
  , f_1^#(pair(X, Z), N, M, Y) ->
    c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M))
  , f_2^#(true(), N, M, Y, X, Z) -> c_9()
  , f_2^#(false(), N, M, Y, X, Z) -> c_10()
  , qsort^#(nil()) -> c_11()
  , qsort^#(add(N, X)) ->
    c_12(f_3^#(split(N, X), N, X), split^#(N, X))
  , f_3^#(pair(Y, Z), N, X) ->
    c_13(append^#(qsort(Y), add(X, qsort(Z))),
         qsort^#(Y),
         qsort^#(Z)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lt^#(0(), s(X)) -> c_1()
  , lt^#(s(X), 0()) -> c_2()
  , lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
  , append^#(nil(), Y) -> c_4()
  , append^#(add(N, X), Y) -> c_5(append^#(X, Y))
  , split^#(N, nil()) -> c_6()
  , split^#(N, add(M, Y)) ->
    c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))
  , f_1^#(pair(X, Z), N, M, Y) ->
    c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M))
  , f_2^#(true(), N, M, Y, X, Z) -> c_9()
  , f_2^#(false(), N, M, Y, X, Z) -> c_10()
  , qsort^#(nil()) -> c_11()
  , qsort^#(add(N, X)) ->
    c_12(f_3^#(split(N, X), N, X), split^#(N, X))
  , f_3^#(pair(Y, Z), N, X) ->
    c_13(append^#(qsort(Y), add(X, qsort(Z))),
         qsort^#(Y),
         qsort^#(Z)) }
Weak Trs:
  { lt(0(), s(X)) -> true()
  , lt(s(X), 0()) -> false()
  , lt(s(X), s(Y)) -> lt(X, Y)
  , append(nil(), Y) -> Y
  , append(add(N, X), Y) -> add(N, append(X, Y))
  , split(N, nil()) -> pair(nil(), nil())
  , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
  , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
  , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
  , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
  , qsort(nil()) -> nil()
  , qsort(add(N, X)) -> f_3(split(N, X), N, X)
  , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1,2,4,6,9,10,11} by
applications of Pre({1,2,4,6,9,10,11}) = {3,5,7,8,12,13}. Here
rules are labeled as follows:

  DPs:
    { 1: lt^#(0(), s(X)) -> c_1()
    , 2: lt^#(s(X), 0()) -> c_2()
    , 3: lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
    , 4: append^#(nil(), Y) -> c_4()
    , 5: append^#(add(N, X), Y) -> c_5(append^#(X, Y))
    , 6: split^#(N, nil()) -> c_6()
    , 7: split^#(N, add(M, Y)) ->
         c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))
    , 8: f_1^#(pair(X, Z), N, M, Y) ->
         c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M))
    , 9: f_2^#(true(), N, M, Y, X, Z) -> c_9()
    , 10: f_2^#(false(), N, M, Y, X, Z) -> c_10()
    , 11: qsort^#(nil()) -> c_11()
    , 12: qsort^#(add(N, X)) ->
          c_12(f_3^#(split(N, X), N, X), split^#(N, X))
    , 13: f_3^#(pair(Y, Z), N, X) ->
          c_13(append^#(qsort(Y), add(X, qsort(Z))),
               qsort^#(Y),
               qsort^#(Z)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
  , append^#(add(N, X), Y) -> c_5(append^#(X, Y))
  , split^#(N, add(M, Y)) ->
    c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))
  , f_1^#(pair(X, Z), N, M, Y) ->
    c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M))
  , qsort^#(add(N, X)) ->
    c_12(f_3^#(split(N, X), N, X), split^#(N, X))
  , f_3^#(pair(Y, Z), N, X) ->
    c_13(append^#(qsort(Y), add(X, qsort(Z))),
         qsort^#(Y),
         qsort^#(Z)) }
Weak DPs:
  { lt^#(0(), s(X)) -> c_1()
  , lt^#(s(X), 0()) -> c_2()
  , append^#(nil(), Y) -> c_4()
  , split^#(N, nil()) -> c_6()
  , f_2^#(true(), N, M, Y, X, Z) -> c_9()
  , f_2^#(false(), N, M, Y, X, Z) -> c_10()
  , qsort^#(nil()) -> c_11() }
Weak Trs:
  { lt(0(), s(X)) -> true()
  , lt(s(X), 0()) -> false()
  , lt(s(X), s(Y)) -> lt(X, Y)
  , append(nil(), Y) -> Y
  , append(add(N, X), Y) -> add(N, append(X, Y))
  , split(N, nil()) -> pair(nil(), nil())
  , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
  , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
  , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
  , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
  , qsort(nil()) -> nil()
  , qsort(add(N, X)) -> f_3(split(N, X), N, X)
  , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
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.

{ lt^#(0(), s(X)) -> c_1()
, lt^#(s(X), 0()) -> c_2()
, append^#(nil(), Y) -> c_4()
, split^#(N, nil()) -> c_6()
, f_2^#(true(), N, M, Y, X, Z) -> c_9()
, f_2^#(false(), N, M, Y, X, Z) -> c_10()
, qsort^#(nil()) -> c_11() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y))
  , append^#(add(N, X), Y) -> c_5(append^#(X, Y))
  , split^#(N, add(M, Y)) ->
    c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))
  , f_1^#(pair(X, Z), N, M, Y) ->
    c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M))
  , qsort^#(add(N, X)) ->
    c_12(f_3^#(split(N, X), N, X), split^#(N, X))
  , f_3^#(pair(Y, Z), N, X) ->
    c_13(append^#(qsort(Y), add(X, qsort(Z))),
         qsort^#(Y),
         qsort^#(Z)) }
Weak Trs:
  { lt(0(), s(X)) -> true()
  , lt(s(X), 0()) -> false()
  , lt(s(X), s(Y)) -> lt(X, Y)
  , append(nil(), Y) -> Y
  , append(add(N, X), Y) -> add(N, append(X, Y))
  , split(N, nil()) -> pair(nil(), nil())
  , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
  , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
  , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
  , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
  , qsort(nil()) -> nil()
  , qsort(add(N, X)) -> f_3(split(N, X), N, X)
  , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { f_1^#(pair(X, Z), N, M, Y) ->
    c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { lt^#(s(X), s(Y)) -> c_1(lt^#(X, Y))
  , append^#(add(N, X), Y) -> c_2(append^#(X, Y))
  , split^#(N, add(M, Y)) ->
    c_3(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))
  , f_1^#(pair(X, Z), N, M, Y) -> c_4(lt^#(N, M))
  , qsort^#(add(N, X)) ->
    c_5(f_3^#(split(N, X), N, X), split^#(N, X))
  , f_3^#(pair(Y, Z), N, X) ->
    c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z)) }
Weak Trs:
  { lt(0(), s(X)) -> true()
  , lt(s(X), 0()) -> false()
  , lt(s(X), s(Y)) -> lt(X, Y)
  , append(nil(), Y) -> Y
  , append(add(N, X), Y) -> add(N, append(X, Y))
  , split(N, nil()) -> pair(nil(), nil())
  , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
  , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
  , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
  , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
  , qsort(nil()) -> nil()
  , qsort(add(N, X)) -> f_3(split(N, X), N, X)
  , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..