MAYBE

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

Strict Trs:
  { min(0(), y) -> 0()
  , min(s(x), 0()) -> 0()
  , min(s(x), s(y)) -> min(x, y)
  , len(nil()) -> 0()
  , len(cons(x, xs)) -> s(len(xs))
  , sum(x, 0()) -> x
  , sum(x, s(y)) -> s(sum(x, y))
  , le(0(), x) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , take(0(), cons(y, ys)) -> y
  , take(s(x), cons(y, ys)) -> take(x, ys)
  , addList(x, y) ->
    if(le(0(), min(len(x), len(y))), 0(), x, y, nil())
  , if(true(), c, xs, ys, z) ->
    if(le(s(c), min(len(xs), len(ys))),
       s(c),
       xs,
       ys,
       cons(sum(take(c, xs), take(c, ys)), z))
  , if(false(), c, x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { min^#(0(), y) -> c_1()
  , min^#(s(x), 0()) -> c_2()
  , min^#(s(x), s(y)) -> c_3(min^#(x, y))
  , len^#(nil()) -> c_4()
  , len^#(cons(x, xs)) -> c_5(len^#(xs))
  , sum^#(x, 0()) -> c_6()
  , sum^#(x, s(y)) -> c_7(sum^#(x, y))
  , le^#(0(), x) -> c_8()
  , le^#(s(x), 0()) -> c_9()
  , le^#(s(x), s(y)) -> c_10(le^#(x, y))
  , take^#(0(), cons(y, ys)) -> c_11()
  , take^#(s(x), cons(y, ys)) -> c_12(take^#(x, ys))
  , addList^#(x, y) ->
    c_13(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
         le^#(0(), min(len(x), len(y))),
         min^#(len(x), len(y)),
         len^#(x),
         len^#(y))
  , if^#(true(), c, xs, ys, z) ->
    c_14(if^#(le(s(c), min(len(xs), len(ys))),
              s(c),
              xs,
              ys,
              cons(sum(take(c, xs), take(c, ys)), z)),
         le^#(s(c), min(len(xs), len(ys))),
         min^#(len(xs), len(ys)),
         len^#(xs),
         len^#(ys),
         sum^#(take(c, xs), take(c, ys)),
         take^#(c, xs),
         take^#(c, ys))
  , if^#(false(), c, x, y, z) -> c_15() }

and mark the set of starting terms.

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

Strict DPs:
  { min^#(0(), y) -> c_1()
  , min^#(s(x), 0()) -> c_2()
  , min^#(s(x), s(y)) -> c_3(min^#(x, y))
  , len^#(nil()) -> c_4()
  , len^#(cons(x, xs)) -> c_5(len^#(xs))
  , sum^#(x, 0()) -> c_6()
  , sum^#(x, s(y)) -> c_7(sum^#(x, y))
  , le^#(0(), x) -> c_8()
  , le^#(s(x), 0()) -> c_9()
  , le^#(s(x), s(y)) -> c_10(le^#(x, y))
  , take^#(0(), cons(y, ys)) -> c_11()
  , take^#(s(x), cons(y, ys)) -> c_12(take^#(x, ys))
  , addList^#(x, y) ->
    c_13(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
         le^#(0(), min(len(x), len(y))),
         min^#(len(x), len(y)),
         len^#(x),
         len^#(y))
  , if^#(true(), c, xs, ys, z) ->
    c_14(if^#(le(s(c), min(len(xs), len(ys))),
              s(c),
              xs,
              ys,
              cons(sum(take(c, xs), take(c, ys)), z)),
         le^#(s(c), min(len(xs), len(ys))),
         min^#(len(xs), len(ys)),
         len^#(xs),
         len^#(ys),
         sum^#(take(c, xs), take(c, ys)),
         take^#(c, xs),
         take^#(c, ys))
  , if^#(false(), c, x, y, z) -> c_15() }
Weak Trs:
  { min(0(), y) -> 0()
  , min(s(x), 0()) -> 0()
  , min(s(x), s(y)) -> min(x, y)
  , len(nil()) -> 0()
  , len(cons(x, xs)) -> s(len(xs))
  , sum(x, 0()) -> x
  , sum(x, s(y)) -> s(sum(x, y))
  , le(0(), x) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , take(0(), cons(y, ys)) -> y
  , take(s(x), cons(y, ys)) -> take(x, ys)
  , addList(x, y) ->
    if(le(0(), min(len(x), len(y))), 0(), x, y, nil())
  , if(true(), c, xs, ys, z) ->
    if(le(s(c), min(len(xs), len(ys))),
       s(c),
       xs,
       ys,
       cons(sum(take(c, xs), take(c, ys)), z))
  , if(false(), c, x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: min^#(0(), y) -> c_1()
    , 2: min^#(s(x), 0()) -> c_2()
    , 3: min^#(s(x), s(y)) -> c_3(min^#(x, y))
    , 4: len^#(nil()) -> c_4()
    , 5: len^#(cons(x, xs)) -> c_5(len^#(xs))
    , 6: sum^#(x, 0()) -> c_6()
    , 7: sum^#(x, s(y)) -> c_7(sum^#(x, y))
    , 8: le^#(0(), x) -> c_8()
    , 9: le^#(s(x), 0()) -> c_9()
    , 10: le^#(s(x), s(y)) -> c_10(le^#(x, y))
    , 11: take^#(0(), cons(y, ys)) -> c_11()
    , 12: take^#(s(x), cons(y, ys)) -> c_12(take^#(x, ys))
    , 13: addList^#(x, y) ->
          c_13(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
               le^#(0(), min(len(x), len(y))),
               min^#(len(x), len(y)),
               len^#(x),
               len^#(y))
    , 14: if^#(true(), c, xs, ys, z) ->
          c_14(if^#(le(s(c), min(len(xs), len(ys))),
                    s(c),
                    xs,
                    ys,
                    cons(sum(take(c, xs), take(c, ys)), z)),
               le^#(s(c), min(len(xs), len(ys))),
               min^#(len(xs), len(ys)),
               len^#(xs),
               len^#(ys),
               sum^#(take(c, xs), take(c, ys)),
               take^#(c, xs),
               take^#(c, ys))
    , 15: if^#(false(), c, x, y, z) -> c_15() }

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

Strict DPs:
  { min^#(s(x), s(y)) -> c_3(min^#(x, y))
  , len^#(cons(x, xs)) -> c_5(len^#(xs))
  , sum^#(x, s(y)) -> c_7(sum^#(x, y))
  , le^#(s(x), s(y)) -> c_10(le^#(x, y))
  , take^#(s(x), cons(y, ys)) -> c_12(take^#(x, ys))
  , addList^#(x, y) ->
    c_13(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
         le^#(0(), min(len(x), len(y))),
         min^#(len(x), len(y)),
         len^#(x),
         len^#(y))
  , if^#(true(), c, xs, ys, z) ->
    c_14(if^#(le(s(c), min(len(xs), len(ys))),
              s(c),
              xs,
              ys,
              cons(sum(take(c, xs), take(c, ys)), z)),
         le^#(s(c), min(len(xs), len(ys))),
         min^#(len(xs), len(ys)),
         len^#(xs),
         len^#(ys),
         sum^#(take(c, xs), take(c, ys)),
         take^#(c, xs),
         take^#(c, ys)) }
Weak DPs:
  { min^#(0(), y) -> c_1()
  , min^#(s(x), 0()) -> c_2()
  , len^#(nil()) -> c_4()
  , sum^#(x, 0()) -> c_6()
  , le^#(0(), x) -> c_8()
  , le^#(s(x), 0()) -> c_9()
  , take^#(0(), cons(y, ys)) -> c_11()
  , if^#(false(), c, x, y, z) -> c_15() }
Weak Trs:
  { min(0(), y) -> 0()
  , min(s(x), 0()) -> 0()
  , min(s(x), s(y)) -> min(x, y)
  , len(nil()) -> 0()
  , len(cons(x, xs)) -> s(len(xs))
  , sum(x, 0()) -> x
  , sum(x, s(y)) -> s(sum(x, y))
  , le(0(), x) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , take(0(), cons(y, ys)) -> y
  , take(s(x), cons(y, ys)) -> take(x, ys)
  , addList(x, y) ->
    if(le(0(), min(len(x), len(y))), 0(), x, y, nil())
  , if(true(), c, xs, ys, z) ->
    if(le(s(c), min(len(xs), len(ys))),
       s(c),
       xs,
       ys,
       cons(sum(take(c, xs), take(c, ys)), z))
  , if(false(), c, x, y, z) -> 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.

{ min^#(0(), y) -> c_1()
, min^#(s(x), 0()) -> c_2()
, len^#(nil()) -> c_4()
, sum^#(x, 0()) -> c_6()
, le^#(0(), x) -> c_8()
, le^#(s(x), 0()) -> c_9()
, take^#(0(), cons(y, ys)) -> c_11()
, if^#(false(), c, x, y, z) -> c_15() }

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

Strict DPs:
  { min^#(s(x), s(y)) -> c_3(min^#(x, y))
  , len^#(cons(x, xs)) -> c_5(len^#(xs))
  , sum^#(x, s(y)) -> c_7(sum^#(x, y))
  , le^#(s(x), s(y)) -> c_10(le^#(x, y))
  , take^#(s(x), cons(y, ys)) -> c_12(take^#(x, ys))
  , addList^#(x, y) ->
    c_13(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
         le^#(0(), min(len(x), len(y))),
         min^#(len(x), len(y)),
         len^#(x),
         len^#(y))
  , if^#(true(), c, xs, ys, z) ->
    c_14(if^#(le(s(c), min(len(xs), len(ys))),
              s(c),
              xs,
              ys,
              cons(sum(take(c, xs), take(c, ys)), z)),
         le^#(s(c), min(len(xs), len(ys))),
         min^#(len(xs), len(ys)),
         len^#(xs),
         len^#(ys),
         sum^#(take(c, xs), take(c, ys)),
         take^#(c, xs),
         take^#(c, ys)) }
Weak Trs:
  { min(0(), y) -> 0()
  , min(s(x), 0()) -> 0()
  , min(s(x), s(y)) -> min(x, y)
  , len(nil()) -> 0()
  , len(cons(x, xs)) -> s(len(xs))
  , sum(x, 0()) -> x
  , sum(x, s(y)) -> s(sum(x, y))
  , le(0(), x) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , take(0(), cons(y, ys)) -> y
  , take(s(x), cons(y, ys)) -> take(x, ys)
  , addList(x, y) ->
    if(le(0(), min(len(x), len(y))), 0(), x, y, nil())
  , if(true(), c, xs, ys, z) ->
    if(le(s(c), min(len(xs), len(ys))),
       s(c),
       xs,
       ys,
       cons(sum(take(c, xs), take(c, ys)), z))
  , if(false(), c, x, y, z) -> 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:

  { addList^#(x, y) ->
    c_13(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
         le^#(0(), min(len(x), len(y))),
         min^#(len(x), len(y)),
         len^#(x),
         len^#(y)) }

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

Strict DPs:
  { min^#(s(x), s(y)) -> c_1(min^#(x, y))
  , len^#(cons(x, xs)) -> c_2(len^#(xs))
  , sum^#(x, s(y)) -> c_3(sum^#(x, y))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , take^#(s(x), cons(y, ys)) -> c_5(take^#(x, ys))
  , addList^#(x, y) ->
    c_6(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
        min^#(len(x), len(y)),
        len^#(x),
        len^#(y))
  , if^#(true(), c, xs, ys, z) ->
    c_7(if^#(le(s(c), min(len(xs), len(ys))),
             s(c),
             xs,
             ys,
             cons(sum(take(c, xs), take(c, ys)), z)),
        le^#(s(c), min(len(xs), len(ys))),
        min^#(len(xs), len(ys)),
        len^#(xs),
        len^#(ys),
        sum^#(take(c, xs), take(c, ys)),
        take^#(c, xs),
        take^#(c, ys)) }
Weak Trs:
  { min(0(), y) -> 0()
  , min(s(x), 0()) -> 0()
  , min(s(x), s(y)) -> min(x, y)
  , len(nil()) -> 0()
  , len(cons(x, xs)) -> s(len(xs))
  , sum(x, 0()) -> x
  , sum(x, s(y)) -> s(sum(x, y))
  , le(0(), x) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , take(0(), cons(y, ys)) -> y
  , take(s(x), cons(y, ys)) -> take(x, ys)
  , addList(x, y) ->
    if(le(0(), min(len(x), len(y))), 0(), x, y, nil())
  , if(true(), c, xs, ys, z) ->
    if(le(s(c), min(len(xs), len(ys))),
       s(c),
       xs,
       ys,
       cons(sum(take(c, xs), take(c, ys)), z))
  , if(false(), c, x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { min(0(), y) -> 0()
    , min(s(x), 0()) -> 0()
    , min(s(x), s(y)) -> min(x, y)
    , len(nil()) -> 0()
    , len(cons(x, xs)) -> s(len(xs))
    , sum(x, 0()) -> x
    , sum(x, s(y)) -> s(sum(x, y))
    , le(0(), x) -> true()
    , le(s(x), 0()) -> false()
    , le(s(x), s(y)) -> le(x, y)
    , take(0(), cons(y, ys)) -> y
    , take(s(x), cons(y, ys)) -> take(x, ys) }

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

Strict DPs:
  { min^#(s(x), s(y)) -> c_1(min^#(x, y))
  , len^#(cons(x, xs)) -> c_2(len^#(xs))
  , sum^#(x, s(y)) -> c_3(sum^#(x, y))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , take^#(s(x), cons(y, ys)) -> c_5(take^#(x, ys))
  , addList^#(x, y) ->
    c_6(if^#(le(0(), min(len(x), len(y))), 0(), x, y, nil()),
        min^#(len(x), len(y)),
        len^#(x),
        len^#(y))
  , if^#(true(), c, xs, ys, z) ->
    c_7(if^#(le(s(c), min(len(xs), len(ys))),
             s(c),
             xs,
             ys,
             cons(sum(take(c, xs), take(c, ys)), z)),
        le^#(s(c), min(len(xs), len(ys))),
        min^#(len(xs), len(ys)),
        len^#(xs),
        len^#(ys),
        sum^#(take(c, xs), take(c, ys)),
        take^#(c, xs),
        take^#(c, ys)) }
Weak Trs:
  { min(0(), y) -> 0()
  , min(s(x), 0()) -> 0()
  , min(s(x), s(y)) -> min(x, y)
  , len(nil()) -> 0()
  , len(cons(x, xs)) -> s(len(xs))
  , sum(x, 0()) -> x
  , sum(x, s(y)) -> s(sum(x, y))
  , le(0(), x) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , take(0(), cons(y, ys)) -> y
  , take(s(x), cons(y, ys)) -> take(x, ys) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..