Consider the TRS R consisting of the rewrite rules

1: is_empty(nil) -> true
2: is_empty(cons(x,l)) -> false
3: hd(cons(x,l)) -> x
4: tl(cons(x,l)) -> l
5: append(l1,l2) -> ifappend(l1,l2,l1)
6: ifappend(l1,l2,nil) -> l2
7: ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2))

There are 2 dependency pairs:

8: APPEND(l1,l2) -> IFAPPEND(l1,l2,l1)
9: IFAPPEND(l1,l2,cons(x,l)) -> APPEND(l,l2)

The approximated dependency graph contains one SCC:
{8,9}.

- Consider the SCC {8,9}.
There are no usable rules.
By taking the polynomial interpretation
[APPEND](x,y) = [cons](x,y) = x + y + 1
and [IFAPPEND](x,y,z) = y + z + 1,
rule 8
is weakly decreasing and
rule 9
is strictly decreasing.

Hence the TRS is terminating.