YES

Problem:
 div(0(),y) -> 0()
 div(x,y) -> quot(x,y,y)
 quot(0(),s(y),z) -> 0()
 quot(s(x),s(y),z) -> quot(x,y,z)
 quot(x,0(),s(z)) -> s(div(x,s(z)))

Proof:
 DP Processor:
  DPs:
   div#(x,y) -> quot#(x,y,y)
   quot#(s(x),s(y),z) -> quot#(x,y,z)
   quot#(x,0(),s(z)) -> div#(x,s(z))
  TRS:
   div(0(),y) -> 0()
   div(x,y) -> quot(x,y,y)
   quot(0(),s(y),z) -> 0()
   quot(s(x),s(y),z) -> quot(x,y,z)
   quot(x,0(),s(z)) -> s(div(x,s(z)))
  EDG Processor:
   DPs:
    div#(x,y) -> quot#(x,y,y)
    quot#(s(x),s(y),z) -> quot#(x,y,z)
    quot#(x,0(),s(z)) -> div#(x,s(z))
   TRS:
    div(0(),y) -> 0()
    div(x,y) -> quot(x,y,y)
    quot(0(),s(y),z) -> 0()
    quot(s(x),s(y),z) -> quot(x,y,z)
    quot(x,0(),s(z)) -> s(div(x,s(z)))
   graph:
    quot#(s(x),s(y),z) -> quot#(x,y,z) ->
    quot#(s(x),s(y),z) -> quot#(x,y,z)
    quot#(s(x),s(y),z) -> quot#(x,y,z) ->
    quot#(x,0(),s(z)) -> div#(x,s(z))
    quot#(x,0(),s(z)) -> div#(x,s(z)) -> div#(x,y) -> quot#(x,y,y)
    div#(x,y) -> quot#(x,y,y) -> quot#(s(x),s(y),z) -> quot#(x,y,z)
    div#(x,y) -> quot#(x,y,y) -> quot#(x,0(),s(z)) -> div#(x,s(z))
   Subterm Criterion Processor:
    simple projection:
     pi(div#) = 0
     pi(quot#) = 0
    problem:
     DPs:
      div#(x,y) -> quot#(x,y,y)
      quot#(x,0(),s(z)) -> div#(x,s(z))
     TRS:
      div(0(),y) -> 0()
      div(x,y) -> quot(x,y,y)
      quot(0(),s(y),z) -> 0()
      quot(s(x),s(y),z) -> quot(x,y,z)
      quot(x,0(),s(z)) -> s(div(x,s(z)))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [quot#](x0, x1, x2) = x1,
      
      [div#](x0, x1) = x1,
      
      [s](x0) = 0,
      
      [quot](x0, x1, x2) = 1,
      
      [div](x0, x1) = 1,
      
      [0] = 1
     orientation:
      div#(x,y) = y >= y = quot#(x,y,y)
      
      quot#(x,0(),s(z)) = 1 >= 0 = div#(x,s(z))
      
      div(0(),y) = 1 >= 1 = 0()
      
      div(x,y) = 1 >= 1 = quot(x,y,y)
      
      quot(0(),s(y),z) = 1 >= 1 = 0()
      
      quot(s(x),s(y),z) = 1 >= 1 = quot(x,y,z)
      
      quot(x,0(),s(z)) = 1 >= 0 = s(div(x,s(z)))
     problem:
      DPs:
       div#(x,y) -> quot#(x,y,y)
      TRS:
       div(0(),y) -> 0()
       div(x,y) -> quot(x,y,y)
       quot(0(),s(y),z) -> 0()
       quot(s(x),s(y),z) -> quot(x,y,z)
       quot(x,0(),s(z)) -> s(div(x,s(z)))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [quot#](x0, x1, x2) = 0,
       
       [div#](x0, x1) = 1,
       
       [s](x0) = 0,
       
       [quot](x0, x1, x2) = 0,
       
       [div](x0, x1) = 0,
       
       [0] = 0
      orientation:
       div#(x,y) = 1 >= 0 = quot#(x,y,y)
       
       div(0(),y) = 0 >= 0 = 0()
       
       div(x,y) = 0 >= 0 = quot(x,y,y)
       
       quot(0(),s(y),z) = 0 >= 0 = 0()
       
       quot(s(x),s(y),z) = 0 >= 0 = quot(x,y,z)
       
       quot(x,0(),s(z)) = 0 >= 0 = s(div(x,s(z)))
      problem:
       DPs:
        
       TRS:
        div(0(),y) -> 0()
        div(x,y) -> quot(x,y,y)
        quot(0(),s(y),z) -> 0()
        quot(s(x),s(y),z) -> quot(x,y,z)
        quot(x,0(),s(z)) -> s(div(x,s(z)))
      Qed