MAYBE

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

Strict Trs:
  { isEmpty(nil()) -> true()
  , isEmpty(cons(x, xs)) -> false()
  , last(cons(x, nil())) -> x
  , last(cons(x, cons(y, ys))) -> last(cons(y, ys))
  , dropLast(nil()) -> nil()
  , dropLast(cons(x, nil())) -> nil()
  , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
  , append(nil(), ys) -> ys
  , append(cons(x, xs), ys) -> cons(x, append(xs, ys))
  , reverse(xs) -> rev(xs, nil())
  , rev(xs, ys) ->
    if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)
  , if(true(), xs, ys, zs) -> zs
  , if(false(), xs, ys, zs) -> rev(xs, ys) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..