Problem CiME 04 list-sum-prod

TIMEOUT

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

Strict Trs:
  { +(x, 0()) -> x
  , +(0(), x) -> x
  , +(s(x), s(y)) -> s(s(+(x, y)))
  , *(x, 0()) -> 0()
  , *(0(), x) -> 0()
  , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
  , sum(nil()) -> 0()
  , sum(cons(x, l)) -> +(x, sum(l))
  , prod(nil()) -> s(0())
  , prod(cons(x, l)) -> *(x, prod(l)) }
Obligation:
  innermost runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 20.0 seconds.

Arrrr..

MAYBE

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

Strict Trs:
  { +(x, 0()) -> x
  , +(0(), x) -> x
  , +(s(x), s(y)) -> s(s(+(x, y)))
  , *(x, 0()) -> 0()
  , *(0(), x) -> 0()
  , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
  , sum(nil()) -> 0()
  , sum(cons(x, l)) -> +(x, sum(l))
  , prod(nil()) -> s(0())
  , prod(cons(x, l)) -> *(x, prod(l)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

YES(?,PRIMREC)

We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).

Strict Trs:
  { +(x, 0()) -> x
  , +(0(), x) -> x
  , +(s(x), s(y)) -> s(s(+(x, y)))
  , *(x, 0()) -> 0()
  , *(0(), x) -> 0()
  , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
  , sum(nil()) -> 0()
  , sum(cons(x, l)) -> +(x, sum(l))
  , prod(nil()) -> s(0())
  , prod(cons(x, l)) -> *(x, prod(l)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

The input was oriented with the instance of'multiset path orders'
as induced by the precedence

 + > s, * > +, * > s, sum > +, nil > 0, nil > s, cons > *,
 cons > prod .

Hurray, we answered YES(?,PRIMREC)

MAYBE

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

Strict Trs:
  { +(x, 0()) -> x
  , +(0(), x) -> x
  , +(s(x), s(y)) -> s(s(+(x, y)))
  , *(x, 0()) -> 0()
  , *(0(), x) -> 0()
  , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
  , sum(nil()) -> 0()
  , sum(cons(x, l)) -> +(x, sum(l))
  , prod(nil()) -> s(0())
  , prod(cons(x, l)) -> *(x, prod(l)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { +(x, 0()) -> x
  , +(0(), x) -> x
  , +(s(x), s(y)) -> s(s(+(x, y)))
  , *(x, 0()) -> 0()
  , *(0(), x) -> 0()
  , *(s(x), s(y)) -> s(+(*(x, y), +(x, y)))
  , sum(nil()) -> 0()
  , sum(cons(x, l)) -> +(x, sum(l))
  , prod(nil()) -> s(0())
  , prod(cons(x, l)) -> *(x, prod(l)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..