*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        ++(x,nil()) -> x
        ++(++(x,y),z) -> ++(x,++(y,z))
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {++/2} / {./2,nil/0}
      Obligation:
        Full
        basic terms: {++}/{.,nil}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following weak dependency pairs:
      
      Strict DPs
        ++#(x,nil()) -> c_1(x)
        ++#(++(x,y),z) -> c_2(++#(x,++(y,z)))
        ++#(.(x,y),z) -> c_3(x,++#(y,z))
        ++#(nil(),y) -> c_4(y)
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        ++#(x,nil()) -> c_1(x)
        ++#(++(x,y),z) -> c_2(++#(x,++(y,z)))
        ++#(.(x,y),z) -> c_3(x,++#(y,z))
        ++#(nil(),y) -> c_4(y)
      Strict TRS Rules:
        ++(x,nil()) -> x
        ++(++(x,y),z) -> ++(x,++(y,z))
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {++/2,++#/2} / {./2,nil/0,c_1/1,c_2/1,c_3/2,c_4/1}
      Obligation:
        Full
        basic terms: {++#}/{.,nil}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 0, 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(++) = {2},
          uargs(.) = {2},
          uargs(++#) = {2},
          uargs(c_2) = {1},
          uargs(c_3) = {2},
          uargs(c_4) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
           p(++) = [2] x1 + [1] x2 + [2]
            p(.) = [1] x2 + [0]         
          p(nil) = [0]                  
          p(++#) = [4] x1 + [1] x2 + [0]
          p(c_1) = [4] x1 + [0]         
          p(c_2) = [1] x1 + [0]         
          p(c_3) = [1] x2 + [0]         
          p(c_4) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        ++#(++(x,y),z) = [8] x + [4] y + [1] z + [8]
                       > [4] x + [2] y + [1] z + [2]
                       = c_2(++#(x,++(y,z)))        
        
           ++(x,nil()) = [2] x + [2]                
                       > [1] x + [0]                
                       = x                          
        
         ++(++(x,y),z) = [4] x + [2] y + [1] z + [6]
                       > [2] x + [2] y + [1] z + [4]
                       = ++(x,++(y,z))              
        
           ++(nil(),y) = [1] y + [2]                
                       > [1] y + [0]                
                       = y                          
        
        
        Following rules are (at-least) weakly oriented:
         ++#(x,nil()) =  [4] x + [0]        
                      >= [4] x + [0]        
                      =  c_1(x)             
        
        ++#(.(x,y),z) =  [4] y + [1] z + [0]
                      >= [4] y + [1] z + [0]
                      =  c_3(x,++#(y,z))    
        
         ++#(nil(),y) =  [1] y + [0]        
                      >= [1] y + [0]        
                      =  c_4(y)             
        
         ++(.(x,y),z) =  [2] y + [1] z + [2]
                      >= [2] y + [1] z + [2]
                      =  .(x,++(y,z))       
        
      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:
        ++#(x,nil()) -> c_1(x)
        ++#(.(x,y),z) -> c_3(x,++#(y,z))
        ++#(nil(),y) -> c_4(y)
      Strict TRS Rules:
        ++(.(x,y),z) -> .(x,++(y,z))
      Weak DP Rules:
        ++#(++(x,y),z) -> c_2(++#(x,++(y,z)))
      Weak TRS Rules:
        ++(x,nil()) -> x
        ++(++(x,y),z) -> ++(x,++(y,z))
        ++(nil(),y) -> y
      Signature:
        {++/2,++#/2} / {./2,nil/0,c_1/1,c_2/1,c_3/2,c_4/1}
      Obligation:
        Full
        basic terms: {++#}/{.,nil}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 0, 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(++) = {2},
          uargs(.) = {2},
          uargs(++#) = {2},
          uargs(c_2) = {1},
          uargs(c_3) = {2},
          uargs(c_4) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
           p(++) = [2] x1 + [1] x2 + [0]
            p(.) = [1] x2 + [0]         
          p(nil) = [0]                  
          p(++#) = [4] x1 + [1] x2 + [9]
          p(c_1) = [4] x1 + [0]         
          p(c_2) = [1] x1 + [0]         
          p(c_3) = [1] x2 + [0]         
          p(c_4) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        ++#(x,nil()) = [4] x + [9]
                     > [4] x + [0]
                     = c_1(x)     
        
        ++#(nil(),y) = [1] y + [9]
                     > [1] y + [0]
                     = c_4(y)     
        
        
        Following rules are (at-least) weakly oriented:
        ++#(++(x,y),z) =  [8] x + [4] y + [1] z + [9]
                       >= [4] x + [2] y + [1] z + [9]
                       =  c_2(++#(x,++(y,z)))        
        
         ++#(.(x,y),z) =  [4] y + [1] z + [9]        
                       >= [4] y + [1] z + [9]        
                       =  c_3(x,++#(y,z))            
        
           ++(x,nil()) =  [2] x + [0]                
                       >= [1] x + [0]                
                       =  x                          
        
         ++(++(x,y),z) =  [4] x + [2] y + [1] z + [0]
                       >= [2] x + [2] y + [1] z + [0]
                       =  ++(x,++(y,z))              
        
          ++(.(x,y),z) =  [2] y + [1] z + [0]        
                       >= [2] y + [1] z + [0]        
                       =  .(x,++(y,z))               
        
           ++(nil(),y) =  [1] y + [0]                
                       >= [1] y + [0]                
                       =  y                          
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        ++#(.(x,y),z) -> c_3(x,++#(y,z))
      Strict TRS Rules:
        ++(.(x,y),z) -> .(x,++(y,z))
      Weak DP Rules:
        ++#(x,nil()) -> c_1(x)
        ++#(++(x,y),z) -> c_2(++#(x,++(y,z)))
        ++#(nil(),y) -> c_4(y)
      Weak TRS Rules:
        ++(x,nil()) -> x
        ++(++(x,y),z) -> ++(x,++(y,z))
        ++(nil(),y) -> y
      Signature:
        {++/2,++#/2} / {./2,nil/0,c_1/1,c_2/1,c_3/2,c_4/1}
      Obligation:
        Full
        basic terms: {++#}/{.,nil}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 0, 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(++) = {2},
          uargs(.) = {2},
          uargs(++#) = {2},
          uargs(c_2) = {1},
          uargs(c_3) = {2},
          uargs(c_4) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
           p(++) = [2] x1 + [1] x2 + [0]
            p(.) = [1] x2 + [1]         
          p(nil) = [0]                  
          p(++#) = [8] x1 + [1] x2 + [0]
          p(c_1) = [0]                  
          p(c_2) = [1] x1 + [0]         
          p(c_3) = [1] x2 + [0]         
          p(c_4) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        ++#(.(x,y),z) = [8] y + [1] z + [8]
                      > [8] y + [1] z + [0]
                      = c_3(x,++#(y,z))    
        
         ++(.(x,y),z) = [2] y + [1] z + [2]
                      > [2] y + [1] z + [1]
                      = .(x,++(y,z))       
        
        
        Following rules are (at-least) weakly oriented:
          ++#(x,nil()) =  [8] x + [0]                 
                       >= [0]                         
                       =  c_1(x)                      
        
        ++#(++(x,y),z) =  [16] x + [8] y + [1] z + [0]
                       >= [8] x + [2] y + [1] z + [0] 
                       =  c_2(++#(x,++(y,z)))         
        
          ++#(nil(),y) =  [1] y + [0]                 
                       >= [1] y + [0]                 
                       =  c_4(y)                      
        
           ++(x,nil()) =  [2] x + [0]                 
                       >= [1] x + [0]                 
                       =  x                           
        
         ++(++(x,y),z) =  [4] x + [2] y + [1] z + [0] 
                       >= [2] x + [2] y + [1] z + [0] 
                       =  ++(x,++(y,z))               
        
           ++(nil(),y) =  [1] y + [0]                 
                       >= [1] y + [0]                 
                       =  y                           
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        ++#(x,nil()) -> c_1(x)
        ++#(++(x,y),z) -> c_2(++#(x,++(y,z)))
        ++#(.(x,y),z) -> c_3(x,++#(y,z))
        ++#(nil(),y) -> c_4(y)
      Weak TRS Rules:
        ++(x,nil()) -> x
        ++(++(x,y),z) -> ++(x,++(y,z))
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
      Signature:
        {++/2,++#/2} / {./2,nil/0,c_1/1,c_2/1,c_3/2,c_4/1}
      Obligation:
        Full
        basic terms: {++#}/{.,nil}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).