MAYBE

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)))
  Usable Rule 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:
    f6(x,y) -> x
    f6(x,y) -> y
   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:
     f6(x,y) -> x
     f6(x,y) -> y
    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))
    Restore Modifier:
     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)))
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 5/9
      DPs:
       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)
      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)))
      Open