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))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs:
  { +(x, 0()) -> x
  , +(x, i(x)) -> 0() }

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

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(+) = {1, 2}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
    [+](x1, x2) = [2] x1 + [1] x2 + [0]
                                       
            [0] = [1]                  
                                       
        [i](x1) = [5]                  
                                       
    [*](x1, x2) = [0]                  
  
  The order satisfies the following ordering constraints:
  
        [+(x, 0())] =  [2] x + [1]                
                    >  [1] x + [0]                
                    =  [x]                        
                                                  
       [+(x, i(x))] =  [2] x + [5]                
                    >  [1]                        
                    =  [0()]                      
                                                  
    [+(+(x, y), z)] =  [4] x + [2] y + [1] z + [0]
                    >= [2] x + [2] y + [1] z + [0]
                    =  [+(x, +(y, z))]            
                                                  
    [*(x, +(y, z))] =  [0]                        
                    >= [0]                        
                    =  [+(*(x, y), *(x, z))]      
                                                  
    [*(+(x, y), z)] =  [0]                        
                    >= [0]                        
                    =  [+(*(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))
  , *(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 'custom shape 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) = 2 + x1 + x2              
                                         
        [0]() = 0                        
                                         
      [i](x1) = 2                        
                                         
  [*](x1, x2) = 1 + 2*x1 + 2*x1*x2 + 2*x2
                                         
  
  This order satisfies the following ordering constraints.
  
        [+(x, 0())] =  2 + x                              
                    >  x                                  
                    =  [x]                                
                                                          
       [+(x, i(x))] =  4 + x                              
                    >                                     
                    =  [0()]                              
                                                          
    [+(+(x, y), z)] =  4 + x + y + z                      
                    >= 4 + x + y + z                      
                    =  [+(x, +(y, z))]                    
                                                          
    [*(x, +(y, z))] =  5 + 6*x + 2*x*y + 2*x*z + 2*y + 2*z
                    >  4 + 4*x + 2*x*y + 2*y + 2*x*z + 2*z
                    =  [+(*(x, y), *(x, z))]              
                                                          
    [*(+(x, y), z)] =  5 + 2*x + 2*y + 6*z + 2*x*z + 2*y*z
                    >  4 + 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 'custom shape 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
                                 
  
  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))