YES
Time: 0.011157
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:
  DP:
   {            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)}
  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)}
  EDG:
   {(ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y))
    (ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y))
    (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y))
    (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> minus#(X, Y))
    (minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y))
    (minus#(s X, Y) -> le#(s X, Y), le#(s X, s Y) -> le#(X, Y))
    (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y))
    (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y))
    (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))}
   SCCS (3):
    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 (1):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [ifMinus](x0, x1, x2) = x0,
       
       [le](x0, x1) = 0,
       
       [minus](x0, x1) = x0,
       
       [quot](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [true] = 0,
       
       [0] = 0,
       
       [false] = 0,
       
       [quot#](x0, x1) = x0 + 1
      Strict:
       quot#(s X, s Y) -> quot#(minus(X, Y), s Y)
       2 + 0Y + 1X >= 1 + 0Y + 1X
      Weak:
       
     Qed
   SCC (2):
    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 (0):
       
       Qed
   SCC (1):
    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#) = 1
     Strict:
      {}
     Qed