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