YES

Problem:
 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))

Proof:
 DP Processor:
  DPs:
   minus#(X,s(Y)) -> minus#(X,Y)
   minus#(X,s(Y)) -> pred#(minus(X,Y))
   le#(s(X),s(Y)) -> le#(X,Y)
   gcd#(s(X),s(Y)) -> le#(Y,X)
   gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y))
   if#(true(),s(X),s(Y)) -> minus#(X,Y)
   if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y))
   if#(false(),s(X),s(Y)) -> minus#(Y,X)
   if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X))
  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))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [if#](x0, x1, x2) = 2x1 + 2x2 + 1,
    
    [gcd#](x0, x1) = 4x0 + 2x1 + 4,
    
    [le#](x0, x1) = x1 + 4,
    
    [pred#](x0) = 6,
    
    [minus#](x0, x1) = 4x1 + 1,
    
    [if](x0, x1, x2) = x0 + 3x1 + 2x2 + 7,
    
    [gcd](x0, x1) = 4x0 + 2x1 + 6,
    
    [true] = 1,
    
    [false] = 2,
    
    [le](x0, x1) = x1 + 1,
    
    [0] = 6,
    
    [pred](x0) = x0,
    
    [minus](x0, x1) = x0,
    
    [s](x0) = 2x0 + 2
   orientation:
    minus#(X,s(Y)) = 8Y + 9 >= 4Y + 1 = minus#(X,Y)
    
    minus#(X,s(Y)) = 8Y + 9 >= 6 = pred#(minus(X,Y))
    
    le#(s(X),s(Y)) = 2Y + 6 >= Y + 4 = le#(X,Y)
    
    gcd#(s(X),s(Y)) = 8X + 4Y + 16 >= X + 4 = le#(Y,X)
    
    gcd#(s(X),s(Y)) = 8X + 4Y + 16 >= 4X + 4Y + 9 = if#(le(Y,X),s(X),s(Y))
    
    if#(true(),s(X),s(Y)) = 4X + 4Y + 9 >= 4Y + 1 = minus#(X,Y)
    
    if#(true(),s(X),s(Y)) = 4X + 4Y + 9 >= 4X + 4Y + 8 = gcd#(minus(X,Y),s(Y))
    
    if#(false(),s(X),s(Y)) = 4X + 4Y + 9 >= 4X + 1 = minus#(Y,X)
    
    if#(false(),s(X),s(Y)) = 4X + 4Y + 9 >= 4X + 4Y + 8 = gcd#(minus(Y,X),s(X))
    
    minus(X,s(Y)) = X >= X = pred(minus(X,Y))
    
    minus(X,0()) = X >= X = X
    
    pred(s(X)) = 2X + 2 >= X = X
    
    le(s(X),s(Y)) = 2Y + 3 >= Y + 1 = le(X,Y)
    
    le(s(X),0()) = 7 >= 2 = false()
    
    le(0(),Y) = Y + 1 >= 1 = true()
    
    gcd(0(),Y) = 2Y + 30 >= 6 = 0()
    
    gcd(s(X),0()) = 8X + 26 >= 2X + 2 = s(X)
    
    gcd(s(X),s(Y)) = 8X + 4Y + 18 >= 7X + 4Y + 18 = if(le(Y,X),s(X),s(Y))
    
    if(true(),s(X),s(Y)) = 6X + 4Y + 18 >= 4X + 4Y + 10 = gcd(minus(X,Y),s(Y))
    
    if(false(),s(X),s(Y)) = 6X + 4Y + 19 >= 4X + 4Y + 10 = gcd(minus(Y,X),s(X))
   problem:
    DPs:
     
    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))
   Qed