MAYBE

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

Strict Trs:
  { f(true(), x, y) ->
    f(and(gt(x, y), gt(y, s(s(0())))), plus(s(0()), x), double(y))
  , and(x, true()) -> x
  , and(x, false()) -> false()
  , gt(s(u), s(v)) -> gt(u, v)
  , gt(s(u), 0()) -> true()
  , gt(0(), v) -> false()
  , plus(n, s(m)) -> s(plus(n, m))
  , plus(n, 0()) -> n
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { f^#(true(), x, y) ->
    c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
            plus(s(0()), x),
            double(y)),
        and^#(gt(x, y), gt(y, s(s(0())))),
        gt^#(x, y),
        gt^#(y, s(s(0()))),
        plus^#(s(0()), x),
        double^#(y))
  , and^#(x, true()) -> c_2()
  , and^#(x, false()) -> c_3()
  , gt^#(s(u), s(v)) -> c_4(gt^#(u, v))
  , gt^#(s(u), 0()) -> c_5()
  , gt^#(0(), v) -> c_6()
  , plus^#(n, s(m)) -> c_7(plus^#(n, m))
  , plus^#(n, 0()) -> c_8()
  , double^#(s(x)) -> c_9(double^#(x))
  , double^#(0()) -> c_10() }

and mark the set of starting terms.

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

Strict DPs:
  { f^#(true(), x, y) ->
    c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
            plus(s(0()), x),
            double(y)),
        and^#(gt(x, y), gt(y, s(s(0())))),
        gt^#(x, y),
        gt^#(y, s(s(0()))),
        plus^#(s(0()), x),
        double^#(y))
  , and^#(x, true()) -> c_2()
  , and^#(x, false()) -> c_3()
  , gt^#(s(u), s(v)) -> c_4(gt^#(u, v))
  , gt^#(s(u), 0()) -> c_5()
  , gt^#(0(), v) -> c_6()
  , plus^#(n, s(m)) -> c_7(plus^#(n, m))
  , plus^#(n, 0()) -> c_8()
  , double^#(s(x)) -> c_9(double^#(x))
  , double^#(0()) -> c_10() }
Weak Trs:
  { f(true(), x, y) ->
    f(and(gt(x, y), gt(y, s(s(0())))), plus(s(0()), x), double(y))
  , and(x, true()) -> x
  , and(x, false()) -> false()
  , gt(s(u), s(v)) -> gt(u, v)
  , gt(s(u), 0()) -> true()
  , gt(0(), v) -> false()
  , plus(n, s(m)) -> s(plus(n, m))
  , plus(n, 0()) -> n
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: f^#(true(), x, y) ->
         c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
                 plus(s(0()), x),
                 double(y)),
             and^#(gt(x, y), gt(y, s(s(0())))),
             gt^#(x, y),
             gt^#(y, s(s(0()))),
             plus^#(s(0()), x),
             double^#(y))
    , 2: and^#(x, true()) -> c_2()
    , 3: and^#(x, false()) -> c_3()
    , 4: gt^#(s(u), s(v)) -> c_4(gt^#(u, v))
    , 5: gt^#(s(u), 0()) -> c_5()
    , 6: gt^#(0(), v) -> c_6()
    , 7: plus^#(n, s(m)) -> c_7(plus^#(n, m))
    , 8: plus^#(n, 0()) -> c_8()
    , 9: double^#(s(x)) -> c_9(double^#(x))
    , 10: double^#(0()) -> c_10() }

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

Strict DPs:
  { f^#(true(), x, y) ->
    c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
            plus(s(0()), x),
            double(y)),
        and^#(gt(x, y), gt(y, s(s(0())))),
        gt^#(x, y),
        gt^#(y, s(s(0()))),
        plus^#(s(0()), x),
        double^#(y))
  , gt^#(s(u), s(v)) -> c_4(gt^#(u, v))
  , plus^#(n, s(m)) -> c_7(plus^#(n, m))
  , double^#(s(x)) -> c_9(double^#(x)) }
Weak DPs:
  { and^#(x, true()) -> c_2()
  , and^#(x, false()) -> c_3()
  , gt^#(s(u), 0()) -> c_5()
  , gt^#(0(), v) -> c_6()
  , plus^#(n, 0()) -> c_8()
  , double^#(0()) -> c_10() }
Weak Trs:
  { f(true(), x, y) ->
    f(and(gt(x, y), gt(y, s(s(0())))), plus(s(0()), x), double(y))
  , and(x, true()) -> x
  , and(x, false()) -> false()
  , gt(s(u), s(v)) -> gt(u, v)
  , gt(s(u), 0()) -> true()
  , gt(0(), v) -> false()
  , plus(n, s(m)) -> s(plus(n, m))
  , plus(n, 0()) -> n
  , 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.

{ and^#(x, true()) -> c_2()
, and^#(x, false()) -> c_3()
, gt^#(s(u), 0()) -> c_5()
, gt^#(0(), v) -> c_6()
, plus^#(n, 0()) -> c_8()
, double^#(0()) -> c_10() }

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

Strict DPs:
  { f^#(true(), x, y) ->
    c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
            plus(s(0()), x),
            double(y)),
        and^#(gt(x, y), gt(y, s(s(0())))),
        gt^#(x, y),
        gt^#(y, s(s(0()))),
        plus^#(s(0()), x),
        double^#(y))
  , gt^#(s(u), s(v)) -> c_4(gt^#(u, v))
  , plus^#(n, s(m)) -> c_7(plus^#(n, m))
  , double^#(s(x)) -> c_9(double^#(x)) }
Weak Trs:
  { f(true(), x, y) ->
    f(and(gt(x, y), gt(y, s(s(0())))), plus(s(0()), x), double(y))
  , and(x, true()) -> x
  , and(x, false()) -> false()
  , gt(s(u), s(v)) -> gt(u, v)
  , gt(s(u), 0()) -> true()
  , gt(0(), v) -> false()
  , plus(n, s(m)) -> s(plus(n, m))
  , plus(n, 0()) -> n
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { f^#(true(), x, y) ->
    c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
            plus(s(0()), x),
            double(y)),
        and^#(gt(x, y), gt(y, s(s(0())))),
        gt^#(x, y),
        gt^#(y, s(s(0()))),
        plus^#(s(0()), x),
        double^#(y)) }

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

Strict DPs:
  { f^#(true(), x, y) ->
    c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
            plus(s(0()), x),
            double(y)),
        gt^#(x, y),
        gt^#(y, s(s(0()))),
        plus^#(s(0()), x),
        double^#(y))
  , gt^#(s(u), s(v)) -> c_2(gt^#(u, v))
  , plus^#(n, s(m)) -> c_3(plus^#(n, m))
  , double^#(s(x)) -> c_4(double^#(x)) }
Weak Trs:
  { f(true(), x, y) ->
    f(and(gt(x, y), gt(y, s(s(0())))), plus(s(0()), x), double(y))
  , and(x, true()) -> x
  , and(x, false()) -> false()
  , gt(s(u), s(v)) -> gt(u, v)
  , gt(s(u), 0()) -> true()
  , gt(0(), v) -> false()
  , plus(n, s(m)) -> s(plus(n, m))
  , plus(n, 0()) -> n
  , 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:
    { and(x, true()) -> x
    , and(x, false()) -> false()
    , gt(s(u), s(v)) -> gt(u, v)
    , gt(s(u), 0()) -> true()
    , gt(0(), v) -> false()
    , plus(n, s(m)) -> s(plus(n, m))
    , plus(n, 0()) -> n
    , 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^#(true(), x, y) ->
    c_1(f^#(and(gt(x, y), gt(y, s(s(0())))),
            plus(s(0()), x),
            double(y)),
        gt^#(x, y),
        gt^#(y, s(s(0()))),
        plus^#(s(0()), x),
        double^#(y))
  , gt^#(s(u), s(v)) -> c_2(gt^#(u, v))
  , plus^#(n, s(m)) -> c_3(plus^#(n, m))
  , double^#(s(x)) -> c_4(double^#(x)) }
Weak Trs:
  { and(x, true()) -> x
  , and(x, false()) -> false()
  , gt(s(u), s(v)) -> gt(u, v)
  , gt(s(u), 0()) -> true()
  , gt(0(), v) -> false()
  , plus(n, s(m)) -> s(plus(n, m))
  , plus(n, 0()) -> n
  , double(s(x)) -> s(s(double(x)))
  , double(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..