YES

TRS:

  minus(X,s(Y)) -> pred(minus(X,Y))
  minus(X,0()) -> X
  pred(s(X)) -> X
  le(s(X),s(Y)) -> le(X,Y)
  le(s(X),0()) -> false()
  le(0(),Y) -> true()
  gcd(0(),Y) -> 0()
  gcd(s(X),0()) -> s(X)
  gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
  if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
  if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X))

linear polynomial interpretations on N:

  minus_A(x1,x2) = x1 + 1
  minus#_A(x1,x2) = x1 + x2
  s_A(x1) = x1 + 3
  s#_A(x1) = 6
  pred_A(x1) = x1
  pred#_A(x1) = 0
  0_A = 0
  0#_A = 3
  le_A(x1,x2) = x2 + 1
  le#_A(x1,x2) = 1
  false_A = 1
  false#_A = 2
  true_A = 1
  true#_A = 0
  gcd_A(x1,x2) = x1 + x2
  gcd#_A(x1,x2) = x1 + x2 + 4
  if_A(x1,x2,x3) = x2 + x3
  if#_A(x1,x2,x3) = x2 + x3 + 3

precedence:

  gcd > minus = pred = 0 = if > s > false > le > true