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