Consider the TRS R consisting of the rewrite rules

1: bin(x,0) -> s(0)
2: bin(0,s(y)) -> 0
3: bin(s(x),s(y)) -> bin(x,s(y)) + bin(x,y)

There are 2 dependency pairs:

4: BIN(s(x),s(y)) -> BIN(x,s(y))
5: BIN(s(x),s(y)) -> BIN(x,y)

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

- Consider the SCC {4,5}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [BIN](x,y) = x + y + 1,
the rules in {4,5}
are strictly decreasing.

Hence the TRS is terminating.