YES
Time: 0.005062
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:
   DP:
    {              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))}
   TRS:
   {              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#(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))
     (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)))
     (less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), concat#(cons(u, v), y) -> concat#(v, y))}
    SCCS (2):
     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 (1):
      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:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [concat](x0, x1) = x0,
        
        [cons](x0, x1) = x0 + 1,
        
        [less_leaves](x0, x1) = x0 + 1,
        
        [less_leaves#](x0, x1) = x0
       Strict:
        less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(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)),
      less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
     SPSC:
      Simple Projection:
       pi(concat#) = 0
      Strict:
       {}
      Qed