MAYBE

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

Strict Trs:
  { ite(tt(), x, y) -> x
  , ite(ff(), x, y) -> y
  , lt(x, 0()) -> ff()
  , lt(0(), s(y)) -> tt()
  , lt(s(x), s(y)) -> lt(x, y)
  , insert(a, nil()) -> cons(a, nil())
  , insert(a, cons(b, l)) ->
    ite(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l)))
  , sort(nil()) -> nil()
  , sort(cons(a, l)) -> insert(a, sort(l)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { ite^#(tt(), x, y) -> c_1()
  , ite^#(ff(), x, y) -> c_2()
  , lt^#(x, 0()) -> c_3()
  , lt^#(0(), s(y)) -> c_4()
  , lt^#(s(x), s(y)) -> c_5(lt^#(x, y))
  , insert^#(a, nil()) -> c_6()
  , insert^#(a, cons(b, l)) ->
    c_7(ite^#(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l))),
        lt^#(a, b),
        insert^#(a, l))
  , sort^#(nil()) -> c_8()
  , sort^#(cons(a, l)) -> c_9(insert^#(a, sort(l)), sort^#(l)) }

and mark the set of starting terms.

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

Strict DPs:
  { ite^#(tt(), x, y) -> c_1()
  , ite^#(ff(), x, y) -> c_2()
  , lt^#(x, 0()) -> c_3()
  , lt^#(0(), s(y)) -> c_4()
  , lt^#(s(x), s(y)) -> c_5(lt^#(x, y))
  , insert^#(a, nil()) -> c_6()
  , insert^#(a, cons(b, l)) ->
    c_7(ite^#(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l))),
        lt^#(a, b),
        insert^#(a, l))
  , sort^#(nil()) -> c_8()
  , sort^#(cons(a, l)) -> c_9(insert^#(a, sort(l)), sort^#(l)) }
Weak Trs:
  { ite(tt(), x, y) -> x
  , ite(ff(), x, y) -> y
  , lt(x, 0()) -> ff()
  , lt(0(), s(y)) -> tt()
  , lt(s(x), s(y)) -> lt(x, y)
  , insert(a, nil()) -> cons(a, nil())
  , insert(a, cons(b, l)) ->
    ite(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l)))
  , sort(nil()) -> nil()
  , sort(cons(a, l)) -> insert(a, sort(l)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: ite^#(tt(), x, y) -> c_1()
    , 2: ite^#(ff(), x, y) -> c_2()
    , 3: lt^#(x, 0()) -> c_3()
    , 4: lt^#(0(), s(y)) -> c_4()
    , 5: lt^#(s(x), s(y)) -> c_5(lt^#(x, y))
    , 6: insert^#(a, nil()) -> c_6()
    , 7: insert^#(a, cons(b, l)) ->
         c_7(ite^#(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l))),
             lt^#(a, b),
             insert^#(a, l))
    , 8: sort^#(nil()) -> c_8()
    , 9: sort^#(cons(a, l)) -> c_9(insert^#(a, sort(l)), sort^#(l)) }

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

Strict DPs:
  { lt^#(s(x), s(y)) -> c_5(lt^#(x, y))
  , insert^#(a, cons(b, l)) ->
    c_7(ite^#(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l))),
        lt^#(a, b),
        insert^#(a, l))
  , sort^#(cons(a, l)) -> c_9(insert^#(a, sort(l)), sort^#(l)) }
Weak DPs:
  { ite^#(tt(), x, y) -> c_1()
  , ite^#(ff(), x, y) -> c_2()
  , lt^#(x, 0()) -> c_3()
  , lt^#(0(), s(y)) -> c_4()
  , insert^#(a, nil()) -> c_6()
  , sort^#(nil()) -> c_8() }
Weak Trs:
  { ite(tt(), x, y) -> x
  , ite(ff(), x, y) -> y
  , lt(x, 0()) -> ff()
  , lt(0(), s(y)) -> tt()
  , lt(s(x), s(y)) -> lt(x, y)
  , insert(a, nil()) -> cons(a, nil())
  , insert(a, cons(b, l)) ->
    ite(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l)))
  , sort(nil()) -> nil()
  , sort(cons(a, l)) -> insert(a, sort(l)) }
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.

{ ite^#(tt(), x, y) -> c_1()
, ite^#(ff(), x, y) -> c_2()
, lt^#(x, 0()) -> c_3()
, lt^#(0(), s(y)) -> c_4()
, insert^#(a, nil()) -> c_6()
, sort^#(nil()) -> c_8() }

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

Strict DPs:
  { lt^#(s(x), s(y)) -> c_5(lt^#(x, y))
  , insert^#(a, cons(b, l)) ->
    c_7(ite^#(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l))),
        lt^#(a, b),
        insert^#(a, l))
  , sort^#(cons(a, l)) -> c_9(insert^#(a, sort(l)), sort^#(l)) }
Weak Trs:
  { ite(tt(), x, y) -> x
  , ite(ff(), x, y) -> y
  , lt(x, 0()) -> ff()
  , lt(0(), s(y)) -> tt()
  , lt(s(x), s(y)) -> lt(x, y)
  , insert(a, nil()) -> cons(a, nil())
  , insert(a, cons(b, l)) ->
    ite(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l)))
  , sort(nil()) -> nil()
  , sort(cons(a, l)) -> insert(a, sort(l)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { insert^#(a, cons(b, l)) ->
    c_7(ite^#(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l))),
        lt^#(a, b),
        insert^#(a, l)) }

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))
  , insert^#(a, cons(b, l)) -> c_2(lt^#(a, b), insert^#(a, l))
  , sort^#(cons(a, l)) -> c_3(insert^#(a, sort(l)), sort^#(l)) }
Weak Trs:
  { ite(tt(), x, y) -> x
  , ite(ff(), x, y) -> y
  , lt(x, 0()) -> ff()
  , lt(0(), s(y)) -> tt()
  , lt(s(x), s(y)) -> lt(x, y)
  , insert(a, nil()) -> cons(a, nil())
  , insert(a, cons(b, l)) ->
    ite(lt(a, b), cons(a, cons(b, l)), cons(b, insert(a, l)))
  , sort(nil()) -> nil()
  , sort(cons(a, l)) -> insert(a, sort(l)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..