YES
Time: 0.018135
TRS:
 {                 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))}
 DP:
  DP:
   {             concat#(cons(U, V), Y) -> concat#(V, Y),
    lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V),
    lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z),
    lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))}
  TRS:
  {                 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))}
  UR:
   {    concat(leaf(), Y) -> Y,
    concat(cons(U, V), Y) -> cons(U, concat(V, Y))}
   EDG:
    {(lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V), concat#(cons(U, V), Y) -> concat#(V, Y))
     (concat#(cons(U, V), Y) -> concat#(V, Y), concat#(cons(U, V), Y) -> concat#(V, Y))
     (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V))
     (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z))
     (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)))
     (lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z), concat#(cons(U, V), Y) -> concat#(V, Y))}
    STATUS:
     arrows: 0.625000
     SCCS (2):
      Scc:
       {lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))}
      Scc:
       {concat#(cons(U, V), Y) -> concat#(V, Y)}
      
      SCC (1):
       Strict:
        {lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))}
       Weak:
       {                 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))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [concat](x0, x1) = x0 + x1,
         
         [cons](x0, x1) = x0 + x1 + 1,
         
         [lessleaves](x0, x1) = 0,
         
         [leaf] = 1,
         
         [false] = 0,
         
         [true] = 0,
         
         [lessleaves#](x0, x1) = x0
        Strict:
         lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))
         1 + 1U + 1V + 0W + 0Z >= 0 + 1U + 1V + 0W + 0Z
        Weak:
         lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
         0 + 0U + 0V + 0W + 0Z >= 0 + 0U + 0V + 0W + 0Z
         lessleaves(leaf(), cons(W, Z)) -> true()
         0 + 0W + 0Z >= 0
         lessleaves(X, leaf()) -> false()
         0 + 0X >= 0
         concat(cons(U, V), Y) -> cons(U, concat(V, Y))
         1 + 1Y + 1U + 1V >= 1 + 1Y + 1U + 1V
         concat(leaf(), Y) -> Y
         1 + 1Y >= 1Y
       Qed
     
     
     SCC (1):
      Strict:
       {concat#(cons(U, V), Y) -> concat#(V, Y)}
      Weak:
      {                 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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [concat](x0, x1) = x0 + 1,
        
        [cons](x0, x1) = x0 + 1,
        
        [lessleaves](x0, x1) = x0 + 1,
        
        [leaf] = 1,
        
        [false] = 0,
        
        [true] = 0,
        
        [concat#](x0, x1) = x0
       Strict:
        concat#(cons(U, V), Y) -> concat#(V, Y)
        1 + 0Y + 0U + 1V >= 0 + 0Y + 1V
       Weak:
        lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
        2 + 0U + 0V + 0W + 1Z >= 2 + 0U + 0V + 1W + 0Z
        lessleaves(leaf(), cons(W, Z)) -> true()
        2 + 0W + 1Z >= 0
        lessleaves(X, leaf()) -> false()
        2 + 0X >= 0
        concat(cons(U, V), Y) -> cons(U, concat(V, Y))
        2 + 0Y + 0U + 1V >= 2 + 0Y + 0U + 1V
        concat(leaf(), Y) -> Y
        2 + 0Y >= 1Y
      Qed