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