Consider the TRS R consisting of the rewrite rules

1: admit(x,nil) -> nil
2: admit(x,u . (v . (w . z))) -> cond(sum(x,u,v) = w,u . (v . (w . admit(carry(x,u,v),z))))
3: cond(true,y) -> y

There are 2 dependency pairs:

4: ADMIT(x,u . (v . (w . z))) -> COND(sum(x,u,v) = w,u . (v . (w . admit(carry(x,u,v),z))))
5: ADMIT(x,u . (v . (w . z))) -> ADMIT(carry(x,u,v),z)

The approximated dependency graph contains one SCC:
{5}.

- Consider the SCC {5}.
There are no usable rules.
By taking the polynomial interpretation
[w] = 1,
[.](x,y) = [ADMIT](x,y) = x + y + 1
and [carry](x,y,z) = x + y + z + 1,
rule 5
is strictly decreasing.

Hence the TRS is terminating.