Problem Transformed CSR 04 Ex5 Zan97 Z

YES(?,O(n^1))

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

Strict Trs:
  { f(X) -> if(X, c(), n__f(true()))
  , f(X) -> n__f(X)
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> activate(Y)
  , activate(X) -> X
  , activate(n__f(X)) -> f(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(f) = {}, Uargs(if) = {}, Uargs(n__f) = {},
  Uargs(activate) = {}

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

           [f](x1) = [1] x1 + [2]
                                 
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [2] x3 + [1]
                                                   
               [c] = [0]
                        
        [n__f](x1) = [1] x1 + [0]
                                 
            [true] = [0]
                        
           [false] = [3]
                        
    [activate](x1) = [2] x1 + [3]

This order satisfies following ordering constraints

               [f(X)] = [1] X + [2]               
                      > [1] X + [1]               
                      = [if(X, c(), n__f(true()))]
                                                  
               [f(X)] = [1] X + [2]               
                      > [1] X + [0]               
                      = [n__f(X)]                 
                                                  
   [if(true(), X, Y)] = [1] X + [2] Y + [1]       
                      > [1] X + [0]               
                      = [X]                       
                                                  
  [if(false(), X, Y)] = [1] X + [2] Y + [4]       
                      > [2] Y + [3]               
                      = [activate(Y)]             
                                                  
        [activate(X)] = [2] X + [3]               
                      > [1] X + [0]               
                      = [X]                       
                                                  
  [activate(n__f(X))] = [2] X + [3]               
                      > [1] X + [2]               
                      = [f(X)]                    
                                                  

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

MAYBE

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

Strict Trs:
  { f(X) -> if(X, c(), n__f(true()))
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> activate(Y)
  , 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(X) -> if(X, c(), n__f(true()))
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> activate(Y)
  , 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(X) -> if(X, c(), n__f(true()))
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> activate(Y)
  , 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(X) -> if(X, c(), n__f(true()))
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> activate(Y)
  , 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..