YES

We show the termination of the TRS R:

  gcd(x,|0|()) -> x
  gcd(|0|(),y) -> y
  gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y)))

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: gcd#(s(x),s(y)) -> gcd#(s(x),-(y,x))
p2: gcd#(s(x),s(y)) -> gcd#(-(x,y),s(y))

and R consists of:

r1: gcd(x,|0|()) -> x
r2: gcd(|0|(),y) -> y
r3: gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y)))

The estimated dependency graph contains the following SCCs:

  (no SCCs)