*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        copy(0(),y,z) -> f(z)
        copy(s(x),y,z) -> copy(x,y,cons(f(y),z))
        f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
        f(cons(nil(),y)) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {copy/3,f/1} / {0/0,cons/2,n/0,nil/0,s/1}
      Obligation:
        Full
        basic terms: {copy,f}/{0,cons,n,nil,s}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(cons) = {1,2},
        uargs(copy) = {2,3},
        uargs(f) = {1}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
           p(0) = 1                           
        p(cons) = x1 + x2                     
        p(copy) = 2*x1 + 4*x1*x2 + 2*x2 + 2*x3
           p(f) = 2*x1                        
           p(n) = 0                           
         p(nil) = 0                           
           p(s) = 1 + x1                      
      
      Following rules are strictly oriented:
       copy(0(),y,z) = 2 + 6*y + 2*z              
                     > 2*z                        
                     = f(z)                       
      
      copy(s(x),y,z) = 2 + 2*x + 4*x*y + 6*y + 2*z
                     > 2*x + 4*x*y + 6*y + 2*z    
                     = copy(x,y,cons(f(y),z))     
      
      
      Following rules are (at-least) weakly oriented:
      f(cons(f(cons(nil(),y)),z)) =  4*y + 2*z    
                                  >= 2*y + 2*z    
                                  =  copy(n(),y,z)
      
                 f(cons(nil(),y)) =  2*y          
                                  >= y            
                                  =  y            
      
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
        f(cons(nil(),y)) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        copy(0(),y,z) -> f(z)
        copy(s(x),y,z) -> copy(x,y,cons(f(y),z))
      Signature:
        {copy/3,f/1} / {0/0,cons/2,n/0,nil/0,s/1}
      Obligation:
        Full
        basic terms: {copy,f}/{0,cons,n,nil,s}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(cons) = {1,2},
        uargs(copy) = {2,3},
        uargs(f) = {1}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
           p(0) = 1                         
        p(cons) = x1 + x2                   
        p(copy) = x1 + 6*x1*x2 + 4*x2 + 2*x3
           p(f) = 2*x1                      
           p(n) = 0                         
         p(nil) = 1                         
           p(s) = 1 + x1                    
      
      Following rules are strictly oriented:
      f(cons(f(cons(nil(),y)),z)) = 4 + 4*y + 2*z
                                  > 4*y + 2*z    
                                  = copy(n(),y,z)
      
                 f(cons(nil(),y)) = 2 + 2*y      
                                  > y            
                                  = y            
      
      
      Following rules are (at-least) weakly oriented:
       copy(0(),y,z) =  1 + 10*y + 2*z            
                     >= 2*z                       
                     =  f(z)                      
      
      copy(s(x),y,z) =  1 + x + 6*x*y + 10*y + 2*z
                     >= x + 6*x*y + 8*y + 2*z     
                     =  copy(x,y,cons(f(y),z))    
      
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        copy(0(),y,z) -> f(z)
        copy(s(x),y,z) -> copy(x,y,cons(f(y),z))
        f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
        f(cons(nil(),y)) -> y
      Signature:
        {copy/3,f/1} / {0/0,cons/2,n/0,nil/0,s/1}
      Obligation:
        Full
        basic terms: {copy,f}/{0,cons,n,nil,s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).