MAYBE Problem: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(div(s(X),s(Y))) -> minus#(X,Y) active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(div(s(X),s(Y))) -> geq#(X,Y) active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(div(X1,X2)) -> active#(X1) active#(div(X1,X2)) -> div#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) s#(mark(X)) -> s#(X) div#(mark(X1),X2) -> div#(X1,X2) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(minus(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(geq(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) minus#(ok(X1),ok(X2)) -> minus#(X1,X2) s#(ok(X)) -> s#(X) geq#(ok(X1),ok(X2)) -> geq#(X1,X2) div#(ok(X1),ok(X2)) -> div#(X1,X2) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(div(s(X),s(Y))) -> minus#(X,Y) active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(div(s(X),s(Y))) -> geq#(X,Y) active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(div(X1,X2)) -> active#(X1) active#(div(X1,X2)) -> div#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) s#(mark(X)) -> s#(X) div#(mark(X1),X2) -> div#(X1,X2) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(minus(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(geq(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) minus#(ok(X1),ok(X2)) -> minus#(X1,X2) s#(ok(X)) -> s#(X) geq#(ok(X1),ok(X2)) -> geq#(X1,X2) div#(ok(X1),ok(X2)) -> div#(X1,X2) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(div(X1,X2)) -> div#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> geq#(X,Y) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> minus#(X,Y) top#(ok(X)) -> active#(X) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) top#(ok(X)) -> active#(X) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(div(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(div(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(div(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(div(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(div(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(div(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) -> div#(mark(X1),X2) -> div#(X1,X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) -> geq#(ok(X1),ok(X2)) -> geq#(X1,X2) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X) proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) div#(ok(X1),ok(X2)) -> div#(X1,X2) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) div#(ok(X1),ok(X2)) -> div#(X1,X2) -> div#(mark(X1),X2) -> div#(X1,X2) div#(mark(X1),X2) -> div#(X1,X2) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) div#(mark(X1),X2) -> div#(X1,X2) -> div#(mark(X1),X2) -> div#(X1,X2) geq#(ok(X1),ok(X2)) -> geq#(X1,X2) -> geq#(ok(X1),ok(X2)) -> geq#(X1,X2) minus#(ok(X1),ok(X2)) -> minus#(X1,X2) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(X1,X2)) -> div#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> geq#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> minus#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) -> s#(ok(X)) -> s#(X) active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) -> s#(mark(X)) -> s#(X) active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) -> div#(mark(X1),X2) -> div#(X1,X2) active#(div(s(X),s(Y))) -> geq#(X,Y) -> geq#(ok(X1),ok(X2)) -> geq#(X1,X2) active#(div(s(X),s(Y))) -> minus#(X,Y) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2) active#(div(X1,X2)) -> div#(active(X1),X2) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) active#(div(X1,X2)) -> div#(active(X1),X2) -> div#(mark(X1),X2) -> div#(X1,X2) active#(div(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(div(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(div(X1,X2)) -> active#(X1) -> active#(div(X1,X2)) -> div#(active(X1),X2) active#(div(X1,X2)) -> active#(X1) -> active#(div(X1,X2)) -> active#(X1) active#(div(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(div(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> geq#(X,Y) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> minus#(X,Y) active#(div(X1,X2)) -> active#(X1) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(div(X1,X2)) -> active#(X1) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(geq(s(X),s(Y))) -> geq#(X,Y) -> geq#(ok(X1),ok(X2)) -> geq#(X1,X2) active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X) active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(div(X1,X2)) -> div#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> geq#(X,Y) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> minus#(X,Y) active#(s(X)) -> active#(X) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(s(X)) -> active#(X) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(minus(s(X),s(Y))) -> minus#(X,Y) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2) EDG Processor: DPs: active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(div(s(X),s(Y))) -> minus#(X,Y) active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(div(s(X),s(Y))) -> geq#(X,Y) active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(div(X1,X2)) -> active#(X1) active#(div(X1,X2)) -> div#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) s#(mark(X)) -> s#(X) div#(mark(X1),X2) -> div#(X1,X2) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(minus(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(geq(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) minus#(ok(X1),ok(X2)) -> minus#(X1,X2) s#(ok(X)) -> s#(X) geq#(ok(X1),ok(X2)) -> geq#(X1,X2) div#(ok(X1),ok(X2)) -> div#(X1,X2) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> active#(X) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) top#(ok(X)) -> active#(X) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> minus#(X,Y) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> geq#(X,Y) top#(ok(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) top#(ok(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(div(X1,X2)) -> div#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(div(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(div(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) proper#(div(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(div(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(div(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) -> div#(mark(X1),X2) -> div#(X1,X2) proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) -> geq#(ok(X1),ok(X2)) -> geq#(X1,X2) proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X) proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(geq(X1,X2)) -> geq#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(div(X1,X2)) -> div#(proper(X1),proper(X2)) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(minus(X1,X2)) -> minus#(proper(X1),proper(X2)) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X) div#(ok(X1),ok(X2)) -> div#(X1,X2) -> div#(mark(X1),X2) -> div#(X1,X2) div#(ok(X1),ok(X2)) -> div#(X1,X2) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) div#(mark(X1),X2) -> div#(X1,X2) -> div#(mark(X1),X2) -> div#(X1,X2) div#(mark(X1),X2) -> div#(X1,X2) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) geq#(ok(X1),ok(X2)) -> geq#(X1,X2) -> geq#(ok(X1),ok(X2)) -> geq#(X1,X2) minus#(ok(X1),ok(X2)) -> minus#(X1,X2) -> minus#(ok(X1),ok(X2)) -> minus#(X1,X2) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> minus#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> geq#(X,Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(div(X1,X2)) -> div#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) -> s#(mark(X)) -> s#(X) active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) -> s#(ok(X)) -> s#(X) active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) -> div#(mark(X1),X2) -> div#(X1,X2) active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) active#(div(X1,X2)) -> div#(active(X1),X2) -> div#(mark(X1),X2) -> div#(X1,X2) active#(div(X1,X2)) -> div#(active(X1),X2) -> div#(ok(X1),ok(X2)) -> div#(X1,X2) active#(div(X1,X2)) -> active#(X1) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(div(X1,X2)) -> active#(X1) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> minus#(X,Y) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> geq#(X,Y) active#(div(X1,X2)) -> active#(X1) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(div(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(div(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(div(X1,X2)) -> active#(X1) -> active#(div(X1,X2)) -> active#(X1) active#(div(X1,X2)) -> active#(X1) -> active#(div(X1,X2)) -> div#(active(X1),X2) active#(div(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(div(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X) active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X) active#(s(X)) -> active#(X) -> active#(minus(s(X),s(Y))) -> minus#(X,Y) active#(s(X)) -> active#(X) -> active#(geq(s(X),s(Y))) -> geq#(X,Y) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> minus#(X,Y) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y)) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y))) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> geq#(X,Y) active#(s(X)) -> active#(X) -> active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(s(X)) -> active#(X) -> active#(div(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(div(X1,X2)) -> div#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) SCC Processor: #sccs: 8 #rules: 23 #arcs: 258/1600 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Open DPs: proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(div(X1,X2)) -> proper#(X1) proper#(div(X1,X2)) -> proper#(X2) proper#(geq(X1,X2)) -> proper#(X1) proper#(geq(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0 + 1, [top](x0) = 0, [ok](x0) = 0, [proper](x0) = x0, [if](x0, x1, x2) = x0 + x1 + x2 + 1, [div](x0, x1) = x0 + x1 + 1, [false] = 1, [true] = 0, [geq](x0, x1) = x0 + x1 + 1, [s](x0) = x0, [mark](x0) = 0, [active](x0) = x0, [minus](x0, x1) = x0 + x1, [0] = 0 orientation: 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#(div(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(div(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(geq(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(geq(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) proper#(s(X)) = X + 1 >= X + 1 = proper#(X) proper#(minus(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = proper#(X1) proper#(minus(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = proper#(X2) active(minus(0(),Y)) = Y >= 0 = mark(0()) active(minus(s(X),s(Y))) = X + Y >= 0 = mark(minus(X,Y)) active(geq(X,0())) = X + 1 >= 0 = mark(true()) active(geq(0(),s(Y))) = Y + 1 >= 0 = mark(false()) active(geq(s(X),s(Y))) = X + Y + 1 >= 0 = mark(geq(X,Y)) active(div(0(),s(Y))) = Y + 1 >= 0 = mark(0()) active(div(s(X),s(Y))) = X + Y + 1 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = X + Y + 1 >= 0 = mark(X) active(if(false(),X,Y)) = X + Y + 2 >= 0 = mark(Y) active(s(X)) = X >= X = s(active(X)) active(div(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = div(active(X1),X2) active(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(active(X1),X2,X3) s(mark(X)) = 0 >= 0 = mark(s(X)) div(mark(X1),X2) = X2 + 1 >= 0 = mark(div(X1,X2)) if(mark(X1),X2,X3) = X2 + X3 + 1 >= 0 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = X1 + X2 >= X1 + X2 = minus(proper(X1),proper(X2)) proper(0()) = 0 >= 0 = ok(0()) proper(s(X)) = X >= X = s(proper(X)) proper(geq(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = geq(proper(X1),proper(X2)) proper(true()) = 0 >= 0 = ok(true()) proper(false()) = 1 >= 0 = ok(false()) proper(div(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = 0 >= 0 = ok(minus(X1,X2)) s(ok(X)) = 0 >= 0 = ok(s(X)) geq(ok(X1),ok(X2)) = 1 >= 0 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = 1 >= 0 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = 1 >= 0 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: proper#(s(X)) -> proper#(X) proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0 + 1, [top](x0) = 1, [ok](x0) = 0, [proper](x0) = x0, [if](x0, x1, x2) = x0 + 1, [div](x0, x1) = 0, [false] = 1, [true] = 1, [geq](x0, x1) = 1, [s](x0) = x0 + 1, [mark](x0) = 0, [active](x0) = x0, [minus](x0, x1) = x0 + x1, [0] = 0 orientation: proper#(s(X)) = X + 2 >= X + 1 = proper#(X) proper#(minus(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = proper#(X1) proper#(minus(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = proper#(X2) active(minus(0(),Y)) = Y >= 0 = mark(0()) active(minus(s(X),s(Y))) = X + Y + 2 >= 0 = mark(minus(X,Y)) active(geq(X,0())) = 1 >= 0 = mark(true()) active(geq(0(),s(Y))) = 1 >= 0 = mark(false()) active(geq(s(X),s(Y))) = 1 >= 0 = mark(geq(X,Y)) active(div(0(),s(Y))) = 0 >= 0 = mark(0()) active(div(s(X),s(Y))) = 0 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = 2 >= 0 = mark(X) active(if(false(),X,Y)) = 2 >= 0 = mark(Y) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(div(X1,X2)) = 0 >= 0 = div(active(X1),X2) active(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(active(X1),X2,X3) s(mark(X)) = 1 >= 0 = mark(s(X)) div(mark(X1),X2) = 0 >= 0 = mark(div(X1,X2)) if(mark(X1),X2,X3) = 1 >= 0 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = X1 + X2 >= X1 + X2 = minus(proper(X1),proper(X2)) proper(0()) = 0 >= 0 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(geq(X1,X2)) = 1 >= 1 = geq(proper(X1),proper(X2)) proper(true()) = 1 >= 0 = ok(true()) proper(false()) = 1 >= 0 = ok(false()) proper(div(X1,X2)) = 0 >= 0 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = 0 >= 0 = ok(minus(X1,X2)) s(ok(X)) = 1 >= 0 = ok(s(X)) geq(ok(X1),ok(X2)) = 1 >= 0 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = 0 >= 0 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = 1 >= 0 = ok(if(X1,X2,X3)) top(mark(X)) = 1 >= 1 = top(proper(X)) top(ok(X)) = 1 >= 1 = top(active(X)) problem: DPs: proper#(minus(X1,X2)) -> proper#(X1) proper#(minus(X1,X2)) -> proper#(X2) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [proper#](x0) = x0 + 1, [top](x0) = 0, [ok](x0) = 0, [proper](x0) = x0, [if](x0, x1, x2) = x0, [div](x0, x1) = 0, [false] = 0, [true] = 0, [geq](x0, x1) = x0 + 1, [s](x0) = 0, [mark](x0) = 0, [active](x0) = x0 + 1, [minus](x0, x1) = x0 + x1 + 1, [0] = 1 orientation: proper#(minus(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1) proper#(minus(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2) active(minus(0(),Y)) = Y + 3 >= 0 = mark(0()) active(minus(s(X),s(Y))) = 2 >= 0 = mark(minus(X,Y)) active(geq(X,0())) = X + 2 >= 0 = mark(true()) active(geq(0(),s(Y))) = 3 >= 0 = mark(false()) active(geq(s(X),s(Y))) = 2 >= 0 = mark(geq(X,Y)) active(div(0(),s(Y))) = 1 >= 0 = mark(0()) active(div(s(X),s(Y))) = 1 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = 1 >= 0 = mark(X) active(if(false(),X,Y)) = 1 >= 0 = mark(Y) active(s(X)) = 1 >= 0 = s(active(X)) active(div(X1,X2)) = 1 >= 0 = div(active(X1),X2) active(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(active(X1),X2,X3) s(mark(X)) = 0 >= 0 = mark(s(X)) div(mark(X1),X2) = 0 >= 0 = mark(div(X1,X2)) if(mark(X1),X2,X3) = 0 >= 0 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = minus(proper(X1),proper(X2)) proper(0()) = 1 >= 0 = ok(0()) proper(s(X)) = 0 >= 0 = s(proper(X)) proper(geq(X1,X2)) = X1 + 1 >= X1 + 1 = geq(proper(X1),proper(X2)) proper(true()) = 0 >= 0 = ok(true()) proper(false()) = 0 >= 0 = ok(false()) proper(div(X1,X2)) = 0 >= 0 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 >= X1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = 1 >= 0 = ok(minus(X1,X2)) s(ok(X)) = 0 >= 0 = ok(s(X)) geq(ok(X1),ok(X2)) = 1 >= 0 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = 0 >= 0 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = 0 >= 0 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: minus#(ok(X1),ok(X2)) -> minus#(X1,X2) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [minus#](x0, x1) = x1 + 1, [top](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [if](x0, x1, x2) = x0, [div](x0, x1) = x0, [false] = 0, [true] = 1, [geq](x0, x1) = x1 + 1, [s](x0) = x0, [mark](x0) = 0, [active](x0) = 1, [minus](x0, x1) = x1, [0] = 0 orientation: minus#(ok(X1),ok(X2)) = X2 + 2 >= X2 + 1 = minus#(X1,X2) active(minus(0(),Y)) = 1 >= 0 = mark(0()) active(minus(s(X),s(Y))) = 1 >= 0 = mark(minus(X,Y)) active(geq(X,0())) = 1 >= 0 = mark(true()) active(geq(0(),s(Y))) = 1 >= 0 = mark(false()) active(geq(s(X),s(Y))) = 1 >= 0 = mark(geq(X,Y)) active(div(0(),s(Y))) = 1 >= 0 = mark(0()) active(div(s(X),s(Y))) = 1 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = 1 >= 0 = mark(X) active(if(false(),X,Y)) = 1 >= 0 = mark(Y) active(s(X)) = 1 >= 1 = s(active(X)) active(div(X1,X2)) = 1 >= 1 = div(active(X1),X2) active(if(X1,X2,X3)) = 1 >= 1 = if(active(X1),X2,X3) s(mark(X)) = 0 >= 0 = mark(s(X)) div(mark(X1),X2) = 0 >= 0 = mark(div(X1,X2)) if(mark(X1),X2,X3) = 0 >= 0 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = X2 + 1 >= X2 + 1 = minus(proper(X1),proper(X2)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(geq(X1,X2)) = X2 + 2 >= X2 + 2 = geq(proper(X1),proper(X2)) proper(true()) = 2 >= 2 = ok(true()) proper(false()) = 1 >= 1 = ok(false()) proper(div(X1,X2)) = X1 + 1 >= X1 + 1 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(minus(X1,X2)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) geq(ok(X1),ok(X2)) = X2 + 2 >= X2 + 2 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X1 + 1 >= X1 + 1 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: geq#(ok(X1),ok(X2)) -> geq#(X1,X2) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [geq#](x0, x1) = x1 + 1, [top](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [if](x0, x1, x2) = x0, [div](x0, x1) = x0, [false] = 0, [true] = 1, [geq](x0, x1) = x1 + 1, [s](x0) = x0, [mark](x0) = 0, [active](x0) = 1, [minus](x0, x1) = x1, [0] = 0 orientation: geq#(ok(X1),ok(X2)) = X2 + 2 >= X2 + 1 = geq#(X1,X2) active(minus(0(),Y)) = 1 >= 0 = mark(0()) active(minus(s(X),s(Y))) = 1 >= 0 = mark(minus(X,Y)) active(geq(X,0())) = 1 >= 0 = mark(true()) active(geq(0(),s(Y))) = 1 >= 0 = mark(false()) active(geq(s(X),s(Y))) = 1 >= 0 = mark(geq(X,Y)) active(div(0(),s(Y))) = 1 >= 0 = mark(0()) active(div(s(X),s(Y))) = 1 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = 1 >= 0 = mark(X) active(if(false(),X,Y)) = 1 >= 0 = mark(Y) active(s(X)) = 1 >= 1 = s(active(X)) active(div(X1,X2)) = 1 >= 1 = div(active(X1),X2) active(if(X1,X2,X3)) = 1 >= 1 = if(active(X1),X2,X3) s(mark(X)) = 0 >= 0 = mark(s(X)) div(mark(X1),X2) = 0 >= 0 = mark(div(X1,X2)) if(mark(X1),X2,X3) = 0 >= 0 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = X2 + 1 >= X2 + 1 = minus(proper(X1),proper(X2)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(geq(X1,X2)) = X2 + 2 >= X2 + 2 = geq(proper(X1),proper(X2)) proper(true()) = 2 >= 2 = ok(true()) proper(false()) = 1 >= 1 = ok(false()) proper(div(X1,X2)) = X1 + 1 >= X1 + 1 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(minus(X1,X2)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) geq(ok(X1),ok(X2)) = X2 + 2 >= X2 + 2 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X1 + 1 >= X1 + 1 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: active#(if(X1,X2,X3)) -> active#(X1) active#(div(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [active#](x0) = x0 + 1, [top](x0) = 1, [ok](x0) = x0, [proper](x0) = x0, [if](x0, x1, x2) = x0 + 1, [div](x0, x1) = x0 + 1, [false] = 0, [true] = 0, [geq](x0, x1) = 1, [s](x0) = x0 + 1, [mark](x0) = 1, [active](x0) = x0 + 1, [minus](x0, x1) = 0, [0] = 1 orientation: active#(if(X1,X2,X3)) = X1 + 2 >= X1 + 1 = active#(X1) active#(div(X1,X2)) = X1 + 2 >= X1 + 1 = active#(X1) active#(s(X)) = X + 2 >= X + 1 = active#(X) active(minus(0(),Y)) = 1 >= 1 = mark(0()) active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y)) active(geq(X,0())) = 2 >= 1 = mark(true()) active(geq(0(),s(Y))) = 2 >= 1 = mark(false()) active(geq(s(X),s(Y))) = 2 >= 1 = mark(geq(X,Y)) active(div(0(),s(Y))) = 3 >= 1 = mark(0()) active(div(s(X),s(Y))) = X + 3 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = 2 >= 1 = mark(X) active(if(false(),X,Y)) = 2 >= 1 = mark(Y) active(s(X)) = X + 2 >= X + 2 = s(active(X)) active(div(X1,X2)) = X1 + 2 >= X1 + 2 = div(active(X1),X2) active(if(X1,X2,X3)) = X1 + 2 >= X1 + 2 = if(active(X1),X2,X3) s(mark(X)) = 2 >= 1 = mark(s(X)) div(mark(X1),X2) = 2 >= 1 = mark(div(X1,X2)) if(mark(X1),X2,X3) = 2 >= 1 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = 0 >= 0 = minus(proper(X1),proper(X2)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(geq(X1,X2)) = 1 >= 1 = geq(proper(X1),proper(X2)) proper(true()) = 0 >= 0 = ok(true()) proper(false()) = 0 >= 0 = ok(false()) proper(div(X1,X2)) = X1 + 1 >= X1 + 1 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = 0 >= 0 = ok(minus(X1,X2)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) geq(ok(X1),ok(X2)) = 1 >= 1 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X1 + 1 >= X1 + 1 = ok(if(X1,X2,X3)) top(mark(X)) = 1 >= 1 = top(proper(X)) top(ok(X)) = 1 >= 1 = top(active(X)) problem: DPs: TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: s#(ok(X)) -> s#(X) s#(mark(X)) -> s#(X) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [s#](x0) = x0 + 1, [top](x0) = 0, [ok](x0) = x0, [proper](x0) = x0, [if](x0, x1, x2) = x0 + x1 + x2, [div](x0, x1) = x0 + x1 + 1, [false] = 0, [true] = 0, [geq](x0, x1) = x0, [s](x0) = x0, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [minus](x0, x1) = 0, [0] = 0 orientation: s#(ok(X)) = X + 1 >= X + 1 = s#(X) s#(mark(X)) = X + 2 >= X + 1 = s#(X) active(minus(0(),Y)) = 1 >= 1 = mark(0()) active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y)) active(geq(X,0())) = X + 1 >= 1 = mark(true()) active(geq(0(),s(Y))) = 1 >= 1 = mark(false()) active(geq(s(X),s(Y))) = X + 1 >= X + 1 = mark(geq(X,Y)) active(div(0(),s(Y))) = Y + 2 >= 1 = mark(0()) active(div(s(X),s(Y))) = X + Y + 2 >= X + Y + 2 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X) active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(div(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = div(active(X1),X2) active(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(active(X1),X2,X3) s(mark(X)) = X + 1 >= X + 1 = mark(s(X)) div(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 2 = mark(div(X1,X2)) if(mark(X1),X2,X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = 0 >= 0 = minus(proper(X1),proper(X2)) proper(0()) = 0 >= 0 = ok(0()) proper(s(X)) = X >= X = s(proper(X)) proper(geq(X1,X2)) = X1 >= X1 = geq(proper(X1),proper(X2)) proper(true()) = 0 >= 0 = ok(true()) proper(false()) = 0 >= 0 = ok(false()) proper(div(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = 0 >= 0 = ok(minus(X1,X2)) s(ok(X)) = X >= X = ok(s(X)) geq(ok(X1),ok(X2)) = X1 >= X1 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: s#(ok(X)) -> s#(X) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [s#](x0) = x0 + 1, [top](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 1, [if](x0, x1, x2) = x0, [div](x0, x1) = x0, [false] = 0, [true] = 0, [geq](x0, x1) = x0, [s](x0) = x0, [mark](x0) = 0, [active](x0) = 0, [minus](x0, x1) = x0, [0] = 0 orientation: s#(ok(X)) = X + 2 >= X + 1 = s#(X) active(minus(0(),Y)) = 0 >= 0 = mark(0()) active(minus(s(X),s(Y))) = 0 >= 0 = mark(minus(X,Y)) active(geq(X,0())) = 0 >= 0 = mark(true()) active(geq(0(),s(Y))) = 0 >= 0 = mark(false()) active(geq(s(X),s(Y))) = 0 >= 0 = mark(geq(X,Y)) active(div(0(),s(Y))) = 0 >= 0 = mark(0()) active(div(s(X),s(Y))) = 0 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = 0 >= 0 = mark(X) active(if(false(),X,Y)) = 0 >= 0 = mark(Y) active(s(X)) = 0 >= 0 = s(active(X)) active(div(X1,X2)) = 0 >= 0 = div(active(X1),X2) active(if(X1,X2,X3)) = 0 >= 0 = if(active(X1),X2,X3) s(mark(X)) = 0 >= 0 = mark(s(X)) div(mark(X1),X2) = 0 >= 0 = mark(div(X1,X2)) if(mark(X1),X2,X3) = 0 >= 0 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = 1 >= 1 = minus(proper(X1),proper(X2)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = 1 >= 1 = s(proper(X)) proper(geq(X1,X2)) = 1 >= 1 = geq(proper(X1),proper(X2)) proper(true()) = 1 >= 1 = ok(true()) proper(false()) = 1 >= 1 = ok(false()) proper(div(X1,X2)) = 1 >= 1 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = 1 >= 1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(minus(X1,X2)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) geq(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X1 + 1 >= X1 + 1 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: div#(ok(X1),ok(X2)) -> div#(X1,X2) div#(mark(X1),X2) -> div#(X1,X2) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [div#](x0, x1) = x1 + 1, [top](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [if](x0, x1, x2) = x1 + 1, [div](x0, x1) = x0 + 1, [false] = 0, [true] = 0, [geq](x0, x1) = x1 + 1, [s](x0) = x0, [mark](x0) = 0, [active](x0) = x0, [minus](x0, x1) = x0, [0] = 0 orientation: div#(ok(X1),ok(X2)) = X2 + 2 >= X2 + 1 = div#(X1,X2) div#(mark(X1),X2) = X2 + 1 >= X2 + 1 = div#(X1,X2) active(minus(0(),Y)) = 0 >= 0 = mark(0()) active(minus(s(X),s(Y))) = X >= 0 = mark(minus(X,Y)) active(geq(X,0())) = 1 >= 0 = mark(true()) active(geq(0(),s(Y))) = Y + 1 >= 0 = mark(false()) active(geq(s(X),s(Y))) = Y + 1 >= 0 = mark(geq(X,Y)) active(div(0(),s(Y))) = 1 >= 0 = mark(0()) active(div(s(X),s(Y))) = X + 1 >= 0 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = X + 1 >= 0 = mark(X) active(if(false(),X,Y)) = X + 1 >= 0 = mark(Y) active(s(X)) = X >= X = s(active(X)) active(div(X1,X2)) = X1 + 1 >= X1 + 1 = div(active(X1),X2) active(if(X1,X2,X3)) = X2 + 1 >= X2 + 1 = if(active(X1),X2,X3) s(mark(X)) = 0 >= 0 = mark(s(X)) div(mark(X1),X2) = 1 >= 0 = mark(div(X1,X2)) if(mark(X1),X2,X3) = X2 + 1 >= 0 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = X1 + 1 >= X1 + 1 = minus(proper(X1),proper(X2)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(geq(X1,X2)) = X2 + 2 >= X2 + 2 = geq(proper(X1),proper(X2)) proper(true()) = 1 >= 1 = ok(true()) proper(false()) = 1 >= 1 = ok(false()) proper(div(X1,X2)) = X1 + 2 >= X1 + 2 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X2 + 2 >= X2 + 2 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(minus(X1,X2)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) geq(ok(X1),ok(X2)) = X2 + 2 >= X2 + 2 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = X1 + 2 >= X1 + 2 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X2 + 2 >= X2 + 2 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: div#(mark(X1),X2) -> div#(X1,X2) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [div#](x0, x1) = x0 + 1, [top](x0) = 0, [ok](x0) = 0, [proper](x0) = 0, [if](x0, x1, x2) = x0 + x1 + x2, [div](x0, x1) = x0, [false] = 0, [true] = 0, [geq](x0, x1) = x0, [s](x0) = x0, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [minus](x0, x1) = 0, [0] = 0 orientation: div#(mark(X1),X2) = X1 + 2 >= X1 + 1 = div#(X1,X2) active(minus(0(),Y)) = 1 >= 1 = mark(0()) active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y)) active(geq(X,0())) = X + 1 >= 1 = mark(true()) active(geq(0(),s(Y))) = 1 >= 1 = mark(false()) active(geq(s(X),s(Y))) = X + 1 >= X + 1 = mark(geq(X,Y)) active(div(0(),s(Y))) = 1 >= 1 = mark(0()) active(div(s(X),s(Y))) = X + 1 >= X + 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X) active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y) active(s(X)) = X + 1 >= X + 1 = s(active(X)) active(div(X1,X2)) = X1 + 1 >= X1 + 1 = div(active(X1),X2) active(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(active(X1),X2,X3) s(mark(X)) = X + 1 >= X + 1 = mark(s(X)) div(mark(X1),X2) = X1 + 1 >= X1 + 1 = mark(div(X1,X2)) if(mark(X1),X2,X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = 0 >= 0 = minus(proper(X1),proper(X2)) proper(0()) = 0 >= 0 = ok(0()) proper(s(X)) = 0 >= 0 = s(proper(X)) proper(geq(X1,X2)) = 0 >= 0 = geq(proper(X1),proper(X2)) proper(true()) = 0 >= 0 = ok(true()) proper(false()) = 0 >= 0 = ok(false()) proper(div(X1,X2)) = 0 >= 0 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = 0 >= 0 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = 0 >= 0 = ok(minus(X1,X2)) s(ok(X)) = 0 >= 0 = ok(s(X)) geq(ok(X1),ok(X2)) = 0 >= 0 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = 0 >= 0 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = 0 >= 0 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [if#](x0, x1, x2) = x2 + 1, [top](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = x0 + 1, [if](x0, x1, x2) = x0, [div](x0, x1) = x0, [false] = 1, [true] = 1, [geq](x0, x1) = x1, [s](x0) = x0, [mark](x0) = 1, [active](x0) = 1, [minus](x0, x1) = 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(minus(0(),Y)) = 1 >= 1 = mark(0()) active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y)) active(geq(X,0())) = 1 >= 1 = mark(true()) active(geq(0(),s(Y))) = 1 >= 1 = mark(false()) active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y)) active(div(0(),s(Y))) = 1 >= 1 = mark(0()) active(div(s(X),s(Y))) = 1 >= 1 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = 1 >= 1 = mark(X) active(if(false(),X,Y)) = 1 >= 1 = mark(Y) active(s(X)) = 1 >= 1 = s(active(X)) active(div(X1,X2)) = 1 >= 1 = div(active(X1),X2) active(if(X1,X2,X3)) = 1 >= 1 = if(active(X1),X2,X3) s(mark(X)) = 1 >= 1 = mark(s(X)) div(mark(X1),X2) = 1 >= 1 = mark(div(X1,X2)) if(mark(X1),X2,X3) = 1 >= 1 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = X1 + 1 >= X1 + 1 = minus(proper(X1),proper(X2)) proper(0()) = 1 >= 1 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(geq(X1,X2)) = X2 + 1 >= X2 + 1 = geq(proper(X1),proper(X2)) proper(true()) = 2 >= 2 = ok(true()) proper(false()) = 2 >= 2 = ok(false()) proper(div(X1,X2)) = X1 + 1 >= X1 + 1 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + 1 >= X1 + 1 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(minus(X1,X2)) s(ok(X)) = X + 1 >= X + 1 = ok(s(X)) geq(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = X1 + 1 >= X1 + 1 = ok(if(X1,X2,X3)) 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(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [if#](x0, x1, x2) = x0, [top](x0) = 0, [ok](x0) = 0, [proper](x0) = x0, [if](x0, x1, x2) = x0 + x1 + x2, [div](x0, x1) = x0 + x1, [false] = 0, [true] = 0, [geq](x0, x1) = 0, [s](x0) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [minus](x0, x1) = 0, [0] = 0 orientation: if#(mark(X1),X2,X3) = X1 + 1 >= X1 = if#(X1,X2,X3) active(minus(0(),Y)) = 1 >= 1 = mark(0()) active(minus(s(X),s(Y))) = 1 >= 1 = mark(minus(X,Y)) active(geq(X,0())) = 1 >= 1 = mark(true()) active(geq(0(),s(Y))) = 1 >= 1 = mark(false()) active(geq(s(X),s(Y))) = 1 >= 1 = mark(geq(X,Y)) active(div(0(),s(Y))) = Y + 2 >= 1 = mark(0()) active(div(s(X),s(Y))) = X + Y + 3 >= Y + 3 = mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) = X + Y + 1 >= X + 1 = mark(X) active(if(false(),X,Y)) = X + Y + 1 >= Y + 1 = mark(Y) active(s(X)) = X + 2 >= X + 2 = s(active(X)) active(div(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = div(active(X1),X2) active(if(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = if(active(X1),X2,X3) s(mark(X)) = X + 2 >= X + 2 = mark(s(X)) div(mark(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = mark(div(X1,X2)) if(mark(X1),X2,X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 1 = mark(if(X1,X2,X3)) proper(minus(X1,X2)) = 0 >= 0 = minus(proper(X1),proper(X2)) proper(0()) = 0 >= 0 = ok(0()) proper(s(X)) = X + 1 >= X + 1 = s(proper(X)) proper(geq(X1,X2)) = 0 >= 0 = geq(proper(X1),proper(X2)) proper(true()) = 0 >= 0 = ok(true()) proper(false()) = 0 >= 0 = ok(false()) proper(div(X1,X2)) = X1 + X2 >= X1 + X2 = div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) = 0 >= 0 = ok(minus(X1,X2)) s(ok(X)) = 1 >= 0 = ok(s(X)) geq(ok(X1),ok(X2)) = 0 >= 0 = ok(geq(X1,X2)) div(ok(X1),ok(X2)) = 0 >= 0 = ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) = 0 >= 0 = ok(if(X1,X2,X3)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(minus(0(),Y)) -> mark(0()) active(minus(s(X),s(Y))) -> mark(minus(X,Y)) active(geq(X,0())) -> mark(true()) active(geq(0(),s(Y))) -> mark(false()) active(geq(s(X),s(Y))) -> mark(geq(X,Y)) active(div(0(),s(Y))) -> mark(0()) active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(s(X)) -> s(active(X)) active(div(X1,X2)) -> div(active(X1),X2) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) s(mark(X)) -> mark(s(X)) div(mark(X1),X2) -> mark(div(X1,X2)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(div(X1,X2)) -> div(proper(X1),proper(X2)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) s(ok(X)) -> ok(s(X)) geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) div(ok(X1),ok(X2)) -> ok(div(X1,X2)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed