MAYBE

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

Strict Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h()), l))
  , a(x, s(y), h()) -> a(x, y, s(h()))
  , a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z))
  , a(h(), h(), x) -> s(x)
  , a(s(x), h(), z) -> a(x, z, z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { app^#(l, nil()) -> c_1()
  , app^#(nil(), k) -> c_2()
  , app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, nil())) -> c_4()
  , sum^#(cons(x, cons(y, l))) ->
    c_5(sum^#(cons(a(x, y, h()), l)), a^#(x, y, h()))
  , a^#(x, s(y), h()) -> c_6(a^#(x, y, s(h())))
  , a^#(x, s(y), s(z)) ->
    c_7(a^#(x, y, a(x, s(y), z)), a^#(x, s(y), z))
  , a^#(h(), h(), x) -> c_8()
  , a^#(s(x), h(), z) -> c_9(a^#(x, z, z)) }

and mark the set of starting terms.

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

Strict DPs:
  { app^#(l, nil()) -> c_1()
  , app^#(nil(), k) -> c_2()
  , app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, nil())) -> c_4()
  , sum^#(cons(x, cons(y, l))) ->
    c_5(sum^#(cons(a(x, y, h()), l)), a^#(x, y, h()))
  , a^#(x, s(y), h()) -> c_6(a^#(x, y, s(h())))
  , a^#(x, s(y), s(z)) ->
    c_7(a^#(x, y, a(x, s(y), z)), a^#(x, s(y), z))
  , a^#(h(), h(), x) -> c_8()
  , a^#(s(x), h(), z) -> c_9(a^#(x, z, z)) }
Weak Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h()), l))
  , a(x, s(y), h()) -> a(x, y, s(h()))
  , a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z))
  , a(h(), h(), x) -> s(x)
  , a(s(x), h(), z) -> a(x, z, z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: app^#(l, nil()) -> c_1()
    , 2: app^#(nil(), k) -> c_2()
    , 3: app^#(cons(x, l), k) -> c_3(app^#(l, k))
    , 4: sum^#(cons(x, nil())) -> c_4()
    , 5: sum^#(cons(x, cons(y, l))) ->
         c_5(sum^#(cons(a(x, y, h()), l)), a^#(x, y, h()))
    , 6: a^#(x, s(y), h()) -> c_6(a^#(x, y, s(h())))
    , 7: a^#(x, s(y), s(z)) ->
         c_7(a^#(x, y, a(x, s(y), z)), a^#(x, s(y), z))
    , 8: a^#(h(), h(), x) -> c_8()
    , 9: a^#(s(x), h(), z) -> c_9(a^#(x, z, z)) }

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

Strict DPs:
  { app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, cons(y, l))) ->
    c_5(sum^#(cons(a(x, y, h()), l)), a^#(x, y, h()))
  , a^#(x, s(y), h()) -> c_6(a^#(x, y, s(h())))
  , a^#(x, s(y), s(z)) ->
    c_7(a^#(x, y, a(x, s(y), z)), a^#(x, s(y), z))
  , a^#(s(x), h(), z) -> c_9(a^#(x, z, z)) }
Weak DPs:
  { app^#(l, nil()) -> c_1()
  , app^#(nil(), k) -> c_2()
  , sum^#(cons(x, nil())) -> c_4()
  , a^#(h(), h(), x) -> c_8() }
Weak Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h()), l))
  , a(x, s(y), h()) -> a(x, y, s(h()))
  , a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z))
  , a(h(), h(), x) -> s(x)
  , a(s(x), h(), z) -> a(x, 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.

{ app^#(l, nil()) -> c_1()
, app^#(nil(), k) -> c_2()
, sum^#(cons(x, nil())) -> c_4()
, a^#(h(), h(), x) -> c_8() }

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

Strict DPs:
  { app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, cons(y, l))) ->
    c_5(sum^#(cons(a(x, y, h()), l)), a^#(x, y, h()))
  , a^#(x, s(y), h()) -> c_6(a^#(x, y, s(h())))
  , a^#(x, s(y), s(z)) ->
    c_7(a^#(x, y, a(x, s(y), z)), a^#(x, s(y), z))
  , a^#(s(x), h(), z) -> c_9(a^#(x, z, z)) }
Weak Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h()), l))
  , a(x, s(y), h()) -> a(x, y, s(h()))
  , a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z))
  , a(h(), h(), x) -> s(x)
  , a(s(x), h(), z) -> a(x, z, z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { a(x, s(y), h()) -> a(x, y, s(h()))
    , a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z))
    , a(h(), h(), x) -> s(x)
    , a(s(x), h(), z) -> a(x, z, z) }

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

Strict DPs:
  { app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, cons(y, l))) ->
    c_5(sum^#(cons(a(x, y, h()), l)), a^#(x, y, h()))
  , a^#(x, s(y), h()) -> c_6(a^#(x, y, s(h())))
  , a^#(x, s(y), s(z)) ->
    c_7(a^#(x, y, a(x, s(y), z)), a^#(x, s(y), z))
  , a^#(s(x), h(), z) -> c_9(a^#(x, z, z)) }
Weak Trs:
  { a(x, s(y), h()) -> a(x, y, s(h()))
  , a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z))
  , a(h(), h(), x) -> s(x)
  , a(s(x), h(), z) -> a(x, z, z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..