MAYBE

Problem:
 active(minus(0(),Y)) -> mark(0())
 active(minus(s(X),s(Y))) -> mark(minus(X,Y))
 active(geq(X,0())) -> mark(true())
 active(geq(0(),s(Y))) -> mark(false())
 active(geq(s(X),s(Y))) -> mark(geq(X,Y))
 active(div(0(),s(Y))) -> mark(0())
 active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 active(s(X)) -> s(active(X))
 active(div(X1,X2)) -> div(active(X1),X2)
 active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
 s(mark(X)) -> mark(s(X))
 div(mark(X1),X2) -> mark(div(X1,X2))
 if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
 proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(s(X)) -> s(proper(X))
 proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
 proper(true()) -> ok(true())
 proper(false()) -> ok(false())
 proper(div(X1,X2)) -> div(proper(X1),proper(X2))
 proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
 minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
 s(ok(X)) -> ok(s(X))
 geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
 div(ok(X1),ok(X2)) -> ok(div(X1,X2))
 if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(minus(s(X),s(Y))) -> minus#(X,Y)
   active#(geq(s(X),s(Y))) -> geq#(X,Y)
   active#(div(s(X),s(Y))) -> minus#(X,Y)
   active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
   active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
   active#(div(s(X),s(Y))) -> geq#(X,Y)
   active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   active#(s(X)) -> active#(X)
   active#(s(X)) -> s#(active(X))
   active#(div(X1,X2)) -> active#(X1)
   active#(div(X1,X2)) -> div#(active(X1),X2)
   active#(if(X1,X2,X3)) -> active#(X1)
   active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
   s#(mark(X)) -> s#(X)
   div#(mark(X1),X2) -> div#(X1,X2)
   if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
   proper#(minus(X1,X2)) -> proper#(X2)
   proper#(minus(X1,X2)) -> proper#(X1)
   proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
   proper#(s(X)) -> proper#(X)
   proper#(s(X)) -> s#(proper(X))
   proper#(geq(X1,X2)) -> proper#(X2)
   proper#(geq(X1,X2)) -> proper#(X1)
   proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
   proper#(div(X1,X2)) -> proper#(X2)
   proper#(div(X1,X2)) -> proper#(X1)
   proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
   proper#(if(X1,X2,X3)) -> proper#(X3)
   proper#(if(X1,X2,X3)) -> proper#(X2)
   proper#(if(X1,X2,X3)) -> proper#(X1)
   proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
   minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
   s#(ok(X)) -> s#(X)
   geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
   div#(ok(X1),ok(X2)) -> div#(X1,X2)
   if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
   top#(mark(X)) -> proper#(X)
   top#(mark(X)) -> top#(proper(X))
   top#(ok(X)) -> active#(X)
   top#(ok(X)) -> top#(active(X))
  TRS:
   active(minus(0(),Y)) -> mark(0())
   active(minus(s(X),s(Y))) -> mark(minus(X,Y))
   active(geq(X,0())) -> mark(true())
   active(geq(0(),s(Y))) -> mark(false())
   active(geq(s(X),s(Y))) -> mark(geq(X,Y))
   active(div(0(),s(Y))) -> mark(0())
   active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
   active(if(true(),X,Y)) -> mark(X)
   active(if(false(),X,Y)) -> mark(Y)
   active(s(X)) -> s(active(X))
   active(div(X1,X2)) -> div(active(X1),X2)
   active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
   s(mark(X)) -> mark(s(X))
   div(mark(X1),X2) -> mark(div(X1,X2))
   if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
   proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
   proper(0()) -> ok(0())
   proper(s(X)) -> s(proper(X))
   proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
   proper(true()) -> ok(true())
   proper(false()) -> ok(false())
   proper(div(X1,X2)) -> div(proper(X1),proper(X2))
   proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
   minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
   s(ok(X)) -> ok(s(X))
   geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
   div(ok(X1),ok(X2)) -> ok(div(X1,X2))
   if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  EDG Processor:
   DPs:
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    active#(div(s(X),s(Y))) -> geq#(X,Y)
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    active#(s(X)) -> active#(X)
    active#(s(X)) -> s#(active(X))
    active#(div(X1,X2)) -> active#(X1)
    active#(div(X1,X2)) -> div#(active(X1),X2)
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    s#(mark(X)) -> s#(X)
    div#(mark(X1),X2) -> div#(X1,X2)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> s#(proper(X))
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
    s#(ok(X)) -> s#(X)
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    div#(ok(X1),ok(X2)) -> div#(X1,X2)
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
   TRS:
    active(minus(0(),Y)) -> mark(0())
    active(minus(s(X),s(Y))) -> mark(minus(X,Y))
    active(geq(X,0())) -> mark(true())
    active(geq(0(),s(Y))) -> mark(false())
    active(geq(s(X),s(Y))) -> mark(geq(X,Y))
    active(div(0(),s(Y))) -> mark(0())
    active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
    active(if(true(),X,Y)) -> mark(X)
    active(if(false(),X,Y)) -> mark(Y)
    active(s(X)) -> s(active(X))
    active(div(X1,X2)) -> div(active(X1),X2)
    active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
    s(mark(X)) -> mark(s(X))
    div(mark(X1),X2) -> mark(div(X1,X2))
    if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
    proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
    proper(0()) -> ok(0())
    proper(s(X)) -> s(proper(X))
    proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
    proper(true()) -> ok(true())
    proper(false()) -> ok(false())
    proper(div(X1,X2)) -> div(proper(X1),proper(X2))
    proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
    minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
    s(ok(X)) -> ok(s(X))
    geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
    div(ok(X1),ok(X2)) -> ok(div(X1,X2))
    if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X))
   graph:
    top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
    top#(ok(X)) -> top#(active(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
    top#(ok(X)) -> active#(X) -> active#(minus(s(X),s(Y))) -> minus#(X,Y)
    top#(ok(X)) -> active#(X) -> active#(geq(s(X),s(Y))) -> geq#(X,Y)
    top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> minus#(X,Y)
    top#(ok(X)) -> active#(X) ->
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    top#(ok(X)) -> active#(X) ->
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> geq#(X,Y)
    top#(ok(X)) -> active#(X) ->
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    top#(ok(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(div(X1,X2)) -> div#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
    top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X))
    top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3)
    top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(s(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) ->
    div#(ok(X1),ok(X2)) -> div#(X1,X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) ->
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
    proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) ->
    minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) ->
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3) ->
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    div#(ok(X1),ok(X2)) -> div#(X1,X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    div#(ok(X1),ok(X2)) -> div#(X1,X2) ->
    div#(ok(X1),ok(X2)) -> div#(X1,X2)
    div#(mark(X1),X2) -> div#(X1,X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    div#(mark(X1),X2) -> div#(X1,X2) ->
    div#(ok(X1),ok(X2)) -> div#(X1,X2)
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2) ->
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    minus#(ok(X1),ok(X2)) -> minus#(X1,X2) ->
    minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) ->
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> geq#(X,Y)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(div(X1,X2)) -> active#(X1)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(div(X1,X2)) -> div#(active(X1),X2)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) ->
    s#(mark(X)) -> s#(X)
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) ->
    s#(ok(X)) -> s#(X)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) ->
    div#(ok(X1),ok(X2)) -> div#(X1,X2)
    active#(div(s(X),s(Y))) -> geq#(X,Y) ->
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    active#(div(s(X),s(Y))) -> minus#(X,Y) ->
    minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
    active#(div(X1,X2)) -> div#(active(X1),X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    active#(div(X1,X2)) -> div#(active(X1),X2) ->
    div#(ok(X1),ok(X2)) -> div#(X1,X2)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(geq(s(X),s(Y))) -> geq#(X,Y)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> geq#(X,Y)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    active#(div(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(X1,X2)) -> active#(X1)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(X1,X2)) -> div#(active(X1),X2)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(geq(s(X),s(Y))) -> geq#(X,Y) ->
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
    active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
    active#(s(X)) -> active#(X) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(s(X)) -> active#(X) -> active#(geq(s(X),s(Y))) -> geq#(X,Y)
    active#(s(X)) -> active#(X) ->
    active#(div(s(X),s(Y))) -> minus#(X,Y)
    active#(s(X)) -> active#(X) ->
    active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
    active#(s(X)) -> active#(X) ->
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
    active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> geq#(X,Y)
    active#(s(X)) -> active#(X) ->
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(s(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(div(X1,X2)) -> div#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(minus(s(X),s(Y))) -> minus#(X,Y) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
   SCC Processor:
    #sccs: 8
    #rules: 23
    #arcs: 262/1600
    DPs:
     top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> top#(proper(X))
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     proper#(if(X1,X2,X3)) -> proper#(X1)
     proper#(if(X1,X2,X3)) -> proper#(X2)
     proper#(if(X1,X2,X3)) -> proper#(X3)
     proper#(div(X1,X2)) -> proper#(X1)
     proper#(div(X1,X2)) -> proper#(X2)
     proper#(geq(X1,X2)) -> proper#(X1)
     proper#(geq(X1,X2)) -> proper#(X2)
     proper#(s(X)) -> proper#(X)
     proper#(minus(X1,X2)) -> proper#(X1)
     proper#(minus(X1,X2)) -> proper#(X2)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     active#(if(X1,X2,X3)) -> active#(X1)
     active#(div(X1,X2)) -> active#(X1)
     active#(s(X)) -> active#(X)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     s#(ok(X)) -> s#(X)
     s#(mark(X)) -> s#(X)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     div#(ok(X1),ok(X2)) -> div#(X1,X2)
     div#(mark(X1),X2) -> div#(X1,X2)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
     if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    TRS:
     active(minus(0(),Y)) -> mark(0())
     active(minus(s(X),s(Y))) -> mark(minus(X,Y))
     active(geq(X,0())) -> mark(true())
     active(geq(0(),s(Y))) -> mark(false())
     active(geq(s(X),s(Y))) -> mark(geq(X,Y))
     active(div(0(),s(Y))) -> mark(0())
     active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(s(X)) -> s(active(X))
     active(div(X1,X2)) -> div(active(X1),X2)
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     s(mark(X)) -> mark(s(X))
     div(mark(X1),X2) -> mark(div(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(div(X1,X2)) -> div(proper(X1),proper(X2))
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
     s(ok(X)) -> ok(s(X))
     geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
     div(ok(X1),ok(X2)) -> ok(div(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open