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:
 RT 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
   interpretation:
    [true] = 0,
    
    [false] = 0,
    
    [lessleaves](x0, x1) = x0 + x1 + 2,
    
    [cons](x0, x1) = x0 + x1 + 4,
    
    [concat](x0, x1) = x0 + x1,
    
    [leaf] = 11
   orientation:
    concat(leaf(),Y) = Y + 11 >= Y = Y
    
    concat(cons(U,V),Y) = U + V + Y + 4 >= U + V + Y + 4 = cons(U,concat(V,Y))
    
    lessleaves(X,leaf()) = X + 13 >= 0 = false()
    
    lessleaves(leaf(),cons(W,Z)) = W + Z + 17 >= 0 = true()
    
    lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 10 >= U + V + W + Z + 2 = lessleaves(concat(U,V),concat(W,Z))
   problem:
    strict:
     concat(cons(U,V),Y) -> cons(U,concat(V,Y))
    weak:
     concat(leaf(),Y) -> 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))
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
              [0]
     [true] = [2],
     
               [0]
     [false] = [0],
     
                            [1 2]     [1 2]     [1]
     [lessleaves](x0, x1) = [0 0]x0 + [0 0]x1 + [2],
     
                      [1 1]          [0]
     [cons](x0, x1) = [0 1]x0 + x1 + [1],
     
                        [1 1]          [2]
     [concat](x0, x1) = [0 1]x0 + x1 + [0],
     
              [1 ]
     [leaf] = [12]
    orientation:
                           [1 2]    [1 1]        [3]    [1 1]    [1 1]        [2]                      
     concat(cons(U,V),Y) = [0 1]U + [0 1]V + Y + [1] >= [0 1]U + [0 1]V + Y + [1] = cons(U,concat(V,Y))
     
                            [15]         
     concat(leaf(),Y) = Y + [12] >= Y = Y
     
                            [1 2]    [26]    [0]          
     lessleaves(X,leaf()) = [0 0]X + [2 ] >= [0] = false()
     
                                    [1 3]    [1 2]    [28]    [0]         
     lessleaves(leaf(),cons(W,Z)) = [0 0]W + [0 0]Z + [2 ] >= [2] = true()
     
                                       [1 3]    [1 2]    [1 3]    [1 2]    [5]    [1 3]    [1 2]    [1 3]    [1 2]    [5]                                      
     lessleaves(cons(U,V),cons(W,Z)) = [0 0]U + [0 0]V + [0 0]W + [0 0]Z + [2] >= [0 0]U + [0 0]V + [0 0]W + [0 0]Z + [2] = lessleaves(concat(U,V),concat(W,Z))
    problem:
     strict:
      
     weak:
      concat(cons(U,V),Y) -> cons(U,concat(V,Y))
      concat(leaf(),Y) -> 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))
    Qed