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))} Fail