YES
Time: 0.007136
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))}
 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(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))}
  EDG:
   {(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)))}
   STATUS:
    arrows: 0.812500
    SCCS (1):
     Scc:
      {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
     
     
     SCC (1):
      Strict:
       {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
      Weak:
      {                  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))}
      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,
        
        [less_leaves](x0, x1) = 0,
        
        [leaf] = 1,
        
        [false] = 0,
        
        [true] = 0,
        
        [less_leaves#](x0, x1) = x0
       Strict:
        less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))
        1 + 1u + 1v + 0w + 0z >= 0 + 1u + 1v + 0w + 0z
       Weak:
        less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
        0 + 0u + 0v + 0w + 0z >= 0 + 0u + 0v + 0w + 0z
        less_leaves(leaf(), cons(w, z)) -> true()
        0 + 0w + 0z >= 0
        less_leaves(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