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)),
                  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#(x, s(y)) -> pred#(minus(x, y)),
                minus#(x, s(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),
                    pred(s(x)) -> x,
                 minus(x, 0()) -> x,
                minus(x, s(y)) -> pred(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#(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_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)) -> minus#(x, 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), le#(s(x), s(y)) -> le#(x, y))
    (if_mod#(true(), s(x), s(y)) -> minus#(x, y), minus#(x, s(y)) -> pred#(minus(x, y)))
    (if_mod#(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))}
   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#(x, s(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),
                       pred(s(x)) -> x,
                    minus(x, 0()) -> x,
                   minus(x, s(y)) -> pred(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(minus) = 0, pi(pred) = 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),
                         pred(s(x)) -> x,
                      minus(x, 0()) -> x,
                     minus(x, s(y)) -> pred(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#(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)),
                      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(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)),
                      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