MAYBE

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

Strict Trs:
  { fib(N) -> sel(N, fib1(s(0()), s(0())))
  , sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
  , sel(0(), cons(X, XS)) -> X
  , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
  , fib1(X1, X2) -> n__fib1(X1, X2)
  , add(X1, X2) -> n__add(X1, X2)
  , add(s(X), Y) -> s(add(X, Y))
  , add(0(), X) -> X
  , activate(X) -> X
  , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
  , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { fib^#(N) ->
    c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0())))
  , sel^#(s(N), cons(X, XS)) ->
    c_2(sel^#(N, activate(XS)), activate^#(XS))
  , sel^#(0(), cons(X, XS)) -> c_3()
  , fib1^#(X, Y) -> c_4()
  , fib1^#(X1, X2) -> c_5()
  , activate^#(X) -> c_9()
  , activate^#(n__fib1(X1, X2)) ->
    c_10(fib1^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__add(X1, X2)) ->
    c_11(add^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , add^#(X1, X2) -> c_6()
  , add^#(s(X), Y) -> c_7(add^#(X, Y))
  , add^#(0(), X) -> c_8() }

and mark the set of starting terms.

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

Strict DPs:
  { fib^#(N) ->
    c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0())))
  , sel^#(s(N), cons(X, XS)) ->
    c_2(sel^#(N, activate(XS)), activate^#(XS))
  , sel^#(0(), cons(X, XS)) -> c_3()
  , fib1^#(X, Y) -> c_4()
  , fib1^#(X1, X2) -> c_5()
  , activate^#(X) -> c_9()
  , activate^#(n__fib1(X1, X2)) ->
    c_10(fib1^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__add(X1, X2)) ->
    c_11(add^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , add^#(X1, X2) -> c_6()
  , add^#(s(X), Y) -> c_7(add^#(X, Y))
  , add^#(0(), X) -> c_8() }
Weak Trs:
  { fib(N) -> sel(N, fib1(s(0()), s(0())))
  , sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
  , sel(0(), cons(X, XS)) -> X
  , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
  , fib1(X1, X2) -> n__fib1(X1, X2)
  , add(X1, X2) -> n__add(X1, X2)
  , add(s(X), Y) -> s(add(X, Y))
  , add(0(), X) -> X
  , activate(X) -> X
  , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
  , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: fib^#(N) ->
         c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0())))
    , 2: sel^#(s(N), cons(X, XS)) ->
         c_2(sel^#(N, activate(XS)), activate^#(XS))
    , 3: sel^#(0(), cons(X, XS)) -> c_3()
    , 4: fib1^#(X, Y) -> c_4()
    , 5: fib1^#(X1, X2) -> c_5()
    , 6: activate^#(X) -> c_9()
    , 7: activate^#(n__fib1(X1, X2)) ->
         c_10(fib1^#(activate(X1), activate(X2)),
              activate^#(X1),
              activate^#(X2))
    , 8: activate^#(n__add(X1, X2)) ->
         c_11(add^#(activate(X1), activate(X2)),
              activate^#(X1),
              activate^#(X2))
    , 9: add^#(X1, X2) -> c_6()
    , 10: add^#(s(X), Y) -> c_7(add^#(X, Y))
    , 11: add^#(0(), X) -> c_8() }

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

Strict DPs:
  { fib^#(N) ->
    c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0())))
  , sel^#(s(N), cons(X, XS)) ->
    c_2(sel^#(N, activate(XS)), activate^#(XS))
  , activate^#(n__fib1(X1, X2)) ->
    c_10(fib1^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__add(X1, X2)) ->
    c_11(add^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , add^#(s(X), Y) -> c_7(add^#(X, Y)) }
Weak DPs:
  { sel^#(0(), cons(X, XS)) -> c_3()
  , fib1^#(X, Y) -> c_4()
  , fib1^#(X1, X2) -> c_5()
  , activate^#(X) -> c_9()
  , add^#(X1, X2) -> c_6()
  , add^#(0(), X) -> c_8() }
Weak Trs:
  { fib(N) -> sel(N, fib1(s(0()), s(0())))
  , sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
  , sel(0(), cons(X, XS)) -> X
  , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
  , fib1(X1, X2) -> n__fib1(X1, X2)
  , add(X1, X2) -> n__add(X1, X2)
  , add(s(X), Y) -> s(add(X, Y))
  , add(0(), X) -> X
  , activate(X) -> X
  , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
  , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) }
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.

{ sel^#(0(), cons(X, XS)) -> c_3()
, fib1^#(X, Y) -> c_4()
, fib1^#(X1, X2) -> c_5()
, activate^#(X) -> c_9()
, add^#(X1, X2) -> c_6()
, add^#(0(), X) -> c_8() }

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

Strict DPs:
  { fib^#(N) ->
    c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0())))
  , sel^#(s(N), cons(X, XS)) ->
    c_2(sel^#(N, activate(XS)), activate^#(XS))
  , activate^#(n__fib1(X1, X2)) ->
    c_10(fib1^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__add(X1, X2)) ->
    c_11(add^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , add^#(s(X), Y) -> c_7(add^#(X, Y)) }
Weak Trs:
  { fib(N) -> sel(N, fib1(s(0()), s(0())))
  , sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
  , sel(0(), cons(X, XS)) -> X
  , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
  , fib1(X1, X2) -> n__fib1(X1, X2)
  , add(X1, X2) -> n__add(X1, X2)
  , add(s(X), Y) -> s(add(X, Y))
  , add(0(), X) -> X
  , activate(X) -> X
  , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
  , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { fib^#(N) ->
    c_1(sel^#(N, fib1(s(0()), s(0()))), fib1^#(s(0()), s(0())))
  , activate^#(n__fib1(X1, X2)) ->
    c_10(fib1^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2)) }

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

Strict DPs:
  { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))))
  , sel^#(s(N), cons(X, XS)) ->
    c_2(sel^#(N, activate(XS)), activate^#(XS))
  , activate^#(n__fib1(X1, X2)) ->
    c_3(activate^#(X1), activate^#(X2))
  , activate^#(n__add(X1, X2)) ->
    c_4(add^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , add^#(s(X), Y) -> c_5(add^#(X, Y)) }
Weak Trs:
  { fib(N) -> sel(N, fib1(s(0()), s(0())))
  , sel(s(N), cons(X, XS)) -> sel(N, activate(XS))
  , sel(0(), cons(X, XS)) -> X
  , fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
  , fib1(X1, X2) -> n__fib1(X1, X2)
  , add(X1, X2) -> n__add(X1, X2)
  , add(s(X), Y) -> s(add(X, Y))
  , add(0(), X) -> X
  , activate(X) -> X
  , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
  , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
    , fib1(X1, X2) -> n__fib1(X1, X2)
    , add(X1, X2) -> n__add(X1, X2)
    , add(s(X), Y) -> s(add(X, Y))
    , add(0(), X) -> X
    , activate(X) -> X
    , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
    , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) }

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

Strict DPs:
  { fib^#(N) -> c_1(sel^#(N, fib1(s(0()), s(0()))))
  , sel^#(s(N), cons(X, XS)) ->
    c_2(sel^#(N, activate(XS)), activate^#(XS))
  , activate^#(n__fib1(X1, X2)) ->
    c_3(activate^#(X1), activate^#(X2))
  , activate^#(n__add(X1, X2)) ->
    c_4(add^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , add^#(s(X), Y) -> c_5(add^#(X, Y)) }
Weak Trs:
  { fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y)))
  , fib1(X1, X2) -> n__fib1(X1, X2)
  , add(X1, X2) -> n__add(X1, X2)
  , add(s(X), Y) -> s(add(X, Y))
  , add(0(), X) -> X
  , activate(X) -> X
  , activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2))
  , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..