Problem SK90 2.41

YES(?,O(n^1))

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

Strict Trs:
  { norm(nil()) -> 0()
  , norm(g(x, y)) -> s(norm(x))
  , f(x, nil()) -> g(nil(), x)
  , f(x, g(y, z)) -> g(f(x, y), z)
  , rem(nil(), y) -> nil()
  , rem(g(x, y), 0()) -> g(x, y)
  , rem(g(x, y), s(z)) -> rem(x, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(norm) = {}, Uargs(g) = {1}, Uargs(s) = {1}, Uargs(f) = {},
  Uargs(rem) = {}

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

     [norm](x1) = [2] x1 + [0]
                              
          [nil] = [2]
                     
            [0] = [0]
                     
    [g](x1, x2) = [1] x1 + [2]
                              
        [s](x1) = [1] x1 + [3]
                              
    [f](x1, x2) = [1] x1 + [3] x2 + [3]
                                       
  [rem](x1, x2) = [1] x1 + [1]

This order satisfies following ordering constraints

         [norm(nil())] = [4]                
                       > [0]                
                       = [0()]              
                                            
       [norm(g(x, y))] = [2] x + [4]        
                       > [2] x + [3]        
                       = [s(norm(x))]       
                                            
         [f(x, nil())] = [1] x + [9]        
                       > [4]                
                       = [g(nil(), x)]      
                                            
       [f(x, g(y, z))] = [1] x + [3] y + [9]
                       > [1] x + [3] y + [5]
                       = [g(f(x, y), z)]    
                                            
       [rem(nil(), y)] = [3]                
                       > [2]                
                       = [nil()]            
                                            
   [rem(g(x, y), 0())] = [1] x + [3]        
                       > [1] x + [2]        
                       = [g(x, y)]          
                                            
  [rem(g(x, y), s(z))] = [1] x + [3]        
                       > [1] x + [1]        
                       = [rem(x, z)]        
                                            

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

YES(?,ELEMENTARY)

We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).

Strict Trs:
  { norm(nil()) -> 0()
  , norm(g(x, y)) -> s(norm(x))
  , f(x, nil()) -> g(nil(), x)
  , f(x, g(y, z)) -> g(f(x, y), z)
  , rem(nil(), y) -> nil()
  , rem(g(x, y), 0()) -> g(x, y)
  , rem(g(x, y), s(z)) -> rem(x, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,ELEMENTARY)

The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping

 safe(norm) = {}, safe(nil) = {}, safe(0) = {}, safe(g) = {1, 2},
 safe(s) = {1}, safe(f) = {}, safe(rem) = {1}

and precedence

 empty .

Following symbols are considered recursive:

 {norm, f, rem}

The recursion depth is 1.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { norm(nil();) -> 0()
   , norm(g(; x,  y);) -> s(; norm(x;))
   , f(x,  nil();) -> g(; nil(),  x)
   , f(x,  g(; y,  z);) -> g(; f(x,  y;),  z)
   , rem(y; nil()) -> nil()
   , rem(0(); g(; x,  y)) -> g(; x,  y)
   , rem(s(; z); g(; x,  y)) -> rem(z; x) }
 Weak Trs  : 

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).

Strict Trs:
  { norm(nil()) -> 0()
  , norm(g(x, y)) -> s(norm(x))
  , f(x, nil()) -> g(nil(), x)
  , f(x, g(y, z)) -> g(f(x, y), z)
  , rem(nil(), y) -> nil()
  , rem(g(x, y), 0()) -> g(x, y)
  , rem(g(x, y), s(z)) -> rem(x, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

The input was oriented with the instance of'multiset path orders'
as induced by the precedence

 norm > s, nil > 0, f > g .

Hurray, we answered YES(?,PRIMREC)

YES(?,POLY)

We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).

Strict Trs:
  { norm(nil()) -> 0()
  , norm(g(x, y)) -> s(norm(x))
  , f(x, nil()) -> g(nil(), x)
  , f(x, g(y, z)) -> g(f(x, y), z)
  , rem(nil(), y) -> nil()
  , rem(g(x, y), 0()) -> g(x, y)
  , rem(g(x, y), s(z)) -> rem(x, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

The input was oriented with the instance of 'Polynomial Path Order'
as induced by the safe mapping

 safe(norm) = {}, safe(nil) = {}, safe(0) = {}, safe(g) = {1, 2},
 safe(s) = {1}, safe(f) = {}, safe(rem) = {1}

and precedence

 empty .

Following symbols are considered recursive:

 {norm, f, rem}

The recursion depth is 1.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { norm(nil();) -> 0()
   , norm(g(; x,  y);) -> s(; norm(x;))
   , f(x,  nil();) -> g(; nil(),  x)
   , f(x,  g(; y,  z);) -> g(; f(x,  y;),  z)
   , rem(y; nil()) -> nil()
   , rem(0(); g(; x,  y)) -> g(; x,  y)
   , rem(s(; z); g(; x,  y)) -> rem(z; x) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)

YES(?,POLY)

We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).

Strict Trs:
  { norm(nil()) -> 0()
  , norm(g(x, y)) -> s(norm(x))
  , f(x, nil()) -> g(nil(), x)
  , f(x, g(y, z)) -> g(f(x, y), z)
  , rem(nil(), y) -> nil()
  , rem(g(x, y), 0()) -> g(x, y)
  , rem(g(x, y), s(z)) -> rem(x, z) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping

 safe(norm) = {}, safe(nil) = {}, safe(0) = {}, safe(g) = {1, 2},
 safe(s) = {1}, safe(f) = {1}, safe(rem) = {1}

and precedence

 empty .

Following symbols are considered recursive:

 {norm, f, rem}

The recursion depth is 1.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { norm(nil();) -> 0()
   , norm(g(; x,  y);) -> s(; norm(x;))
   , f(nil(); x) -> g(; nil(),  x)
   , f(g(; y,  z); x) -> g(; f(y; x),  z)
   , rem(y; nil()) -> nil()
   , rem(0(); g(; x,  y)) -> g(; x,  y)
   , rem(s(; z); g(; x,  y)) -> rem(z; x) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)