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))
  TDG 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#(ok(X)) -> top#(active(X))
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
    top#(ok(X)) -> active#(X) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(div(X1,X2)) -> div#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(Y))
    top#(ok(X)) -> active#(X) -> active#(div(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#(minus(s(X),s(Y))) -> minus#(X,Y)
    top#(mark(X)) -> top#(proper(X)) ->
    top#(ok(X)) -> top#(active(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
    top#(mark(X)) -> top#(proper(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3)
    top#(mark(X)) -> proper#(X) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    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#(X3) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(div(X1,X2)) -> div#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(s(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),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)) -> proper#(X2)
    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#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),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)) -> proper#(X2)
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(div(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) ->
    div#(ok(X1),ok(X2)) -> div#(X1,X2)
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(geq(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) ->
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(s(X)) -> proper#(X) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
    proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X2) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    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#(X3)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(div(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(geq(X1,X2)) -> proper#(X2)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X1)
    proper#(minus(X1,X2)) -> proper#(X1) ->
    proper#(minus(X1,X2)) -> proper#(X2)
    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#(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#(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)
    s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    div#(ok(X1),ok(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#(ok(X1),ok(X2)) -> div#(X1,X2)
    div#(mark(X1),X2) -> div#(X1,X2) ->
    div#(mark(X1),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#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> 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#(div(X1,X2)) -> active#(X1)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(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#(geq(s(X),s(Y))) -> geq#(X,Y)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    if#(ok(X1),ok(X2),ok(X3)) -> if#(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#(ok(X)) -> s#(X)
    active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) ->
    s#(mark(X)) -> s#(X)
    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))) -> div#(minus(X,Y),s(Y)) ->
    div#(mark(X1),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#(ok(X1),ok(X2)) -> div#(X1,X2)
    active#(div(X1,X2)) -> div#(active(X1),X2) ->
    div#(mark(X1),X2) -> div#(X1,X2)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(X1,X2)) -> div#(active(X1),X2)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(X1,X2)) -> active#(X1)
    active#(div(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(div(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(Y))
    active#(div(X1,X2)) -> active#(X1) ->
    active#(div(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#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(geq(s(X),s(Y))) -> geq#(X,Y) ->
    geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
    active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
    active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
    active#(s(X)) -> active#(X) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(div(X1,X2)) -> div#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(Y))
    active#(s(X)) -> active#(X) ->
    active#(div(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#(minus(s(X),s(Y))) -> minus#(X,Y)
    active#(minus(s(X),s(Y))) -> minus#(X,Y) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
   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)
    CDG 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#(ok(X)) -> top#(active(X))
      top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
      top#(ok(X)) -> top#(active(X)) ->
      top#(mark(X)) -> top#(proper(X))
      top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
      top#(ok(X)) -> active#(X) ->
      active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
      top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
      top#(ok(X)) -> active#(X) ->
      active#(div(X1,X2)) -> div#(active(X1),X2)
      top#(ok(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1)
      top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
      top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
      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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(Y))
      top#(ok(X)) -> active#(X) -> active#(div(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#(minus(s(X),s(Y))) -> minus#(X,Y)
      top#(mark(X)) -> top#(proper(X)) ->
      top#(ok(X)) -> top#(active(X))
      top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
      top#(mark(X)) -> top#(proper(X)) ->
      top#(mark(X)) -> top#(proper(X))
      top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
      top#(mark(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      top#(mark(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      top#(mark(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> proper#(X2)
      top#(mark(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> proper#(X3)
      top#(mark(X)) -> proper#(X) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1)
      top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2)
      top#(mark(X)) -> proper#(X) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1)
      top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2)
      top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
      top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
      top#(mark(X)) -> proper#(X) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      top#(mark(X)) -> proper#(X) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      top#(mark(X)) -> proper#(X) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      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#(X3) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(if(X1,X2,X3)) -> proper#(X3) ->
      proper#(div(X1,X2)) -> div#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X3) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X3) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(if(X1,X2,X3)) -> proper#(X3) ->
      proper#(s(X)) -> proper#(X)
      proper#(if(X1,X2,X3)) -> proper#(X3) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),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)) -> proper#(X2)
      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#(X2) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(if(X1,X2,X3)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> div#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X2) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(if(X1,X2,X3)) -> proper#(X2) ->
      proper#(s(X)) -> proper#(X)
      proper#(if(X1,X2,X3)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> proper#(X3)
      proper#(if(X1,X2,X3)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> div#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> proper#(X1) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(if(X1,X2,X3)) -> proper#(X1) ->
      proper#(s(X)) -> proper#(X)
      proper#(if(X1,X2,X3)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),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)) -> proper#(X2)
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
      if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) ->
      if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> proper#(X1)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> proper#(X2)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> proper#(X1)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> proper#(X2)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(s(X)) -> proper#(X)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      proper#(div(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> proper#(X1)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> proper#(X2)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> proper#(X1)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> proper#(X2)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(s(X)) -> proper#(X)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      proper#(div(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) ->
      div#(ok(X1),ok(X2)) -> div#(X1,X2)
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) ->
      div#(mark(X1),X2) -> div#(X1,X2)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> proper#(X1)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> proper#(X2)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> proper#(X1)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> proper#(X2)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(s(X)) -> proper#(X)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      proper#(geq(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> proper#(X1)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> proper#(X2)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> proper#(X1)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> proper#(X2)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(s(X)) -> proper#(X)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      proper#(geq(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) ->
      geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
      proper#(s(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      proper#(s(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      proper#(s(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> proper#(X2)
      proper#(s(X)) -> proper#(X) ->
      proper#(if(X1,X2,X3)) -> proper#(X3)
      proper#(s(X)) -> proper#(X) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1)
      proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2)
      proper#(s(X)) -> proper#(X) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1)
      proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2)
      proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
      proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
      proper#(s(X)) -> proper#(X) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      proper#(s(X)) -> proper#(X) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      proper#(s(X)) -> proper#(X) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
      proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> proper#(X1)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(div(X1,X2)) -> proper#(X2)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> proper#(X1)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(geq(X1,X2)) -> proper#(X2)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(s(X)) -> proper#(X)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      proper#(minus(X1,X2)) -> proper#(X2) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(X3)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> div#(proper(X1),proper(X2))
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> proper#(X1)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(div(X1,X2)) -> proper#(X2)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2))
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> proper#(X1)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(geq(X1,X2)) -> proper#(X2)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(s(X)) -> s#(proper(X))
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(s(X)) -> proper#(X)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2))
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> proper#(X1)
      proper#(minus(X1,X2)) -> proper#(X1) ->
      proper#(minus(X1,X2)) -> proper#(X2)
      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#(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#(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)
      s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
      s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
      s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
      s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
      div#(ok(X1),ok(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#(ok(X1),ok(X2)) -> div#(X1,X2)
      div#(mark(X1),X2) -> div#(X1,X2) ->
      div#(mark(X1),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#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
      active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) ->
      if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
      active#(if(X1,X2,X3)) -> active#(X1) ->
      active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
      active#(if(X1,X2,X3)) -> active#(X1) ->
      active#(if(X1,X2,X3)) -> 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#(div(X1,X2)) -> active#(X1)
      active#(if(X1,X2,X3)) -> active#(X1) ->
      active#(s(X)) -> s#(active(X))
      active#(if(X1,X2,X3)) -> active#(X1) ->
      active#(s(X)) -> active#(X)
      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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(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#(geq(s(X),s(Y))) -> geq#(X,Y)
      active#(if(X1,X2,X3)) -> active#(X1) ->
      active#(minus(s(X),s(Y))) -> minus#(X,Y)
      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#(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#(ok(X1),ok(X2)) -> div#(X1,X2)
      active#(div(X1,X2)) -> div#(active(X1),X2) ->
      div#(mark(X1),X2) -> div#(X1,X2)
      active#(div(X1,X2)) -> active#(X1) ->
      active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
      active#(div(X1,X2)) -> active#(X1) ->
      active#(if(X1,X2,X3)) -> active#(X1)
      active#(div(X1,X2)) -> active#(X1) ->
      active#(div(X1,X2)) -> div#(active(X1),X2)
      active#(div(X1,X2)) -> active#(X1) ->
      active#(div(X1,X2)) -> active#(X1)
      active#(div(X1,X2)) -> active#(X1) ->
      active#(s(X)) -> s#(active(X))
      active#(div(X1,X2)) -> active#(X1) ->
      active#(s(X)) -> active#(X)
      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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(Y))
      active#(div(X1,X2)) -> active#(X1) ->
      active#(div(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#(minus(s(X),s(Y))) -> minus#(X,Y)
      active#(geq(s(X),s(Y))) -> geq#(X,Y) ->
      geq#(ok(X1),ok(X2)) -> geq#(X1,X2)
      active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
      active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
      active#(s(X)) -> active#(X) ->
      active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
      active#(s(X)) -> active#(X) ->
      active#(if(X1,X2,X3)) -> active#(X1)
      active#(s(X)) -> active#(X) ->
      active#(div(X1,X2)) -> div#(active(X1),X2)
      active#(s(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1)
      active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
      active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
      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#(div(s(X),s(Y))) -> geq#(X,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))) -> div#(minus(X,Y),s(Y))
      active#(s(X)) -> active#(X) ->
      active#(div(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#(minus(s(X),s(Y))) -> minus#(X,Y)
      active#(minus(s(X),s(Y))) -> minus#(X,Y) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2)
     SCC Processor:
      #sccs: 8
      #rules: 23
      #arcs: 259/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:
       active#(s(X)) -> active#(X)
       active#(div(X1,X2)) -> active#(X1)
       active#(if(X1,X2,X3)) -> active#(X1)
      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#(minus(X1,X2)) -> proper#(X2)
       proper#(minus(X1,X2)) -> proper#(X1)
       proper#(s(X)) -> proper#(X)
       proper#(geq(X1,X2)) -> proper#(X2)
       proper#(geq(X1,X2)) -> proper#(X1)
       proper#(div(X1,X2)) -> proper#(X2)
       proper#(div(X1,X2)) -> proper#(X1)
       proper#(if(X1,X2,X3)) -> proper#(X3)
       proper#(if(X1,X2,X3)) -> proper#(X2)
       proper#(if(X1,X2,X3)) -> proper#(X1)
      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#(mark(X1),X2,X3) -> if#(X1,X2,X3)
       if#(ok(X1),ok(X2),ok(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
      
      DPs:
       div#(mark(X1),X2) -> div#(X1,X2)
       div#(ok(X1),ok(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:
       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#(mark(X)) -> s#(X)
       s#(ok(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:
       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