YES
TRS:
 {                  concat(leaf(), y) -> y,
                concat(cons(u, v), y) -> cons(u, concat(v, y)),
               less_leaves(x, leaf()) -> false(),
      less_leaves(leaf(), cons(w, z)) -> true(),
  less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
 RUF:
  Strict:
   {              concat(cons(u, v), y) -> cons(u, concat(v, y)),
    less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
  Weak:
   {}
  DP:
   Strict:
    {              concat#(cons(u, v), y) -> concat#(v, y),
     less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v),
     less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z),
     less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
   Weak:
   {              concat(cons(u, v), y) -> cons(u, concat(v, y)),
    less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
   EDG:
    {(less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), concat#(cons(u, v), y) -> concat#(v, y))
     (less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), concat#(cons(u, v), y) -> concat#(v, y))
     (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v))
     (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z))
     (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)))
     (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))}
    SCCS:
     Scc:
      {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
     Scc:
      {concat#(cons(u, v), y) -> concat#(v, y)}
     SCC:
      Strict:
       {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
      Weak:
      {              concat(cons(u, v), y) -> cons(u, concat(v, y)),
       less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
      POLY:
       Argument Filtering:
        pi(less_leaves#) = [0,1], pi(less_leaves) = [], pi(cons) = [0,1], pi(concat) = 0
       Usable Rules:
        {}
       Interpretation:
        [less_leaves#](x0, x1) = x0 + x1,
        [cons](x0, x1) = x0 + x1 + 1
       Strict:
        {}
       Weak:
        {              concat(cons(u, v), y) -> cons(u, concat(v, y)),
         less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
       Qed
     SCC:
      Strict:
       {concat#(cons(u, v), y) -> concat#(v, y)}
      Weak:
      {              concat(cons(u, v), y) -> cons(u, concat(v, y)),
       less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
      SPSC:
       Simple Projection:
        pi(concat#) = 0
       Strict:
        {}
       Qed