MAYBE

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

Strict Trs:
  { sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
  , sum(cons(0(), x), y) -> sum(x, y)
  , sum(nil(), y) -> y
  , weight(cons(n, cons(m, x))) ->
    weight(sum(cons(n, cons(m, x)), cons(0(), x)))
  , weight(cons(n, nil())) -> n }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { sum^#(cons(s(n), x), cons(m, y)) ->
    c_1(sum^#(cons(n, x), cons(s(m), y)))
  , sum^#(cons(0(), x), y) -> c_2(sum^#(x, y))
  , sum^#(nil(), y) -> c_3()
  , weight^#(cons(n, cons(m, x))) ->
    c_4(weight^#(sum(cons(n, cons(m, x)), cons(0(), x))),
        sum^#(cons(n, cons(m, x)), cons(0(), x)))
  , weight^#(cons(n, nil())) -> c_5() }

and mark the set of starting terms.

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

Strict DPs:
  { sum^#(cons(s(n), x), cons(m, y)) ->
    c_1(sum^#(cons(n, x), cons(s(m), y)))
  , sum^#(cons(0(), x), y) -> c_2(sum^#(x, y))
  , sum^#(nil(), y) -> c_3()
  , weight^#(cons(n, cons(m, x))) ->
    c_4(weight^#(sum(cons(n, cons(m, x)), cons(0(), x))),
        sum^#(cons(n, cons(m, x)), cons(0(), x)))
  , weight^#(cons(n, nil())) -> c_5() }
Weak Trs:
  { sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
  , sum(cons(0(), x), y) -> sum(x, y)
  , sum(nil(), y) -> y
  , weight(cons(n, cons(m, x))) ->
    weight(sum(cons(n, cons(m, x)), cons(0(), x)))
  , weight(cons(n, nil())) -> n }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: sum^#(cons(s(n), x), cons(m, y)) ->
         c_1(sum^#(cons(n, x), cons(s(m), y)))
    , 2: sum^#(cons(0(), x), y) -> c_2(sum^#(x, y))
    , 3: sum^#(nil(), y) -> c_3()
    , 4: weight^#(cons(n, cons(m, x))) ->
         c_4(weight^#(sum(cons(n, cons(m, x)), cons(0(), x))),
             sum^#(cons(n, cons(m, x)), cons(0(), x)))
    , 5: weight^#(cons(n, nil())) -> c_5() }

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

Strict DPs:
  { sum^#(cons(s(n), x), cons(m, y)) ->
    c_1(sum^#(cons(n, x), cons(s(m), y)))
  , sum^#(cons(0(), x), y) -> c_2(sum^#(x, y))
  , weight^#(cons(n, cons(m, x))) ->
    c_4(weight^#(sum(cons(n, cons(m, x)), cons(0(), x))),
        sum^#(cons(n, cons(m, x)), cons(0(), x))) }
Weak DPs:
  { sum^#(nil(), y) -> c_3()
  , weight^#(cons(n, nil())) -> c_5() }
Weak Trs:
  { sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
  , sum(cons(0(), x), y) -> sum(x, y)
  , sum(nil(), y) -> y
  , weight(cons(n, cons(m, x))) ->
    weight(sum(cons(n, cons(m, x)), cons(0(), x)))
  , weight(cons(n, nil())) -> n }
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.

{ sum^#(nil(), y) -> c_3()
, weight^#(cons(n, nil())) -> c_5() }

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

Strict DPs:
  { sum^#(cons(s(n), x), cons(m, y)) ->
    c_1(sum^#(cons(n, x), cons(s(m), y)))
  , sum^#(cons(0(), x), y) -> c_2(sum^#(x, y))
  , weight^#(cons(n, cons(m, x))) ->
    c_4(weight^#(sum(cons(n, cons(m, x)), cons(0(), x))),
        sum^#(cons(n, cons(m, x)), cons(0(), x))) }
Weak Trs:
  { sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
  , sum(cons(0(), x), y) -> sum(x, y)
  , sum(nil(), y) -> y
  , weight(cons(n, cons(m, x))) ->
    weight(sum(cons(n, cons(m, x)), cons(0(), x)))
  , weight(cons(n, nil())) -> n }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
    , sum(cons(0(), x), y) -> sum(x, y)
    , sum(nil(), y) -> y }

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

Strict DPs:
  { sum^#(cons(s(n), x), cons(m, y)) ->
    c_1(sum^#(cons(n, x), cons(s(m), y)))
  , sum^#(cons(0(), x), y) -> c_2(sum^#(x, y))
  , weight^#(cons(n, cons(m, x))) ->
    c_4(weight^#(sum(cons(n, cons(m, x)), cons(0(), x))),
        sum^#(cons(n, cons(m, x)), cons(0(), x))) }
Weak Trs:
  { sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
  , sum(cons(0(), x), y) -> sum(x, y)
  , sum(nil(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..