MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { sub(0(), 0()) -> 0() , sub(0(), s(x)) -> 0() , sub(s(x), 0()) -> s(x) , sub(s(x), s(y)) -> sub(x, y) , zero(nil()) -> zero2(0(), nil()) , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) , zero2(0(), nil()) -> nil() , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) , zero2(s(y), nil()) -> zero(nil()) , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..