MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { is_empty(nil()) -> true() , is_empty(cons(x, l)) -> false() , hd(cons(x, l)) -> x , tl(cons(x, l)) -> cons(x, l) , append(l1, l2) -> ifappend(l1, l2, is_empty(l1)) , ifappend(l1, l2, true()) -> l2 , ifappend(l1, l2, false()) -> cons(hd(l1), append(tl(l1), l2)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..