Consider the TRS R consisting of the rewrite rules

1: minus(X,s(Y)) -> pred(minus(X,Y))
2: minus(X,0) -> X
3: pred(s(X)) -> X
4: le(s(X),s(Y)) -> le(X,Y)
5: le(s(X),0) -> false
6: le(0,Y) -> true
7: gcd(0,Y) -> 0
8: gcd(s(X),0) -> s(X)
9: gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
10: if(true,s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
11: if(false,s(X),s(Y)) -> gcd(minus(Y,X),s(X))

There are 9 dependency pairs:

12: MINUS(X,s(Y)) -> PRED(minus(X,Y))
13: MINUS(X,s(Y)) -> MINUS(X,Y)
14: LE(s(X),s(Y)) -> LE(X,Y)
15: GCD(s(X),s(Y)) -> IF(le(Y,X),s(X),s(Y))
16: GCD(s(X),s(Y)) -> LE(Y,X)
17: IF(true,s(X),s(Y)) -> GCD(minus(X,Y),s(Y))
18: IF(true,s(X),s(Y)) -> MINUS(X,Y)
19: IF(false,s(X),s(Y)) -> GCD(minus(Y,X),s(X))
20: IF(false,s(X),s(Y)) -> MINUS(Y,X)

The approximated dependency graph contains 3 SCCs:
{14},
{13}
and {15,17,19}.

- Consider the SCC {14}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [LE](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 [MINUS](x,y) = x + y + 1,
rule 13
is strictly decreasing.

- Consider the SCC {15,17,19}.
The usable rules are {1-6}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[minus](x,y) = [pred](x) = x,
[s](x) = x + 1,
[GCD](x,y) = [le](x,y) = x + y + 1
and [IF](x,y,z) = y + z + 1,
the rules in {1,2,15}
are weakly decreasing and
the rules in {3-6,17,19}
are strictly decreasing.

Hence the TRS is terminating.