YES

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)
   SCC Processor:
    #sccs: 8
    #rules: 23
    #arcs: 263/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))
    LPO Processor:
     argument filtering:
      pi(0) = []
      pi(minus) = [0]
      pi(active) = 0
      pi(mark) = [0]
      pi(s) = [0]
      pi(geq) = [1]
      pi(true) = []
      pi(false) = []
      pi(div) = [0,1]
      pi(if) = [0,1,2]
      pi(proper) = 0
      pi(ok) = 0
      pi(top) = 0
      pi(top#) = 0
     precedence:
      div > s > minus > if > geq > top# ~ top ~ ok ~ proper ~ false ~ true ~ mark ~ active ~ 0
     problem:
      DPs:
       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))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [top#](x0) = x0,
       
       [top](x0) = 0,
       
       [ok](x0) = 1x0 + 0,
       
       [proper](x0) = 1x0 + 0,
       
       [if](x0, x1, x2) = 1x1 + 0,
       
       [div](x0, x1) = 1x1 + 0,
       
       [false] = 0,
       
       [true] = 4,
       
       [geq](x0, x1) = 1x0 + 0,
       
       [s](x0) = x0,
       
       [mark](x0) = 0,
       
       [active](x0) = x0,
       
       [minus](x0, x1) = x0 + 1x1 + 0,
       
       [0] = 4
      orientation:
       top#(ok(X)) = 1X + 0 >= X = top#(active(X))
       
       active(minus(0(),Y)) = 1Y + 4 >= 0 = mark(0())
       
       active(minus(s(X),s(Y))) = X + 1Y + 0 >= 0 = mark(minus(X,Y))
       
       active(geq(X,0())) = 1X + 0 >= 0 = mark(true())
       
       active(geq(0(),s(Y))) = 5 >= 0 = mark(false())
       
       active(geq(s(X),s(Y))) = 1X + 0 >= 0 = mark(geq(X,Y))
       
       active(div(0(),s(Y))) = 1Y + 0 >= 0 = mark(0())
       
       active(div(s(X),s(Y))) = 1Y + 0 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       
       active(if(true(),X,Y)) = 1X + 0 >= 0 = mark(X)
       
       active(if(false(),X,Y)) = 1X + 0 >= 0 = mark(Y)
       
       active(s(X)) = X >= X = s(active(X))
       
       active(div(X1,X2)) = 1X2 + 0 >= 1X2 + 0 = div(active(X1),X2)
       
       active(if(X1,X2,X3)) = 1X2 + 0 >= 1X2 + 0 = if(active(X1),X2,X3)
       
       s(mark(X)) = 0 >= 0 = mark(s(X))
       
       div(mark(X1),X2) = 1X2 + 0 >= 0 = mark(div(X1,X2))
       
       if(mark(X1),X2,X3) = 1X2 + 0 >= 0 = mark(if(X1,X2,X3))
       
       proper(minus(X1,X2)) = 1X1 + 2X2 + 1 >= 1X1 + 2X2 + 1 = minus(proper(X1),proper(X2))
       
       proper(0()) = 5 >= 5 = ok(0())
       
       proper(s(X)) = 1X + 0 >= 1X + 0 = s(proper(X))
       
       proper(geq(X1,X2)) = 2X1 + 1 >= 2X1 + 1 = geq(proper(X1),proper(X2))
       
       proper(true()) = 5 >= 5 = ok(true())
       
       proper(false()) = 1 >= 1 = ok(false())
       
       proper(div(X1,X2)) = 2X2 + 1 >= 2X2 + 1 = div(proper(X1),proper(X2))
       
       proper(if(X1,X2,X3)) = 2X2 + 1 >= 2X2 + 1 = if(proper(X1),proper(X2),proper(X3))
       
       minus(ok(X1),ok(X2)) = 1X1 + 2X2 + 1 >= 1X1 + 2X2 + 1 = ok(minus(X1,X2))
       
       s(ok(X)) = 1X + 0 >= 1X + 0 = ok(s(X))
       
       geq(ok(X1),ok(X2)) = 2X1 + 1 >= 2X1 + 1 = ok(geq(X1,X2))
       
       div(ok(X1),ok(X2)) = 2X2 + 1 >= 2X2 + 1 = ok(div(X1,X2))
       
       if(ok(X1),ok(X2),ok(X3)) = 2X2 + 1 >= 2X2 + 1 = ok(if(X1,X2,X3))
       
       top(mark(X)) = 0 >= 0 = top(proper(X))
       
       top(ok(X)) = 0 >= 0 = top(active(X))
      problem:
       DPs:
        
       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))
      Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(active#) = 0
     problem:
      DPs:
       
      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))
     Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(proper#) = 0
     problem:
      DPs:
       
      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))
     Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(if#) = 2
     problem:
      DPs:
       if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(s(X)) -> s(active(X))
       active(div(X1,X2)) -> div(active(X1),X2)
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       s(mark(X)) -> mark(s(X))
       div(mark(X1),X2) -> mark(div(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(div(X1,X2)) -> div(proper(X1),proper(X2))
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
       s(ok(X)) -> ok(s(X))
       geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
       div(ok(X1),ok(X2)) -> ok(div(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(if#) = 0
      problem:
       DPs:
        
       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))
      Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(div#) = 1
     problem:
      DPs:
       div#(mark(X1),X2) -> div#(X1,X2)
      TRS:
       active(minus(0(),Y)) -> mark(0())
       active(minus(s(X),s(Y))) -> mark(minus(X,Y))
       active(geq(X,0())) -> mark(true())
       active(geq(0(),s(Y))) -> mark(false())
       active(geq(s(X),s(Y))) -> mark(geq(X,Y))
       active(div(0(),s(Y))) -> mark(0())
       active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(s(X)) -> s(active(X))
       active(div(X1,X2)) -> div(active(X1),X2)
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       s(mark(X)) -> mark(s(X))
       div(mark(X1),X2) -> mark(div(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       proper(minus(X1,X2)) -> minus(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(geq(X1,X2)) -> geq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(div(X1,X2)) -> div(proper(X1),proper(X2))
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       minus(ok(X1),ok(X2)) -> ok(minus(X1,X2))
       s(ok(X)) -> ok(s(X))
       geq(ok(X1),ok(X2)) -> ok(geq(X1,X2))
       div(ok(X1),ok(X2)) -> ok(div(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(div#) = 0
      problem:
       DPs:
        
       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))
      Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(geq#) = 1
     problem:
      DPs:
       
      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))
     Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      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))
     Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(minus#) = 1
     problem:
      DPs:
       
      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))
     Qed