MAYBE

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

Strict Trs:
  { gt(0(), y) -> false()
  , gt(s(x), 0()) -> true()
  , gt(s(x), s(y)) -> gt(x, y)
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , average(x, y) -> aver(plus(x, y), 0())
  , aver(sum, z) -> if(gt(sum, double(z)), sum, z)
  , if(false(), sum, z) -> z
  , if(true(), sum, z) -> aver(sum, s(z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { gt^#(0(), y) -> c_1()
  , gt^#(s(x), 0()) -> c_2()
  , gt^#(s(x), s(y)) -> c_3(gt^#(x, y))
  , plus^#(0(), y) -> c_4()
  , plus^#(s(x), y) -> c_5(plus^#(x, y))
  , double^#(0()) -> c_6()
  , double^#(s(x)) -> c_7(double^#(x))
  , average^#(x, y) -> c_8(aver^#(plus(x, y), 0()), plus^#(x, y))
  , aver^#(sum, z) ->
    c_9(if^#(gt(sum, double(z)), sum, z),
        gt^#(sum, double(z)),
        double^#(z))
  , if^#(false(), sum, z) -> c_10()
  , if^#(true(), sum, z) -> c_11(aver^#(sum, s(z))) }

and mark the set of starting terms.

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

Strict DPs:
  { gt^#(0(), y) -> c_1()
  , gt^#(s(x), 0()) -> c_2()
  , gt^#(s(x), s(y)) -> c_3(gt^#(x, y))
  , plus^#(0(), y) -> c_4()
  , plus^#(s(x), y) -> c_5(plus^#(x, y))
  , double^#(0()) -> c_6()
  , double^#(s(x)) -> c_7(double^#(x))
  , average^#(x, y) -> c_8(aver^#(plus(x, y), 0()), plus^#(x, y))
  , aver^#(sum, z) ->
    c_9(if^#(gt(sum, double(z)), sum, z),
        gt^#(sum, double(z)),
        double^#(z))
  , if^#(false(), sum, z) -> c_10()
  , if^#(true(), sum, z) -> c_11(aver^#(sum, s(z))) }
Weak Trs:
  { gt(0(), y) -> false()
  , gt(s(x), 0()) -> true()
  , gt(s(x), s(y)) -> gt(x, y)
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , average(x, y) -> aver(plus(x, y), 0())
  , aver(sum, z) -> if(gt(sum, double(z)), sum, z)
  , if(false(), sum, z) -> z
  , if(true(), sum, z) -> aver(sum, s(z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: gt^#(0(), y) -> c_1()
    , 2: gt^#(s(x), 0()) -> c_2()
    , 3: gt^#(s(x), s(y)) -> c_3(gt^#(x, y))
    , 4: plus^#(0(), y) -> c_4()
    , 5: plus^#(s(x), y) -> c_5(plus^#(x, y))
    , 6: double^#(0()) -> c_6()
    , 7: double^#(s(x)) -> c_7(double^#(x))
    , 8: average^#(x, y) -> c_8(aver^#(plus(x, y), 0()), plus^#(x, y))
    , 9: aver^#(sum, z) ->
         c_9(if^#(gt(sum, double(z)), sum, z),
             gt^#(sum, double(z)),
             double^#(z))
    , 10: if^#(false(), sum, z) -> c_10()
    , 11: if^#(true(), sum, z) -> c_11(aver^#(sum, s(z))) }

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

Strict DPs:
  { gt^#(s(x), s(y)) -> c_3(gt^#(x, y))
  , plus^#(s(x), y) -> c_5(plus^#(x, y))
  , double^#(s(x)) -> c_7(double^#(x))
  , average^#(x, y) -> c_8(aver^#(plus(x, y), 0()), plus^#(x, y))
  , aver^#(sum, z) ->
    c_9(if^#(gt(sum, double(z)), sum, z),
        gt^#(sum, double(z)),
        double^#(z))
  , if^#(true(), sum, z) -> c_11(aver^#(sum, s(z))) }
Weak DPs:
  { gt^#(0(), y) -> c_1()
  , gt^#(s(x), 0()) -> c_2()
  , plus^#(0(), y) -> c_4()
  , double^#(0()) -> c_6()
  , if^#(false(), sum, z) -> c_10() }
Weak Trs:
  { gt(0(), y) -> false()
  , gt(s(x), 0()) -> true()
  , gt(s(x), s(y)) -> gt(x, y)
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , average(x, y) -> aver(plus(x, y), 0())
  , aver(sum, z) -> if(gt(sum, double(z)), sum, z)
  , if(false(), sum, z) -> z
  , if(true(), sum, z) -> aver(sum, s(z)) }
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.

{ gt^#(0(), y) -> c_1()
, gt^#(s(x), 0()) -> c_2()
, plus^#(0(), y) -> c_4()
, double^#(0()) -> c_6()
, if^#(false(), sum, z) -> c_10() }

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

Strict DPs:
  { gt^#(s(x), s(y)) -> c_3(gt^#(x, y))
  , plus^#(s(x), y) -> c_5(plus^#(x, y))
  , double^#(s(x)) -> c_7(double^#(x))
  , average^#(x, y) -> c_8(aver^#(plus(x, y), 0()), plus^#(x, y))
  , aver^#(sum, z) ->
    c_9(if^#(gt(sum, double(z)), sum, z),
        gt^#(sum, double(z)),
        double^#(z))
  , if^#(true(), sum, z) -> c_11(aver^#(sum, s(z))) }
Weak Trs:
  { gt(0(), y) -> false()
  , gt(s(x), 0()) -> true()
  , gt(s(x), s(y)) -> gt(x, y)
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x)))
  , average(x, y) -> aver(plus(x, y), 0())
  , aver(sum, z) -> if(gt(sum, double(z)), sum, z)
  , if(false(), sum, z) -> z
  , if(true(), sum, z) -> aver(sum, s(z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { gt(0(), y) -> false()
    , gt(s(x), 0()) -> true()
    , gt(s(x), s(y)) -> gt(x, y)
    , plus(0(), y) -> y
    , plus(s(x), y) -> s(plus(x, y))
    , double(0()) -> 0()
    , double(s(x)) -> s(s(double(x))) }

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

Strict DPs:
  { gt^#(s(x), s(y)) -> c_3(gt^#(x, y))
  , plus^#(s(x), y) -> c_5(plus^#(x, y))
  , double^#(s(x)) -> c_7(double^#(x))
  , average^#(x, y) -> c_8(aver^#(plus(x, y), 0()), plus^#(x, y))
  , aver^#(sum, z) ->
    c_9(if^#(gt(sum, double(z)), sum, z),
        gt^#(sum, double(z)),
        double^#(z))
  , if^#(true(), sum, z) -> c_11(aver^#(sum, s(z))) }
Weak Trs:
  { gt(0(), y) -> false()
  , gt(s(x), 0()) -> true()
  , gt(s(x), s(y)) -> gt(x, y)
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..