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