MAYBE

Problem:
 active(p(0())) -> mark(0())
 active(p(s(X))) -> mark(X)
 active(leq(0(),Y)) -> mark(true())
 active(leq(s(X),0())) -> mark(false())
 active(leq(s(X),s(Y))) -> mark(leq(X,Y))
 active(if(true(),X,Y)) -> mark(X)
 active(if(false(),X,Y)) -> mark(Y)
 active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
 active(p(X)) -> p(active(X))
 active(s(X)) -> s(active(X))
 active(leq(X1,X2)) -> leq(active(X1),X2)
 active(leq(X1,X2)) -> leq(X1,active(X2))
 active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
 active(diff(X1,X2)) -> diff(active(X1),X2)
 active(diff(X1,X2)) -> diff(X1,active(X2))
 p(mark(X)) -> mark(p(X))
 s(mark(X)) -> mark(s(X))
 leq(mark(X1),X2) -> mark(leq(X1,X2))
 leq(X1,mark(X2)) -> mark(leq(X1,X2))
 if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
 diff(mark(X1),X2) -> mark(diff(X1,X2))
 diff(X1,mark(X2)) -> mark(diff(X1,X2))
 proper(p(X)) -> p(proper(X))
 proper(0()) -> ok(0())
 proper(s(X)) -> s(proper(X))
 proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
 proper(true()) -> ok(true())
 proper(false()) -> ok(false())
 proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
 proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
 p(ok(X)) -> ok(p(X))
 s(ok(X)) -> ok(s(X))
 leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
 if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
 diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(leq(s(X),s(Y))) -> leq#(X,Y)
   active#(diff(X,Y)) -> p#(X)
   active#(diff(X,Y)) -> diff#(p(X),Y)
   active#(diff(X,Y)) -> s#(diff(p(X),Y))
   active#(diff(X,Y)) -> leq#(X,Y)
   active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
   active#(p(X)) -> active#(X)
   active#(p(X)) -> p#(active(X))
   active#(s(X)) -> active#(X)
   active#(s(X)) -> s#(active(X))
   active#(leq(X1,X2)) -> active#(X1)
   active#(leq(X1,X2)) -> leq#(active(X1),X2)
   active#(leq(X1,X2)) -> active#(X2)
   active#(leq(X1,X2)) -> leq#(X1,active(X2))
   active#(if(X1,X2,X3)) -> active#(X1)
   active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
   active#(diff(X1,X2)) -> active#(X1)
   active#(diff(X1,X2)) -> diff#(active(X1),X2)
   active#(diff(X1,X2)) -> active#(X2)
   active#(diff(X1,X2)) -> diff#(X1,active(X2))
   p#(mark(X)) -> p#(X)
   s#(mark(X)) -> s#(X)
   leq#(mark(X1),X2) -> leq#(X1,X2)
   leq#(X1,mark(X2)) -> leq#(X1,X2)
   if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
   diff#(mark(X1),X2) -> diff#(X1,X2)
   diff#(X1,mark(X2)) -> diff#(X1,X2)
   proper#(p(X)) -> proper#(X)
   proper#(p(X)) -> p#(proper(X))
   proper#(s(X)) -> proper#(X)
   proper#(s(X)) -> s#(proper(X))
   proper#(leq(X1,X2)) -> proper#(X2)
   proper#(leq(X1,X2)) -> proper#(X1)
   proper#(leq(X1,X2)) -> leq#(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))
   proper#(diff(X1,X2)) -> proper#(X2)
   proper#(diff(X1,X2)) -> proper#(X1)
   proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
   p#(ok(X)) -> p#(X)
   s#(ok(X)) -> s#(X)
   leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
   if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
   diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
   top#(mark(X)) -> proper#(X)
   top#(mark(X)) -> top#(proper(X))
   top#(ok(X)) -> active#(X)
   top#(ok(X)) -> top#(active(X))
  TRS:
   active(p(0())) -> mark(0())
   active(p(s(X))) -> mark(X)
   active(leq(0(),Y)) -> mark(true())
   active(leq(s(X),0())) -> mark(false())
   active(leq(s(X),s(Y))) -> mark(leq(X,Y))
   active(if(true(),X,Y)) -> mark(X)
   active(if(false(),X,Y)) -> mark(Y)
   active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
   active(p(X)) -> p(active(X))
   active(s(X)) -> s(active(X))
   active(leq(X1,X2)) -> leq(active(X1),X2)
   active(leq(X1,X2)) -> leq(X1,active(X2))
   active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
   active(diff(X1,X2)) -> diff(active(X1),X2)
   active(diff(X1,X2)) -> diff(X1,active(X2))
   p(mark(X)) -> mark(p(X))
   s(mark(X)) -> mark(s(X))
   leq(mark(X1),X2) -> mark(leq(X1,X2))
   leq(X1,mark(X2)) -> mark(leq(X1,X2))
   if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
   diff(mark(X1),X2) -> mark(diff(X1,X2))
   diff(X1,mark(X2)) -> mark(diff(X1,X2))
   proper(p(X)) -> p(proper(X))
   proper(0()) -> ok(0())
   proper(s(X)) -> s(proper(X))
   proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
   proper(true()) -> ok(true())
   proper(false()) -> ok(false())
   proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
   proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
   p(ok(X)) -> ok(p(X))
   s(ok(X)) -> ok(s(X))
   leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
   if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
   diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  TDG Processor:
   DPs:
    active#(leq(s(X),s(Y))) -> leq#(X,Y)
    active#(diff(X,Y)) -> p#(X)
    active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(diff(X,Y)) -> leq#(X,Y)
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(p(X)) -> active#(X)
    active#(p(X)) -> p#(active(X))
    active#(s(X)) -> active#(X)
    active#(s(X)) -> s#(active(X))
    active#(leq(X1,X2)) -> active#(X1)
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(leq(X1,X2)) -> active#(X2)
    active#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(diff(X1,X2)) -> active#(X1)
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(diff(X1,X2)) -> active#(X2)
    active#(diff(X1,X2)) -> diff#(X1,active(X2))
    p#(mark(X)) -> p#(X)
    s#(mark(X)) -> s#(X)
    leq#(mark(X1),X2) -> leq#(X1,X2)
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    diff#(mark(X1),X2) -> diff#(X1,X2)
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    proper#(p(X)) -> proper#(X)
    proper#(p(X)) -> p#(proper(X))
    proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> s#(proper(X))
    proper#(leq(X1,X2)) -> proper#(X2)
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(leq(X1,X2)) -> leq#(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))
    proper#(diff(X1,X2)) -> proper#(X2)
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    p#(ok(X)) -> p#(X)
    s#(ok(X)) -> s#(X)
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
   TRS:
    active(p(0())) -> mark(0())
    active(p(s(X))) -> mark(X)
    active(leq(0(),Y)) -> mark(true())
    active(leq(s(X),0())) -> mark(false())
    active(leq(s(X),s(Y))) -> mark(leq(X,Y))
    active(if(true(),X,Y)) -> mark(X)
    active(if(false(),X,Y)) -> mark(Y)
    active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
    active(p(X)) -> p(active(X))
    active(s(X)) -> s(active(X))
    active(leq(X1,X2)) -> leq(active(X1),X2)
    active(leq(X1,X2)) -> leq(X1,active(X2))
    active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
    active(diff(X1,X2)) -> diff(active(X1),X2)
    active(diff(X1,X2)) -> diff(X1,active(X2))
    p(mark(X)) -> mark(p(X))
    s(mark(X)) -> mark(s(X))
    leq(mark(X1),X2) -> mark(leq(X1,X2))
    leq(X1,mark(X2)) -> mark(leq(X1,X2))
    if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
    diff(mark(X1),X2) -> mark(diff(X1,X2))
    diff(X1,mark(X2)) -> mark(diff(X1,X2))
    proper(p(X)) -> p(proper(X))
    proper(0()) -> ok(0())
    proper(s(X)) -> s(proper(X))
    proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
    proper(true()) -> ok(true())
    proper(false()) -> ok(false())
    proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
    proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
    p(ok(X)) -> ok(p(X))
    s(ok(X)) -> ok(s(X))
    leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
    if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
    diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
    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#(diff(X1,X2)) -> diff#(X1,active(X2))
    top#(ok(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X1)
    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#(leq(X1,X2)) -> leq#(X1,active(X2))
    top#(ok(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(leq(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#(p(X)) -> p#(active(X))
    top#(ok(X)) -> active#(X) -> active#(p(X)) -> active#(X)
    top#(ok(X)) -> active#(X) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    top#(ok(X)) -> active#(X) -> active#(diff(X,Y)) -> leq#(X,Y)
    top#(ok(X)) -> active#(X) -> active#(diff(X,Y)) -> s#(diff(p(X),Y))
    top#(ok(X)) -> active#(X) -> active#(diff(X,Y)) -> diff#(p(X),Y)
    top#(ok(X)) -> active#(X) -> active#(diff(X,Y)) -> p#(X)
    top#(ok(X)) -> active#(X) ->
    active#(leq(s(X),s(Y))) -> leq#(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#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X2)
    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#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(leq(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#(p(X)) -> p#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> proper#(X2)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(leq(X1,X2)) -> proper#(X2)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(p(X)) -> p#(proper(X))
    proper#(diff(X1,X2)) -> proper#(X2) ->
    proper#(p(X)) -> proper#(X)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> proper#(X2)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(leq(X1,X2)) -> proper#(X2)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(p(X)) -> p#(proper(X))
    proper#(diff(X1,X2)) -> proper#(X1) ->
    proper#(p(X)) -> proper#(X)
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) ->
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) ->
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) ->
    diff#(mark(X1),X2) -> diff#(X1,X2)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(diff(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#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(leq(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#(p(X)) -> p#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X3) ->
    proper#(p(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(diff(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#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(leq(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#(p(X)) -> p#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X2) ->
    proper#(p(X)) -> proper#(X)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(diff(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#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(leq(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#(p(X)) -> p#(proper(X))
    proper#(if(X1,X2,X3)) -> proper#(X1) ->
    proper#(p(X)) -> proper#(X)
    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#(leq(X1,X2)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(diff(X1,X2)) -> proper#(X2)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(leq(X1,X2)) -> proper#(X2)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(p(X)) -> p#(proper(X))
    proper#(leq(X1,X2)) -> proper#(X2) ->
    proper#(p(X)) -> proper#(X)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> proper#(X1)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(diff(X1,X2)) -> proper#(X2)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(leq(X1,X2)) -> proper#(X1)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(leq(X1,X2)) -> proper#(X2)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(p(X)) -> p#(proper(X))
    proper#(leq(X1,X2)) -> proper#(X1) ->
    proper#(p(X)) -> proper#(X)
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) ->
    leq#(mark(X1),X2) -> leq#(X1,X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(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#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(leq(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#(p(X)) -> p#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X)
    proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
    proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
    proper#(p(X)) -> proper#(X) ->
    proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2))
    proper#(p(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X1)
    proper#(p(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X2)
    proper#(p(X)) -> proper#(X) ->
    proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
    proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1)
    proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2)
    proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3)
    proper#(p(X)) -> proper#(X) ->
    proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2))
    proper#(p(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X1)
    proper#(p(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X2)
    proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X))
    proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X)
    proper#(p(X)) -> p#(proper(X)) -> p#(ok(X)) -> p#(X)
    proper#(p(X)) -> p#(proper(X)) ->
    p#(mark(X)) -> p#(X)
    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)
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2) ->
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2) ->
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2) ->
    diff#(mark(X1),X2) -> diff#(X1,X2)
    diff#(mark(X1),X2) -> diff#(X1,X2) ->
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    diff#(mark(X1),X2) -> diff#(X1,X2) ->
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    diff#(mark(X1),X2) -> diff#(X1,X2) ->
    diff#(mark(X1),X2) -> diff#(X1,X2)
    diff#(X1,mark(X2)) -> diff#(X1,X2) ->
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    diff#(X1,mark(X2)) -> diff#(X1,X2) ->
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    diff#(X1,mark(X2)) -> diff#(X1,X2) -> diff#(mark(X1),X2) -> diff#(X1,X2)
    p#(ok(X)) -> p#(X) -> p#(ok(X)) -> p#(X)
    p#(ok(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
    p#(mark(X)) -> p#(X) -> p#(ok(X)) -> p#(X)
    p#(mark(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2) ->
    leq#(mark(X1),X2) -> leq#(X1,X2)
    leq#(mark(X1),X2) -> leq#(X1,X2) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    leq#(mark(X1),X2) -> leq#(X1,X2) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    leq#(mark(X1),X2) -> leq#(X1,X2) ->
    leq#(mark(X1),X2) -> leq#(X1,X2)
    leq#(X1,mark(X2)) -> leq#(X1,X2) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    leq#(X1,mark(X2)) -> leq#(X1,X2) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    leq#(X1,mark(X2)) -> leq#(X1,X2) ->
    leq#(mark(X1),X2) -> leq#(X1,X2)
    active#(diff(X1,X2)) -> diff#(active(X1),X2) ->
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    active#(diff(X1,X2)) -> diff#(active(X1),X2) ->
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    active#(diff(X1,X2)) -> diff#(active(X1),X2) ->
    diff#(mark(X1),X2) -> diff#(X1,X2)
    active#(diff(X1,X2)) -> diff#(X1,active(X2)) ->
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    active#(diff(X1,X2)) -> diff#(X1,active(X2)) ->
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    active#(diff(X1,X2)) -> diff#(X1,active(X2)) ->
    diff#(mark(X1),X2) -> diff#(X1,X2)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> diff#(X1,active(X2))
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> active#(X2)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> active#(X1)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> active#(X2)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> active#(X1)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(p(X)) -> p#(active(X))
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(p(X)) -> active#(X)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> leq#(X,Y)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> p#(X)
    active#(diff(X1,X2)) -> active#(X2) ->
    active#(leq(s(X),s(Y))) -> leq#(X,Y)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> diff#(X1,active(X2))
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> active#(X2)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> active#(X1)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> active#(X2)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> active#(X1)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(p(X)) -> p#(active(X))
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(p(X)) -> active#(X)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> leq#(X,Y)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> p#(X)
    active#(diff(X1,X2)) -> active#(X1) ->
    active#(leq(s(X),s(Y))) -> leq#(X,Y)
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y))) ->
    if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y))) ->
    if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
    active#(diff(X,Y)) -> s#(diff(p(X),Y)) ->
    s#(ok(X)) -> s#(X)
    active#(diff(X,Y)) -> s#(diff(p(X),Y)) ->
    s#(mark(X)) -> s#(X)
    active#(diff(X,Y)) -> diff#(p(X),Y) ->
    diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    active#(diff(X,Y)) -> diff#(p(X),Y) ->
    diff#(X1,mark(X2)) -> diff#(X1,X2)
    active#(diff(X,Y)) -> diff#(p(X),Y) ->
    diff#(mark(X1),X2) -> diff#(X1,X2)
    active#(diff(X,Y)) -> p#(X) -> p#(ok(X)) -> p#(X)
    active#(diff(X,Y)) -> p#(X) -> p#(mark(X)) -> p#(X)
    active#(diff(X,Y)) -> leq#(X,Y) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    active#(diff(X,Y)) -> leq#(X,Y) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    active#(diff(X,Y)) -> leq#(X,Y) ->
    leq#(mark(X1),X2) -> leq#(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#(diff(X1,X2)) -> diff#(X1,active(X2))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X1,X2)) -> active#(X2)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X1,X2)) -> active#(X1)
    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#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(leq(X1,X2)) -> active#(X2)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(leq(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#(p(X)) -> p#(active(X))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(p(X)) -> active#(X)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X,Y)) -> leq#(X,Y)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(diff(X,Y)) -> p#(X)
    active#(if(X1,X2,X3)) -> active#(X1) ->
    active#(leq(s(X),s(Y))) -> leq#(X,Y)
    active#(leq(s(X),s(Y))) -> leq#(X,Y) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    active#(leq(s(X),s(Y))) -> leq#(X,Y) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    active#(leq(s(X),s(Y))) -> leq#(X,Y) ->
    leq#(mark(X1),X2) -> leq#(X1,X2)
    active#(leq(X1,X2)) -> leq#(active(X1),X2) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    active#(leq(X1,X2)) -> leq#(active(X1),X2) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    active#(leq(X1,X2)) -> leq#(active(X1),X2) ->
    leq#(mark(X1),X2) -> leq#(X1,X2)
    active#(leq(X1,X2)) -> leq#(X1,active(X2)) ->
    leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    active#(leq(X1,X2)) -> leq#(X1,active(X2)) ->
    leq#(X1,mark(X2)) -> leq#(X1,X2)
    active#(leq(X1,X2)) -> leq#(X1,active(X2)) ->
    leq#(mark(X1),X2) -> leq#(X1,X2)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> diff#(X1,active(X2))
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> active#(X2)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X1,X2)) -> active#(X1)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> active#(X2)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(leq(X1,X2)) -> active#(X1)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(p(X)) -> p#(active(X))
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(p(X)) -> active#(X)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> leq#(X,Y)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(diff(X,Y)) -> p#(X)
    active#(leq(X1,X2)) -> active#(X2) ->
    active#(leq(s(X),s(Y))) -> leq#(X,Y)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> diff#(X1,active(X2))
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> active#(X2)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X1,X2)) -> active#(X1)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(if(X1,X2,X3)) -> active#(X1)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> active#(X2)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(leq(X1,X2)) -> active#(X1)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(p(X)) -> p#(active(X))
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(p(X)) -> active#(X)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> leq#(X,Y)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(diff(X,Y)) -> p#(X)
    active#(leq(X1,X2)) -> active#(X1) ->
    active#(leq(s(X),s(Y))) -> leq#(X,Y)
    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#(diff(X1,X2)) -> diff#(X1,active(X2))
    active#(s(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X1)
    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#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(s(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(leq(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#(p(X)) -> p#(active(X))
    active#(s(X)) -> active#(X) -> active#(p(X)) -> active#(X)
    active#(s(X)) -> active#(X) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(s(X)) -> active#(X) -> active#(diff(X,Y)) -> leq#(X,Y)
    active#(s(X)) -> active#(X) ->
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(s(X)) -> active#(X) -> active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(s(X)) -> active#(X) -> active#(diff(X,Y)) -> p#(X)
    active#(s(X)) -> active#(X) ->
    active#(leq(s(X),s(Y))) -> leq#(X,Y)
    active#(p(X)) -> p#(active(X)) -> p#(ok(X)) -> p#(X)
    active#(p(X)) -> p#(active(X)) -> p#(mark(X)) -> p#(X)
    active#(p(X)) -> active#(X) ->
    active#(diff(X1,X2)) -> diff#(X1,active(X2))
    active#(p(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X2)
    active#(p(X)) -> active#(X) ->
    active#(diff(X1,X2)) -> diff#(active(X1),X2)
    active#(p(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X1)
    active#(p(X)) -> active#(X) ->
    active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
    active#(p(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1)
    active#(p(X)) -> active#(X) ->
    active#(leq(X1,X2)) -> leq#(X1,active(X2))
    active#(p(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X2)
    active#(p(X)) -> active#(X) ->
    active#(leq(X1,X2)) -> leq#(active(X1),X2)
    active#(p(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X1)
    active#(p(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(p(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(p(X)) -> active#(X) -> active#(p(X)) -> p#(active(X))
    active#(p(X)) -> active#(X) -> active#(p(X)) -> active#(X)
    active#(p(X)) -> active#(X) ->
    active#(diff(X,Y)) -> if#(leq(X,Y),0(),s(diff(p(X),Y)))
    active#(p(X)) -> active#(X) -> active#(diff(X,Y)) -> leq#(X,Y)
    active#(p(X)) -> active#(X) ->
    active#(diff(X,Y)) -> s#(diff(p(X),Y))
    active#(p(X)) -> active#(X) -> active#(diff(X,Y)) -> diff#(p(X),Y)
    active#(p(X)) -> active#(X) -> active#(diff(X,Y)) -> p#(X)
    active#(p(X)) -> active#(X) -> active#(leq(s(X),s(Y))) -> leq#(X,Y)
   SCC Processor:
    #sccs: 8
    #rules: 30
    #arcs: 383/2500
    DPs:
     top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> top#(proper(X))
    TRS:
     active(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     active#(p(X)) -> active#(X)
     active#(s(X)) -> active#(X)
     active#(leq(X1,X2)) -> active#(X1)
     active#(leq(X1,X2)) -> active#(X2)
     active#(if(X1,X2,X3)) -> active#(X1)
     active#(diff(X1,X2)) -> active#(X1)
     active#(diff(X1,X2)) -> active#(X2)
    TRS:
     active(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(active#) = 0
     problem:
      DPs:
       
      TRS:
       active(p(0())) -> mark(0())
       active(p(s(X))) -> mark(X)
       active(leq(0(),Y)) -> mark(true())
       active(leq(s(X),0())) -> mark(false())
       active(leq(s(X),s(Y))) -> mark(leq(X,Y))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
       active(p(X)) -> p(active(X))
       active(s(X)) -> s(active(X))
       active(leq(X1,X2)) -> leq(active(X1),X2)
       active(leq(X1,X2)) -> leq(X1,active(X2))
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       active(diff(X1,X2)) -> diff(active(X1),X2)
       active(diff(X1,X2)) -> diff(X1,active(X2))
       p(mark(X)) -> mark(p(X))
       s(mark(X)) -> mark(s(X))
       leq(mark(X1),X2) -> mark(leq(X1,X2))
       leq(X1,mark(X2)) -> mark(leq(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       diff(mark(X1),X2) -> mark(diff(X1,X2))
       diff(X1,mark(X2)) -> mark(diff(X1,X2))
       proper(p(X)) -> p(proper(X))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
       p(ok(X)) -> ok(p(X))
       s(ok(X)) -> ok(s(X))
       leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     proper#(p(X)) -> proper#(X)
     proper#(s(X)) -> proper#(X)
     proper#(leq(X1,X2)) -> proper#(X2)
     proper#(leq(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)
     proper#(diff(X1,X2)) -> proper#(X2)
     proper#(diff(X1,X2)) -> proper#(X1)
    TRS:
     active(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(proper#) = 0
     problem:
      DPs:
       
      TRS:
       active(p(0())) -> mark(0())
       active(p(s(X))) -> mark(X)
       active(leq(0(),Y)) -> mark(true())
       active(leq(s(X),0())) -> mark(false())
       active(leq(s(X),s(Y))) -> mark(leq(X,Y))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
       active(p(X)) -> p(active(X))
       active(s(X)) -> s(active(X))
       active(leq(X1,X2)) -> leq(active(X1),X2)
       active(leq(X1,X2)) -> leq(X1,active(X2))
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       active(diff(X1,X2)) -> diff(active(X1),X2)
       active(diff(X1,X2)) -> diff(X1,active(X2))
       p(mark(X)) -> mark(p(X))
       s(mark(X)) -> mark(s(X))
       leq(mark(X1),X2) -> mark(leq(X1,X2))
       leq(X1,mark(X2)) -> mark(leq(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       diff(mark(X1),X2) -> mark(diff(X1,X2))
       diff(X1,mark(X2)) -> mark(diff(X1,X2))
       proper(p(X)) -> p(proper(X))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
       p(ok(X)) -> ok(p(X))
       s(ok(X)) -> ok(s(X))
       leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     diff#(mark(X1),X2) -> diff#(X1,X2)
     diff#(X1,mark(X2)) -> diff#(X1,X2)
     diff#(ok(X1),ok(X2)) -> diff#(X1,X2)
    TRS:
     active(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(diff#) = 1
     problem:
      DPs:
       diff#(mark(X1),X2) -> diff#(X1,X2)
      TRS:
       active(p(0())) -> mark(0())
       active(p(s(X))) -> mark(X)
       active(leq(0(),Y)) -> mark(true())
       active(leq(s(X),0())) -> mark(false())
       active(leq(s(X),s(Y))) -> mark(leq(X,Y))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
       active(p(X)) -> p(active(X))
       active(s(X)) -> s(active(X))
       active(leq(X1,X2)) -> leq(active(X1),X2)
       active(leq(X1,X2)) -> leq(X1,active(X2))
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       active(diff(X1,X2)) -> diff(active(X1),X2)
       active(diff(X1,X2)) -> diff(X1,active(X2))
       p(mark(X)) -> mark(p(X))
       s(mark(X)) -> mark(s(X))
       leq(mark(X1),X2) -> mark(leq(X1,X2))
       leq(X1,mark(X2)) -> mark(leq(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       diff(mark(X1),X2) -> mark(diff(X1,X2))
       diff(X1,mark(X2)) -> mark(diff(X1,X2))
       proper(p(X)) -> p(proper(X))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
       p(ok(X)) -> ok(p(X))
       s(ok(X)) -> ok(s(X))
       leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(diff#) = 0
      problem:
       DPs:
        
       TRS:
        active(p(0())) -> mark(0())
        active(p(s(X))) -> mark(X)
        active(leq(0(),Y)) -> mark(true())
        active(leq(s(X),0())) -> mark(false())
        active(leq(s(X),s(Y))) -> mark(leq(X,Y))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
        active(p(X)) -> p(active(X))
        active(s(X)) -> s(active(X))
        active(leq(X1,X2)) -> leq(active(X1),X2)
        active(leq(X1,X2)) -> leq(X1,active(X2))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(diff(X1,X2)) -> diff(active(X1),X2)
        active(diff(X1,X2)) -> diff(X1,active(X2))
        p(mark(X)) -> mark(p(X))
        s(mark(X)) -> mark(s(X))
        leq(mark(X1),X2) -> mark(leq(X1,X2))
        leq(X1,mark(X2)) -> mark(leq(X1,X2))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        diff(mark(X1),X2) -> mark(diff(X1,X2))
        diff(X1,mark(X2)) -> mark(diff(X1,X2))
        proper(p(X)) -> p(proper(X))
        proper(0()) -> ok(0())
        proper(s(X)) -> s(proper(X))
        proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
        p(ok(X)) -> ok(p(X))
        s(ok(X)) -> ok(s(X))
        leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
        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(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     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(p(0())) -> mark(0())
       active(p(s(X))) -> mark(X)
       active(leq(0(),Y)) -> mark(true())
       active(leq(s(X),0())) -> mark(false())
       active(leq(s(X),s(Y))) -> mark(leq(X,Y))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
       active(p(X)) -> p(active(X))
       active(s(X)) -> s(active(X))
       active(leq(X1,X2)) -> leq(active(X1),X2)
       active(leq(X1,X2)) -> leq(X1,active(X2))
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       active(diff(X1,X2)) -> diff(active(X1),X2)
       active(diff(X1,X2)) -> diff(X1,active(X2))
       p(mark(X)) -> mark(p(X))
       s(mark(X)) -> mark(s(X))
       leq(mark(X1),X2) -> mark(leq(X1,X2))
       leq(X1,mark(X2)) -> mark(leq(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       diff(mark(X1),X2) -> mark(diff(X1,X2))
       diff(X1,mark(X2)) -> mark(diff(X1,X2))
       proper(p(X)) -> p(proper(X))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
       p(ok(X)) -> ok(p(X))
       s(ok(X)) -> ok(s(X))
       leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(if#) = 0
      problem:
       DPs:
        
       TRS:
        active(p(0())) -> mark(0())
        active(p(s(X))) -> mark(X)
        active(leq(0(),Y)) -> mark(true())
        active(leq(s(X),0())) -> mark(false())
        active(leq(s(X),s(Y))) -> mark(leq(X,Y))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
        active(p(X)) -> p(active(X))
        active(s(X)) -> s(active(X))
        active(leq(X1,X2)) -> leq(active(X1),X2)
        active(leq(X1,X2)) -> leq(X1,active(X2))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(diff(X1,X2)) -> diff(active(X1),X2)
        active(diff(X1,X2)) -> diff(X1,active(X2))
        p(mark(X)) -> mark(p(X))
        s(mark(X)) -> mark(s(X))
        leq(mark(X1),X2) -> mark(leq(X1,X2))
        leq(X1,mark(X2)) -> mark(leq(X1,X2))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        diff(mark(X1),X2) -> mark(diff(X1,X2))
        diff(X1,mark(X2)) -> mark(diff(X1,X2))
        proper(p(X)) -> p(proper(X))
        proper(0()) -> ok(0())
        proper(s(X)) -> s(proper(X))
        proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
        p(ok(X)) -> ok(p(X))
        s(ok(X)) -> ok(s(X))
        leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed
    
    DPs:
     leq#(mark(X1),X2) -> leq#(X1,X2)
     leq#(X1,mark(X2)) -> leq#(X1,X2)
     leq#(ok(X1),ok(X2)) -> leq#(X1,X2)
    TRS:
     active(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(leq#) = 1
     problem:
      DPs:
       leq#(mark(X1),X2) -> leq#(X1,X2)
      TRS:
       active(p(0())) -> mark(0())
       active(p(s(X))) -> mark(X)
       active(leq(0(),Y)) -> mark(true())
       active(leq(s(X),0())) -> mark(false())
       active(leq(s(X),s(Y))) -> mark(leq(X,Y))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
       active(p(X)) -> p(active(X))
       active(s(X)) -> s(active(X))
       active(leq(X1,X2)) -> leq(active(X1),X2)
       active(leq(X1,X2)) -> leq(X1,active(X2))
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       active(diff(X1,X2)) -> diff(active(X1),X2)
       active(diff(X1,X2)) -> diff(X1,active(X2))
       p(mark(X)) -> mark(p(X))
       s(mark(X)) -> mark(s(X))
       leq(mark(X1),X2) -> mark(leq(X1,X2))
       leq(X1,mark(X2)) -> mark(leq(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       diff(mark(X1),X2) -> mark(diff(X1,X2))
       diff(X1,mark(X2)) -> mark(diff(X1,X2))
       proper(p(X)) -> p(proper(X))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
       p(ok(X)) -> ok(p(X))
       s(ok(X)) -> ok(s(X))
       leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(leq#) = 0
      problem:
       DPs:
        
       TRS:
        active(p(0())) -> mark(0())
        active(p(s(X))) -> mark(X)
        active(leq(0(),Y)) -> mark(true())
        active(leq(s(X),0())) -> mark(false())
        active(leq(s(X),s(Y))) -> mark(leq(X,Y))
        active(if(true(),X,Y)) -> mark(X)
        active(if(false(),X,Y)) -> mark(Y)
        active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
        active(p(X)) -> p(active(X))
        active(s(X)) -> s(active(X))
        active(leq(X1,X2)) -> leq(active(X1),X2)
        active(leq(X1,X2)) -> leq(X1,active(X2))
        active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
        active(diff(X1,X2)) -> diff(active(X1),X2)
        active(diff(X1,X2)) -> diff(X1,active(X2))
        p(mark(X)) -> mark(p(X))
        s(mark(X)) -> mark(s(X))
        leq(mark(X1),X2) -> mark(leq(X1,X2))
        leq(X1,mark(X2)) -> mark(leq(X1,X2))
        if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
        diff(mark(X1),X2) -> mark(diff(X1,X2))
        diff(X1,mark(X2)) -> mark(diff(X1,X2))
        proper(p(X)) -> p(proper(X))
        proper(0()) -> ok(0())
        proper(s(X)) -> s(proper(X))
        proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
        proper(true()) -> ok(true())
        proper(false()) -> ok(false())
        proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
        proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
        p(ok(X)) -> ok(p(X))
        s(ok(X)) -> ok(s(X))
        leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
        if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
        diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
        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(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       active(p(0())) -> mark(0())
       active(p(s(X))) -> mark(X)
       active(leq(0(),Y)) -> mark(true())
       active(leq(s(X),0())) -> mark(false())
       active(leq(s(X),s(Y))) -> mark(leq(X,Y))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
       active(p(X)) -> p(active(X))
       active(s(X)) -> s(active(X))
       active(leq(X1,X2)) -> leq(active(X1),X2)
       active(leq(X1,X2)) -> leq(X1,active(X2))
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       active(diff(X1,X2)) -> diff(active(X1),X2)
       active(diff(X1,X2)) -> diff(X1,active(X2))
       p(mark(X)) -> mark(p(X))
       s(mark(X)) -> mark(s(X))
       leq(mark(X1),X2) -> mark(leq(X1,X2))
       leq(X1,mark(X2)) -> mark(leq(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       diff(mark(X1),X2) -> mark(diff(X1,X2))
       diff(X1,mark(X2)) -> mark(diff(X1,X2))
       proper(p(X)) -> p(proper(X))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
       p(ok(X)) -> ok(p(X))
       s(ok(X)) -> ok(s(X))
       leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     p#(mark(X)) -> p#(X)
     p#(ok(X)) -> p#(X)
    TRS:
     active(p(0())) -> mark(0())
     active(p(s(X))) -> mark(X)
     active(leq(0(),Y)) -> mark(true())
     active(leq(s(X),0())) -> mark(false())
     active(leq(s(X),s(Y))) -> mark(leq(X,Y))
     active(if(true(),X,Y)) -> mark(X)
     active(if(false(),X,Y)) -> mark(Y)
     active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
     active(p(X)) -> p(active(X))
     active(s(X)) -> s(active(X))
     active(leq(X1,X2)) -> leq(active(X1),X2)
     active(leq(X1,X2)) -> leq(X1,active(X2))
     active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
     active(diff(X1,X2)) -> diff(active(X1),X2)
     active(diff(X1,X2)) -> diff(X1,active(X2))
     p(mark(X)) -> mark(p(X))
     s(mark(X)) -> mark(s(X))
     leq(mark(X1),X2) -> mark(leq(X1,X2))
     leq(X1,mark(X2)) -> mark(leq(X1,X2))
     if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
     diff(mark(X1),X2) -> mark(diff(X1,X2))
     diff(X1,mark(X2)) -> mark(diff(X1,X2))
     proper(p(X)) -> p(proper(X))
     proper(0()) -> ok(0())
     proper(s(X)) -> s(proper(X))
     proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
     proper(true()) -> ok(true())
     proper(false()) -> ok(false())
     proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
     proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
     p(ok(X)) -> ok(p(X))
     s(ok(X)) -> ok(s(X))
     leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
     if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
     diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      TRS:
       active(p(0())) -> mark(0())
       active(p(s(X))) -> mark(X)
       active(leq(0(),Y)) -> mark(true())
       active(leq(s(X),0())) -> mark(false())
       active(leq(s(X),s(Y))) -> mark(leq(X,Y))
       active(if(true(),X,Y)) -> mark(X)
       active(if(false(),X,Y)) -> mark(Y)
       active(diff(X,Y)) -> mark(if(leq(X,Y),0(),s(diff(p(X),Y))))
       active(p(X)) -> p(active(X))
       active(s(X)) -> s(active(X))
       active(leq(X1,X2)) -> leq(active(X1),X2)
       active(leq(X1,X2)) -> leq(X1,active(X2))
       active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
       active(diff(X1,X2)) -> diff(active(X1),X2)
       active(diff(X1,X2)) -> diff(X1,active(X2))
       p(mark(X)) -> mark(p(X))
       s(mark(X)) -> mark(s(X))
       leq(mark(X1),X2) -> mark(leq(X1,X2))
       leq(X1,mark(X2)) -> mark(leq(X1,X2))
       if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
       diff(mark(X1),X2) -> mark(diff(X1,X2))
       diff(X1,mark(X2)) -> mark(diff(X1,X2))
       proper(p(X)) -> p(proper(X))
       proper(0()) -> ok(0())
       proper(s(X)) -> s(proper(X))
       proper(leq(X1,X2)) -> leq(proper(X1),proper(X2))
       proper(true()) -> ok(true())
       proper(false()) -> ok(false())
       proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
       proper(diff(X1,X2)) -> diff(proper(X1),proper(X2))
       p(ok(X)) -> ok(p(X))
       s(ok(X)) -> ok(s(X))
       leq(ok(X1),ok(X2)) -> ok(leq(X1,X2))
       if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
       diff(ok(X1),ok(X2)) -> ok(diff(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed