MAYBE

Problem:
 a__minus(0(),Y) -> 0()
 a__minus(s(X),s(Y)) -> a__minus(X,Y)
 a__geq(X,0()) -> true()
 a__geq(0(),s(Y)) -> false()
 a__geq(s(X),s(Y)) -> a__geq(X,Y)
 a__div(0(),s(Y)) -> 0()
 a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
 a__if(true(),X,Y) -> mark(X)
 a__if(false(),X,Y) -> mark(Y)
 mark(minus(X1,X2)) -> a__minus(X1,X2)
 mark(geq(X1,X2)) -> a__geq(X1,X2)
 mark(div(X1,X2)) -> a__div(mark(X1),X2)
 mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
 mark(0()) -> 0()
 mark(s(X)) -> s(mark(X))
 mark(true()) -> true()
 mark(false()) -> false()
 a__minus(X1,X2) -> minus(X1,X2)
 a__geq(X1,X2) -> geq(X1,X2)
 a__div(X1,X2) -> div(X1,X2)
 a__if(X1,X2,X3) -> if(X1,X2,X3)

Proof:
 DP Processor:
  DPs:
   a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
   a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
   a__div#(s(X),s(Y)) -> a__geq#(X,Y)
   a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   a__if#(true(),X,Y) -> mark#(X)
   a__if#(false(),X,Y) -> mark#(Y)
   mark#(minus(X1,X2)) -> a__minus#(X1,X2)
   mark#(geq(X1,X2)) -> a__geq#(X1,X2)
   mark#(div(X1,X2)) -> mark#(X1)
   mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
   mark#(if(X1,X2,X3)) -> mark#(X1)
   mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
   mark#(s(X)) -> mark#(X)
  TRS:
   a__minus(0(),Y) -> 0()
   a__minus(s(X),s(Y)) -> a__minus(X,Y)
   a__geq(X,0()) -> true()
   a__geq(0(),s(Y)) -> false()
   a__geq(s(X),s(Y)) -> a__geq(X,Y)
   a__div(0(),s(Y)) -> 0()
   a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   a__if(true(),X,Y) -> mark(X)
   a__if(false(),X,Y) -> mark(Y)
   mark(minus(X1,X2)) -> a__minus(X1,X2)
   mark(geq(X1,X2)) -> a__geq(X1,X2)
   mark(div(X1,X2)) -> a__div(mark(X1),X2)
   mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
   mark(0()) -> 0()
   mark(s(X)) -> s(mark(X))
   mark(true()) -> true()
   mark(false()) -> false()
   a__minus(X1,X2) -> minus(X1,X2)
   a__geq(X1,X2) -> geq(X1,X2)
   a__div(X1,X2) -> div(X1,X2)
   a__if(X1,X2,X3) -> if(X1,X2,X3)
  EDG Processor:
   DPs:
    a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    a__div#(s(X),s(Y)) -> a__geq#(X,Y)
    a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    a__if#(true(),X,Y) -> mark#(X)
    a__if#(false(),X,Y) -> mark#(Y)
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    mark#(div(X1,X2)) -> mark#(X1)
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    mark#(s(X)) -> mark#(X)
   TRS:
    a__minus(0(),Y) -> 0()
    a__minus(s(X),s(Y)) -> a__minus(X,Y)
    a__geq(X,0()) -> true()
    a__geq(0(),s(Y)) -> false()
    a__geq(s(X),s(Y)) -> a__geq(X,Y)
    a__div(0(),s(Y)) -> 0()
    a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    a__if(true(),X,Y) -> mark(X)
    a__if(false(),X,Y) -> mark(Y)
    mark(minus(X1,X2)) -> a__minus(X1,X2)
    mark(geq(X1,X2)) -> a__geq(X1,X2)
    mark(div(X1,X2)) -> a__div(mark(X1),X2)
    mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
    mark(0()) -> 0()
    mark(s(X)) -> s(mark(X))
    mark(true()) -> true()
    mark(false()) -> false()
    a__minus(X1,X2) -> minus(X1,X2)
    a__geq(X1,X2) -> geq(X1,X2)
    a__div(X1,X2) -> div(X1,X2)
    a__if(X1,X2,X3) -> if(X1,X2,X3)
   graph:
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(s(X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) ->
    a__if#(true(),X,Y) -> mark#(X)
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) ->
    a__if#(false(),X,Y) -> mark#(Y)
    mark#(geq(X1,X2)) -> a__geq#(X1,X2) ->
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    mark#(div(X1,X2)) -> mark#(X1) -> mark#(div(X1,X2)) -> mark#(X1)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> mark#(X)
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2) ->
    a__div#(s(X),s(Y)) -> a__geq#(X,Y)
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2) ->
    a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    mark#(minus(X1,X2)) -> a__minus#(X1,X2) ->
    a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
    mark#(s(X)) -> mark#(X) -> mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    mark#(s(X)) -> mark#(X) -> mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(div(X1,X2)) -> mark#(X1)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    a__if#(false(),X,Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    a__if#(true(),X,Y) -> mark#(X) -> mark#(div(X1,X2)) -> mark#(X1)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    a__if#(true(),X,Y) -> mark#(X)
    a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    a__if#(false(),X,Y) -> mark#(Y)
    a__div#(s(X),s(Y)) -> a__geq#(X,Y) ->
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y) ->
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    a__minus#(s(X),s(Y)) -> a__minus#(X,Y) -> a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
   SCC Processor:
    #sccs: 3
    #rules: 10
    #arcs: 46/169
    DPs:
     mark#(if(X1,X2,X3)) -> mark#(X1)
     mark#(s(X)) -> mark#(X)
     mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
     a__if#(false(),X,Y) -> mark#(Y)
     mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
     a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
     a__if#(true(),X,Y) -> mark#(X)
     mark#(div(X1,X2)) -> mark#(X1)
    TRS:
     a__minus(0(),Y) -> 0()
     a__minus(s(X),s(Y)) -> a__minus(X,Y)
     a__geq(X,0()) -> true()
     a__geq(0(),s(Y)) -> false()
     a__geq(s(X),s(Y)) -> a__geq(X,Y)
     a__div(0(),s(Y)) -> 0()
     a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
     a__if(true(),X,Y) -> mark(X)
     a__if(false(),X,Y) -> mark(Y)
     mark(minus(X1,X2)) -> a__minus(X1,X2)
     mark(geq(X1,X2)) -> a__geq(X1,X2)
     mark(div(X1,X2)) -> a__div(mark(X1),X2)
     mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
     mark(0()) -> 0()
     mark(s(X)) -> s(mark(X))
     mark(true()) -> true()
     mark(false()) -> false()
     a__minus(X1,X2) -> minus(X1,X2)
     a__geq(X1,X2) -> geq(X1,X2)
     a__div(X1,X2) -> div(X1,X2)
     a__if(X1,X2,X3) -> if(X1,X2,X3)
    Open
    
    DPs:
     a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
    TRS:
     a__minus(0(),Y) -> 0()
     a__minus(s(X),s(Y)) -> a__minus(X,Y)
     a__geq(X,0()) -> true()
     a__geq(0(),s(Y)) -> false()
     a__geq(s(X),s(Y)) -> a__geq(X,Y)
     a__div(0(),s(Y)) -> 0()
     a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
     a__if(true(),X,Y) -> mark(X)
     a__if(false(),X,Y) -> mark(Y)
     mark(minus(X1,X2)) -> a__minus(X1,X2)
     mark(geq(X1,X2)) -> a__geq(X1,X2)
     mark(div(X1,X2)) -> a__div(mark(X1),X2)
     mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
     mark(0()) -> 0()
     mark(s(X)) -> s(mark(X))
     mark(true()) -> true()
     mark(false()) -> false()
     a__minus(X1,X2) -> minus(X1,X2)
     a__geq(X1,X2) -> geq(X1,X2)
     a__div(X1,X2) -> div(X1,X2)
     a__if(X1,X2,X3) -> if(X1,X2,X3)
    Open
    
    DPs:
     a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    TRS:
     a__minus(0(),Y) -> 0()
     a__minus(s(X),s(Y)) -> a__minus(X,Y)
     a__geq(X,0()) -> true()
     a__geq(0(),s(Y)) -> false()
     a__geq(s(X),s(Y)) -> a__geq(X,Y)
     a__div(0(),s(Y)) -> 0()
     a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
     a__if(true(),X,Y) -> mark(X)
     a__if(false(),X,Y) -> mark(Y)
     mark(minus(X1,X2)) -> a__minus(X1,X2)
     mark(geq(X1,X2)) -> a__geq(X1,X2)
     mark(div(X1,X2)) -> a__div(mark(X1),X2)
     mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
     mark(0()) -> 0()
     mark(s(X)) -> s(mark(X))
     mark(true()) -> true()
     mark(false()) -> false()
     a__minus(X1,X2) -> minus(X1,X2)
     a__geq(X1,X2) -> geq(X1,X2)
     a__div(X1,X2) -> div(X1,X2)
     a__if(X1,X2,X3) -> if(X1,X2,X3)
    Open