MAYBE

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

Strict Trs:
  { f(tt(), x) -> f(eq(x, half(double(x))), s(x))
  , eq(s(x), s(y)) -> eq(x, y)
  , eq(0(), 0()) -> tt()
  , half(s(s(x))) -> s(half(x))
  , half(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { f^#(tt(), x) ->
    c_1(f^#(eq(x, half(double(x))), s(x)),
        eq^#(x, half(double(x))),
        half^#(double(x)),
        double^#(x))
  , eq^#(s(x), s(y)) -> c_2(eq^#(x, y))
  , eq^#(0(), 0()) -> c_3()
  , half^#(s(s(x))) -> c_4(half^#(x))
  , half^#(0()) -> c_5()
  , double^#(s(x)) -> c_6(double^#(x))
  , double^#(0()) -> c_7() }

and mark the set of starting terms.

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

Strict DPs:
  { f^#(tt(), x) ->
    c_1(f^#(eq(x, half(double(x))), s(x)),
        eq^#(x, half(double(x))),
        half^#(double(x)),
        double^#(x))
  , eq^#(s(x), s(y)) -> c_2(eq^#(x, y))
  , eq^#(0(), 0()) -> c_3()
  , half^#(s(s(x))) -> c_4(half^#(x))
  , half^#(0()) -> c_5()
  , double^#(s(x)) -> c_6(double^#(x))
  , double^#(0()) -> c_7() }
Weak Trs:
  { f(tt(), x) -> f(eq(x, half(double(x))), s(x))
  , eq(s(x), s(y)) -> eq(x, y)
  , eq(0(), 0()) -> tt()
  , half(s(s(x))) -> s(half(x))
  , half(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {3,5,7} by applications of
Pre({3,5,7}) = {1,2,4,6}. Here rules are labeled as follows:

  DPs:
    { 1: f^#(tt(), x) ->
         c_1(f^#(eq(x, half(double(x))), s(x)),
             eq^#(x, half(double(x))),
             half^#(double(x)),
             double^#(x))
    , 2: eq^#(s(x), s(y)) -> c_2(eq^#(x, y))
    , 3: eq^#(0(), 0()) -> c_3()
    , 4: half^#(s(s(x))) -> c_4(half^#(x))
    , 5: half^#(0()) -> c_5()
    , 6: double^#(s(x)) -> c_6(double^#(x))
    , 7: double^#(0()) -> c_7() }

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

Strict DPs:
  { f^#(tt(), x) ->
    c_1(f^#(eq(x, half(double(x))), s(x)),
        eq^#(x, half(double(x))),
        half^#(double(x)),
        double^#(x))
  , eq^#(s(x), s(y)) -> c_2(eq^#(x, y))
  , half^#(s(s(x))) -> c_4(half^#(x))
  , double^#(s(x)) -> c_6(double^#(x)) }
Weak DPs:
  { eq^#(0(), 0()) -> c_3()
  , half^#(0()) -> c_5()
  , double^#(0()) -> c_7() }
Weak Trs:
  { f(tt(), x) -> f(eq(x, half(double(x))), s(x))
  , eq(s(x), s(y)) -> eq(x, y)
  , eq(0(), 0()) -> tt()
  , half(s(s(x))) -> s(half(x))
  , half(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ eq^#(0(), 0()) -> c_3()
, half^#(0()) -> c_5()
, double^#(0()) -> c_7() }

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

Strict DPs:
  { f^#(tt(), x) ->
    c_1(f^#(eq(x, half(double(x))), s(x)),
        eq^#(x, half(double(x))),
        half^#(double(x)),
        double^#(x))
  , eq^#(s(x), s(y)) -> c_2(eq^#(x, y))
  , half^#(s(s(x))) -> c_4(half^#(x))
  , double^#(s(x)) -> c_6(double^#(x)) }
Weak Trs:
  { f(tt(), x) -> f(eq(x, half(double(x))), s(x))
  , eq(s(x), s(y)) -> eq(x, y)
  , eq(0(), 0()) -> tt()
  , half(s(s(x))) -> s(half(x))
  , half(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { eq(s(x), s(y)) -> eq(x, y)
    , eq(0(), 0()) -> tt()
    , half(s(s(x))) -> s(half(x))
    , half(0()) -> 0()
    , double(s(x)) -> s(s(double(x)))
    , double(0()) -> 0() }

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

Strict DPs:
  { f^#(tt(), x) ->
    c_1(f^#(eq(x, half(double(x))), s(x)),
        eq^#(x, half(double(x))),
        half^#(double(x)),
        double^#(x))
  , eq^#(s(x), s(y)) -> c_2(eq^#(x, y))
  , half^#(s(s(x))) -> c_4(half^#(x))
  , double^#(s(x)) -> c_6(double^#(x)) }
Weak Trs:
  { eq(s(x), s(y)) -> eq(x, y)
  , eq(0(), 0()) -> tt()
  , half(s(s(x))) -> s(half(x))
  , half(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..