YES(?,O(n^2))

Problem:
 concat(leaf(),Y) -> Y
 concat(cons(U,V),Y) -> cons(U,concat(V,Y))
 lessleaves(X,leaf()) -> false()
 lessleaves(leaf(),cons(W,Z)) -> true()
 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))

Proof:
 Complexity Transformation Processor:
  strict:
   concat(leaf(),Y) -> Y
   concat(cons(U,V),Y) -> cons(U,concat(V,Y))
   lessleaves(X,leaf()) -> false()
   lessleaves(leaf(),cons(W,Z)) -> true()
   lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [true] = 0,
     
     [false] = 0,
     
     [lessleaves](x0, x1) = x0 + x1,
     
     [cons](x0, x1) = x0 + x1,
     
     [concat](x0, x1) = x0 + x1,
     
     [leaf] = 1
    orientation:
     concat(leaf(),Y) = Y + 1 >= Y = Y
     
     concat(cons(U,V),Y) = U + V + Y >= U + V + Y = cons(U,concat(V,Y))
     
     lessleaves(X,leaf()) = X + 1 >= 0 = false()
     
     lessleaves(leaf(),cons(W,Z)) = W + Z + 1 >= 0 = true()
     
     lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z >= U + V + W + Z = lessleaves(concat(U,V),concat(W,Z))
    problem:
     strict:
      concat(cons(U,V),Y) -> cons(U,concat(V,Y))
      lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
     weak:
      concat(leaf(),Y) -> Y
      lessleaves(X,leaf()) -> false()
      lessleaves(leaf(),cons(W,Z)) -> true()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [true] = 1,
       
       [false] = 0,
       
       [lessleaves](x0, x1) = x0 + x1,
       
       [cons](x0, x1) = x0 + x1 + 1,
       
       [concat](x0, x1) = x0 + x1,
       
       [leaf] = 0
      orientation:
       concat(cons(U,V),Y) = U + V + Y + 1 >= U + V + Y + 1 = cons(U,concat(V,Y))
       
       lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 2 >= U + V + W + Z = lessleaves(concat(U,V),concat(W,Z))
       
       concat(leaf(),Y) = Y >= Y = Y
       
       lessleaves(X,leaf()) = X >= 0 = false()
       
       lessleaves(leaf(),cons(W,Z)) = W + Z + 1 >= 1 = true()
      problem:
       strict:
        concat(cons(U,V),Y) -> cons(U,concat(V,Y))
       weak:
        lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
        concat(leaf(),Y) -> Y
        lessleaves(X,leaf()) -> false()
        lessleaves(leaf(),cons(W,Z)) -> true()
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                  [0]
         [true] = [1],
         
                   [0]
         [false] = [0],
         
                                [1 0]     [1 0]     [0]
         [lessleaves](x0, x1) = [0 0]x0 + [0 0]x1 + [1],
         
                          [1 1]          [1]
         [cons](x0, x1) = [0 0]x0 + x1 + [1],
         
                            [1 1]          [1]
         [concat](x0, x1) = [0 1]x0 + x1 + [0],
         
                  [0]
         [leaf] = [0]
        orientation:
                               [1 1]    [1 1]        [3]    [1 1]    [1 1]        [2]                      
         concat(cons(U,V),Y) = [0 0]U + [0 1]V + Y + [1] >= [0 0]U + [0 1]V + Y + [1] = cons(U,concat(V,Y))
         
                                           [1 1]    [1 0]    [1 1]    [1 0]    [2]    [1 1]    [1 0]    [1 1]    [1 0]    [2]                                      
         lessleaves(cons(U,V),cons(W,Z)) = [0 0]U + [0 0]V + [0 0]W + [0 0]Z + [1] >= [0 0]U + [0 0]V + [0 0]W + [0 0]Z + [1] = lessleaves(concat(U,V),concat(W,Z))
         
                                [1]         
         concat(leaf(),Y) = Y + [0] >= Y = Y
         
                                [1 0]    [0]    [0]          
         lessleaves(X,leaf()) = [0 0]X + [1] >= [0] = false()
         
                                        [1 1]    [1 0]    [1]    [0]         
         lessleaves(leaf(),cons(W,Z)) = [0 0]W + [0 0]Z + [1] >= [1] = true()
        problem:
         strict:
          
         weak:
          concat(cons(U,V),Y) -> cons(U,concat(V,Y))
          lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
          concat(leaf(),Y) -> Y
          lessleaves(X,leaf()) -> false()
          lessleaves(leaf(),cons(W,Z)) -> true()
        Qed