MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict 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)) , le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , 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)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..