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..