YES
Time: 0.011562
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)}
  UR:
   {  minus(X, 0()) -> X,
    minus(s X, s Y) -> p minus(X, Y),
              p s X -> X,
            a(x, y) -> x,
            a(x, y) -> 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))}
    STATUS:
     arrows: 0.625000
     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:
         div(s X, s Y) -> s div(minus(X, Y), s Y)
         2 + 1X + 1Y >= 2 + 1X + 1Y
         div(0(), s Y) -> 0()
         1 + 1Y >= 0
         p s X -> X
         2 + 1X >= 1X
         minus(s X, s Y) -> p minus(X, Y)
         1 + 1X + 0Y >= 1 + 1X + 0Y
         minus(X, 0()) -> X
         0 + 1X >= 1X
       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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [minus](x0, x1) = x0 + 1,
        
        [div](x0, x1) = x0 + x1 + 1,
        
        [p](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 0,
        
        [minus#](x0, x1) = x0
       Strict:
        minus#(s X, s Y) -> minus#(X, Y)
        1 + 0X + 1Y >= 0 + 0X + 1Y
       Weak:
        div(s X, s Y) -> s div(minus(X, Y), s Y)
        3 + 1X + 1Y >= 4 + 1X + 1Y
        div(0(), s Y) -> 0()
        2 + 1Y >= 0
        p s X -> X
        2 + 1X >= 1X
        minus(s X, s Y) -> p minus(X, Y)
        2 + 1X + 0Y >= 2 + 1X + 0Y
        minus(X, 0()) -> X
        1 + 1X >= 1X
      Qed