MAYBE

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

Strict Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { pred^#(s(x)) -> c_1()
  , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
  , minus^#(x, 0()) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , quot^#(0(), s(y)) -> c_5()
  , log^#(s(s(x))) ->
    c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0()))))
  , log^#(s(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:
  { pred^#(s(x)) -> c_1()
  , minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
  , minus^#(x, 0()) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , quot^#(0(), s(y)) -> c_5()
  , log^#(s(s(x))) ->
    c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0()))))
  , log^#(s(0())) -> c_7() }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: pred^#(s(x)) -> c_1()
    , 2: minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
    , 3: minus^#(x, 0()) -> c_3()
    , 4: quot^#(s(x), s(y)) ->
         c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
    , 5: quot^#(0(), s(y)) -> c_5()
    , 6: log^#(s(s(x))) ->
         c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0()))))
    , 7: log^#(s(0())) -> c_7() }

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

Strict DPs:
  { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) ->
    c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
Weak DPs:
  { pred^#(s(x)) -> c_1()
  , minus^#(x, 0()) -> c_3()
  , quot^#(0(), s(y)) -> c_5()
  , log^#(s(0())) -> c_7() }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(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.

{ pred^#(s(x)) -> c_1()
, minus^#(x, 0()) -> c_3()
, quot^#(0(), s(y)) -> c_5()
, log^#(s(0())) -> c_7() }

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

Strict DPs:
  { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) ->
    c_6(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(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:

  { minus^#(x, s(y)) -> c_2(pred^#(minus(x, y)), minus^#(x, y)) }

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

Strict DPs:
  { minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) ->
    c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0()
  , log(s(s(x))) -> s(log(s(quot(x, s(s(0()))))))
  , log(s(0())) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { pred(s(x)) -> x
    , minus(x, s(y)) -> pred(minus(x, y))
    , minus(x, 0()) -> x
    , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
    , quot(0(), s(y)) -> 0() }

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

Strict DPs:
  { minus^#(x, s(y)) -> c_1(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , log^#(s(s(x))) ->
    c_3(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) }
Weak Trs:
  { pred(s(x)) -> x
  , minus(x, s(y)) -> pred(minus(x, y))
  , minus(x, 0()) -> x
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , quot(0(), s(y)) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..