MAYBE
TRS:
 {       isLeaf(leaf()) -> true(),
     isLeaf(cons(u, v)) -> false(),
       left(cons(u, v)) -> u,
      right(cons(u, v)) -> v,
      concat(leaf(), y) -> y,
  concat(cons(u, v), y) -> cons(u, concat(v, y)),
   if1(b, true(), u, v) -> false(),
  if1(b, false(), u, v) -> if2(b, u, v),
      less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v),
      if2(true(), u, v) -> true(),
     if2(false(), u, v) -> less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
 DP:
  Strict:
   {concat#(cons(u, v), y) -> concat#(v, y),
    if1#(b, false(), u, v) -> if2#(b, u, v),
        less_leaves#(u, v) -> isLeaf#(u),
        less_leaves#(u, v) -> isLeaf#(v),
        less_leaves#(u, v) -> if1#(isLeaf(u), isLeaf(v), u, v),
       if2#(false(), u, v) -> left#(u),
       if2#(false(), u, v) -> left#(v),
       if2#(false(), u, v) -> right#(u),
       if2#(false(), u, v) -> right#(v),
       if2#(false(), u, v) -> concat#(left(u), right(u)),
       if2#(false(), u, v) -> concat#(left(v), right(v)),
       if2#(false(), u, v) -> less_leaves#(concat(left(u), right(u)), concat(left(v), right(v)))}
  Weak:
  {       isLeaf(leaf()) -> true(),
      isLeaf(cons(u, v)) -> false(),
        left(cons(u, v)) -> u,
       right(cons(u, v)) -> v,
       concat(leaf(), y) -> y,
   concat(cons(u, v), y) -> cons(u, concat(v, y)),
    if1(b, true(), u, v) -> false(),
   if1(b, false(), u, v) -> if2(b, u, v),
       less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v),
       if2(true(), u, v) -> true(),
      if2(false(), u, v) -> less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
  EDG:
   {(if2#(false(), u, v) -> concat#(left(u), right(u)), concat#(cons(u, v), y) -> concat#(v, y))
    (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
    (if2#(false(), u, v) -> less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))), less_leaves#(u, v) -> if1#(isLeaf(u), isLeaf(v), u, v))
    (if2#(false(), u, v) -> less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))), less_leaves#(u, v) -> isLeaf#(v))
    (if2#(false(), u, v) -> less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))), less_leaves#(u, v) -> isLeaf#(u))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> left#(u))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> left#(v))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> right#(u))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> right#(v))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> concat#(left(u), right(u)))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> concat#(left(v), right(v)))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))))
    (less_leaves#(u, v) -> if1#(isLeaf(u), isLeaf(v), u, v), if1#(b, false(), u, v) -> if2#(b, u, v))
    (if2#(false(), u, v) -> concat#(left(v), right(v)), concat#(cons(u, v), y) -> concat#(v, y))}
   SCCS:
    Scc:
     {if1#(b, false(), u, v) -> if2#(b, u, v),
          less_leaves#(u, v) -> if1#(isLeaf(u), isLeaf(v), u, v),
         if2#(false(), u, v) -> less_leaves#(concat(left(u), right(u)), concat(left(v), right(v)))}
    Scc:
     {concat#(cons(u, v), y) -> concat#(v, y)}
    SCC:
     Strict:
      {if1#(b, false(), u, v) -> if2#(b, u, v),
           less_leaves#(u, v) -> if1#(isLeaf(u), isLeaf(v), u, v),
          if2#(false(), u, v) -> less_leaves#(concat(left(u), right(u)), concat(left(v), right(v)))}
     Weak:
     {       isLeaf(leaf()) -> true(),
         isLeaf(cons(u, v)) -> false(),
           left(cons(u, v)) -> u,
          right(cons(u, v)) -> v,
          concat(leaf(), y) -> y,
      concat(cons(u, v), y) -> cons(u, concat(v, y)),
       if1(b, true(), u, v) -> false(),
      if1(b, false(), u, v) -> if2(b, u, v),
          less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v),
          if2(true(), u, v) -> true(),
         if2(false(), u, v) -> less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
     Fail
    SCC:
     Strict:
      {concat#(cons(u, v), y) -> concat#(v, y)}
     Weak:
     {       isLeaf(leaf()) -> true(),
         isLeaf(cons(u, v)) -> false(),
           left(cons(u, v)) -> u,
          right(cons(u, v)) -> v,
          concat(leaf(), y) -> y,
      concat(cons(u, v), y) -> cons(u, concat(v, y)),
       if1(b, true(), u, v) -> false(),
      if1(b, false(), u, v) -> if2(b, u, v),
          less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v),
          if2(true(), u, v) -> true(),
         if2(false(), u, v) -> less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
     SPSC:
      Simple Projection:
       pi(concat#) = 0
      Strict:
       {}
      Qed