YES
Time: 0.007243
TRS:
 {  minus(X, 0()) -> X,
  minus(s X, s Y) -> p minus(X, Y),
            p s X -> X,
    div(0(), s Y) -> 0(),
    div(s X, s Y) -> s div(minus(X, Y), s Y)}
 DP:
  DP:
   {minus#(s X, s Y) -> minus#(X, Y),
    minus#(s X, s Y) -> p# minus(X, Y),
      div#(s X, s Y) -> minus#(X, Y),
      div#(s X, s Y) -> div#(minus(X, Y), s Y)}
  TRS:
  {  minus(X, 0()) -> X,
   minus(s X, s Y) -> p minus(X, Y),
             p s X -> X,
     div(0(), s Y) -> 0(),
     div(s X, s Y) -> s div(minus(X, Y), s Y)}
  EDG:
   {(minus#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> p# minus(X, Y))
    (minus#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
    (div#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
    (div#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> p# minus(X, Y))
    (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> minus#(X, Y))
    (div#(s X, s Y) -> div#(minus(X, Y), s Y), div#(s X, s Y) -> div#(minus(X, Y), s Y))}
   SCCS (2):
    Scc:
     {div#(s X, s Y) -> div#(minus(X, Y), s Y)}
    Scc:
     {minus#(s X, s Y) -> minus#(X, Y)}
    SCC (1):
     Strict:
      {div#(s X, s Y) -> div#(minus(X, Y), s Y)}
     Weak:
     {  minus(X, 0()) -> X,
      minus(s X, s Y) -> p minus(X, Y),
                p s X -> X,
        div(0(), s Y) -> 0(),
        div(s X, s Y) -> s div(minus(X, Y), s Y)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [minus](x0, x1) = x0,
       
       [div](x0, x1) = x0 + x1,
       
       [p](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [0] = 0,
       
       [div#](x0, x1) = x0 + 1
      Strict:
       div#(s X, s Y) -> div#(minus(X, Y), s Y)
       2 + 1X + 0Y >= 1 + 1X + 0Y
      Weak:
       
     Qed
   SCC (1):
    Strict:
     {minus#(s X, s Y) -> minus#(X, Y)}
    Weak:
    {  minus(X, 0()) -> X,
     minus(s X, s Y) -> p minus(X, Y),
               p s X -> X,
       div(0(), s Y) -> 0(),
       div(s X, s Y) -> s div(minus(X, Y), s Y)}
    SPSC:
     Simple Projection:
      pi(minus#) = 1
     Strict:
      {}
     Qed