Problem Transformed CSR 04 ExProp7 Luc06 Z

YES(?,O(n^3))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

Strict Trs:
  { f(X) -> n__f(X)
  , f(0()) -> cons(0(), n__f(s(0())))
  , f(s(0())) -> f(p(s(0())))
  , p(s(X)) -> X
  , activate(X) -> X
  , activate(n__f(X)) -> f(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

The following argument positions are usable:
  Uargs(f) = {1}, Uargs(cons) = {}, Uargs(n__f) = {}, Uargs(s) = {},
  Uargs(p) = {}, Uargs(activate) = {}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

                   [1 2 3]      [1]
         [f](x1) = [0 0 0] x1 + [0]
                   [0 0 0]      [1]
                                   
                   [0]
             [0] = [0]
                   [0]
                      
                   [0 0 0]      [0]
  [cons](x1, x2) = [0 0 0] x1 + [0]
                   [0 1 1]      [0]
                                   
                   [1 1 1]      [0]
      [n__f](x1) = [0 0 0] x1 + [0]
                   [0 0 0]      [1]
                                   
                   [1 0 0]      [0]
         [s](x1) = [0 0 0] x1 + [2]
                   [0 1 1]      [1]
                                   
                   [1 0 1]      [0]
         [p](x1) = [0 0 1] x1 + [0]
                   [0 0 1]      [0]
                                   
                   [3 0 0]      [3]
  [activate](x1) = [0 1 0] x1 + [0]
                   [0 0 1]      [0]

This order satisfies following ordering constraints

               [f(X)] = [1 2 3]     [1]          
                        [0 0 0] X + [0]          
                        [0 0 0]     [1]          
                      > [1 1 1]     [0]          
                        [0 0 0] X + [0]          
                        [0 0 0]     [1]          
                      = [n__f(X)]                
                                                 
             [f(0())] = [1]                      
                        [0]                      
                        [1]                      
                      > [0]                      
                        [0]                      
                        [0]                      
                      = [cons(0(), n__f(s(0())))]
                                                 
          [f(s(0()))] = [8]                      
                        [0]                      
                        [1]                      
                      > [7]                      
                        [0]                      
                        [1]                      
                      = [f(p(s(0())))]           
                                                 
            [p(s(X))] = [1 1 1]     [1]          
                        [0 1 1] X + [1]          
                        [0 1 1]     [1]          
                      > [1 0 0]     [0]          
                        [0 1 0] X + [0]          
                        [0 0 1]     [0]          
                      = [X]                      
                                                 
        [activate(X)] = [3 0 0]     [3]          
                        [0 1 0] X + [0]          
                        [0 0 1]     [0]          
                      > [1 0 0]     [0]          
                        [0 1 0] X + [0]          
                        [0 0 1]     [0]          
                      = [X]                      
                                                 
  [activate(n__f(X))] = [3 3 3]     [3]          
                        [0 0 0] X + [0]          
                        [0 0 0]     [1]          
                      > [1 2 3]     [1]          
                        [0 0 0] X + [0]          
                        [0 0 0]     [1]          
                      = [f(X)]                   
                                                 

Hurray, we answered YES(?,O(n^3))

MAYBE

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

Strict Trs:
  { f(0()) -> cons(0(), n__f(s(0())))
  , f(s(0())) -> f(p(s(0())))
  , p(s(X)) -> X
  , f(X) -> n__f(X)
  , activate(n__f(X)) -> f(X)
  , activate(X) -> X }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { f(0()) -> cons(0(), n__f(s(0())))
  , f(s(0())) -> f(p(s(0())))
  , p(s(X)) -> X
  , f(X) -> n__f(X)
  , activate(n__f(X)) -> f(X)
  , activate(X) -> X }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { f(0()) -> cons(0(), n__f(s(0())))
  , f(s(0())) -> f(p(s(0())))
  , p(s(X)) -> X
  , f(X) -> n__f(X)
  , activate(n__f(X)) -> f(X)
  , activate(X) -> X }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { f(0()) -> cons(0(), n__f(s(0())))
  , f(s(0())) -> f(p(s(0())))
  , p(s(X)) -> X
  , f(X) -> n__f(X)
  , activate(n__f(X)) -> f(X)
  , activate(X) -> X }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..