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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
            [0]
   [true] = [0],
   
             [0 ]
   [false] = [12],
   
                          [1 4]     [1 0]     [0 ]
   [lessleaves](x0, x1) = [0 1]x0 + [0 0]x1 + [12],
   
                    [1 8]          [7]
   [cons](x0, x1) = [0 1]x0 + x1 + [4],
   
                      [1 1]          [4]
   [concat](x0, x1) = [0 1]x0 + x1 + [4],
   
            [6]
   [leaf] = [2]
  orientation:
                          [12]         
   concat(leaf(),Y) = Y + [6 ] >= Y = Y
   
                         [1 9]    [1 1]        [15]    [1 8]    [1 1]        [11]                      
   concat(cons(U,V),Y) = [0 1]U + [0 1]V + Y + [8 ] >= [0 1]U + [0 1]V + Y + [8 ] = cons(U,concat(V,Y))
   
                          [1 4]    [6 ]    [0 ]          
   lessleaves(X,leaf()) = [0 1]X + [12] >= [12] = false()
   
                                  [1 8]    [1 0]    [21]    [0]         
   lessleaves(leaf(),cons(W,Z)) = [0 0]W + [0 0]Z + [14] >= [0] = true()
   
                                     [1  12]    [1 4]    [1 8]    [1 0]    [30]    [1 5]    [1 4]    [1 1]    [1 0]    [24]                                      
   lessleaves(cons(U,V),cons(W,Z)) = [0  1 ]U + [0 1]V + [0 0]W + [0 0]Z + [16] >= [0 1]U + [0 1]V + [0 0]W + [0 0]Z + [16] = lessleaves(concat(U,V),concat(W,Z))
  problem:
   
  Qed