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(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z)
  , f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

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

Trs: { copy(s(x), y, z) -> copy(x, y, cons(f(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(f) = {1}, Uargs(cons) = {1, 2}, Uargs(copy) = {2, 3}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
             [f](x1) = x1                      
                                               
      [cons](x1, x2) = x1 + x2                 
                                               
             [nil]() = 0                       
                                               
  [copy](x1, x2, x3) = 2*x1 + 2*x1*x2 + x2 + x3
                                               
               [n]() = 0                       
                                               
               [0]() = 0                       
                                               
             [s](x1) = 2 + x1                  
                                               
  
  The following symbols are considered usable
  
    {f, copy}
  
  This order satisfies the following ordering constraints.
  
    [f(cons(f(cons(nil(), y)), z))] =  y + z                      
                                    >= y + z                      
                                    =  [copy(n(), y, z)]          
                                                                  
                [f(cons(nil(), y))] =  y                          
                                    >= y                          
                                    =  [y]                        
                                                                  
                  [copy(0(), y, z)] =  y + z                      
                                    >= z                          
                                    =  [f(z)]                     
                                                                  
                 [copy(s(x), y, z)] =  4 + 2*x + 5*y + 2*x*y + z  
                                    >  2*x + 2*x*y + 2*y + z      
                                    =  [copy(x, y, cons(f(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:
  { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z)
  , f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z) }
Weak Trs: { copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

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

Trs: { copy(0(), y, z) -> f(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(f) = {1}, Uargs(cons) = {1, 2}, Uargs(copy) = {2, 3}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
             [f](x1) = 2*x1                      
                                                 
      [cons](x1, x2) = x1 + x2                   
                                                 
             [nil]() = 0                         
                                                 
  [copy](x1, x2, x3) = 2*x1 + 2*x1*x2 + x2 + 2*x3
                                                 
               [n]() = 0                         
                                                 
               [0]() = 2                         
                                                 
             [s](x1) = 2 + x1                    
                                                 
  
  The following symbols are considered usable
  
    {f, copy}
  
  This order satisfies the following ordering constraints.
  
    [f(cons(f(cons(nil(), y)), z))] =  4*y + 2*z                  
                                    >= y + 2*z                    
                                    =  [copy(n(), y, z)]          
                                                                  
                [f(cons(nil(), y))] =  2*y                        
                                    >= y                          
                                    =  [y]                        
                                                                  
                  [copy(0(), y, z)] =  4 + 5*y + 2*z              
                                    >  2*z                        
                                    =  [f(z)]                     
                                                                  
                 [copy(s(x), y, z)] =  4 + 2*x + 5*y + 2*x*y + 2*z
                                    >  2*x + 2*x*y + 5*y + 2*z    
                                    =  [copy(x, y, cons(f(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:
  { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z)
  , f(cons(nil(), y)) -> y }
Weak Trs:
  { copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

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

Trs:
  { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z)
  , f(cons(nil(), y)) -> 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(f) = {1}, Uargs(cons) = {1, 2}, Uargs(copy) = {2, 3}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
             [f](x1) = x1               
                                        
      [cons](x1, x2) = x1 + x2          
                                        
             [nil]() = 1                
                                        
  [copy](x1, x2, x3) = 2*x1*x2 + x2 + x3
                                        
               [n]() = 0                
                                        
               [0]() = 0                
                                        
             [s](x1) = 1 + x1           
                                        
  
  The following symbols are considered usable
  
    {f, copy}
  
  This order satisfies the following ordering constraints.
  
    [f(cons(f(cons(nil(), y)), z))] =  1 + y + z                  
                                    >  y + z                      
                                    =  [copy(n(), y, z)]          
                                                                  
                [f(cons(nil(), y))] =  1 + y                      
                                    >  y                          
                                    =  [y]                        
                                                                  
                  [copy(0(), y, z)] =  y + z                      
                                    >= z                          
                                    =  [f(z)]                     
                                                                  
                 [copy(s(x), y, z)] =  3*y + 2*x*y + z            
                                    >= 2*x*y + 2*y + z            
                                    =  [copy(x, y, cons(f(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:
  { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z)
  , f(cons(nil(), y)) -> y
  , copy(0(), y, z) -> f(z)
  , copy(s(x), y, z) -> copy(x, y, cons(f(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))