MAYBE

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

Strict Trs:
  { last(nil()) -> 0()
  , last(cons(x, nil())) -> x
  , last(cons(x, cons(y, xs))) -> last(cons(y, xs))
  , del(x, nil()) -> nil()
  , del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs)
  , if(true(), x, y, xs) -> xs
  , if(false(), x, y, xs) -> cons(y, del(x, xs))
  , eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , reverse(nil()) -> nil()
  , reverse(cons(x, xs)) ->
    cons(last(cons(x, xs)),
         reverse(del(last(cons(x, xs)), cons(x, xs)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..