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) EDG 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#(mark(X)) -> proper#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> active#(X) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) top#(ok(X)) -> active#(X) -> active#(diff(X,Y)) -> p#(X) top#(ok(X)) -> active#(X) -> active#(diff(X,Y)) -> diff#(p(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)) -> leq#(X,Y) 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#(p(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) top#(ok(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(leq(X1,X2)) -> leq#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) top#(ok(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(diff(X1,X2)) -> diff#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) top#(mark(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> proper#(X) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> p#(proper(X)) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(leq(X1,X2)) -> proper#(X2) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(leq(X1,X2)) -> proper#(X1) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) 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#(X1) 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#(diff(X1,X2)) -> proper#(X2) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(diff(X1,X2)) -> proper#(X1) proper#(diff(X1,X2)) -> proper#(X2) -> proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> proper#(X) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> p#(proper(X)) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(leq(X1,X2)) -> proper#(X2) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(leq(X1,X2)) -> proper#(X1) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) 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#(X1) 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#(diff(X1,X2)) -> proper#(X2) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(diff(X1,X2)) -> proper#(X1) proper#(diff(X1,X2)) -> proper#(X1) -> proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) -> diff#(mark(X1),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#(ok(X1),ok(X2)) -> diff#(X1,X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(p(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(p(X)) -> p#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(leq(X1,X2)) -> 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)) -> leq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(diff(X1,X2)) -> 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)) -> diff#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(p(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(p(X)) -> p#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(leq(X1,X2)) -> 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)) -> leq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(diff(X1,X2)) -> 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)) -> diff#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(p(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(p(X)) -> p#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(leq(X1,X2)) -> 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)) -> leq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(diff(X1,X2)) -> 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)) -> diff#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> proper#(X) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(p(X)) -> p#(proper(X)) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(leq(X1,X2)) -> proper#(X2) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(leq(X1,X2)) -> proper#(X1) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) 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#(X1) 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#(diff(X1,X2)) -> proper#(X2) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(diff(X1,X2)) -> proper#(X1) proper#(leq(X1,X2)) -> proper#(X2) -> proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> proper#(X) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(p(X)) -> p#(proper(X)) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(leq(X1,X2)) -> proper#(X2) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(leq(X1,X2)) -> proper#(X1) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) 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#(X1) 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#(diff(X1,X2)) -> proper#(X2) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(diff(X1,X2)) -> proper#(X1) proper#(leq(X1,X2)) -> proper#(X1) -> proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) -> leq#(mark(X1),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#(ok(X1),ok(X2)) -> leq#(X1,X2) proper#(s(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(s(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X) proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X) proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> proper#(X) proper#(p(X)) -> proper#(X) -> proper#(p(X)) -> p#(proper(X)) proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(p(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(p(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X2) proper#(p(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> proper#(X1) proper#(p(X)) -> proper#(X) -> proper#(leq(X1,X2)) -> leq#(proper(X1),proper(X2)) proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(p(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(p(X)) -> 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)) proper#(p(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X2) proper#(p(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> proper#(X1) proper#(p(X)) -> proper#(X) -> proper#(diff(X1,X2)) -> diff#(proper(X1),proper(X2)) proper#(p(X)) -> p#(proper(X)) -> p#(mark(X)) -> p#(X) proper#(p(X)) -> p#(proper(X)) -> p#(ok(X)) -> p#(X) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X) diff#(ok(X1),ok(X2)) -> diff#(X1,X2) -> diff#(mark(X1),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#(ok(X1),ok(X2)) -> diff#(X1,X2) diff#(mark(X1),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#(mark(X1),X2) -> diff#(X1,X2) -> diff#(ok(X1),ok(X2)) -> diff#(X1,X2) diff#(X1,mark(X2)) -> diff#(X1,X2) -> diff#(mark(X1),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#(ok(X1),ok(X2)) -> diff#(X1,X2) p#(ok(X)) -> p#(X) -> p#(mark(X)) -> p#(X) p#(ok(X)) -> p#(X) -> p#(ok(X)) -> p#(X) p#(mark(X)) -> p#(X) -> p#(mark(X)) -> p#(X) p#(mark(X)) -> p#(X) -> p#(ok(X)) -> p#(X) leq#(ok(X1),ok(X2)) -> leq#(X1,X2) -> leq#(mark(X1),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#(ok(X1),ok(X2)) -> leq#(X1,X2) leq#(mark(X1),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#(mark(X1),X2) -> leq#(X1,X2) -> leq#(ok(X1),ok(X2)) -> leq#(X1,X2) leq#(X1,mark(X2)) -> leq#(X1,X2) -> leq#(mark(X1),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#(ok(X1),ok(X2)) -> leq#(X1,X2) active#(diff(X1,X2)) -> diff#(active(X1),X2) -> diff#(mark(X1),X2) -> diff#(X1,X2) active#(diff(X1,X2)) -> diff#(active(X1),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#(ok(X1),ok(X2)) -> diff#(X1,X2) active#(diff(X1,X2)) -> active#(X2) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) active#(diff(X1,X2)) -> active#(X2) -> active#(diff(X,Y)) -> p#(X) active#(diff(X1,X2)) -> active#(X2) -> active#(diff(X,Y)) -> diff#(p(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)) -> leq#(X,Y) 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#(p(X)) -> active#(X) active#(diff(X1,X2)) -> active#(X2) -> active#(p(X)) -> p#(active(X)) active#(diff(X1,X2)) -> active#(X2) -> active#(s(X)) -> active#(X) active#(diff(X1,X2)) -> active#(X2) -> active#(s(X)) -> s#(active(X)) active#(diff(X1,X2)) -> active#(X2) -> active#(leq(X1,X2)) -> active#(X1) 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#(X2) active#(diff(X1,X2)) -> active#(X2) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) active#(diff(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> 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#(diff(X1,X2)) -> active#(X1) 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#(X2) active#(diff(X1,X2)) -> active#(X2) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) active#(diff(X1,X2)) -> active#(X1) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) active#(diff(X1,X2)) -> active#(X1) -> active#(diff(X,Y)) -> p#(X) active#(diff(X1,X2)) -> active#(X1) -> active#(diff(X,Y)) -> diff#(p(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)) -> leq#(X,Y) 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#(p(X)) -> active#(X) active#(diff(X1,X2)) -> active#(X1) -> active#(p(X)) -> p#(active(X)) active#(diff(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(diff(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(diff(X1,X2)) -> active#(X1) -> active#(leq(X1,X2)) -> active#(X1) 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#(X2) active#(diff(X1,X2)) -> active#(X1) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) active#(diff(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> 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#(diff(X1,X2)) -> active#(X1) 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#(X2) active#(diff(X1,X2)) -> active#(X1) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) 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#(mark(X)) -> s#(X) active#(diff(X,Y)) -> s#(diff(p(X),Y)) -> s#(ok(X)) -> s#(X) active#(diff(X,Y)) -> p#(X) -> p#(ok(X)) -> p#(X) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(diff(X,Y)) -> p#(X) 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)) -> 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)) -> if#(leq(X,Y),0(),s(diff(p(X),Y))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(p(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(p(X)) -> p#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(leq(X1,X2)) -> active#(X1) 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#(X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(diff(X1,X2)) -> active#(X1) 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#(X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) active#(leq(X1,X2)) -> leq#(active(X1),X2) -> 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#(X1,active(X2)) -> leq#(X1,mark(X2)) -> leq#(X1,X2) active#(leq(X1,X2)) -> leq#(X1,active(X2)) -> leq#(ok(X1),ok(X2)) -> leq#(X1,X2) active#(leq(X1,X2)) -> active#(X2) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) active#(leq(X1,X2)) -> active#(X2) -> active#(diff(X,Y)) -> p#(X) active#(leq(X1,X2)) -> active#(X2) -> active#(diff(X,Y)) -> diff#(p(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)) -> leq#(X,Y) 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#(p(X)) -> active#(X) active#(leq(X1,X2)) -> active#(X2) -> active#(p(X)) -> p#(active(X)) active#(leq(X1,X2)) -> active#(X2) -> active#(s(X)) -> active#(X) active#(leq(X1,X2)) -> active#(X2) -> active#(s(X)) -> s#(active(X)) active#(leq(X1,X2)) -> active#(X2) -> active#(leq(X1,X2)) -> active#(X1) 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#(X2) active#(leq(X1,X2)) -> active#(X2) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) active#(leq(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> 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#(diff(X1,X2)) -> active#(X1) 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#(X2) active#(leq(X1,X2)) -> active#(X2) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) active#(leq(X1,X2)) -> active#(X1) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) active#(leq(X1,X2)) -> active#(X1) -> active#(diff(X,Y)) -> p#(X) active#(leq(X1,X2)) -> active#(X1) -> active#(diff(X,Y)) -> diff#(p(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)) -> leq#(X,Y) 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#(p(X)) -> active#(X) active#(leq(X1,X2)) -> active#(X1) -> active#(p(X)) -> p#(active(X)) active#(leq(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(leq(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(leq(X1,X2)) -> active#(X1) -> active#(leq(X1,X2)) -> active#(X1) 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#(X2) active#(leq(X1,X2)) -> active#(X1) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) active#(leq(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> 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#(diff(X1,X2)) -> active#(X1) 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#(X2) active#(leq(X1,X2)) -> active#(X1) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X) active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X) active#(s(X)) -> active#(X) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) active#(s(X)) -> active#(X) -> active#(diff(X,Y)) -> p#(X) active#(s(X)) -> active#(X) -> active#(diff(X,Y)) -> diff#(p(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)) -> leq#(X,Y) 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#(p(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(s(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(leq(X1,X2)) -> leq#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(s(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(diff(X1,X2)) -> diff#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) active#(p(X)) -> p#(active(X)) -> p#(mark(X)) -> p#(X) active#(p(X)) -> p#(active(X)) -> p#(ok(X)) -> p#(X) active#(p(X)) -> active#(X) -> active#(leq(s(X),s(Y))) -> leq#(X,Y) active#(p(X)) -> active#(X) -> active#(diff(X,Y)) -> p#(X) active#(p(X)) -> active#(X) -> active#(diff(X,Y)) -> diff#(p(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)) -> leq#(X,Y) 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#(p(X)) -> active#(X) active#(p(X)) -> active#(X) -> active#(p(X)) -> p#(active(X)) active#(p(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(p(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(p(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X1) active#(p(X)) -> active#(X) -> active#(leq(X1,X2)) -> leq#(active(X1),X2) active#(p(X)) -> active#(X) -> active#(leq(X1,X2)) -> active#(X2) active#(p(X)) -> active#(X) -> active#(leq(X1,X2)) -> leq#(X1,active(X2)) active#(p(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(p(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(p(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X1) active#(p(X)) -> active#(X) -> active#(diff(X1,X2)) -> diff#(active(X1),X2) active#(p(X)) -> active#(X) -> active#(diff(X1,X2)) -> active#(X2) active#(p(X)) -> active#(X) -> active#(diff(X1,X2)) -> diff#(X1,active(X2)) SCC Processor: #sccs: 8 #rules: 30 #arcs: 368/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: proper#(diff(X1,X2)) -> proper#(X1) proper#(diff(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(leq(X1,X2)) -> proper#(X1) proper#(leq(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) proper#(p(X)) -> 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0 + 1, [top](x0) = 1, [ok](x0) = 0, [proper](x0) = x0, [diff](x0, x1) = x0 + x1 + 1, [if](x0, x1, x2) = x0 + x1 + x2 + 1, [false] = 1, [true] = 1, [leq](x0, x1) = x0 + x1 + 1, [s](x0) = x0, [mark](x0) = 0, [active](x0) = x0, [p](x0) = x0, [0] = 0 orientation: proper#(diff(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(diff(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(if(X1,X2,X3)) = X1 + X2 + X3 + 2 >= X1 + 1 = proper#(X1) proper#(if(X1,X2,X3)) = X1 + X2 + X3 + 2 >= X2 + 1 = proper#(X2) proper#(if(X1,X2,X3)) = X1 + X2 + X3 + 2 >= X3 + 1 = proper#(X3) proper#(leq(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(leq(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(s(X)) = X + 1 >= X + 1 = proper#(X) proper#(p(X)) = X + 1 >= X + 1 = proper#(X) active(p(0())) = 0 >= 0 = mark(0()) active(p(s(X))) = X >= 0 = mark(X) active(leq(0(),Y)) = Y + 1 >= 0 = mark(true()) active(leq(s(X),0())) = X + 1 >= 0 = mark(false()) active(leq(s(X),s(Y))) = X + Y + 1 >= 0 = mark(leq(X,Y)) active(if(true(),X,Y)) = X + Y + 2 >= 0 = mark(X) active(if(false(),X,Y)) = X + Y + 2 >= 0 = mark(Y) active(diff(X,Y)) = X + Y + 1 >= 0 = mark(if(leq(X,Y),0(),s(diff(p(X),Y)))) active(p(X)) = X >= X = p(active(X)) active(s(X)) = X >= X = s(active(X)) active(leq(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = leq(active(X1),X2) active(leq(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = leq(X1,active(X2)) active(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(active(X1),X2,X3) active(diff(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = diff(active(X1),X2) active(diff(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = diff(X1,active(X2)) p(mark(X)) = 0 >= 0 = mark(p(X)) s(mark(X)) = 0 >= 0 = mark(s(X)) leq(mark(X1),X2) = X2 + 1 >= 0 = mark(leq(X1,X2)) leq(X1,mark(X2)) = X1 + 1 >= 0 = mark(leq(X1,X2)) if(mark(X1),X2,X3) = X2 + X3 + 1 >= 0 = mark(if(X1,X2,X3)) diff(mark(X1),X2) = X2 + 1 >= 0 = mark(diff(X1,X2)) diff(X1,mark(X2)) = X1 + 1 >= 0 = mark(diff(X1,X2)) proper(p(X)) = X >= X = p(proper(X)) proper(0()) = 0 >= 0 = ok(0()) proper(s(X)) = X >= X = s(proper(X)) proper(leq(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = leq(proper(X1),proper(X2)) proper(true()) = 1 >= 0 = ok(true()) proper(false()) = 1 >= 0 = ok(false()) proper(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(proper(X1),proper(X2),proper(X3)) proper(diff(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = diff(proper(X1),proper(X2)) p(ok(X)) = 0 >= 0 = ok(p(X)) s(ok(X)) = 0 >= 0 = ok(s(X)) leq(ok(X1),ok(X2)) = 1 >= 0 = ok(leq(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = 1 >= 0 = ok(if(X1,X2,X3)) diff(ok(X1),ok(X2)) = 1 >= 0 = ok(diff(X1,X2)) top(mark(X)) = 1 >= 1 = top(proper(X)) top(ok(X)) = 1 >= 1 = top(active(X)) problem: DPs: proper#(s(X)) -> proper#(X) proper#(p(X)) -> 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0 + 1, [top](x0) = 0, [ok](x0) = 0, [proper](x0) = x0 + 1, [diff](x0, x1) = x0 + 1, [if](x0, x1, x2) = x0, [false] = 1, [true] = 0, [leq](x0, x1) = x1, [s](x0) = x0 + 1, [mark](x0) = 0, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [0] = 0 orientation: proper#(s(X)) = X + 2 >= X + 1 = proper#(X) proper#(p(X)) = X + 2 >= X + 1 = proper#(X) active(p(0())) = 2 >= 0 = mark(0()) active(p(s(X))) = X + 3 >= 0 = mark(X) active(leq(0(),Y)) = Y + 1 >= 0 = mark(true()) active(leq(s(X),0())) = 1 >= 0 = mark(false()) active(leq(s(X),s(Y))) = Y + 2 >= 0 = mark(leq(X,Y)) active(if(true(),X,Y)) = 1 >= 0 = mark(X) active(if(false(),X,Y)) = 2 >= 0 = mark(Y) active(diff(X,Y)) = X + 2 >= 0 = mark(if(leq(X,Y),0(),s(diff(p(X),Y)))) active(p(X)) = X + 2 >= X + 2 = p(active(X)) active(s(X)) = X + 2 >= X + 2 = s(active(X)) active(leq(X1,X2)) = X2 + 1 >= X2 = leq(active(X1),X2) active(leq(X1,X2)) = X2 + 1 >= X2 + 1 = leq(X1,active(X2)) active(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(active(X1),X2,X3) active(diff(X1,X2)) = X1 + 2 >= X1 + 2 = diff(active(X1),X2) active(diff(X1,X2)) = X1 + 2 >= X1 + 1 = diff(X1,active(X2)) p(mark(X)) = 1 >= 0 = mark(p(X)) s(mark(X)) = 1 >= 0 = mark(s(X)) leq(mark(X1),X2) = X2 >= 0 = mark(leq(X1,X2)) leq(X1,mark(X2)) = 0 >= 0 = mark(leq(X1,X2)) if(mark(X1),X2,X3) = 0 >= 0 = mark(if(X1,X2,X3)) diff(mark(X1),X2) = 1 >= 0 = mark(diff(X1,X2)) diff(X1,mark(X2)) = X1 + 1 >= 0 = mark(diff(X1,X2)) proper(p(X)) = X + 2 >= X + 2 = p(proper(X)) proper(0()) = 1 >= 0 = ok(0()) proper(s(X)) = X + 2 >= X + 2 = s(proper(X)) proper(leq(X1,X2)) = X2 + 1 >= X2 + 1 = leq(proper(X1),proper(X2)) proper(true()) = 1 >= 0 = ok(true()) proper(false()) = 2 >= 0 = ok(false()) proper(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(proper(X1),proper(X2),proper(X3)) proper(diff(X1,X2)) = X1 + 2 >= X1 + 2 = diff(proper(X1),proper(X2)) p(ok(X)) = 1 >= 0 = ok(p(X)) s(ok(X)) = 1 >= 0 = ok(s(X)) leq(ok(X1),ok(X2)) = 0 >= 0 = ok(leq(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = 0 >= 0 = ok(if(X1,X2,X3)) diff(ok(X1),ok(X2)) = 1 >= 0 = ok(diff(X1,X2)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) 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: active#(diff(X1,X2)) -> active#(X2) active#(diff(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) active#(leq(X1,X2)) -> active#(X2) active#(leq(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) active#(p(X)) -> 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [active#](x0) = x0 + 1, [top](x0) = 0, [ok](x0) = x0, [proper](x0) = x0, [diff](x0, x1) = x0 + x1 + 1, [if](x0, x1, x2) = x0 + 1, [false] = 0, [true] = 0, [leq](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [mark](x0) = 0, [active](x0) = x0, [p](x0) = x0 + 1, [0] = 1 orientation: active#(diff(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2) active#(diff(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1) active#(if(X1,X2,X3)) = X1 + 2 >= X1 + 1 = active#(X1) active#(leq(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2) active#(leq(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1) active#(s(X)) = X + 2 >= X + 1 = active#(X) active#(p(X)) = X + 2 >= X + 1 = active#(X) active(p(0())) = 2 >= 0 = mark(0()) active(p(s(X))) = X + 2 >= 0 = mark(X) active(leq(0(),Y)) = Y + 2 >= 0 = mark(true()) active(leq(s(X),0())) = X + 3 >= 0 = mark(false()) active(leq(s(X),s(Y))) = X + Y + 3 >= 0 = mark(leq(X,Y)) active(if(true(),X,Y)) = 1 >= 0 = mark(X) active(if(false(),X,Y)) = 1 >= 0 = mark(Y) active(diff(X,Y)) = X + Y + 1 >= 0 = mark(if(leq(X,Y),0(),s(diff(p(X),Y)))) active(p(X)) = X + 1 >= X + 1 = p(active(X)) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(leq(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = leq(active(X1),X2) active(leq(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = leq(X1,active(X2)) active(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(active(X1),X2,X3) active(diff(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = diff(active(X1),X2) active(diff(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = diff(X1,active(X2)) p(mark(X)) = 1 >= 0 = mark(p(X)) s(mark(X)) = 1 >= 0 = mark(s(X)) leq(mark(X1),X2) = X2 + 1 >= 0 = mark(leq(X1,X2)) leq(X1,mark(X2)) = X1 + 1 >= 0 = mark(leq(X1,X2)) if(mark(X1),X2,X3) = 1 >= 0 = mark(if(X1,X2,X3)) diff(mark(X1),X2) = X2 + 1 >= 0 = mark(diff(X1,X2)) diff(X1,mark(X2)) = X1 + 1 >= 0 = mark(diff(X1,X2)) proper(p(X)) = X + 1 >= X + 1 = p(proper(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(leq(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = leq(proper(X1),proper(X2)) proper(true()) = 0 >= 0 = ok(true()) proper(false()) = 0 >= 0 = ok(false()) proper(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(proper(X1),proper(X2),proper(X3)) proper(diff(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = diff(proper(X1),proper(X2)) p(ok(X)) = X + 1 >= X + 1 = ok(p(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) leq(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(leq(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X1 + 1 >= X1 + 1 = ok(if(X1,X2,X3)) diff(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(diff(X1,X2)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) 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#(ok(X)) -> p#(X) p#(mark(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)) Open DPs: s#(ok(X)) -> s#(X) s#(mark(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)) Open DPs: leq#(ok(X1),ok(X2)) -> leq#(X1,X2) leq#(X1,mark(X2)) -> leq#(X1,X2) 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)) Open DPs: if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [if#](x0, x1, x2) = x2 + 1, [top](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 1, [diff](x0, x1) = x1, [if](x0, x1, x2) = x2, [false] = 0, [true] = 0, [leq](x0, x1) = x1, [s](x0) = x0, [mark](x0) = 0, [active](x0) = x0 + 1, [p](x0) = x0, [0] = 0 orientation: if#(ok(X1),ok(X2),ok(X3)) = X3 + 2 >= X3 + 1 = if#(X1,X2,X3) if#(mark(X1),X2,X3) = X3 + 1 >= X3 + 1 = if#(X1,X2,X3) active(p(0())) = 1 >= 0 = mark(0()) active(p(s(X))) = X + 1 >= 0 = mark(X) active(leq(0(),Y)) = Y + 1 >= 0 = mark(true()) active(leq(s(X),0())) = 1 >= 0 = mark(false()) active(leq(s(X),s(Y))) = Y + 1 >= 0 = mark(leq(X,Y)) active(if(true(),X,Y)) = Y + 1 >= 0 = mark(X) active(if(false(),X,Y)) = Y + 1 >= 0 = mark(Y) active(diff(X,Y)) = Y + 1 >= 0 = mark(if(leq(X,Y),0(),s(diff(p(X),Y)))) active(p(X)) = X + 1 >= X + 1 = p(active(X)) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(leq(X1,X2)) = X2 + 1 >= X2 = leq(active(X1),X2) active(leq(X1,X2)) = X2 + 1 >= X2 + 1 = leq(X1,active(X2)) active(if(X1,X2,X3)) = X3 + 1 >= X3 = if(active(X1),X2,X3) active(diff(X1,X2)) = X2 + 1 >= X2 = diff(active(X1),X2) active(diff(X1,X2)) = X2 + 1 >= X2 + 1 = diff(X1,active(X2)) p(mark(X)) = 0 >= 0 = mark(p(X)) s(mark(X)) = 0 >= 0 = mark(s(X)) leq(mark(X1),X2) = X2 >= 0 = mark(leq(X1,X2)) leq(X1,mark(X2)) = 0 >= 0 = mark(leq(X1,X2)) if(mark(X1),X2,X3) = X3 >= 0 = mark(if(X1,X2,X3)) diff(mark(X1),X2) = X2 >= 0 = mark(diff(X1,X2)) diff(X1,mark(X2)) = 0 >= 0 = mark(diff(X1,X2)) proper(p(X)) = 1 >= 1 = p(proper(X)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = 1 >= 1 = s(proper(X)) proper(leq(X1,X2)) = 1 >= 1 = leq(proper(X1),proper(X2)) proper(true()) = 1 >= 1 = ok(true()) proper(false()) = 1 >= 1 = ok(false()) proper(if(X1,X2,X3)) = 1 >= 1 = if(proper(X1),proper(X2),proper(X3)) proper(diff(X1,X2)) = 1 >= 1 = diff(proper(X1),proper(X2)) p(ok(X)) = X + 1 >= X + 1 = ok(p(X)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) leq(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(leq(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X3 + 1 >= X3 + 1 = ok(if(X1,X2,X3)) diff(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(diff(X1,X2)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) 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)) Open DPs: diff#(ok(X1),ok(X2)) -> diff#(X1,X2) diff#(X1,mark(X2)) -> diff#(X1,X2) 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)) Open