YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),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(1),O(n^1))

We add following weak dependency pairs:

Strict DPs:
  { norm^#(nil()) -> c_1()
  , norm^#(g(x, y)) -> c_2(norm^#(x))
  , f^#(x, nil()) -> c_3()
  , f^#(x, g(y, z)) -> c_4(f^#(x, y))
  , rem^#(nil(), y) -> c_5()
  , rem^#(g(x, y), 0()) -> c_6()
  , rem^#(g(x, y), s(z)) -> c_7(rem^#(x, z)) }

and mark the set of starting terms.

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

Strict DPs:
  { norm^#(nil()) -> c_1()
  , norm^#(g(x, y)) -> c_2(norm^#(x))
  , f^#(x, nil()) -> c_3()
  , f^#(x, g(y, z)) -> c_4(f^#(x, y))
  , rem^#(nil(), y) -> c_5()
  , rem^#(g(x, y), 0()) -> c_6()
  , rem^#(g(x, y), s(z)) -> c_7(rem^#(x, z)) }
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(1),O(n^1))

No rule is usable, rules are removed from the input problem.

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

Strict DPs:
  { norm^#(nil()) -> c_1()
  , norm^#(g(x, y)) -> c_2(norm^#(x))
  , f^#(x, nil()) -> c_3()
  , f^#(x, g(y, z)) -> c_4(f^#(x, y))
  , rem^#(nil(), y) -> c_5()
  , rem^#(g(x, y), 0()) -> c_6()
  , rem^#(g(x, y), s(z)) -> c_7(rem^#(x, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

            [nil] = [0]         
                                
              [0] = [1]         
                                
      [g](x1, x2) = [1] x1 + [0]
                                
          [s](x1) = [1] x1 + [2]
                                
     [norm^#](x1) = [1]         
                                
            [c_1] = [0]         
                                
        [c_2](x1) = [1] x1 + [0]
                                
    [f^#](x1, x2) = [2] x1 + [0]
                                
            [c_3] = [1]         
                                
        [c_4](x1) = [1] x1 + [2]
                                
  [rem^#](x1, x2) = [0]         
                                
            [c_5] = [1]         
                                
            [c_6] = [1]         
                                
        [c_7](x1) = [1] x1 + [2]

This order satisfies following ordering constraints:


Further, it can be verified that all rules not oriented are covered by the weightgap condition.

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

Strict DPs:
  { norm^#(g(x, y)) -> c_2(norm^#(x))
  , f^#(x, nil()) -> c_3()
  , f^#(x, g(y, z)) -> c_4(f^#(x, y))
  , rem^#(nil(), y) -> c_5()
  , rem^#(g(x, y), 0()) -> c_6()
  , rem^#(g(x, y), s(z)) -> c_7(rem^#(x, z)) }
Weak DPs: { norm^#(nil()) -> c_1() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

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

  DPs:
    { 1: norm^#(g(x, y)) -> c_2(norm^#(x))
    , 2: f^#(x, nil()) -> c_3()
    , 3: f^#(x, g(y, z)) -> c_4(f^#(x, y))
    , 4: rem^#(nil(), y) -> c_5()
    , 5: rem^#(g(x, y), 0()) -> c_6()
    , 6: rem^#(g(x, y), s(z)) -> c_7(rem^#(x, z))
    , 7: norm^#(nil()) -> c_1() }

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

Strict DPs:
  { norm^#(g(x, y)) -> c_2(norm^#(x))
  , f^#(x, g(y, z)) -> c_4(f^#(x, y))
  , rem^#(g(x, y), s(z)) -> c_7(rem^#(x, z)) }
Weak DPs:
  { norm^#(nil()) -> c_1()
  , f^#(x, nil()) -> c_3()
  , rem^#(nil(), y) -> c_5()
  , rem^#(g(x, y), 0()) -> c_6() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ norm^#(nil()) -> c_1()
, f^#(x, nil()) -> c_3()
, rem^#(nil(), y) -> c_5()
, rem^#(g(x, y), 0()) -> c_6() }

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

Strict DPs:
  { norm^#(g(x, y)) -> c_2(norm^#(x))
  , f^#(x, g(y, z)) -> c_4(f^#(x, y))
  , rem^#(g(x, y), s(z)) -> c_7(rem^#(x, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

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

 safe(g) = {1, 2}, safe(s) = {1}, safe(norm^#) = {}, safe(c_2) = {},
 safe(f^#) = {}, safe(c_4) = {}, safe(rem^#) = {}, safe(c_7) = {}

and precedence

 norm^# ~ f^#, norm^# ~ rem^#, f^# ~ rem^# .

Following symbols are considered recursive:

 {norm^#, f^#, rem^#}

The recursion depth is 1.

Further, following argument filtering is employed:

 pi(g) = [1, 2], pi(s) = 1, pi(norm^#) = [1], pi(c_2) = [1],
 pi(f^#) = [1, 2], pi(c_4) = [1], pi(rem^#) = [1, 2], pi(c_7) = [1]

Usable defined function symbols are a subset of:

 {norm^#, f^#, rem^#}

For your convenience, here are the satisfied ordering constraints:

       pi(norm^#(g(x, y))) = norm^#(g(; x,  y);)   
                           > c_2(norm^#(x;);)      
                           = pi(c_2(norm^#(x)))    
                                                   
       pi(f^#(x, g(y, z))) = f^#(x,  g(; y,  z);)  
                           > c_4(f^#(x,  y;);)     
                           = pi(c_4(f^#(x, y)))    
                                                   
  pi(rem^#(g(x, y), s(z))) = rem^#(g(; x,  y),  z;)
                           > c_7(rem^#(x,  z;);)   
                           = pi(c_7(rem^#(x, z)))  
                                                   

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