MAYBE

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

Strict Trs:
  { double(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , 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)
  , first(nil()) -> 0()
  , first(cons(x, xs)) -> x
  , doublelist(nil()) -> nil()
  , doublelist(cons(x, xs)) ->
    cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..