YES
Time: 0.005610
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))}
 RUF:
  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:
   {}
  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(cons(U, V), Y) -> cons(U, concat(V, Y)),
    lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))}
   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))}
    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(cons(U, V), Y) -> cons(U, concat(V, Y)),
       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,
        
        [cons](x0, x1) = x0 + 1,
        
        [lessleaves](x0, x1) = x0 + 1,
        
        [lessleaves#](x0, x1) = x0
       Strict:
        lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))
        1 + 1U + 0V + 0W + 0Z >= 0 + 1U + 0V + 0W + 0Z
       Weak:
        
      Qed
    SCC (1):
     Strict:
      {concat#(cons(U, V), Y) -> concat#(V, Y)}
     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))}
     SPSC:
      Simple Projection:
       pi(concat#) = 0
      Strict:
       {}
      Qed