MAYBE

Problem:
 minus(0(),Y) -> 0()
 minus(s(X),s(Y)) -> minus(X,Y)
 geq(X,0()) -> true()
 geq(0(),s(Y)) -> false()
 geq(s(X),s(Y)) -> geq(X,Y)
 div(0(),s(Y)) -> 0()
 div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
 if(true(),X,Y) -> X
 if(false(),X,Y) -> Y

Proof:
 DP Processor:
  DPs:
   minus#(s(X),s(Y)) -> minus#(X,Y)
   geq#(s(X),s(Y)) -> geq#(X,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)) -> geq#(X,Y)
   div#(s(X),s(Y)) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
  TRS:
   minus(0(),Y) -> 0()
   minus(s(X),s(Y)) -> minus(X,Y)
   geq(X,0()) -> true()
   geq(0(),s(Y)) -> false()
   geq(s(X),s(Y)) -> geq(X,Y)
   div(0(),s(Y)) -> 0()
   div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   if(true(),X,Y) -> X
   if(false(),X,Y) -> Y
  TDG Processor:
   DPs:
    minus#(s(X),s(Y)) -> minus#(X,Y)
    geq#(s(X),s(Y)) -> geq#(X,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)) -> geq#(X,Y)
    div#(s(X),s(Y)) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   TRS:
    minus(0(),Y) -> 0()
    minus(s(X),s(Y)) -> minus(X,Y)
    geq(X,0()) -> true()
    geq(0(),s(Y)) -> false()
    geq(s(X),s(Y)) -> geq(X,Y)
    div(0(),s(Y)) -> 0()
    div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    if(true(),X,Y) -> X
    if(false(),X,Y) -> Y
   graph:
    div#(s(X),s(Y)) -> div#(minus(X,Y),s(Y)) ->
    div#(s(X),s(Y)) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    div#(s(X),s(Y)) -> div#(minus(X,Y),s(Y)) ->
    div#(s(X),s(Y)) -> geq#(X,Y)
    div#(s(X),s(Y)) -> div#(minus(X,Y),s(Y)) ->
    div#(s(X),s(Y)) -> div#(minus(X,Y),s(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)) -> geq#(X,Y) -> geq#(s(X),s(Y)) -> geq#(X,Y)
    div#(s(X),s(Y)) -> minus#(X,Y) -> minus#(s(X),s(Y)) -> minus#(X,Y)
    geq#(s(X),s(Y)) -> geq#(X,Y) -> geq#(s(X),s(Y)) -> geq#(X,Y)
    minus#(s(X),s(Y)) -> minus#(X,Y) -> minus#(s(X),s(Y)) -> minus#(X,Y)
   Restore Modifier:
    DPs:
     minus#(s(X),s(Y)) -> minus#(X,Y)
     geq#(s(X),s(Y)) -> geq#(X,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)) -> geq#(X,Y)
     div#(s(X),s(Y)) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    TRS:
     minus(0(),Y) -> 0()
     minus(s(X),s(Y)) -> minus(X,Y)
     geq(X,0()) -> true()
     geq(0(),s(Y)) -> false()
     geq(s(X),s(Y)) -> geq(X,Y)
     div(0(),s(Y)) -> 0()
     div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
     if(true(),X,Y) -> X
     if(false(),X,Y) -> Y
    SCC Processor:
     #sccs: 3
     #rules: 3
     #arcs: 8/36
     DPs:
      div#(s(X),s(Y)) -> div#(minus(X,Y),s(Y))
     TRS:
      minus(0(),Y) -> 0()
      minus(s(X),s(Y)) -> minus(X,Y)
      geq(X,0()) -> true()
      geq(0(),s(Y)) -> false()
      geq(s(X),s(Y)) -> geq(X,Y)
      div(0(),s(Y)) -> 0()
      div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
      if(true(),X,Y) -> X
      if(false(),X,Y) -> Y
     Open
     
     DPs:
      geq#(s(X),s(Y)) -> geq#(X,Y)
     TRS:
      minus(0(),Y) -> 0()
      minus(s(X),s(Y)) -> minus(X,Y)
      geq(X,0()) -> true()
      geq(0(),s(Y)) -> false()
      geq(s(X),s(Y)) -> geq(X,Y)
      div(0(),s(Y)) -> 0()
      div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
      if(true(),X,Y) -> X
      if(false(),X,Y) -> Y
     Open
     
     DPs:
      minus#(s(X),s(Y)) -> minus#(X,Y)
     TRS:
      minus(0(),Y) -> 0()
      minus(s(X),s(Y)) -> minus(X,Y)
      geq(X,0()) -> true()
      geq(0(),s(Y)) -> false()
      geq(s(X),s(Y)) -> geq(X,Y)
      div(0(),s(Y)) -> 0()
      div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
      if(true(),X,Y) -> X
      if(false(),X,Y) -> Y
     Open