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

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

Strict Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(x, s(x))
  , g(0(), y) -> y
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y)) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

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

The following argument positions are usable:
  Uargs(s) = {1}, Uargs(g) = {2}, Uargs(+) = {1}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

      [f](x1) = [1] x1 + [7]
                            
          [0] = [7]         
                            
          [1] = [5]         
                            
      [s](x1) = [1] x1 + [7]
                            
  [g](x1, x2) = [1] x2 + [1]
                            
  [+](x1, x2) = [1] x1 + [7]

The following symbols are considered usable

  {f, g, +}

The order satisfies the following ordering constraints:

      [f(0())] = [14]              
               > [5]               
               = [1()]             
                                   
     [f(s(x))] = [1] x + [14]      
               > [1] x + [8]       
               = [g(x, s(x))]      
                                   
   [g(0(), y)] = [1] y + [1]       
               > [1] y + [0]       
               = [y]               
                                   
  [g(s(x), y)] = [1] y + [1]       
               ? [1] y + [15]      
               = [g(x, s(+(y, x)))]
                                   
  [g(s(x), y)] = [1] y + [1]       
               ? [1] y + [8]       
               = [g(x, +(y, s(x)))]
                                   
   [+(x, 0())] = [1] x + [7]       
               > [1] x + [0]       
               = [x]               
                                   
  [+(x, s(y))] = [1] x + [7]       
               ? [1] x + [14]      
               = [s(+(x, y))]      
                                   

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(n^2)).

Strict Trs:
  { g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(x, s(x))
  , g(0(), y) -> y
  , +(x, 0()) -> x }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'polynomial interpretation' to orient
following rules strictly.

Trs:
  { g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x))) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  The following argument positions are considered usable:
  
    Uargs(s) = {1}, Uargs(g) = {2}, Uargs(+) = {1}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
      [f](x1) = 3*x1 + x1^2       
                                  
        [0]() = 0                 
                                  
        [1]() = 0                 
                                  
      [s](x1) = 1 + x1            
                                  
  [g](x1, x2) = 3*x1 + x1^2 + 2*x2
                                  
  [+](x1, x2) = x1 + x2           
                                  
  
  The following symbols are considered usable
  
    {f, g, +}
  
  This order satisfies the following ordering constraints.
  
        [f(0())] =                     
                 >=                    
                 =  [1()]              
                                       
       [f(s(x))] =  4 + 5*x + x^2      
                 >  5*x + x^2 + 2      
                 =  [g(x, s(x))]       
                                       
     [g(0(), y)] =  2*y                
                 >= y                  
                 =  [y]                
                                       
    [g(s(x), y)] =  4 + 5*x + x^2 + 2*y
                 >  5*x + x^2 + 2 + 2*y
                 =  [g(x, s(+(y, x)))] 
                                       
    [g(s(x), y)] =  4 + 5*x + x^2 + 2*y
                 >  5*x + x^2 + 2*y + 2
                 =  [g(x, +(y, s(x)))] 
                                       
     [+(x, 0())] =  x                  
                 >= x                  
                 =  [x]                
                                       
    [+(x, s(y))] =  x + 1 + y          
                 >= 1 + x + y          
                 =  [s(+(x, y))]       
                                       

We return to the main proof.

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

Strict Trs: { +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(x, s(x))
  , g(0(), y) -> y
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'polynomial interpretation' to orient
following rules strictly.

Trs: { +(x, s(y)) -> s(+(x, y)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  The following argument positions are considered usable:
  
    Uargs(s) = {1}, Uargs(g) = {2}, Uargs(+) = {1}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
      [f](x1) = 2 + 2*x1^2          
                                    
        [0]() = 0                   
                                    
        [1]() = 0                   
                                    
      [s](x1) = 1 + x1              
                                    
  [g](x1, x2) = 2*x1 + 2*x1^2 + 2*x2
                                    
  [+](x1, x2) = x1 + 2*x2           
                                    
  
  The following symbols are considered usable
  
    {f, g, +}
  
  This order satisfies the following ordering constraints.
  
        [f(0())] =  2                    
                 >                       
                 =  [1()]                
                                         
       [f(s(x))] =  4 + 4*x + 2*x^2      
                 >  4*x + 2*x^2 + 2      
                 =  [g(x, s(x))]         
                                         
     [g(0(), y)] =  2*y                  
                 >= y                    
                 =  [y]                  
                                         
    [g(s(x), y)] =  4 + 6*x + 2*x^2 + 2*y
                 >  6*x + 2*x^2 + 2 + 2*y
                 =  [g(x, s(+(y, x)))]   
                                         
    [g(s(x), y)] =  4 + 6*x + 2*x^2 + 2*y
                 >= 6*x + 2*x^2 + 2*y + 4
                 =  [g(x, +(y, s(x)))]   
                                         
     [+(x, 0())] =  x                    
                 >= x                    
                 =  [x]                  
                                         
    [+(x, s(y))] =  x + 2 + 2*y          
                 >  1 + x + 2*y          
                 =  [s(+(x, y))]         
                                         

We return to the main proof.

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

Weak Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(x, s(x))
  , g(0(), y) -> y
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y)) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

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