YES

Problem:
 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)))

Proof:
 DP Processor:
  DPs:
   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)))
  Usable Rule Processor:
   DPs:
    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
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     minus(X,0()) -> X
     minus(s(X),s(Y)) -> p(minus(X,Y))
     p(s(X)) -> X
    interpretation:
     [div#](x0, x1) = x0 + 0,
     
     [p#](x0) = 0,
     
     [minus#](x0, x1) = 1x0,
     
     [p](x0) = 1x0 + 0,
     
     [s](x0) = 2x0 + 1,
     
     [minus](x0, x1) = 1x0 + 0,
     
     [0] = 1
    orientation:
     minus#(s(X),s(Y)) = 3X + 2 >= 1X = minus#(X,Y)
     
     minus#(s(X),s(Y)) = 3X + 2 >= 0 = p#(minus(X,Y))
     
     div#(s(X),s(Y)) = 2X + 1 >= 1X = minus#(X,Y)
     
     div#(s(X),s(Y)) = 2X + 1 >= 1X + 0 = div#(minus(X,Y),s(Y))
     
     minus(X,0()) = 1X + 0 >= X = X
     
     minus(s(X),s(Y)) = 3X + 2 >= 2X + 1 = p(minus(X,Y))
     
     p(s(X)) = 3X + 2 >= X = X
    problem:
     DPs:
      
     TRS:
      minus(X,0()) -> X
      minus(s(X),s(Y)) -> p(minus(X,Y))
      p(s(X)) -> X
    Qed