TRS:
 {           lessElements(l, t) -> lessE(l, t, 0()),
                 lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n),
         if(true(), b, l, t, n) -> l,
   if(false(), true(), l, t, n) -> t,
  if(false(), false(), l, t, n) -> lessE(l, t, s(n)),
                  length(nil()) -> 0(),
             length(cons(n, l)) -> s(length(l)),
                 toList(leaf()) -> nil(),
        toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))),
              append(nil(), l2) -> l2,
        append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                  le(s(n), 0()) -> false(),
                     le(0(), m) -> true(),
                 le(s(n), s(m)) -> le(n, m),
                            a() -> c(),
                            a() -> d()}
 Fail