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:
  { f(g(x), s(0()), y) -> f(g(s(0())), y, g(x))
  , g(s(x)) -> s(g(x))
  , g(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following innermost weak dependency pairs:

Strict DPs:
  { f^#(g(x), s(0()), y) -> c_1(f^#(g(s(0())), y, g(x)))
  , g^#(s(x)) -> c_2(g^#(x))
  , g^#(0()) -> c_3() }

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:
  { f^#(g(x), s(0()), y) -> c_1(f^#(g(s(0())), y, g(x)))
  , g^#(s(x)) -> c_2(g^#(x))
  , g^#(0()) -> c_3() }
Strict Trs:
  { f(g(x), s(0()), y) -> f(g(s(0())), y, g(x))
  , g(s(x)) -> s(g(x))
  , g(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { g(s(x)) -> s(g(x))
    , g(0()) -> 0() }

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

Strict DPs:
  { f^#(g(x), s(0()), y) -> c_1(f^#(g(s(0())), y, g(x)))
  , g^#(s(x)) -> c_2(g^#(x))
  , g^#(0()) -> c_3() }
Strict Trs:
  { g(s(x)) -> s(g(x))
  , g(0()) -> 0() }
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(s) = {1}, Uargs(f^#) = {1}, Uargs(c_1) = {1},
  Uargs(c_2) = {1}

TcT has computed the following constructor-restricted matrix
interpretation.

            [g](x1) = [0 1] x1 + [0]
                      [0 1]      [0]
                                    
            [s](x1) = [1 0] x1 + [0]
                      [0 1]      [1]
                                    
                [0] = [0]           
                      [1]           
                                    
  [f^#](x1, x2, x3) = [1 0] x1 + [2]
                      [0 0]      [2]
                                    
          [c_1](x1) = [1 0] x1 + [2]
                      [0 1]      [2]
                                    
          [g^#](x1) = [2 2] x1 + [2]
                      [1 1]      [1]
                                    
          [c_2](x1) = [1 0] x1 + [1]
                      [0 1]      [1]
                                    
              [c_3] = [1]           
                      [1]           

The following symbols are considered usable

  {g, f^#, g^#}

The order satisfies the following ordering constraints:

               [g(s(x))] = [0 1] x + [1]                 
                           [0 1]     [1]                 
                         > [0 1] x + [0]                 
                           [0 1]     [1]                 
                         = [s(g(x))]                     
                                                         
                [g(0())] = [1]                           
                           [1]                           
                         > [0]                           
                           [1]                           
                         = [0()]                         
                                                         
  [f^#(g(x), s(0()), y)] = [0 1] x + [2]                 
                           [0 0]     [2]                 
                         ? [6]                           
                           [4]                           
                         = [c_1(f^#(g(s(0())), y, g(x)))]
                                                         
             [g^#(s(x))] = [2 2] x + [4]                 
                           [1 1]     [2]                 
                         > [2 2] x + [3]                 
                           [1 1]     [2]                 
                         = [c_2(g^#(x))]                 
                                                         
              [g^#(0())] = [4]                           
                           [2]                           
                         > [1]                           
                           [1]                           
                         = [c_3()]                       
                                                         

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(1),O(1)).

Strict DPs:
  { f^#(g(x), s(0()), y) -> c_1(f^#(g(s(0())), y, g(x))) }
Weak DPs:
  { g^#(s(x)) -> c_2(g^#(x))
  , g^#(0()) -> c_3() }
Weak Trs:
  { g(s(x)) -> s(g(x))
  , g(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Consider the dependency graph:

  1: f^#(g(x), s(0()), y) -> c_1(f^#(g(s(0())), y, g(x)))
     -->_1 f^#(g(x), s(0()), y) -> c_1(f^#(g(s(0())), y, g(x))) :1
  
  2: g^#(s(x)) -> c_2(g^#(x))
     -->_1 g^#(0()) -> c_3() :3
     -->_1 g^#(s(x)) -> c_2(g^#(x)) :2
  
  3: g^#(0()) -> c_3()
  

Only the nodes {2,3} are reachable from nodes {2,3} that start
derivation from marked basic terms. The nodes not reachable are
removed from the problem.

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

Weak DPs:
  { g^#(s(x)) -> c_2(g^#(x))
  , g^#(0()) -> c_3() }
Weak Trs:
  { g(s(x)) -> s(g(x))
  , g(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

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

{ g^#(s(x)) -> c_2(g^#(x))
, g^#(0()) -> c_3() }

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

Weak Trs:
  { g(s(x)) -> s(g(x))
  , g(0()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(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(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

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