Consider the TRS R consisting of the rewrite rules

1: gcd(x,0) -> x
2: gcd(0,y) -> y
3: gcd(s(x),s(y)) -> if(x < y,gcd(s(x),y - x),gcd(x - y,s(y)))

There are 2 dependency pairs:

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

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.