*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
        duplicate(Nil()) -> Nil()
        goal(x) -> duplicate(x)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {duplicate/1,goal/1} / {Cons/2,Nil/0}
      Obligation:
        Innermost
        basic terms: {duplicate,goal}/{Cons,Nil}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(Cons) = {2}
      
      Following symbols are considered usable:
        {duplicate,goal}
      TcT has computed the following interpretation:
             p(Cons) = [1] x2 + [0]
              p(Nil) = [0]         
        p(duplicate) = [0]         
             p(goal) = [9]         
      
      Following rules are strictly oriented:
      goal(x) = [9]         
              > [0]         
              = duplicate(x)
      
      
      Following rules are (at-least) weakly oriented:
      duplicate(Cons(x,xs)) =  [0]                          
                            >= [0]                          
                            =  Cons(x,Cons(x,duplicate(xs)))
      
           duplicate(Nil()) =  [0]                          
                            >= [0]                          
                            =  Nil()                        
      
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
        duplicate(Nil()) -> Nil()
      Weak DP Rules:
        
      Weak TRS Rules:
        goal(x) -> duplicate(x)
      Signature:
        {duplicate/1,goal/1} / {Cons/2,Nil/0}
      Obligation:
        Innermost
        basic terms: {duplicate,goal}/{Cons,Nil}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(Cons) = {2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
               p(Cons) = [1] x2 + [0]
                p(Nil) = [0]         
          p(duplicate) = [5]         
               p(goal) = [5]         
        
        Following rules are strictly oriented:
        duplicate(Nil()) = [5]  
                         > [0]  
                         = Nil()
        
        
        Following rules are (at-least) weakly oriented:
        duplicate(Cons(x,xs)) =  [5]                          
                              >= [5]                          
                              =  Cons(x,Cons(x,duplicate(xs)))
        
                      goal(x) =  [5]                          
                              >= [5]                          
                              =  duplicate(x)                 
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
      Weak DP Rules:
        
      Weak TRS Rules:
        duplicate(Nil()) -> Nil()
        goal(x) -> duplicate(x)
      Signature:
        {duplicate/1,goal/1} / {Cons/2,Nil/0}
      Obligation:
        Innermost
        basic terms: {duplicate,goal}/{Cons,Nil}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(Cons) = {2}
      
      Following symbols are considered usable:
        {duplicate,goal}
      TcT has computed the following interpretation:
             p(Cons) = [1] x2 + [3]
              p(Nil) = [3]         
        p(duplicate) = [6] x1 + [1]
             p(goal) = [6] x1 + [1]
      
      Following rules are strictly oriented:
      duplicate(Cons(x,xs)) = [6] xs + [19]                
                            > [6] xs + [7]                 
                            = Cons(x,Cons(x,duplicate(xs)))
      
      
      Following rules are (at-least) weakly oriented:
      duplicate(Nil()) =  [19]        
                       >= [3]         
                       =  Nil()       
      
               goal(x) =  [6] x + [1] 
                       >= [6] x + [1] 
                       =  duplicate(x)
      
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        duplicate(Cons(x,xs)) -> Cons(x,Cons(x,duplicate(xs)))
        duplicate(Nil()) -> Nil()
        goal(x) -> duplicate(x)
      Signature:
        {duplicate/1,goal/1} / {Cons/2,Nil/0}
      Obligation:
        Innermost
        basic terms: {duplicate,goal}/{Cons,Nil}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).