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)))
  TDG 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#(x,0(),s(z)) -> div#(x,s(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)) -> div#(x,y) -> quot#(x,y,y)
    div#(x,y) -> quot#(x,y,y) -> quot#(x,0(),s(z)) -> div#(x,s(z))
    div#(x,y) -> quot#(x,y,y) -> quot#(s(x),s(y),z) -> quot#(x,y,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)))
    EDG Processor:
     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)))
     graph:
      quot#(x,0(),s(z)) -> div#(x,s(z)) -> div#(x,y) -> quot#(x,y,y)
      div#(x,y) -> quot#(x,y,y) -> quot#(x,0(),s(z)) -> div#(x,s(z))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [quot#](x0, x1, x2) = x1 + x2 + 0,
       
       [div#](x0, x1) = 2x1 + 1,
       
       [s](x0) = 1,
       
       [quot](x0, x1, x2) = 6x2 + 3,
       
       [div](x0, x1) = x0 + 6x1 + 3,
       
       [0] = 3
      orientation:
       div#(x,y) = 2y + 1 >= y + 0 = quot#(x,y,y)
       
       quot#(x,0(),s(z)) = 3 >= 3 = div#(x,s(z))
       
       div(0(),y) = 6y + 3 >= 3 = 0()
       
       div(x,y) = x + 6y + 3 >= 6y + 3 = quot(x,y,y)
       
       quot(0(),s(y),z) = 6z + 3 >= 3 = 0()
       
       quot(s(x),s(y),z) = 6z + 3 >= 6z + 3 = quot(x,y,z)
       
       quot(x,0(),s(z)) = 7 >= 1 = s(div(x,s(z)))
      problem:
       DPs:
        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)))
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 2/1