YES(?,O(n^2))

Problem:
 ++(nil(),y) -> y
 ++(x,nil()) -> x
 ++(.(x,y),z) -> .(x,++(y,z))
 ++(++(x,y),z) -> ++(x,++(y,z))

Proof:
 Complexity Transformation Processor:
  strict:
   ++(nil(),y) -> y
   ++(x,nil()) -> x
   ++(.(x,y),z) -> .(x,++(y,z))
   ++(++(x,y),z) -> ++(x,++(y,z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [.](x0, x1) = x0 + x1,
     
     [++](x0, x1) = x0 + x1,
     
     [nil] = 1
    orientation:
     ++(nil(),y) = y + 1 >= y = y
     
     ++(x,nil()) = x + 1 >= x = x
     
     ++(.(x,y),z) = x + y + z >= x + y + z = .(x,++(y,z))
     
     ++(++(x,y),z) = x + y + z >= x + y + z = ++(x,++(y,z))
    problem:
     strict:
      ++(.(x,y),z) -> .(x,++(y,z))
      ++(++(x,y),z) -> ++(x,++(y,z))
     weak:
      ++(nil(),y) -> y
      ++(x,nil()) -> x
    Matrix Interpretation Processor:
     dimension: 2
     max_matrix:
      [1 1]
      [0 1]
      interpretation:
                     [1 0]       
       [.](x0, x1) = [0 0]x0 + x1,
       
                      [1 1]          [0]
       [++](x0, x1) = [0 1]x0 + x1 + [1],
       
               [0]
       [nil] = [1]
      orientation:
                      [1 0]    [1 1]        [0]    [1 0]    [1 1]        [0]               
       ++(.(x,y),z) = [0 0]x + [0 1]y + z + [1] >= [0 0]x + [0 1]y + z + [1] = .(x,++(y,z))
       
                       [1 2]    [1 1]        [1]    [1 1]    [1 1]        [0]                
       ++(++(x,y),z) = [0 1]x + [0 1]y + z + [2] >= [0 1]x + [0 1]y + z + [2] = ++(x,++(y,z))
       
                         [1]         
       ++(nil(),y) = y + [2] >= y = y
       
                     [1 1]    [0]         
       ++(x,nil()) = [0 1]x + [2] >= x = x
      problem:
       strict:
        ++(.(x,y),z) -> .(x,++(y,z))
       weak:
        ++(++(x,y),z) -> ++(x,++(y,z))
        ++(nil(),y) -> y
        ++(x,nil()) -> x
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                       [1 0]          [0]
         [.](x0, x1) = [0 0]x0 + x1 + [1],
         
                        [1 1]       
         [++](x0, x1) = [0 1]x0 + x1,
         
                 [0]
         [nil] = [1]
        orientation:
                        [1 0]    [1 1]        [1]    [1 0]    [1 1]        [0]               
         ++(.(x,y),z) = [0 0]x + [0 1]y + z + [1] >= [0 0]x + [0 1]y + z + [1] = .(x,++(y,z))
         
                         [1 2]    [1 1]         [1 1]    [1 1]                     
         ++(++(x,y),z) = [0 1]x + [0 1]y + z >= [0 1]x + [0 1]y + z = ++(x,++(y,z))
         
                           [1]         
         ++(nil(),y) = y + [1] >= y = y
         
                       [1 1]    [0]         
         ++(x,nil()) = [0 1]x + [1] >= x = x
        problem:
         strict:
          
         weak:
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(++(x,y),z) -> ++(x,++(y,z))
          ++(nil(),y) -> y
          ++(x,nil()) -> x
        Qed