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:
  { +(x, 0()) -> x
  , +(x, i(x)) -> 0()
  , +(+(x, y), z) -> +(x, +(y, z))
  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
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(+) = {1, 2}

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

  [+](x1, x2) = [1] x1 + [1] x2 + [7]
                                     
          [0] = [7]                  
                                     
      [i](x1) = [1] x1 + [7]         
                                     
  [*](x1, x2) = [3]                  

The following symbols are considered usable

  {+, *}

The order satisfies the following ordering constraints:

      [+(x, 0())] =  [1] x + [14]                
                  >  [1] x + [0]                 
                  =  [x]                         
                                                 
     [+(x, i(x))] =  [2] x + [14]                
                  >  [7]                         
                  =  [0()]                       
                                                 
  [+(+(x, y), z)] =  [1] x + [1] y + [1] z + [14]
                  >= [1] x + [1] y + [1] z + [14]
                  =  [+(x, +(y, z))]             
                                                 
  [*(x, +(y, z))] =  [3]                         
                  ?  [13]                        
                  =  [+(*(x, y), *(x, z))]       
                                                 
  [*(+(x, y), z)] =  [3]                         
                  ?  [13]                        
                  =  [+(*(x, z), *(y, z))]       
                                                 

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:
  { +(+(x, y), z) -> +(x, +(y, z))
  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
Weak Trs:
  { +(x, 0()) -> x
  , +(x, i(x)) -> 0() }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

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

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

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(+) = {1, 2}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
  [+](x1, x2) = 1 + x1 + x2          
                                     
        [0]() = 0                    
                                     
      [i](x1) = 0                    
                                     
  [*](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2
                                     
  
  The following symbols are considered usable
  
    {+, *}
  
  This order satisfies the following ordering constraints.
  
        [+(x, 0())] =  1 + x                              
                    >  x                                  
                    =  [x]                                
                                                          
       [+(x, i(x))] =  1 + x                              
                    >                                     
                    =  [0()]                              
                                                          
    [+(+(x, y), z)] =  2 + x + y + z                      
                    >= 2 + x + y + z                      
                    =  [+(x, +(y, z))]                    
                                                          
    [*(x, +(y, z))] =  4*x + 2*x*y + 2*x*z + 2 + 2*y + 2*z
                    >  1 + 4*x + 2*x*y + 2*y + 2*x*z + 2*z
                    =  [+(*(x, y), *(x, z))]              
                                                          
    [*(+(x, y), z)] =  2 + 2*x + 2*y + 4*z + 2*x*z + 2*y*z
                    >  1 + 2*x + 2*x*z + 4*z + 2*y + 2*y*z
                    =  [+(*(x, z), *(y, z))]              
                                                          

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, y), z) -> +(x, +(y, z)) }
Weak Trs:
  { +(x, 0()) -> x
  , +(x, i(x)) -> 0()
  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

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

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

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(+) = {1, 2}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
  [+](x1, x2) = 1 + 2*x1 + x2    
                                 
        [0]() = 0                
                                 
      [i](x1) = 0                
                                 
  [*](x1, x2) = x1 + 2*x1*x2 + x2
                                 
  
  The following symbols are considered usable
  
    {+, *}
  
  This order satisfies the following ordering constraints.
  
        [+(x, 0())] =  1 + 2*x                          
                    >  x                                
                    =  [x]                              
                                                        
       [+(x, i(x))] =  1 + 2*x                          
                    >                                   
                    =  [0()]                            
                                                        
    [+(+(x, y), z)] =  3 + 4*x + 2*y + z                
                    >  2 + 2*x + 2*y + z                
                    =  [+(x, +(y, z))]                  
                                                        
    [*(x, +(y, z))] =  3*x + 4*x*y + 2*x*z + 1 + 2*y + z
                    >= 1 + 3*x + 4*x*y + 2*y + 2*x*z + z
                    =  [+(*(x, y), *(x, z))]            
                                                        
    [*(+(x, y), z)] =  1 + 2*x + y + 3*z + 4*x*z + 2*y*z
                    >= 1 + 2*x + 4*x*z + 3*z + y + 2*y*z
                    =  [+(*(x, z), *(y, z))]            
                                                        

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:
  { +(x, 0()) -> x
  , +(x, i(x)) -> 0()
  , +(+(x, y), z) -> +(x, +(y, z))
  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

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