MAYBE TRS: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} DP: Strict: { active#(minus(s(X), s(Y))) -> minus#(X, Y), active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X)), active#(geq(s(X), s(Y))) -> geq#(X, Y), active#(div(X1, X2)) -> active#(X1), active#(div(X1, X2)) -> div#(active(X1), X2), active#(div(s(X), s(Y))) -> minus#(X, 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))) -> div#(minus(X, Y), s(Y)), 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#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), minus#(ok(X1), ok(X2)) -> minus#(X1, X2), s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X), geq#(ok(X1), ok(X2)) -> geq#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2), div#(ok(X1), ok(X2)) -> div#(X1, X2), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), proper#(minus(X1, X2)) -> minus#(proper(X1), proper(X2)), proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> geq#(proper(X1), proper(X2)), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> div#(proper(X1), proper(X2)), proper#(div(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2), 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#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), top#(mark(X)) -> proper#(X), top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X), top#(ok(X)) -> top#(active(X))} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} EDG: { (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X)) (proper#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X)) (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)) (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)) (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(s(X)) -> proper#(X), proper#(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#(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#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (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))) (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(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))) -> 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))) -> s#(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#(div(X1, X2)) -> div#(active(X1), X2)) (top#(ok(X)) -> active#(X), active#(div(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(geq(s(X), s(Y))) -> geq#(X, Y)) (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#(minus(s(X), s(Y))) -> minus#(X, Y)) (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#(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#(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#(s(X)) -> proper#(X)) (proper#(geq(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (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#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(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#(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#(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#(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))) (geq#(ok(X1), ok(X2)) -> geq#(X1, X2), geq#(ok(X1), ok(X2)) -> geq#(X1, X2)) (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)) (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)) (proper#(geq(X1, X2)) -> geq#(proper(X1), proper(X2)), geq#(ok(X1), ok(X2)) -> geq#(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(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))) -> 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))) -> s#(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#(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#(geq(s(X), s(Y))) -> geq#(X, Y)) (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#(minus(s(X), s(Y))) -> minus#(X, Y)) (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)) -> 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#(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#(s(X)) -> proper#(X)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (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#(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)) -> 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#(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#(s(X)) -> proper#(X)) (proper#(div(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (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#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(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#(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#(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#(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))) (active#(geq(s(X), s(Y))) -> geq#(X, Y), geq#(ok(X1), ok(X2)) -> geq#(X1, X2)) (active#(div(s(X), s(Y))) -> geq#(X, Y), geq#(ok(X1), ok(X2)) -> geq#(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)) (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#(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)) (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))) -> minus#(X, Y), minus#(ok(X1), ok(X2)) -> minus#(X1, X2)) (active#(minus(s(X), s(Y))) -> minus#(X, Y), minus#(ok(X1), ok(X2)) -> minus#(X1, X2)) (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)) -> 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#(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#(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#(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#(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)) -> 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#(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#(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#(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)) (active#(if(X1, X2, X3)) -> active#(X1), active#(minus(s(X), s(Y))) -> minus#(X, Y)) (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#(geq(s(X), s(Y))) -> geq#(X, Y)) (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#(div(s(X), s(Y))) -> minus#(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))) -> geq#(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))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) (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)) (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#(minus(X1, X2)) -> minus#(proper(X1), proper(X2)), minus#(ok(X1), ok(X2)) -> minus#(X1, X2)) (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)) (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)) (minus#(ok(X1), ok(X2)) -> minus#(X1, X2), minus#(ok(X1), ok(X2)) -> minus#(X1, X2)) (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#(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#(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#(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#(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#(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#(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#(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#(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#(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)) (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)) (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#(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#(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#(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)) (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(ok(X)) -> s#(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#(s(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(s(X)) -> active#(X), active#(geq(s(X), s(Y))) -> geq#(X, Y)) (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#(div(s(X), s(Y))) -> minus#(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))) -> geq#(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))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(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)) (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))) (active#(s(X)) -> s#(active(X)), s#(mark(X)) -> s#(X)) (active#(s(X)) -> s#(active(X)), s#(ok(X)) -> s#(X)) } SCCS: Scc: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Scc: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} Scc: { if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)} Scc: { div#(mark(X1), X2) -> div#(X1, X2), div#(ok(X1), ok(X2)) -> div#(X1, X2)} Scc: {geq#(ok(X1), ok(X2)) -> geq#(X1, X2)} Scc: {s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)} Scc: {minus#(ok(X1), ok(X2)) -> minus#(X1, X2)} Scc: { active#(s(X)) -> active#(X), active#(div(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)} SCC: Strict: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} Fail SCC: Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} EDG: {(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#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X1)) (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#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (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#(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#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (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#(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#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (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#(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)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (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)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X2)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (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#(X2), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X2)) (proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (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#(X2), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X2)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (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#(X3), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))} SCCS: Scc: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} SCC: Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)} EDG: {(proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X1)) (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#(X1)) (proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (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#(minus(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (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#(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#(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)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(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)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X3)) (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#(X2), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X3)) (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#(X2), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X3)) (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#(X3), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> 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)) -> proper#(X3))} SCCS: Scc: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)} SCC: Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} EDG: {(proper#(minus(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(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#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(div(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (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#(geq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(geq(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2)) (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#(s(X)) -> proper#(X)) (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#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (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)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> proper#(X2)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (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#(X2), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> proper#(X2)) (proper#(geq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (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#(X3), proper#(s(X)) -> proper#(X)) (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#(div(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))} SCCS: Scc: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} SCC: Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} EDG: {(proper#(minus(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(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#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(s(X)) -> proper#(X), proper#(div(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X1)) (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#(X2), proper#(s(X)) -> proper#(X)) (proper#(div(X1, X2)) -> proper#(X2), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(div(X1, X2)) -> proper#(X2), proper#(div(X1, X2)) -> proper#(X2)) (proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (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)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(geq(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2)) (proper#(geq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (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#(X3), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(geq(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#(if(X1, X2, X3)) -> proper#(X3))} SCCS: Scc: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} SCC: Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(div(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)} EDG: {(proper#(minus(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(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#(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#(X3), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3)) (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)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(geq(X1, X2)) -> proper#(X1), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(geq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (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)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))} SCCS: Scc: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)} SCC: Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(geq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)} EDG: {(proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X1)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(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#(X1), proper#(minus(X1, X2)) -> proper#(X1)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (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#(X3), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))} SCCS: Scc: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)} SCC: Strict: { proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)} EDG: {(proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (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#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (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#(X2), proper#(s(X)) -> proper#(X))} SCCS: Scc: {proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)} SCC: Strict: {proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)} EDG: {(proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(minus(X1, X2)) -> proper#(X1), proper#(minus(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(minus(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))} SCCS: Scc: {proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)} SCC: Strict: {proper#(minus(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(s(X)) -> proper#(X)} EDG: {(proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))} SCCS: Scc: {proper#(s(X)) -> proper#(X)} SCC: Strict: {proper#(s(X)) -> proper#(X)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {} Qed SCC: Strict: { if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(if#) = 0 Strict: {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(if#) = 0 Strict: {} Qed SCC: Strict: { div#(mark(X1), X2) -> div#(X1, X2), div#(ok(X1), ok(X2)) -> div#(X1, X2)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(div#) = 0 Strict: {div#(mark(X1), X2) -> div#(X1, X2)} EDG: {(div#(mark(X1), X2) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2))} SCCS: Scc: {div#(mark(X1), X2) -> div#(X1, X2)} SCC: Strict: {div#(mark(X1), X2) -> div#(X1, X2)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(div#) = 0 Strict: {} Qed SCC: Strict: {geq#(ok(X1), ok(X2)) -> geq#(X1, X2)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(geq#) = 0 Strict: {} Qed SCC: Strict: {s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(ok(X)) -> s#(X)} EDG: {(s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))} SCCS: Scc: {s#(ok(X)) -> s#(X)} SCC: Strict: {s#(ok(X)) -> s#(X)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: {minus#(ok(X1), ok(X2)) -> minus#(X1, X2)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(minus#) = 0 Strict: {} Qed SCC: Strict: { active#(s(X)) -> active#(X), active#(div(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)} EDG: {(active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)) (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))} SCCS: Scc: { active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)} SCC: Strict: { active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {active#(if(X1, X2, X3)) -> active#(X1)} EDG: {(active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))} SCCS: Scc: {active#(if(X1, X2, X3)) -> active#(X1)} SCC: Strict: {active#(if(X1, X2, X3)) -> active#(X1)} Weak: { active(minus(0(), Y)) -> mark(0()), active(minus(s(X), s(Y))) -> mark(minus(X, Y)), active(s(X)) -> s(active(X)), 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(X1, X2)) -> div(active(X1), X2), 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(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)), div(mark(X1), X2) -> mark(div(X1, X2)), div(ok(X1), ok(X2)) -> ok(div(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), proper(0()) -> ok(0()), proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)), 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)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {} Qed