YES TRS: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} DP: Strict: { mark#(0()) -> active#(0()), mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(s(X)) -> s#(mark(X)), mark#(true()) -> active#(true()), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(false()) -> active#(false()), mark#(div(X1, X2)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(div(X1, X2)) -> div#(mark(X1), X2), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), active#(minus(0(), Y)) -> mark#(0()), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(minus(s(X), s(Y))) -> 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#(geq(s(X), s(Y))) -> 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#(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(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y), minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2), minus#(active(X1), X2) -> minus#(X1, X2), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, active(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2), div#(active(X1), X2) -> div#(X1, X2), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: { (mark#(div(X1, X2)) -> div#(mark(X1), X2), div#(active(X1), X2) -> div#(X1, X2)) (mark#(div(X1, X2)) -> div#(mark(X1), X2), div#(mark(X1), X2) -> div#(X1, X2)) (mark#(div(X1, X2)) -> div#(mark(X1), X2), div#(X1, active(X2)) -> div#(X1, X2)) (mark#(div(X1, X2)) -> div#(mark(X1), X2), div#(X1, mark(X2)) -> div#(X1, X2)) (active#(geq(s(X), s(Y))) -> geq#(X, Y), geq#(active(X1), X2) -> geq#(X1, X2)) (active#(geq(s(X), s(Y))) -> geq#(X, Y), geq#(mark(X1), X2) -> geq#(X1, X2)) (active#(geq(s(X), s(Y))) -> geq#(X, Y), geq#(X1, active(X2)) -> geq#(X1, X2)) (active#(geq(s(X), s(Y))) -> geq#(X, Y), geq#(X1, mark(X2)) -> geq#(X1, X2)) (active#(div(s(X), s(Y))) -> geq#(X, Y), geq#(active(X1), X2) -> geq#(X1, X2)) (active#(div(s(X), s(Y))) -> geq#(X, Y), geq#(mark(X1), X2) -> geq#(X1, X2)) (active#(div(s(X), s(Y))) -> geq#(X, Y), geq#(X1, active(X2)) -> geq#(X1, X2)) (active#(div(s(X), s(Y))) -> geq#(X, Y), geq#(X1, mark(X2)) -> geq#(X1, X2)) (active#(minus(0(), Y)) -> mark#(0()), mark#(0()) -> active#(0())) (active#(geq(0(), s(Y))) -> mark#(false()), mark#(false()) -> active#(false())) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> div#(minus(X, Y), s(Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> geq#(X, Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> s#(div(minus(X, Y), s(Y)))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> minus#(X, Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(0(), s(Y))) -> mark#(0())) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> geq#(X, Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(0(), s(Y))) -> mark#(false())) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(X, 0())) -> mark#(true())) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> minus#(X, Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(0(), Y)) -> mark#(0())) (mark#(div(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(div(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(div(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(div(X1, X2)) -> mark#(X1), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (mark#(div(X1, X2)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(div(X1, X2)) -> mark#(X1), mark#(div(X1, X2)) -> mark#(X1)) (mark#(div(X1, X2)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(div(X1, X2)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(div(X1, X2)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(div(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(div(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(div(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(div(X1, X2)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(div(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(active(X1), X2) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(mark(X1), X2) -> minus#(X1, X2), minus#(active(X1), X2) -> minus#(X1, X2)) (minus#(mark(X1), X2) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)) (minus#(mark(X1), X2) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(mark(X1), X2) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, active(X2)) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)) (geq#(mark(X1), X2) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(mark(X1), X2) -> geq#(X1, X2), geq#(X1, active(X2)) -> geq#(X1, X2)) (geq#(mark(X1), X2) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(active(X1), X2) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(mark(X1), X2) -> div#(X1, X2), div#(active(X1), 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#(X1, active(X2)) -> div#(X1, X2)) (div#(mark(X1), X2) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> div#(minus(X, Y), s(Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> geq#(X, Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> s#(div(minus(X, Y), s(Y)))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> minus#(X, Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(0(), s(Y))) -> mark#(0())) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(s(X), s(Y))) -> geq#(X, Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(0(), s(Y))) -> mark#(false())) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(X, 0())) -> mark#(true())) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(minus(s(X), s(Y))) -> minus#(X, Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(minus(0(), Y)) -> mark#(0())) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> div#(minus(X, Y), s(Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> geq#(X, Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> s#(div(minus(X, Y), s(Y)))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> minus#(X, Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(0(), s(Y))) -> mark#(0())) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(s(X), s(Y))) -> geq#(X, Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(0(), s(Y))) -> mark#(false())) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(X, 0())) -> mark#(true())) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(minus(s(X), s(Y))) -> minus#(X, Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(minus(0(), Y)) -> mark#(0())) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> mark#(X1)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(s(X)) -> s#(mark(X))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(s(X)) -> active#(s(mark(X)))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(s(X)) -> mark#(X)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(div(X1, X2)) -> mark#(X1)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(s(X)) -> s#(mark(X))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(s(X)) -> active#(s(mark(X)))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(s(X)) -> mark#(X)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(false()) -> active#(false())) (active#(if(true(), X, Y)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(true()) -> active#(true())) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(0()) -> active#(0())) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(div(s(X), s(Y))) -> s#(div(minus(X, Y), s(Y))), s#(active(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#(X1, mark(X2)) -> div#(X1, X2)) (active#(div(s(X), s(Y))) -> div#(minus(X, Y), s(Y)), div#(X1, active(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))) -> div#(minus(X, Y), s(Y)), div#(active(X1), X2) -> div#(X1, X2)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)) (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(s(X)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(s(X)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(s(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(s(X)) -> mark#(X), mark#(div(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(s(X)) -> mark#(X), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(div(s(X), s(Y))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (active#(div(s(X), s(Y))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), if#(X1, active(X2), 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))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(s(X)) -> mark#(X)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(s(X)) -> active#(s(mark(X)))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(s(X)) -> s#(mark(X))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(div(X1, X2)) -> mark#(X1)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(minus(0(), Y)) -> mark#(0())) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(minus(s(X), s(Y))) -> minus#(X, Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(X, 0())) -> mark#(true())) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(0(), s(Y))) -> mark#(false())) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(s(X), s(Y))) -> geq#(X, Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(0(), s(Y))) -> mark#(0())) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> minus#(X, Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> s#(div(minus(X, Y), s(Y)))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> geq#(X, Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> div#(minus(X, Y), s(Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X)) (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(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#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (div#(active(X1), X2) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(active(X1), X2) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2)) (div#(active(X1), X2) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)) (div#(active(X1), X2) -> div#(X1, X2), div#(active(X1), X2) -> div#(X1, X2)) (div#(X1, active(X2)) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(X1, active(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2)) (div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)) (div#(X1, active(X2)) -> div#(X1, X2), div#(active(X1), X2) -> div#(X1, X2)) (geq#(active(X1), X2) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(active(X1), X2) -> geq#(X1, X2), geq#(X1, active(X2)) -> geq#(X1, X2)) (geq#(active(X1), X2) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(active(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)) (geq#(X1, active(X2)) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(X1, active(X2)) -> geq#(X1, X2), geq#(X1, active(X2)) -> geq#(X1, X2)) (geq#(X1, active(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(X1, active(X2)) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)) (minus#(active(X1), X2) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(active(X1), X2) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(active(X1), X2) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)) (minus#(active(X1), X2) -> minus#(X1, X2), minus#(active(X1), X2) -> minus#(X1, X2)) (minus#(X1, active(X2)) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(X1, active(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)) (minus#(X1, active(X2)) -> minus#(X1, X2), minus#(active(X1), X2) -> minus#(X1, X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(s(X)) -> active#(s(mark(X))), active#(minus(0(), Y)) -> mark#(0())) (mark#(s(X)) -> active#(s(mark(X))), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(minus(s(X), s(Y))) -> minus#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(geq(X, 0())) -> mark#(true())) (mark#(s(X)) -> active#(s(mark(X))), active#(geq(0(), s(Y))) -> mark#(false())) (mark#(s(X)) -> active#(s(mark(X))), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(geq(s(X), s(Y))) -> geq#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(div(0(), s(Y))) -> mark#(0())) (mark#(s(X)) -> active#(s(mark(X))), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(s(X)) -> active#(s(mark(X))), active#(div(s(X), s(Y))) -> minus#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(div(s(X), s(Y))) -> s#(div(minus(X, Y), s(Y)))) (mark#(s(X)) -> active#(s(mark(X))), active#(div(s(X), s(Y))) -> geq#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(div(s(X), s(Y))) -> div#(minus(X, Y), s(Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(div(s(X), s(Y))) -> if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) (mark#(s(X)) -> active#(s(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (active#(div(0(), s(Y))) -> mark#(0()), mark#(0()) -> active#(0())) (active#(geq(X, 0())) -> mark#(true()), mark#(true()) -> active#(true())) (active#(div(s(X), s(Y))) -> minus#(X, Y), minus#(X1, mark(X2)) -> minus#(X1, X2)) (active#(div(s(X), s(Y))) -> minus#(X, Y), minus#(X1, active(X2)) -> minus#(X1, X2)) (active#(div(s(X), s(Y))) -> minus#(X, Y), minus#(mark(X1), X2) -> minus#(X1, X2)) (active#(div(s(X), s(Y))) -> minus#(X, Y), minus#(active(X1), X2) -> minus#(X1, X2)) (active#(minus(s(X), s(Y))) -> minus#(X, Y), minus#(X1, mark(X2)) -> minus#(X1, X2)) (active#(minus(s(X), s(Y))) -> minus#(X, Y), minus#(X1, active(X2)) -> minus#(X1, X2)) (active#(minus(s(X), s(Y))) -> minus#(X, Y), minus#(mark(X1), X2) -> minus#(X1, X2)) (active#(minus(s(X), s(Y))) -> minus#(X, Y), minus#(active(X1), X2) -> minus#(X1, X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(0()) -> active#(0())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> s#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(true()) -> active#(true())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(false()) -> active#(false())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> div#(mark(X1), X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) } SCCS: Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)} Scc: { div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2), div#(active(X1), X2) -> div#(X1, X2)} Scc: { geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, active(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)} Scc: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2), minus#(active(X1), X2) -> minus#(X1, X2)} Scc: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(if#) = 0 Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(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#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(if#) = 2 Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(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#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(if#) = 0 Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(if#) = 2 Strict: { if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: { if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: { if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(if#) = 1 Strict: {if#(X1, active(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, active(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, active(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(if#) = 1 Strict: {} Qed SCC: Strict: { div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2), div#(active(X1), X2) -> div#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(div#) = 0 Strict: { div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)} EDG: {(div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)) (div#(X1, active(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2)) (div#(X1, active(X2)) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(mark(X1), X2) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(mark(X1), X2) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2)) (div#(mark(X1), X2) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2))} SCCS: Scc: { div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)} SCC: Strict: { div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, active(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(div#) = 1 Strict: {div#(X1, mark(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)} EDG: {(div#(mark(X1), X2) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)) (div#(mark(X1), X2) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2)) (div#(X1, mark(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2))} SCCS: Scc: {div#(X1, mark(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)} SCC: Strict: {div#(X1, mark(X2)) -> div#(X1, X2), div#(mark(X1), X2) -> div#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(div#) = 0 Strict: {div#(X1, mark(X2)) -> div#(X1, X2)} EDG: {(div#(X1, mark(X2)) -> div#(X1, X2), div#(X1, mark(X2)) -> div#(X1, X2))} SCCS: Scc: {div#(X1, mark(X2)) -> div#(X1, X2)} SCC: Strict: {div#(X1, mark(X2)) -> div#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(div#) = 1 Strict: {} Qed SCC: Strict: { geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, active(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(geq#) = 1 Strict: { geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)} EDG: {(geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)) (geq#(mark(X1), X2) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(mark(X1), X2) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(active(X1), X2) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(active(X1), X2) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(active(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2))} SCCS: Scc: { geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)} SCC: Strict: { geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2), geq#(active(X1), X2) -> geq#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(geq#) = 0 Strict: {geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)} EDG: {(geq#(mark(X1), X2) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)) (geq#(mark(X1), X2) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2)) (geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2))} SCCS: Scc: {geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)} SCC: Strict: {geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(mark(X1), X2) -> geq#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(geq#) = 0 Strict: {geq#(X1, mark(X2)) -> geq#(X1, X2)} EDG: {(geq#(X1, mark(X2)) -> geq#(X1, X2), geq#(X1, mark(X2)) -> geq#(X1, X2))} SCCS: Scc: {geq#(X1, mark(X2)) -> geq#(X1, X2)} SCC: Strict: {geq#(X1, mark(X2)) -> geq#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(geq#) = 1 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(active(X)) -> s#(X)} EDG: {(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))} SCCS: Scc: {s#(active(X)) -> s#(X)} SCC: Strict: {s#(active(X)) -> s#(X)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2), minus#(active(X1), X2) -> minus#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(minus#) = 0 Strict: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)} EDG: {(minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)) (minus#(X1, active(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(X1, active(X2)) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(mark(X1), X2) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(mark(X1), X2) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(mark(X1), X2) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2))} SCCS: Scc: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)} SCC: Strict: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2), minus#(mark(X1), X2) -> minus#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(minus#) = 0 Strict: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)} EDG: {(minus#(X1, active(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)) (minus#(X1, active(X2)) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, mark(X2)) -> minus#(X1, X2)) (minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2))} SCCS: Scc: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)} SCC: Strict: { minus#(X1, mark(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(minus#) = 1 Strict: {minus#(X1, active(X2)) -> minus#(X1, X2)} EDG: {(minus#(X1, active(X2)) -> minus#(X1, X2), minus#(X1, active(X2)) -> minus#(X1, X2))} SCCS: Scc: {minus#(X1, active(X2)) -> minus#(X1, X2)} SCC: Strict: {minus#(X1, active(X2)) -> minus#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(minus#) = 1 Strict: {} Qed SCC: Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [0,1,2], pi(div) = [0], pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = 0, pi(minus) = [], pi(active#) = 0, pi(active) = 0, pi(0) = [], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [if](x0, x1, x2) = x0 + x1 + x2, [div](x0) = x0 + 1, [geq] = 0, [minus] = 0, [false] = 0, [true] = 0, [0] = 0 Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(s(X)) -> active#(s(mark(X)))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(s(X)) -> mark#(X)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(s(X)) -> active#(s(mark(X)))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(s(X)) -> mark#(X)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(s(X)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(s(X)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(s(X)) -> mark#(X)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(s(X)) -> active#(s(mark(X)))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(s(X)) -> active#(s(mark(X))), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(s(X)) -> active#(s(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(if(false(), X, Y)) -> mark#(Y))} SCCS: Scc: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} SCC: Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [], pi(div) = [], pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [], pi(minus) = [], pi(active#) = 0, pi(active) = [], pi(0) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [if] = 1, [div] = 1, [geq] = 1, [minus] = 1, [s] = 0 Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(s(X)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(s(X)) -> mark#(X)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(s(X)) -> mark#(X)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(s(X)) -> mark#(X)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y))} SCCS: Scc: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} SCC: Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(s(X)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [0,1,2], pi(div) = 0, pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [0], pi(minus) = [], pi(active#) = 0, pi(active) = 0, pi(0) = [], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [if](x0, x1, x2) = x0 + x1 + x2, [geq] = 0, [minus] = 0, [s](x0) = x0 + 1, [false] = 0, [true] = 0, [0] = 0 Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(div(s(X), s(Y))) -> mark#(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)))} SCCS: Scc: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} SCC: Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), 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)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [0,1,2], pi(div) = [0,1], pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [], pi(minus) = [], pi(active#) = 0, pi(active) = 0, pi(0) = [], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [if](x0, x1, x2) = x0 + x1 + x2, [div](x0, x1) = x0 + x1, [geq] = 0, [minus] = 0, [s] = 1, [false] = 0, [true] = 0, [0] = 0 Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (active#(if(true(), X, Y)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)))} SCCS: Scc: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} SCC: Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(minus(s(X), s(Y))) -> mark#(minus(X, Y)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [0,1,2], pi(div) = 0, pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [0], pi(minus) = 0, pi(active#) = 0, pi(active) = 0, pi(0) = [], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [if](x0, x1, x2) = x0 + x1 + x2, [geq] = 0, [s](x0) = x0 + 1, [false] = 0, [true] = 0 Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y))) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (active#(if(true(), X, Y)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)))} SCCS: Scc: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} SCC: Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(geq(s(X), s(Y))) -> mark#(geq(X, Y)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [0,1,2], pi(div) = [0], pi(false) = [], pi(geq) = 0, pi(true) = [], pi(s) = [0], pi(minus) = [], pi(active#) = 0, pi(active) = 0, pi(0) = [], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [if](x0, x1, x2) = x0 + x1 + x2, [div](x0) = x0 + 1, [minus] = 0, [s](x0) = x0 + 1, [false] = 0, [true] = 0 Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(geq(X1, X2)) -> active#(geq(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(minus(X1, X2)) -> active#(minus(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(geq(X1, X2)) -> active#(geq(X1, X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(div(X1, X2)) -> active#(div(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(minus(X1, X2)) -> active#(minus(X1, X2)), active#(if(false(), X, Y)) -> mark#(Y))} SCCS: Scc: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} SCC: Strict: { mark#(minus(X1, X2)) -> active#(minus(X1, X2)), mark#(geq(X1, X2)) -> active#(geq(X1, X2)), mark#(div(X1, X2)) -> active#(div(mark(X1), X2)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [], pi(div) = [], pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [], pi(minus) = [], pi(active#) = 0, pi(active) = [], pi(0) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [if] = 1, [div] = 0, [geq] = 0, [minus] = 0 Strict: { mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)))} SCCS: Scc: { mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} SCC: Strict: { mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [0,1,2], pi(div) = [], pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [], pi(minus) = [], pi(active#) = 0, pi(active) = 0, pi(0) = [], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [if](x0, x1, x2) = x0 + x1 + x2, [false] = 0, [true] = 1 Strict: { mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y))} SCCS: Scc: { mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)} SCC: Strict: { mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} POLY: Argument Filtering: pi(if) = [0,1,2], pi(div) = [0,1], pi(false) = [], pi(geq) = [], pi(true) = [], pi(s) = [], pi(minus) = [], pi(active#) = 0, pi(active) = 0, pi(0) = [], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [if](x0, x1, x2) = x0 + x1 + x2, [false] = 1 Strict: {mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} EDG: {(mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)))} SCCS: Scc: {mark#(if(X1, X2, X3)) -> mark#(X1)} SCC: Strict: {mark#(if(X1, X2, X3)) -> mark#(X1)} Weak: { mark(0()) -> active(0()), mark(minus(X1, X2)) -> active(minus(X1, X2)), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(geq(X1, X2)) -> active(geq(X1, X2)), mark(false()) -> active(false()), mark(div(X1, X2)) -> active(div(mark(X1), X2)), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), 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), minus(X1, mark(X2)) -> minus(X1, X2), minus(X1, active(X2)) -> minus(X1, X2), minus(mark(X1), X2) -> minus(X1, X2), minus(active(X1), X2) -> minus(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), geq(X1, mark(X2)) -> geq(X1, X2), geq(X1, active(X2)) -> geq(X1, X2), geq(mark(X1), X2) -> geq(X1, X2), geq(active(X1), X2) -> geq(X1, X2), div(X1, mark(X2)) -> div(X1, X2), div(X1, active(X2)) -> div(X1, X2), div(mark(X1), X2) -> div(X1, X2), div(active(X1), X2) -> div(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3)} SPSC: Simple Projection: pi(mark#) = 0 Strict: {} Qed