Consider the TRS R consisting of the rewrite rules

1: min(x,0) -> 0
2: min(0,y) -> 0
3: min(s(x),s(y)) -> s(min(x,y))
4: max(x,0) -> x
5: max(0,y) -> y
6: max(s(x),s(y)) -> s(max(x,y))
7: x - 0 -> x
8: s(x) - s(y) -> x - y
9: gcd(s(x),0) -> s(x)
10: gcd(0,s(x)) -> s(x)
11: gcd(s(x),s(y)) -> gcd(max(x,y) - min(x,y),s(min(x,y)))

There are 7 dependency pairs:

12: MIN(s(x),s(y)) -> MIN(x,y)
13: MAX(s(x),s(y)) -> MAX(x,y)
14: s(x) -# s(y) -> x -# y
15: GCD(s(x),s(y)) -> GCD(max(x,y) - min(x,y),s(min(x,y)))
16: GCD(s(x),s(y)) -> max(x,y) -# min(x,y)
17: GCD(s(x),s(y)) -> MAX(x,y)
18: GCD(s(x),s(y)) -> MIN(x,y)

The approximated dependency graph contains 4 SCCs:
{14},
{13},
{12}
and {15}.

- Consider the SCC {14}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [-#](x,y) = x + y + 1,
rule 14
is strictly decreasing.

- Consider the SCC {13}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [MAX](x,y) = x + y + 1,
rule 13
is strictly decreasing.

- Consider the SCC {12}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [MIN](x,y) = x + y + 1,
rule 12
is strictly decreasing.

- Consider the SCC {15}.
The usable rules are {1-8}.
By taking the polynomial interpretation
[0] = 1,
[min](x,y) = 2x + 1,
[s](x) = 3x + 3,
[GCD](x,y) = 3x + y + 1,
[-](x,y) = x
and [max](x,y) = x + y + 1,
the rules in {1,7}
are weakly decreasing and
the rules in {2-6,8,15}
are strictly decreasing.

Hence the TRS is terminating.