YES
TRS:
 {             pred(s(X)) -> X,
           minus(X, s(Y)) -> pred(minus(X, Y)),
            minus(X, 0()) -> X,
           le(s(X), s(Y)) -> le(X, Y),
            le(s(X), 0()) -> false(),
               le(0(), Y) -> true(),
          gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)),
           gcd(s(X), 0()) -> s(X),
              gcd(0(), Y) -> 0(),
  if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)),
   if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y))}
 DP:
  Strict:
   {         minus#(X, s(Y)) -> pred#(minus(X, Y)),
             minus#(X, s(Y)) -> 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#(false(), s(X), s(Y)) -> minus#(Y, X),
    if#(false(), s(X), s(Y)) -> gcd#(minus(Y, X), s(X)),
     if#(true(), s(X), s(Y)) -> minus#(X, Y),
     if#(true(), s(X), s(Y)) -> gcd#(minus(X, Y), s(Y))}
  Weak:
  {             pred(s(X)) -> X,
            minus(X, s(Y)) -> pred(minus(X, Y)),
             minus(X, 0()) -> X,
            le(s(X), s(Y)) -> le(X, Y),
             le(s(X), 0()) -> false(),
                le(0(), Y) -> true(),
           gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)),
            gcd(s(X), 0()) -> s(X),
               gcd(0(), Y) -> 0(),
   if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)),
    if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y))}
  EDG:
   {(le#(s(X), s(Y)) -> le#(X, Y), le#(s(X), s(Y)) -> le#(X, Y))
    (gcd#(s(X), s(Y)) -> le#(Y, X), le#(s(X), s(Y)) -> le#(X, Y))
    (if#(false(), s(X), s(Y)) -> gcd#(minus(Y, X), s(X)), gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y)))
    (if#(false(), s(X), s(Y)) -> gcd#(minus(Y, X), s(X)), gcd#(s(X), s(Y)) -> le#(Y, X))
    (if#(true(), s(X), s(Y)) -> gcd#(minus(X, Y), s(Y)), gcd#(s(X), s(Y)) -> le#(Y, X))
    (if#(true(), s(X), s(Y)) -> gcd#(minus(X, Y), s(Y)), gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y)))
    (gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y)), if#(false(), s(X), s(Y)) -> minus#(Y, X))
    (gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y)), if#(false(), s(X), s(Y)) -> gcd#(minus(Y, X), s(X)))
    (gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y)), if#(true(), s(X), s(Y)) -> minus#(X, Y))
    (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)) -> minus#(Y, X), minus#(X, s(Y)) -> pred#(minus(X, Y)))
    (if#(false(), s(X), s(Y)) -> minus#(Y, X), minus#(X, s(Y)) -> minus#(X, Y))
    (if#(true(), s(X), s(Y)) -> minus#(X, Y), minus#(X, s(Y)) -> pred#(minus(X, Y)))
    (if#(true(), s(X), s(Y)) -> minus#(X, Y), minus#(X, s(Y)) -> minus#(X, Y))
    (minus#(X, s(Y)) -> minus#(X, Y), minus#(X, s(Y)) -> pred#(minus(X, Y)))
    (minus#(X, s(Y)) -> minus#(X, Y), minus#(X, s(Y)) -> minus#(X, Y))}
   SCCS:
    Scc:
     {        gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y)),
      if#(false(), s(X), s(Y)) -> gcd#(minus(Y, X), s(X)),
       if#(true(), s(X), s(Y)) -> gcd#(minus(X, Y), s(Y))}
    Scc:
     {le#(s(X), s(Y)) -> le#(X, Y)}
    Scc:
     {minus#(X, s(Y)) -> minus#(X, Y)}
    SCC:
     Strict:
      {        gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y)),
       if#(false(), s(X), s(Y)) -> gcd#(minus(Y, X), s(X)),
        if#(true(), s(X), s(Y)) -> gcd#(minus(X, Y), s(Y))}
     Weak:
     {             pred(s(X)) -> X,
               minus(X, s(Y)) -> pred(minus(X, Y)),
                minus(X, 0()) -> X,
               le(s(X), s(Y)) -> le(X, Y),
                le(s(X), 0()) -> false(),
                   le(0(), Y) -> true(),
              gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)),
               gcd(s(X), 0()) -> s(X),
                  gcd(0(), Y) -> 0(),
      if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)),
       if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y))}
     POLY:
      Argument Filtering:
       pi(if#) = [1,2], pi(if) = [], pi(gcd#) = [0,1], pi(gcd) = [], pi(true) = [], pi(false) = [], pi(le) = [], pi(0) = [], pi(s) = [0], pi(minus) = 0, pi(pred) = 0
      Usable Rules:
       {}
      Interpretation:
       [if#](x0, x1) = x0 + x1,
       [gcd#](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1
      Strict:
       {gcd#(s(X), s(Y)) -> if#(le(Y, X), s(X), s(Y))}
      Weak:
       {             pred(s(X)) -> X,
                 minus(X, s(Y)) -> pred(minus(X, Y)),
                  minus(X, 0()) -> X,
                 le(s(X), s(Y)) -> le(X, Y),
                  le(s(X), 0()) -> false(),
                     le(0(), Y) -> true(),
                gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)),
                 gcd(s(X), 0()) -> s(X),
                    gcd(0(), Y) -> 0(),
        if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)),
         if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y))}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {le#(s(X), s(Y)) -> le#(X, Y)}
     Weak:
     {             pred(s(X)) -> X,
               minus(X, s(Y)) -> pred(minus(X, Y)),
                minus(X, 0()) -> X,
               le(s(X), s(Y)) -> le(X, Y),
                le(s(X), 0()) -> false(),
                   le(0(), Y) -> true(),
              gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)),
               gcd(s(X), 0()) -> s(X),
                  gcd(0(), Y) -> 0(),
      if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)),
       if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y))}
     SPSC:
      Simple Projection:
       pi(le#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {minus#(X, s(Y)) -> minus#(X, Y)}
     Weak:
     {             pred(s(X)) -> X,
               minus(X, s(Y)) -> pred(minus(X, Y)),
                minus(X, 0()) -> X,
               le(s(X), s(Y)) -> le(X, Y),
                le(s(X), 0()) -> false(),
                   le(0(), Y) -> true(),
              gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)),
               gcd(s(X), 0()) -> s(X),
                  gcd(0(), Y) -> 0(),
      if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)),
       if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y))}
     SPSC:
      Simple Projection:
       pi(minus#) = 1
      Strict:
       {}
      Qed