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