YES
Time: 0.010109
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))}
  UR:
   {    concat(leaf(), y) -> y,
    concat(cons(u, v), y) -> cons(u, concat(v, y))}
   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))}
    STATUS:
     arrows: 0.625000
     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(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
     
     
     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)),
                    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 + 1,
        
        [cons](x0, x1) = x0 + 1,
        
        [less_leaves](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:
        less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))
        2 + 0u + 0v + 0w + 1z >= 2 + 0u + 0v + 1w + 0z
        less_leaves(leaf(), cons(w, z)) -> true()
        2 + 0w + 1z >= 0
        less_leaves(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